From 135110462ab35eea8fd516d94b11ec5b31b73980 Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Mon, 28 Aug 2017 11:04:39 +0200 Subject: [PATCH 1/2] Make the main folder compatible with 8.7. --- .depend | 9 +++--- AbsTheorySyn.v | 2 +- CoqCompat.v | 11 +++++++ Ens.v | 6 ++-- EnsEm.v | 2 +- EnsEmUniv.v | 3 +- EnsLogic.v | 6 ++-- GenLemmas.v | 2 +- GenRealSN.v | 2 +- HFcoc.v | 1 + InstInterp.v | 26 ++++++++-------- InstSem.v | 2 +- InstSyn.v | 78 ++++++++++++++++++++++++------------------------ Lambda.v | 4 +-- ModelNat_ZFind.v | 9 ------ Nest.v | 2 +- NonUniform.v | 1 + ObjectSN.v | 12 ++++---- PIntp.v | 8 ++--- PSem.v | 2 +- PSyn.v | 24 +++++++-------- SATtypes.v | 8 ++--- SN_W.v | 2 -- SN_variance.v | 12 ++++---- Term.v | 2 ++ TheoryInTerm.v | 11 +++---- ZFcoc.v | 6 ++-- ZFcoll.v | 4 +-- ZFfunext.v | 1 - ZFind.v | 1 + ZFind_wnup.v | 1 - ZFnest.v | 2 +- ZFord.v | 2 +- ZFskol.v | 3 +- ZFskolEm.v | 3 +- ZFsposd.v | 2 +- basic.v | 3 ++ hEns.v | 2 +- 38 files changed, 142 insertions(+), 135 deletions(-) create mode 100644 CoqCompat.v diff --git a/.depend b/.depend index 41853eb..c85d113 100644 --- a/.depend +++ b/.depend @@ -46,8 +46,8 @@ ModelZF.vo ModelZF.glob ModelZF.v.beautified: ModelZF.v basic.vo Sublogic.vo Mod Model_variance.vo Model_variance.glob Model_variance.v.beautified: Model_variance.v ZF.vo ZFcoc.vo ZFfunext.vo ModelZF.vo Models.vo Models.glob Models.v.beautified: Models.v basic.vo MyList.vo MyList.glob MyList.v.beautified: MyList.v -Nest.vo Nest.glob Nest.v.beautified: Nest.v -NonUniform.vo NonUniform.glob NonUniform.v.beautified: NonUniform.v +Nest.vo Nest.glob Nest.v.beautified: Nest.v CoqCompat.vo +NonUniform.vo NonUniform.glob NonUniform.v.beautified: NonUniform.v CoqCompat.vo ObjectSN.vo ObjectSN.glob ObjectSN.v.beautified: ObjectSN.v basic.vo Models.vo VarMap.vo Lambda.vo ObjectSN2.vo ObjectSN2.glob ObjectSN2.v.beautified: ObjectSN2.v basic.vo Models.vo VarMap.vo Lambda.vo PIntp.vo PIntp.glob PIntp.v.beautified: PIntp.v GenLemmas.vo AbsTheoryIntp.vo PSyn.vo PSem.vo @@ -76,7 +76,7 @@ Sat.vo Sat.glob Sat.v.beautified: Sat.v Lambda.vo Can.vo SnModels.vo SnModels.glob SnModels.v.beautified: SnModels.v basic.vo Models.vo Sat.vo StrengthenECC.vo StrengthenECC.glob StrengthenECC.v.beautified: StrengthenECC.v TypeECC.vo Sublogic.vo Sublogic.glob Sublogic.v.beautified: Sublogic.v basic.vo Logics.vo -Term.vo Term.glob Term.v.beautified: Term.v +Term.vo Term.glob Term.v.beautified: Term.v CoqCompat.vo TermECC.vo TermECC.glob TermECC.v.beautified: TermECC.v TheoryInTerm.vo TheoryInTerm.glob TheoryInTerm.v.beautified: TheoryInTerm.v ZFtheory.vo GenModel.vo ZFcoc.vo ModelZF.vo TypModels.vo TypModels.glob TypModels.v.beautified: TypModels.v Models.vo @@ -141,5 +141,6 @@ ZFuniv.vo ZFuniv.glob ZFuniv.v.beautified: ZFuniv.v Sat.vo ZF.vo ZFcoc.vo ZFord. ZFuniv_real.vo ZFuniv_real.glob ZFuniv_real.v.beautified: ZFuniv_real.v Sat.vo ZF.vo ZFcoc.vo ZFord.vo ZFgrothendieck.vo ZFlambda.vo Models.vo SnModels.vo ZFwf.vo ZFwf.glob ZFwf.v.beautified: ZFwf.v basic.vo ZF.vo ZFrepl.vo ZFpairs.vo ZFrelations.vo ZFwpaths.vo ZFwpaths.glob ZFwpaths.v.beautified: ZFwpaths.v ZF.vo ZFpairs.vo ZFsum.vo ZFnats.vo ZFrelations.vo ZFtarski.vo ZFstable.vo ZFgrothendieck.vo ZFlist.vo -basic.vo basic.glob basic.v.beautified: basic.v +CoqCompat.vo CoqCompat.glob CoqCompat.v.beautified: CoqCompat.v +basic.vo basic.glob basic.v.beautified: basic.v CoqCompat.vo test.vo test.glob test.v.beautified: test.v Lambda.vo diff --git a/AbsTheorySyn.v b/AbsTheorySyn.v index 0450d23..3e3787c 100644 --- a/AbsTheorySyn.v +++ b/AbsTheorySyn.v @@ -1,5 +1,5 @@ Require Import List. -Require Import Omega. +Require Export CoqCompat. (******************************************************************************************) (******************************************************************************************) diff --git a/CoqCompat.v b/CoqCompat.v new file mode 100644 index 0000000..9c2e2eb --- /dev/null +++ b/CoqCompat.v @@ -0,0 +1,11 @@ +Require Export Coq85. +Require Export AdmitAxiom. + +Require Coq.omega.Omega. +Ltac omega := Coq.omega.Omega.omega. +Global Set Asymmetric Patterns. + +Require Import Morphisms. +Existing Instance respectful_per. + +Notation value := Some. diff --git a/Ens.v b/Ens.v index 4056d8e..87e609a 100644 --- a/Ens.v +++ b/Ens.v @@ -813,7 +813,7 @@ Fixpoint V (x:set) := union (replf x (fun x' => power (V x'))). Lemma V_morph : forall x x', eq_set x x' -> eq_set (V x) (V x'). induction x; destruct x'; intros. -simpl V; unfold replf; simpl sup. +simpl V; unfold replf. apply union_morph. simpl in H0. destruct H0. @@ -1105,7 +1105,7 @@ assert (Pwit : forall x, x ∈ A -> exists y, P x (V y)). apply V_sub with (V x0). apply V_mono; exists tt; apply eq_set_refl. apply V_intro. -destruct (@repl_ax A (fun x y => lst_rk (P x) y)); eauto using lst_fun, lst_ex. +destruct (@repl_ax A (fun x y => lst_rk (P x) y)); simpl; eauto using lst_fun, lst_ex. intros. apply lst_rk_morph with (P x) y; trivial. intros. @@ -1263,7 +1263,7 @@ generalize (H (sup bool (fun b => if b then empty else singl empty)) (sup bool (fun b => if b then singl empty else empty))). simpl; intros. assert (singl empty == empty). - refine (let H1 := H0 _ in _). + simple refine ((fun H1 => _) (H0 _)); swap 1 2. split; intros. exists (negb i). destruct i; apply eq_set_refl. diff --git a/EnsEm.v b/EnsEm.v index 227ad56..bccf427 100644 --- a/EnsEm.v +++ b/EnsEm.v @@ -1115,7 +1115,7 @@ Fixpoint V (x:set) := union (replf x (fun x' => power (V x'))). Lemma V_morph : forall x x', x == x' -> V x == V x'. induction x; destruct x'; intros. -simpl V; unfold replf; simpl sup. +simpl V; unfold replf. apply union_morph. rewrite eq_set_def in H0; simpl in H0. destruct H0. diff --git a/EnsEmUniv.v b/EnsEmUniv.v index 4a53880..5c270f0 100644 --- a/EnsEmUniv.v +++ b/EnsEmUniv.v @@ -322,6 +322,7 @@ refine (let (b,Hb) := S.intuit_repl_ax intuit apply U_intro. apply U_intro. + simpl in Hb. Texists (injU b). apply U_intro. @@ -377,7 +378,7 @@ destruct S.collection_ax with a' (fun x y => R (injU x) (injU y)) as (B,HB). Tdestruct (H1 _ H2). apply down_in_ex with (1:=H0) in H2. Tdestruct H2. - refine (let h := HB _ H5 _ in _). + simple refine (let h := HB _ H5 _ in _). apply U_elim in H3; Tdestruct H3. Texists x2. revert H4; apply H; apply B.eq_set_sym; trivial. diff --git a/EnsLogic.v b/EnsLogic.v index 5967f22..bc9d12b 100644 --- a/EnsLogic.v +++ b/EnsLogic.v @@ -469,8 +469,8 @@ destruct (choice_axiom {i:X|exists w, R i w} set (fun i y => R (proj1_sig i) y)) exists {i:X|exists w, R i w}. exists f. intros. - exists (existT _ i H). - apply (Hf (existT _ i H)). + exists (exist _ i H). + apply (Hf (exist _ i H)). Qed. (* ttcoll rephrased on sets: *) @@ -716,7 +716,7 @@ Fixpoint V (x:set) := union (replf x (fun x' => power (V x'))). Lemma V_morph : forall x x', x == x' -> V x == V x'. induction x; destruct x'; intros. -simpl V; unfold replf; simpl sup. +simpl V; unfold replf. apply union_morph. rewrite eq_set_def in H0; simpl in H0. destruct H0. diff --git a/GenLemmas.v b/GenLemmas.v index 758e3a6..6592d64 100644 --- a/GenLemmas.v +++ b/GenLemmas.v @@ -205,7 +205,7 @@ assert (val_ok (A::e) (V.cons (int D i) i) (I.cons (tm D j) j)) by (apply vcons_add_var; trivial). apply red_typ with (1:=H) in HB; [destruct HB as (HSB, HB)|destruct C; [discriminate|trivial]]. -apply in_int_intro; [destruct B; [discriminate|]| |]; trivial. +apply SN.in_int_intro; [destruct B; [discriminate|]| |]; trivial. revert HB; apply real_morph. rewrite int_subst_eq; reflexivity. diff --git a/GenRealSN.v b/GenRealSN.v index 7a37561..bb929c8 100644 --- a/GenRealSN.v +++ b/GenRealSN.v @@ -1146,7 +1146,7 @@ case_eq (nth_error e n); intros. apply typ_subsumption with (lift (S n) t); auto. apply typ_var; trivial. - destruct t as [(t,tm)|]; simpl; try discriminate. + destruct t as [(t,tm,?,?,?,?)|]; simpl; try discriminate. elim H; trivial. discriminate. diff --git a/HFcoc.v b/HFcoc.v index 190ee46..205d4ac 100644 --- a/HFcoc.v +++ b/HFcoc.v @@ -75,6 +75,7 @@ apply repl_ext; intros. rewrite H4 in H2. clear H4 x0. elim repl_elim with (1:=Pm'') (2 := H2); intros; clear H2. + cbv beta in H1. rewrite H5 in H1 |- *; rewrite snd_def; rewrite fst_def in H1. apply in_hf_reg_r with (F x1); auto. diff --git a/InstInterp.v b/InstInterp.v index c0b8ace..00cc404 100644 --- a/InstInterp.v +++ b/InstInterp.v @@ -10,23 +10,23 @@ Import SN_nat. Fixpoint intp_foterm t:= match t with - | Var i => Ref i - | Cst_0 => Zero - | Cst_1 => App Succ Zero - | Df_Add u v => App (App Add (intp_foterm u)) (intp_foterm v) + | Var' i => Ref i + | Cst_0' => Zero + | Cst_1' => App Succ Zero + | Df_Add' u v => App (App Add (intp_foterm u)) (intp_foterm v) end. Fixpoint intp_fofml f:= match f with - | eq_foterm x y => EQ_term (intp_foterm x) (intp_foterm y) - | TF => True_symb - | BF => False_symb - | neg f => Neg (intp_fofml f) - | conj f1 f2 => Conj (intp_fofml f1) (intp_fofml f2) - | disj f1 f2 => Disj (intp_fofml f1) (intp_fofml f2) - | implf f1 f2 => Impl (intp_fofml f1) (intp_fofml f2) - | fall f => Fall (intp_fofml f) - | exst f => Exst (intp_fofml f) + | eq_foterm' x y => EQ_term (intp_foterm x) (intp_foterm y) + | TF' => True_symb + | BF' => False_symb + | neg' f => Neg (intp_fofml f) + | conj' f1 f2 => Conj (intp_fofml f1) (intp_fofml f2) + | disj' f1 f2 => Disj (intp_fofml f1) (intp_fofml f2) + | implf' f1 f2 => Impl (intp_fofml f1) (intp_fofml f2) + | fall' f => Fall (intp_fofml f) + | exst' f => Exst (intp_fofml f) end. Lemma intp_eq_fml : forall x y, diff --git a/InstSem.v b/InstSem.v index 6fcb1c9..ead1e6d 100644 --- a/InstSem.v +++ b/InstSem.v @@ -1245,7 +1245,7 @@ assert (eq_term (lift_rec 1 0 Add) Add) as Hadd_lift. |unfold V.lams, V.shift; simpl; apply H]. do 3 red; intros. apply app_ext; [apply app_ext; [reflexivity|]|]; trivial. - unfold I.lams, I.shift; simpl; do 2 rewrite H; trivial. + unfold I.lams, I.shift; simpl; rewrite H; trivial. rewrite Hadd_lift. do 2 (rewrite eq_term_lift_ref_fv; [simpl plus|omega]). setoid_replace (lift_rec 1 0 Succ) with Succ using relation eq_term by diff --git a/InstSyn.v b/InstSyn.v index 88d071e..f96b401 100644 --- a/InstSyn.v +++ b/InstSyn.v @@ -17,43 +17,43 @@ Definition Df_Add := Df_Add'. Fixpoint lift_term_rec t n k:= match t with - | Var i => + | Var' i => match le_gt_dec k i with | left _ => Var (i+n) | right _ => Var i end - | Cst_0 => Cst_0 - | Cst_1 => Cst_1 - | Df_Add u v => Df_Add (lift_term_rec u n k) (lift_term_rec v n k) + | Cst_0' => Cst_0 + | Cst_1' => Cst_1 + | Df_Add' u v => Df_Add (lift_term_rec u n k) (lift_term_rec v n k) end. Definition lift_term t n := lift_term_rec t n 0. Fixpoint subst_term_rec M N n:= match M with - | Var i => + | Var' i => match lt_eq_lt_dec n i with | inleft (left _) => Var (pred i) | inleft (right _) => lift_term N n | inright _ => Var i end - | Cst_0 => Cst_0 - | Cst_1 => Cst_1 - | Df_Add M1 M2 => Df_Add (subst_term_rec M1 N n) (subst_term_rec M2 N n) + | Cst_0' => Cst_0 + | Cst_1' => Cst_1 + | Df_Add' M1 M2 => Df_Add (subst_term_rec M1 N n) (subst_term_rec M2 N n) end. Definition subst_term M N := subst_term_rec M N 0. Fixpoint fv_term_rec t k : list nat := match t with - | Var n => + | Var' n => match le_gt_dec k n with | left _ => (n-k)::nil | right _ => nil end - | Cst_0 => nil - | Cst_1 => nil - | Df_Add M N => (fv_term_rec M k) ++ (fv_term_rec N k) + | Cst_0' => nil + | Cst_1' => nil + | Df_Add' M N => (fv_term_rec M k) ++ (fv_term_rec N k) end. Definition fv_term t := fv_term_rec t 0. @@ -82,45 +82,45 @@ Definition exst := exst'. Fixpoint lift_fml_rec f n k:= match f with - | eq_foterm x y => eq_foterm (lift_term_rec x n k) (lift_term_rec y n k) - | TF => TF - | BF => BF - | neg f' => neg (lift_fml_rec f' n k) - | conj A B => conj (lift_fml_rec A n k) (lift_fml_rec B n k) - | disj A B => disj (lift_fml_rec A n k) (lift_fml_rec B n k) - | implf A B => implf (lift_fml_rec A n k) (lift_fml_rec B n k) - | fall A => fall (lift_fml_rec A n (S k)) - | exst A => exst (lift_fml_rec A n (S k)) + | eq_foterm' x y => eq_foterm (lift_term_rec x n k) (lift_term_rec y n k) + | TF' => TF + | BF' => BF + | neg' f' => neg (lift_fml_rec f' n k) + | conj' A B => conj (lift_fml_rec A n k) (lift_fml_rec B n k) + | disj' A B => disj (lift_fml_rec A n k) (lift_fml_rec B n k) + | implf' A B => implf (lift_fml_rec A n k) (lift_fml_rec B n k) + | fall' A => fall (lift_fml_rec A n (S k)) + | exst' A => exst (lift_fml_rec A n (S k)) end. Definition lift_fml t n := lift_fml_rec t n 0. Fixpoint subst_fml_rec f N n := match f with - | eq_foterm x y => eq_foterm (subst_term_rec x N n) (subst_term_rec y N n) - | TF => TF - | BF => BF - | neg f => neg (subst_fml_rec f N n) - | conj f1 f2 => conj (subst_fml_rec f1 N n) (subst_fml_rec f2 N n) - | disj f1 f2 => disj (subst_fml_rec f1 N n) (subst_fml_rec f2 N n) - | implf f1 f2 => implf (subst_fml_rec f1 N n) (subst_fml_rec f2 N n) - | fall f => fall (subst_fml_rec f N (S n)) - | exst f => exst (subst_fml_rec f N (S n)) + | eq_foterm' x y => eq_foterm (subst_term_rec x N n) (subst_term_rec y N n) + | TF' => TF + | BF' => BF + | neg' f => neg (subst_fml_rec f N n) + | conj' f1 f2 => conj (subst_fml_rec f1 N n) (subst_fml_rec f2 N n) + | disj' f1 f2 => disj (subst_fml_rec f1 N n) (subst_fml_rec f2 N n) + | implf' f1 f2 => implf (subst_fml_rec f1 N n) (subst_fml_rec f2 N n) + | fall' f => fall (subst_fml_rec f N (S n)) + | exst' f => exst (subst_fml_rec f N (S n)) end. Definition subst_fml f N := subst_fml_rec f N 0. Fixpoint fv_fml_rec f k : list nat := match f with - | eq_foterm t1 t2 => (fv_term_rec t1 k) ++ (fv_term_rec t2 k) - | TF => nil - | BF => nil - | neg f0 => fv_fml_rec f0 k - | conj f1 f2 => (fv_fml_rec f1 k) ++ (fv_fml_rec f2 k) - | disj f1 f2 => (fv_fml_rec f1 k) ++ (fv_fml_rec f2 k) - | implf f1 f2 => (fv_fml_rec f1 k) ++ (fv_fml_rec f2 k) - | fall f0 => (fv_fml_rec f0 (S k)) - | exst f0 => (fv_fml_rec f0 (S k)) + | eq_foterm' t1 t2 => (fv_term_rec t1 k) ++ (fv_term_rec t2 k) + | TF' => nil + | BF' => nil + | neg' f0 => fv_fml_rec f0 k + | conj' f1 f2 => (fv_fml_rec f1 k) ++ (fv_fml_rec f2 k) + | disj' f1 f2 => (fv_fml_rec f1 k) ++ (fv_fml_rec f2 k) + | implf' f1 f2 => (fv_fml_rec f1 k) ++ (fv_fml_rec f2 k) + | fall' f0 => (fv_fml_rec f0 (S k)) + | exst' f0 => (fv_fml_rec f0 (S k)) end. Definition fv_fml f := fv_fml_rec f 0. diff --git a/Lambda.v b/Lambda.v index 1a743ad..96abf01 100644 --- a/Lambda.v +++ b/Lambda.v @@ -518,7 +518,7 @@ split; intros. destruct n; simpl; trivial. inversion l. - apply NPeano.Nat.lt_pred_le in g. + apply Nat.lt_pred_le in g. elim (Lt.lt_irrefl n). apply Lt.le_lt_trans with k; trivial. @@ -1137,7 +1137,7 @@ induction M; simpl; intros. rewrite <- plus_n_Sm in H0. split; auto with arith. constructor. - rewrite <- NPeano.Nat.sub_succ_l; trivial. + rewrite <- Nat.sub_succ_l; trivial. apply Le.le_trans with (m+k); auto with arith. inversion_clear H0. diff --git a/ModelNat_ZFind.v b/ModelNat_ZFind.v index 067c871..4c53160 100644 --- a/ModelNat_ZFind.v +++ b/ModelNat_ZFind.v @@ -348,12 +348,3 @@ apply fa_morph; intros P. apply fa_morph; intros Pm. rewrite H1; rewrite H; reflexivity. Qed. - -red in H; specialize H with (1:=H0); simpl in H. -rewrite cc_beta_eq; auto with *. -rewrite NATREC_S; auto. - reflexivity. - - do 2 red; intros; apply cc_app_morph; auto with *. - apply cc_app_morph; auto with *. -Qed. diff --git a/Nest.v b/Nest.v index 58a496d..21bc3b7 100644 --- a/Nest.v +++ b/Nest.v @@ -1,4 +1,4 @@ - +Require Export CoqCompat. (** Showing a nested inductive type operator is isomorphic to a W-type. *) diff --git a/NonUniform.v b/NonUniform.v index 1385d97..6abdfa0 100644 --- a/NonUniform.v +++ b/NonUniform.v @@ -1,3 +1,4 @@ +Require Export CoqCompat. (** This file shows how big non-uniform parameters can be encoded as an index without changing the universe of the definition. *) diff --git a/ObjectSN.v b/ObjectSN.v index a0c00d6..a4870b9 100644 --- a/ObjectSN.v +++ b/ObjectSN.v @@ -57,21 +57,21 @@ Definition eq_term (x y:term) := Instance eq_term_refl : Reflexive eq_term. red; intros. -destruct x as [(f,mf,g,mg,sg)|]; simpl; auto. +destruct x as [(f,mf,g,mg,lg,sg)|]; simpl; auto. Qed. Instance eq_term_sym : Symmetric eq_term. red; intros. -destruct x as [(fx,mfx,gx,mgx,sgx)|]; -destruct y as [(fy,mfy,gy,mgy,sgy)|]; simpl in *; auto. +destruct x as [(fx,mfx,gx,mgx,lgx,sgx)|]; +destruct y as [(fy,mfy,gy,mgy,lgy,sgy)|]; simpl in *; auto. destruct H; split; symmetry; trivial. Qed. Instance eq_term_trans : Transitive eq_term. red; intros. -destruct x as [(fx,mfx,gx,mgx,sgx)|]; -destruct y as [(fy,mfy,gy,mgy,sgy)|]; -destruct z as [(fz,mfz,gz,mgz,sgz)|]; +destruct x as [(fx,mfx,gx,mgx,lgx,sgx)|]; +destruct y as [(fy,mfy,gy,mgy,lgy,sgy)|]; +destruct z as [(fz,mfz,gz,mgz,lgz,sgz)|]; try contradiction; simpl in *; auto. destruct H; destruct H0; split. transitivity fy; trivial. diff --git a/PIntp.v b/PIntp.v index 87b28fd..9a56f5f 100644 --- a/PIntp.v +++ b/PIntp.v @@ -15,10 +15,10 @@ Import PresburgerSem. Fixpoint intp_foterm t : term := match t with - | Var i => Ref i - | Cst_0 => Zero - | Cst_1 => App Succ Zero - | Df_Add u v => App (App Add (intp_foterm u)) (intp_foterm v) + | Var' i => Ref i + | Cst_0' => Zero + | Cst_1' => App Succ Zero + | Df_Add' u v => App (App Add (intp_foterm u)) (intp_foterm v) end. Lemma intp_foterm_not_kind : forall t, intp_foterm t <> None. diff --git a/PSem.v b/PSem.v index a081efa..9e2a2c1 100644 --- a/PSem.v +++ b/PSem.v @@ -939,7 +939,7 @@ assert (eq_term (lift_rec 1 0 Add) Add) as Hadd_lift. |unfold V.lams, V.shift; simpl; apply H]. do 3 red; intros. apply app_ext; [apply app_ext; [reflexivity|]|]; trivial. - unfold I.lams, I.shift; simpl; do 2 rewrite H; trivial. + unfold I.lams, I.shift; simpl; rewrite H; trivial. rewrite Hadd_lift. do 2 (rewrite eq_term_lift_ref_fv; [simpl plus|omega]). setoid_replace (lift_rec 1 0 Succ) with Succ using relation eq_term by diff --git a/PSyn.v b/PSyn.v index dabb973..792cb34 100644 --- a/PSyn.v +++ b/PSyn.v @@ -18,14 +18,14 @@ Definition Df_Add := Df_Add'. Fixpoint lift_term_rec t n k:= match t with - | Var i => + | Var' i => match le_gt_dec k i with | left _ => Var (i+n) | right _ => Var i end - | Cst_0 => Cst_0 - | Cst_1 => Cst_1 - | Df_Add u v => Df_Add (lift_term_rec u n k) (lift_term_rec v n k) + | Cst_0' => Cst_0 + | Cst_1' => Cst_1 + | Df_Add' u v => Df_Add (lift_term_rec u n k) (lift_term_rec v n k) end. Definition lift_term t n := lift_term_rec t n 0. @@ -50,29 +50,29 @@ Qed. Fixpoint subst_term_rec M N n:= match M with - | Var i => + | Var' i => match lt_eq_lt_dec n i with | inleft (left _) => Var (pred i) | inleft (right _) => lift_term N n | inright _ => Var i end - | Cst_0 => Cst_0 - | Cst_1 => Cst_1 - | Df_Add M1 M2 => Df_Add (subst_term_rec M1 N n) (subst_term_rec M2 N n) + | Cst_0' => Cst_0 + | Cst_1' => Cst_1 + | Df_Add' M1 M2 => Df_Add (subst_term_rec M1 N n) (subst_term_rec M2 N n) end. Definition subst_term M N := subst_term_rec M N 0. Fixpoint fv_term_rec t k : list nat := match t with - | Var n => + | Var' n => match le_gt_dec k n with | left _ => (n-k)::nil | right _ => nil end - | Cst_0 => nil - | Cst_1 => nil - | Df_Add M N => (fv_term_rec M k) ++ (fv_term_rec N k) + | Cst_0' => nil + | Cst_1' => nil + | Df_Add' M N => (fv_term_rec M k) ++ (fv_term_rec N k) end. Definition fv_term t := fv_term_rec t 0. diff --git a/SATtypes.v b/SATtypes.v index 90261ed..e5cdb58 100644 --- a/SATtypes.v +++ b/SATtypes.v @@ -277,7 +277,7 @@ apply prodSAT_intro; intros. unfold subst; simpl subst_rec. unfold subst; repeat rewrite simpl_subst; auto. repeat rewrite lift0. -apply piSAT0_elim with (x:=x) (u:=t) in H1; auto with *. +pose proof (piSAT0_elim x t H1); auto with *. Qed. Lemma Real_inr RX RY x t : @@ -294,7 +294,7 @@ apply prodSAT_intro; intros. unfold subst; simpl subst_rec. unfold subst; repeat rewrite simpl_subst; auto. repeat rewrite lift0. -apply piSAT0_elim with (x:=x) (u:=t) in H2; auto with *. +pose proof (piSAT0_elim x t H2); auto with *. Qed. Lemma Real_sum_case a RX RY C t b1 b2 : @@ -1405,7 +1405,7 @@ Lemma fixSAT_lower_bound FX A X : red; intros. red; intros. apply interSAT_elim with - (x:=existT (fun X=>Proper (eq_set==>eqSAT) X /\inclFam FX (A X) X) + (x:=exist (fun X=>Proper (eq_set==>eqSAT) X /\inclFam FX (A X) X) X (conj H H0)) in H2; simpl in H2. trivial. Qed. @@ -1503,7 +1503,7 @@ assert (Xpost : inclFam FX (A X) X). red; intros. apply condSAT_smaller. apply interSAT_elim with - (x:=existT (fun X=>Proper (eq_set==>eqSAT) X /\inclFam FX (A X) X) + (x:=exist (fun X=>Proper (eq_set==>eqSAT) X /\inclFam FX (A X) X) X (conj Xm Xpost)) in H0; simpl in H0. revert H0; apply condSAT_neutral; trivial. Qed. diff --git a/SN_W.v b/SN_W.v index 94a2062..7414ffe 100644 --- a/SN_W.v +++ b/SN_W.v @@ -1024,8 +1024,6 @@ eapply inSAT_morph;[reflexivity| |]. apply V.cons_morph. reflexivity. - reflexivity. - apply Bwi_morph. apply RAwi_morph. diff --git a/SN_variance.v b/SN_variance.v index b332ba6..1087034 100644 --- a/SN_variance.v +++ b/SN_variance.v @@ -441,7 +441,7 @@ split. apply typ_subsumption with (lift (S n) t); trivial. apply typ_var; trivial. - destruct t as [(t,tm)|]; simpl in *; auto. + destruct t as [(t,tm,?,?,?,?)|]; simpl in *; auto. discriminate. Qed. @@ -487,7 +487,7 @@ split. apply typ_subsumption with (subst v Ur); trivial. apply typ_app with V; auto. - destruct Ur as [(Ur,Urm)|]; simpl; trivial. + destruct Ur as [(Ur,Urm,?,?,?,?)|]; simpl; trivial. discriminate. Qed. @@ -506,7 +506,7 @@ split. apply typ_subsumption with (lift (S n) t); trivial. apply typ_var; trivial. - destruct t as [(t,tm)|]; simpl in *; auto. + destruct t as [(t,tm,?,?,?,?)|]; simpl in *; auto. discriminate. Qed. @@ -547,12 +547,12 @@ split. apply fx_eq_rec_call with t (lift_rec (S n) 1 u); trivial. apply typ_subsumption with (subst x (lift_rec (S n) 1 u)); auto. - 2:destruct u as [(u,um)|]; trivial. + 2:destruct u as [(u,um,?,?,?,?)|]; trivial. 2:discriminate. apply typ_app with (lift (S n) t); trivial. - destruct t as [(t,tm)|]; trivial. + destruct t as [(t,tm,?,?,?,?)|]; trivial. discriminate. - destruct u as [(u,um)|]; trivial. + destruct u as [(u,um,?,?,?,?)|]; trivial. discriminate. Qed. diff --git a/Term.v b/Term.v index 1e7d913..b8de058 100644 --- a/Term.v +++ b/Term.v @@ -3,6 +3,8 @@ Require Import Arith. Require Export Compare_dec. Require Export Relations. +Require Export CoqCompat. + Hint Resolve t_step rt_step rt_refl: core. Hint Unfold transp: core. diff --git a/TheoryInTerm.v b/TheoryInTerm.v index 218e7f6..8c0a934 100644 --- a/TheoryInTerm.v +++ b/TheoryInTerm.v @@ -80,7 +80,7 @@ elim H using N_ind; intros. rewrite NATREC_0. apply H1. rewrite NATREC_Succ; auto. - refine (let H6 := prod_elim _ _ _ _ _ H2 H4 in _). + simple refine (let H6 := prod_elim _ _ _ _ _ H2 H4 in _). red; intros. apply prod_ext. apply app_ext; try assumption. apply int_morph; try reflexivity. @@ -93,17 +93,18 @@ elim H using N_ind; intros. rewrite H7; reflexivity. - simpl in H6. clear H2. + simpl in H6. clearbody H6. clear H2. replace (fun k : nat => V.cons n0 i k) with (V.cons n0 i) in *; trivial. - refine (let H7 := prod_elim _ _ _ _ _ H6 _ in _). + simple refine (let H7 := prod_elim _ _ _ _ _ H6 _ in _). + shelve. do 2 red; intros. apply app_ext; try reflexivity. apply int_morph; try reflexivity. do 2 red; intros. rewrite H7; reflexivity. rewrite simpl_int_lift1. apply H5. - simpl in H7. revert H7. apply in_set_morph; try reflexivity. + simpl in H7. clearbody H7. revert H7. apply in_set_morph; try reflexivity. set (fS' := fun n y => app (app fS n) y) in |-*. apply app_ext; try reflexivity. replace (fun k : nat => V.cons (NATREC f0 fS' n0) @@ -864,7 +865,7 @@ apply Impl_intro. prod (int P (V.cons z (V.shift 3 i))) (fun _ : X => int P (V.cons (succ z) (V.shift 3 i))))) as H'. red; intros. apply prod_ext; [|do 2 red; intros]; rewrite H2; reflexivity. - specialize Haux with (1:=H') (2:=Hsucc) (3:=H). clear H' Hsucc. + specialize Haux with (1:=H'). clear H' Hsucc. generalize prod_elim; intro Haux1. assert ( eq_fun (int P (V.cons n (V.shift 3 i))) (fun _ : X => int P (V.cons (succ n) (V.shift 3 i))) diff --git a/ZFcoc.v b/ZFcoc.v index 1824174..5e3df0b 100644 --- a/ZFcoc.v +++ b/ZFcoc.v @@ -592,9 +592,9 @@ Lemma cc_ttcoll A R : forall x, x ∈ A -> (exists2 w, w ∈ sets & R x w) -> exists2 i, i ∈ X & R x (cc_app f i). intros. -destruct coll_axU with (A:=A) (R:=fun x y => y ∈ sets /\ R x y) as (B,HB); +destruct coll_axU with (A:=A) (R:=fun x y => y ∈ sets /\ R x y) as (B,HB,?); trivial. - intros. + intros. simpl. rewrite <- H2; rewrite <- H3; trivial. pose (B':= B ∩ sets). @@ -752,7 +752,7 @@ apply sup_ax in H. destruct H0; trivial. do 2 red; intros. - rewrite H1; reflexivity. + rewrite H2; reflexivity. Qed. End ChoicesImpliesDescription. diff --git a/ZFcoll.v b/ZFcoll.v index 33bd5af..b9573be 100644 --- a/ZFcoll.v +++ b/ZFcoll.v @@ -551,7 +551,7 @@ assert (Pwit : forall x, exists y, P x (rk y)). destruct (H1 x). exists (singl x0); exists x0; split; trivial. rewrite <- rk_pow; apply rk_intro. -destruct (@H A (fun x y => lst_rk (P x) y)); eauto using lst_fun, lst_ex. +destruct (@H A (fun x y => lst_rk (P x) y)); simpl; eauto using lst_fun, lst_ex. apply morph_impl_iff2; auto with *. do 4 red; intros. apply lst_rk_morph with (P x) x0; auto with *. @@ -591,7 +591,7 @@ assert (Pwit : forall x, x ∈ A -> exists y, P x (rk y)). destruct (H1 x H2). exists (singl x0); exists x0; split; trivial. rewrite <- rk_pow; apply rk_intro. -destruct (@H A (fun x y => lst_rk (P x) y)); eauto using lst_fun, lst_ex. +destruct (@H A (fun x y => lst_rk (P x) y)); simpl; eauto using lst_fun, lst_ex. apply morph_impl_iff2; auto with *. do 4 red; intros. apply lst_rk_morph with (P x) x0; auto with *. diff --git a/ZFfunext.v b/ZFfunext.v index 1674a19..5d7a38e 100644 --- a/ZFfunext.v +++ b/ZFfunext.v @@ -101,7 +101,6 @@ apply eq_intro; intros. rewrite sup_ax in H1; trivial. destruct H1. rewrite couple_in_app in H2. - specialize in_prod with (1:=H1). apply fdir with x1; trivial. Qed. diff --git a/ZFind.v b/ZFind.v index 6f3fa9c..52771d7 100644 --- a/ZFind.v +++ b/ZFind.v @@ -509,6 +509,7 @@ split; intros. revert H5; apply sigma_mono; auto with *. intros. rewrite <- H8. + clearbody Q. (* See BZ#5156. *) apply TIF_mono; auto with *. apply W0.W_Fd_morph; auto. apply W0.W_Fd_mono; auto. diff --git a/ZFind_wnup.v b/ZFind_wnup.v index aaa9912..61dc32d 100644 --- a/ZFind_wnup.v +++ b/ZFind_wnup.v @@ -493,7 +493,6 @@ constructor; intros. do 2 red; intros. rewrite H4; reflexivity. - specialize ty2 with (1:=H2). apply (iso_typ (H1 _ (ftyp _ _ _ tya tyx H3))). apply subset_intro; auto. rewrite inst in H3,tyx|-*. diff --git a/ZFnest.v b/ZFnest.v index c788f21..937b998 100644 --- a/ZFnest.v +++ b/ZFnest.v @@ -608,7 +608,7 @@ constructor; intros. apply F_elim in H2; destruct H2 as (ty1',(ty2',(ty3',et'))). destruct WFi_inv with (1:=H3); clear H3; intros; auto with *. apply B'm; trivial. - destruct WFi_inv with (1:=H1); clear H1; intros; auto with *. + destruct WFi_inv with (1:=H1); clear H1; intros; simpl; auto with *. rewrite et; rewrite et'. assert (tya' : a'of (fst x) (fun i => f (cc_app (snd (snd x)) i)) ∈ TI (W_F A C) (osucc o)). apply a'of_typ with X; auto. diff --git a/ZFord.v b/ZFord.v index d0f8857..7603b0c 100644 --- a/ZFord.v +++ b/ZFord.v @@ -1204,7 +1204,7 @@ Qed. forall x y, TR_rel x y -> forall y', TR_rel x y' -> y == y'. intros x y (xo,H). apply H; intros. - apply morph_impl_iff2; auto with *. + apply morph_impl_iff2; only 1-2: auto with *. (* Conversion test raised an anomaly *) do 4 red; intros. rewrite <- H1; rewrite <- H0 in H3; auto. apply TR_rel_inv in H4; destruct H4. diff --git a/ZFskol.v b/ZFskol.v index 65bfdbd..00501d3 100644 --- a/ZFskol.v +++ b/ZFskol.v @@ -41,8 +41,7 @@ Lemma set_intro : forall (f:Z.set->Prop) (P:set->Prop), (forall Hex Huniq, P (exist _ f (conj Hex Huniq))) -> sig P. intros. -exists (exist (fun _ => _ /\ _) f (conj H H0)); trivial. (* regression of unification *) -(*exists (exist _ f (conj H H0)); trivial.*) +exists (exist _ f (conj H H0)); trivial. Qed. Inductive in_set_ (x y:set) : Prop := diff --git a/ZFskolEm.v b/ZFskolEm.v index f2112dc..0a86db9 100644 --- a/ZFskolEm.v +++ b/ZFskolEm.v @@ -49,8 +49,7 @@ Lemma set_intro : forall (f:Z.set->Prop) (P:set->Prop), (forall Hex Huniq, P (exist _ f (conj Hex Huniq))) -> sig P. intros. -exists (exist (fun _ => _ /\ _) f (conj H H0)); trivial. (* regression of unification *) -(*exists (exist _ f (conj H H0)); trivial.*) +exists (exist _ f (conj H H0)); trivial. Qed. (** Membership. (Uses an inductive to avoid unwanted unfolding...) *) diff --git a/ZFsposd.v b/ZFsposd.v index b707062..8f4f01f 100644 --- a/ZFsposd.v +++ b/ZFsposd.v @@ -329,7 +329,7 @@ Lemma isDPos_consrec F G : isDPositive F -> isDPositive G -> isDPositive (dpos_consrec F G). -intros (Fp,Fdm,Fdmo,F3m,F4m,Fty) (Gp,Gdm,Gdmo,G3m,G4m,Gty). +intros (Fp,Fdm,Fdmo,F3m,F4m,Fty,?) (Gp,Gdm,Gdmo,G3m,G4m,Gty,?). constructor; simpl; intros. apply isPos_consrec; trivial. diff --git a/basic.v b/basic.v index e223f9f..a6623b5 100644 --- a/basic.v +++ b/basic.v @@ -11,6 +11,9 @@ Require Export Coq.Program.Basics. Require Export Setoid Morphisms Morphisms_Prop. Export ProperNotations. +(* Compatibility file. *) +Require Export CoqCompat. + Hint Resolve t_step rt_step rt_refl: core. Hint Unfold transp: core. diff --git a/hEns.v b/hEns.v index 200b386..f2f050b 100644 --- a/hEns.v +++ b/hEns.v @@ -336,7 +336,7 @@ Qed. Definition quo_i {X} {R:X->X->Prop} (Rr:isRel R) (x:X) : quo X R := - existT (fun P => tr(isClass R P)) + exist (fun P => tr(isClass R P)) (fun y => R x y) (tr_i (isClass_eq Rr x)). From e0183fec41ab8d8b89938a6d4f33deaa38408748 Mon Sep 17 00:00:00 2001 From: Cyprien Mangin Date: Mon, 28 Aug 2017 11:14:57 +0200 Subject: [PATCH 2/2] Fix some dependencies. --- .depend | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.depend b/.depend index c85d113..1b22b6a 100644 --- a/.depend +++ b/.depend @@ -1,7 +1,7 @@ AbsSNT.vo AbsSNT.glob AbsSNT.v.beautified: AbsSNT.v GenLemmas.vo AbsTheoryIntp.vo AbsTheoryIntp.vo AbsTheoryIntp.glob AbsTheoryIntp.v.beautified: AbsTheoryIntp.v GenLemmas.vo AbsTheorySyn.vo AbsTheorySem.vo AbsTheorySem.vo AbsTheorySem.glob AbsTheorySem.v.beautified: AbsTheorySem.v GenLemmas.vo -AbsTheorySyn.vo AbsTheorySyn.glob AbsTheorySyn.v.beautified: AbsTheorySyn.v +AbsTheorySyn.vo AbsTheorySyn.glob AbsTheorySyn.v.beautified: AbsTheorySyn.v CoqCompat.vo CCTnat.vo CCTnat.glob CCTnat.v.beautified: CCTnat.v Explicit_sub.vo FOTheory.vo basic.vo CCUT.vo CCUT.glob CCUT.v.beautified: CCUT.v Models.vo GenModelSN.vo ZF.vo ZFind_nat.vo SN_CC.vo Can.vo Can.glob Can.v.beautified: Can.v Lambda.vo @@ -144,3 +144,4 @@ ZFwpaths.vo ZFwpaths.glob ZFwpaths.v.beautified: ZFwpaths.v ZF.vo ZFpairs.vo ZFs CoqCompat.vo CoqCompat.glob CoqCompat.v.beautified: CoqCompat.v basic.vo basic.glob basic.v.beautified: basic.v CoqCompat.vo test.vo test.glob test.v.beautified: test.v Lambda.vo +hEns.vo hEns.global hEns.v.beautified: hEns.v ZFskol.vo Sublogic.vo