remove last axioms of hol.ml (#158)

Deducteam · Dec 17, 2024 · b0293b4 · b0293b4
1 parent fd69df1
commit b0293b4
Show file tree

Hide file tree

Showing 2 changed files with 81 additions and 0 deletions.
diff --git a/HOLLight.v b/HOLLight.v
@@ -904,3 +904,70 @@ Proof. intros A a. apply mk_dest. Qed.
 
 Lemma axiom_36 : forall {A B : Type'} (r : nat), ((fun x : nat => @IN nat x (dotdot (NUMERAL (BIT1 0)) (Nat.mul (@dimindex A (@UNIV A)) (@dimindex B (@UNIV B))))) r) = ((@dest_finite_prod A B (@mk_finite_prod A B r)) = r).
 Proof. intros A r. apply dest_mk. Qed.
+
+(*****************************************************************************)
+(* Mapping of a subtype of recspace (non-recursive inductive type definition) *)
+(*****************************************************************************)
+
+Section non_recursive_inductive_type.
+
+  Variable A : Type'.
+
+  Definition nr_constr (a:A) : recspace A := CONSTR 0 a (fun n => BOTTOM).
+
+  Definition nr_pred (r : recspace A) := exists a, r = nr_constr a.
+
+  Lemma nr_pred1 : nr_pred (nr_constr (el A)).
+  Proof. exists (el A). reflexivity. Qed.
+
+  Definition nr_type := @subtype (recspace A) _ _ nr_pred1.
+
+  Definition nr_mk : recspace A -> nr_type := @mk (recspace A) _ _ nr_pred1.
+
+  Definition nr_dest : nr_type -> recspace A := @dest (recspace A) _ _ nr_pred1.
+
+  Lemma nr_mk_dest : forall a : nr_type, (nr_mk (nr_dest a)) = a.
+  Proof. intro a. apply mk_dest. Qed.
+
+  Lemma nr_dest_mk : forall r : recspace A, (forall P : recspace A -> Prop, (forall r' : recspace A, nr_pred r' -> P r') -> P r) = (nr_dest (nr_mk r) = r).
+  Proof.
+    intro r. apply prop_ext; intro h.
+    unfold nr_dest, nr_mk. rewrite <- dest_mk.
+    apply h. intros r' [a H]. exists a. exact H.
+    intros P H. apply H. rewrite <- h. destruct (nr_mk r) as [r' [a h']].
+    exists a. unfold nr_dest, dest. simpl. exact h'.
+  Qed.
+
+End non_recursive_inductive_type.
+
+(*****************************************************************************)
+(* Cart.tybit0 *)
+(*****************************************************************************)
+
+Definition tybit0 A := nr_type (finite_sum A A).
+
+Definition _mk_tybit0 : forall {A : Type'}, (recspace (finite_sum A A)) -> tybit0 A := fun A => nr_mk (finite_sum A A).
+
+Definition _dest_tybit0 : forall {A : Type'}, (tybit0 A) -> recspace (finite_sum A A) := fun A => nr_dest (finite_sum A A).
+
+Lemma axiom_37 : forall {A : Type'} (a : tybit0 A), (@_mk_tybit0 A (@_dest_tybit0 A a)) = a.
+Proof. intro A. apply nr_mk_dest. Qed.
+
+Lemma axiom_38 : forall {A : Type'} (r : recspace (finite_sum A A)), ((fun a : recspace (finite_sum A A) => forall tybit0' : (recspace (finite_sum A A)) -> Prop, (forall a' : recspace (finite_sum A A), (exists a'' : finite_sum A A, a' = ((fun a''' : finite_sum A A => @CONSTR (finite_sum A A) (NUMERAL 0) a''' (fun n : nat => @BOTTOM (finite_sum A A))) a'')) -> tybit0' a') -> tybit0' a) r) = ((@_dest_tybit0 A (@_mk_tybit0 A r)) = r).
+Proof. intro A. apply nr_dest_mk. Qed.
+
+(*****************************************************************************)
+(* Cart.tybit1 *)
+(*****************************************************************************)
+
+Definition tybit1 A := nr_type (finite_sum (finite_sum A A) unit).
+
+Definition _mk_tybit1 : forall {A : Type'}, (recspace (finite_sum (finite_sum A A) unit)) -> tybit1 A := fun A => nr_mk (finite_sum (finite_sum A A) unit).
+
+Definition _dest_tybit1 : forall {A : Type'}, (tybit1 A) -> recspace (finite_sum (finite_sum A A) unit) := fun A => nr_dest (finite_sum (finite_sum A A) unit).
+
+Lemma axiom_39 : forall {A : Type'} (a : tybit1 A), (@_mk_tybit1 A (@_dest_tybit1 A a)) = a.
+Proof. intro A. apply nr_mk_dest. Qed.
+
+Lemma axiom_40 : forall {A : Type'} (r : recspace (finite_sum (finite_sum A A) unit)), ((fun a : recspace (finite_sum (finite_sum A A) unit) => forall tybit1' : (recspace (finite_sum (finite_sum A A) unit)) -> Prop, (forall a' : recspace (finite_sum (finite_sum A A) unit), (exists a'' : finite_sum (finite_sum A A) unit, a' = ((fun a''' : finite_sum (finite_sum A A) unit => @CONSTR (finite_sum (finite_sum A A) unit) (NUMERAL 0) a''' (fun n : nat => @BOTTOM (finite_sum (finite_sum A A) unit))) a'')) -> tybit1' a') -> tybit1' a) r) = ((@_dest_tybit1 A (@_mk_tybit1 A r)) = r).
+Proof. intro A. apply nr_dest_mk. Qed.
diff --git a/erasing.lp b/erasing.lp
@@ -339,3 +339,17 @@ builtin "mk_finite_prod" ≔ mk_finite_prod;
 builtin "dest_finite_prod" ≔ dest_finite_prod;
 builtin "axiom_35" ≔ axiom_35;
 builtin "axiom_36" ≔ axiom_36;
+
+// tybit0
+builtin "tybit0" ≔ tybit0;
+builtin "_mk_tybit0" ≔ _mk_tybit0;
+builtin "_dest_tybit0" ≔ _dest_tybit0;
+builtin "axiom_37" ≔ axiom_37;
+builtin "axiom_38" ≔ axiom_38;
+
+// tybit1
+builtin "tybit1" ≔ tybit1;
+builtin "_mk_tybit1" ≔ _mk_tybit1;
+builtin "_dest_tybit1" ≔ _dest_tybit1;
+builtin "axiom_39" ≔ axiom_39;
+builtin "axiom_40" ≔ axiom_40;