From b0293b4bd6967343627c1a96912911aab1614722 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 17 Dec 2024 12:40:30 +0100 Subject: [PATCH] remove last axioms of hol.ml (#158) --- HOLLight.v | 67 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ erasing.lp | 14 ++++++++++++ 2 files changed, 81 insertions(+) diff --git a/HOLLight.v b/HOLLight.v index e830d72..1771a43 100644 --- 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 index c2ebab0..55267b1 100644 --- 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;