From ba417a099b2d745f3986db73b3b2c812ac10632f Mon Sep 17 00:00:00 2001 From: Kenji Maillard Date: Mon, 13 Nov 2023 10:45:21 +0100 Subject: [PATCH] fix compilation errors --- _CoqProject | 133 +-- theories/AutoSubst/Ast.sig | 20 +- theories/AutoSubst/Ast.v | 1500 ++++----------------------------- theories/AutoSubst/unscoped.v | 2 + 4 files changed, 216 insertions(+), 1439 deletions(-) diff --git a/_CoqProject b/_CoqProject index 47e3af4c..023bbb4b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -12,69 +12,70 @@ theories/AutoSubst/Extra.v theories/Context.v theories/Notations.v -theories/NormalForms.v -theories/Weakening.v -theories/UntypedReduction.v -theories/UntypedValues.v -theories/GenericTyping.v - -theories/DeclarativeTyping.v -theories/DeclarativeInstance.v - -theories/LogicalRelation.v -theories/LogicalRelation/Induction.v -theories/LogicalRelation/Escape.v -theories/LogicalRelation/ShapeView.v -theories/LogicalRelation/Reflexivity.v -theories/LogicalRelation/Irrelevance.v -theories/LogicalRelation/Weakening.v -theories/LogicalRelation/Universe.v -theories/LogicalRelation/Neutral.v -theories/LogicalRelation/Transitivity.v -theories/LogicalRelation/Reduction.v -theories/LogicalRelation/NormalRed.v -theories/LogicalRelation/Application.v -theories/LogicalRelation/SimpleArr.v -theories/LogicalRelation/Id.v - -theories/Validity.v -theories/Substitution/Irrelevance.v -theories/Substitution/Properties.v -theories/Substitution/Escape.v -theories/Substitution/Conversion.v -theories/Substitution/Reflexivity.v -theories/Substitution/Reduction.v -theories/Substitution/SingleSubst.v -theories/Substitution/Introductions/Application.v -theories/Substitution/Introductions/Universe.v -theories/Substitution/Introductions/Poly.v -theories/Substitution/Introductions/Pi.v -theories/Substitution/Introductions/Lambda.v -theories/Substitution/Introductions/SimpleArr.v -theories/Substitution/Introductions/Var.v -theories/Substitution/Introductions/Nat.v -theories/Substitution/Introductions/Empty.v -theories/Substitution/Introductions/Sigma.v -theories/Substitution/Introductions/Id.v -theories/Fundamental.v - -theories/AlgorithmicTyping.v -theories/DeclarativeSubst.v -theories/TypeConstructorsInj.v -theories/Normalisation.v -theories/Consequences.v - -theories/BundledAlgorithmicTyping.v -theories/AlgorithmicConvProperties.v -theories/AlgorithmicTypingProperties.v -theories/TypeUniqueness.v - -theories/Decidability/Functions.v -theories/Decidability/Soundness.v -theories/Decidability/Completeness.v -theories/Decidability/Termination.v -theories/Decidability.v - -theories/TermNotations.v -theories/Decidability/Execution.v -theories/Positivity.v +# theories/NormalForms.v +# theories/Weakening.v +# theories/UntypedReduction.v +# theories/UntypedValues.v +# theories/GenericTyping.v +# +# theories/DeclarativeTyping.v +# theories/DeclarativeInstance.v +# +# theories/LogicalRelation.v +# theories/LogicalRelation/Induction.v +# theories/LogicalRelation/Escape.v +# theories/LogicalRelation/ShapeView.v +# theories/LogicalRelation/Reflexivity.v +# theories/LogicalRelation/Irrelevance.v +# theories/LogicalRelation/Weakening.v +# theories/LogicalRelation/Universe.v +# theories/LogicalRelation/Neutral.v +# theories/LogicalRelation/Transitivity.v +# theories/LogicalRelation/Reduction.v +# theories/LogicalRelation/NormalRed.v +# theories/LogicalRelation/Application.v +# theories/LogicalRelation/SimpleArr.v +# theories/LogicalRelation/Id.v +# +# theories/Validity.v +# theories/Substitution/Irrelevance.v +# theories/Substitution/Properties.v +# theories/Substitution/Escape.v +# theories/Substitution/Conversion.v +# theories/Substitution/Reflexivity.v +# theories/Substitution/Reduction.v +# theories/Substitution/SingleSubst.v +# theories/Substitution/Introductions/Application.v +# theories/Substitution/Introductions/Universe.v +# theories/Substitution/Introductions/Poly.v +# theories/Substitution/Introductions/Pi.v +# theories/Substitution/Introductions/Lambda.v +# theories/Substitution/Introductions/SimpleArr.v +# theories/Substitution/Introductions/Var.v +# theories/Substitution/Introductions/Nat.v +# theories/Substitution/Introductions/Empty.v +# theories/Substitution/Introductions/Sigma.v +# theories/Substitution/Introductions/Id.v +# theories/Fundamental.v +# +# theories/AlgorithmicTyping.v +# theories/DeclarativeSubst.v +# theories/TypeConstructorsInj.v +# theories/Normalisation.v +# theories/Consequences.v +# +# theories/BundledAlgorithmicTyping.v +# theories/AlgorithmicConvProperties.v +# theories/AlgorithmicTypingProperties.v +# theories/TypeUniqueness.v +# +# theories/Decidability/Functions.v +# theories/Decidability/Soundness.v +# theories/Decidability/Completeness.v +# theories/Decidability/Termination.v +# theories/Decidability.v +# +# theories/TermNotations.v +# theories/Decidability/Execution.v +# theories/Positivity.v +# \ No newline at end of file diff --git a/theories/AutoSubst/Ast.sig b/theories/AutoSubst/Ast.sig index e137ebb1..71791236 100644 --- a/theories/AutoSubst/Ast.sig +++ b/theories/AutoSubst/Ast.sig @@ -7,19 +7,7 @@ tProd : term -> (bind term in term) -> term tLambda : term -> (bind term in term) -> term tApp : term -> term -> term -tNat : term -tZero : term -tSucc : term -> term -tNatElim : (bind term in term) -> term -> term -> term -> term - -tEmpty : term -tEmptyElim : (bind term in term) -> term -> term - -tSig : term -> (bind term in term) -> term -tPair : term -> (bind term in term) -> term -> term -> term -tFst : term -> term -tSnd : term -> term - -tId : term -> term -> term -> term -tRefl : term -> term -> term -tIdElim : term -> term -> (bind term , term in term) -> term -> term -> term -> term \ No newline at end of file +tBool : term +tTrue : term +tFalse : term +tIfte : term -> term -> term -> term \ No newline at end of file diff --git a/theories/AutoSubst/Ast.v b/theories/AutoSubst/Ast.v index 35f3e85e..65315440 100644 --- a/theories/AutoSubst/Ast.v +++ b/theories/AutoSubst/Ast.v @@ -11,19 +11,10 @@ Inductive term : Type := | tProd : term -> term -> term | tLambda : term -> term -> term | tApp : term -> term -> term - | tNat : term - | tZero : term - | tSucc : term -> term - | tNatElim : term -> term -> term -> term -> term - | tEmpty : term - | tEmptyElim : term -> term -> term - | tSig : term -> term -> term - | tPair : term -> term -> term -> term -> term - | tFst : term -> term - | tSnd : term -> term - | tId : term -> term -> term -> term - | tRefl : term -> term -> term - | tIdElim : term -> term -> term -> term -> term -> term -> term. + | tBool : term + | tTrue : term + | tFalse : term + | tIfte : term -> term -> term -> term. Lemma congr_tSort {s0 : sort} {t0 : sort} (H0 : s0 = t0) : tSort s0 = tSort t0. @@ -52,111 +43,29 @@ exact (eq_trans (eq_trans eq_refl (ap (fun x => tApp x s1) H0)) (ap (fun x => tApp t0 x) H1)). Qed. -Lemma congr_tNat : tNat = tNat. +Lemma congr_tBool : tBool = tBool. Proof. exact (eq_refl). Qed. -Lemma congr_tZero : tZero = tZero. +Lemma congr_tTrue : tTrue = tTrue. Proof. exact (eq_refl). Qed. -Lemma congr_tSucc {s0 : term} {t0 : term} (H0 : s0 = t0) : - tSucc s0 = tSucc t0. -Proof. -exact (eq_trans eq_refl (ap (fun x => tSucc x) H0)). -Qed. - -Lemma congr_tNatElim {s0 : term} {s1 : term} {s2 : term} {s3 : term} - {t0 : term} {t1 : term} {t2 : term} {t3 : term} (H0 : s0 = t0) - (H1 : s1 = t1) (H2 : s2 = t2) (H3 : s3 = t3) : - tNatElim s0 s1 s2 s3 = tNatElim t0 t1 t2 t3. -Proof. -exact (eq_trans - (eq_trans - (eq_trans - (eq_trans eq_refl (ap (fun x => tNatElim x s1 s2 s3) H0)) - (ap (fun x => tNatElim t0 x s2 s3) H1)) - (ap (fun x => tNatElim t0 t1 x s3) H2)) - (ap (fun x => tNatElim t0 t1 t2 x) H3)). -Qed. - -Lemma congr_tEmpty : tEmpty = tEmpty. +Lemma congr_tFalse : tFalse = tFalse. Proof. exact (eq_refl). Qed. -Lemma congr_tEmptyElim {s0 : term} {s1 : term} {t0 : term} {t1 : term} - (H0 : s0 = t0) (H1 : s1 = t1) : tEmptyElim s0 s1 = tEmptyElim t0 t1. -Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => tEmptyElim x s1) H0)) - (ap (fun x => tEmptyElim t0 x) H1)). -Qed. - -Lemma congr_tSig {s0 : term} {s1 : term} {t0 : term} {t1 : term} - (H0 : s0 = t0) (H1 : s1 = t1) : tSig s0 s1 = tSig t0 t1. -Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => tSig x s1) H0)) - (ap (fun x => tSig t0 x) H1)). -Qed. - -Lemma congr_tPair {s0 : term} {s1 : term} {s2 : term} {s3 : term} {t0 : term} - {t1 : term} {t2 : term} {t3 : term} (H0 : s0 = t0) (H1 : s1 = t1) - (H2 : s2 = t2) (H3 : s3 = t3) : tPair s0 s1 s2 s3 = tPair t0 t1 t2 t3. -Proof. -exact (eq_trans - (eq_trans - (eq_trans (eq_trans eq_refl (ap (fun x => tPair x s1 s2 s3) H0)) - (ap (fun x => tPair t0 x s2 s3) H1)) - (ap (fun x => tPair t0 t1 x s3) H2)) - (ap (fun x => tPair t0 t1 t2 x) H3)). -Qed. - -Lemma congr_tFst {s0 : term} {t0 : term} (H0 : s0 = t0) : tFst s0 = tFst t0. -Proof. -exact (eq_trans eq_refl (ap (fun x => tFst x) H0)). -Qed. - -Lemma congr_tSnd {s0 : term} {t0 : term} (H0 : s0 = t0) : tSnd s0 = tSnd t0. -Proof. -exact (eq_trans eq_refl (ap (fun x => tSnd x) H0)). -Qed. - -Lemma congr_tId {s0 : term} {s1 : term} {s2 : term} {t0 : term} {t1 : term} +Lemma congr_tIfte {s0 : term} {s1 : term} {s2 : term} {t0 : term} {t1 : term} {t2 : term} (H0 : s0 = t0) (H1 : s1 = t1) (H2 : s2 = t2) : - tId s0 s1 s2 = tId t0 t1 t2. -Proof. -exact (eq_trans - (eq_trans (eq_trans eq_refl (ap (fun x => tId x s1 s2) H0)) - (ap (fun x => tId t0 x s2) H1)) (ap (fun x => tId t0 t1 x) H2)). -Qed. - -Lemma congr_tRefl {s0 : term} {s1 : term} {t0 : term} {t1 : term} - (H0 : s0 = t0) (H1 : s1 = t1) : tRefl s0 s1 = tRefl t0 t1. -Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => tRefl x s1) H0)) - (ap (fun x => tRefl t0 x) H1)). -Qed. - -Lemma congr_tIdElim {s0 : term} {s1 : term} {s2 : term} {s3 : term} - {s4 : term} {s5 : term} {t0 : term} {t1 : term} {t2 : term} {t3 : term} - {t4 : term} {t5 : term} (H0 : s0 = t0) (H1 : s1 = t1) (H2 : s2 = t2) - (H3 : s3 = t3) (H4 : s4 = t4) (H5 : s5 = t5) : - tIdElim s0 s1 s2 s3 s4 s5 = tIdElim t0 t1 t2 t3 t4 t5. + tIfte s0 s1 s2 = tIfte t0 t1 t2. Proof. exact (eq_trans - (eq_trans - (eq_trans - (eq_trans - (eq_trans - (eq_trans eq_refl - (ap (fun x => tIdElim x s1 s2 s3 s4 s5) H0)) - (ap (fun x => tIdElim t0 x s2 s3 s4 s5) H1)) - (ap (fun x => tIdElim t0 t1 x s3 s4 s5) H2)) - (ap (fun x => tIdElim t0 t1 t2 x s4 s5) H3)) - (ap (fun x => tIdElim t0 t1 t2 t3 x s5) H4)) - (ap (fun x => tIdElim t0 t1 t2 t3 t4 x) H5)). + (eq_trans (eq_trans eq_refl (ap (fun x => tIfte x s1 s2) H0)) + (ap (fun x => tIfte t0 x s2) H1)) + (ap (fun x => tIfte t0 t1 x) H2)). Qed. Lemma upRen_term_term (xi : nat -> nat) : nat -> nat. @@ -173,30 +82,11 @@ Fixpoint ren_term (xi_term : nat -> nat) (s : term) {struct s} : term := | tLambda s0 s1 => tLambda (ren_term xi_term s0) (ren_term (upRen_term_term xi_term) s1) | tApp s0 s1 => tApp (ren_term xi_term s0) (ren_term xi_term s1) - | tNat => tNat - | tZero => tZero - | tSucc s0 => tSucc (ren_term xi_term s0) - | tNatElim s0 s1 s2 s3 => - tNatElim (ren_term (upRen_term_term xi_term) s0) (ren_term xi_term s1) - (ren_term xi_term s2) (ren_term xi_term s3) - | tEmpty => tEmpty - | tEmptyElim s0 s1 => - tEmptyElim (ren_term (upRen_term_term xi_term) s0) - (ren_term xi_term s1) - | tSig s0 s1 => - tSig (ren_term xi_term s0) (ren_term (upRen_term_term xi_term) s1) - | tPair s0 s1 s2 s3 => - tPair (ren_term xi_term s0) (ren_term (upRen_term_term xi_term) s1) - (ren_term xi_term s2) (ren_term xi_term s3) - | tFst s0 => tFst (ren_term xi_term s0) - | tSnd s0 => tSnd (ren_term xi_term s0) - | tId s0 s1 s2 => - tId (ren_term xi_term s0) (ren_term xi_term s1) (ren_term xi_term s2) - | tRefl s0 s1 => tRefl (ren_term xi_term s0) (ren_term xi_term s1) - | tIdElim s0 s1 s2 s3 s4 s5 => - tIdElim (ren_term xi_term s0) (ren_term xi_term s1) - (ren_term (upRen_term_term (upRen_term_term xi_term)) s2) - (ren_term xi_term s3) (ren_term xi_term s4) (ren_term xi_term s5) + | tBool => tBool + | tTrue => tTrue + | tFalse => tFalse + | tIfte s0 s1 s2 => + tIfte (ren_term xi_term s0) (ren_term xi_term s1) (ren_term xi_term s2) end. Lemma up_term_term (sigma : nat -> term) : nat -> term. @@ -216,36 +106,12 @@ term := tLambda (subst_term sigma_term s0) (subst_term (up_term_term sigma_term) s1) | tApp s0 s1 => tApp (subst_term sigma_term s0) (subst_term sigma_term s1) - | tNat => tNat - | tZero => tZero - | tSucc s0 => tSucc (subst_term sigma_term s0) - | tNatElim s0 s1 s2 s3 => - tNatElim (subst_term (up_term_term sigma_term) s0) - (subst_term sigma_term s1) (subst_term sigma_term s2) - (subst_term sigma_term s3) - | tEmpty => tEmpty - | tEmptyElim s0 s1 => - tEmptyElim (subst_term (up_term_term sigma_term) s0) - (subst_term sigma_term s1) - | tSig s0 s1 => - tSig (subst_term sigma_term s0) - (subst_term (up_term_term sigma_term) s1) - | tPair s0 s1 s2 s3 => - tPair (subst_term sigma_term s0) - (subst_term (up_term_term sigma_term) s1) (subst_term sigma_term s2) - (subst_term sigma_term s3) - | tFst s0 => tFst (subst_term sigma_term s0) - | tSnd s0 => tSnd (subst_term sigma_term s0) - | tId s0 s1 s2 => - tId (subst_term sigma_term s0) (subst_term sigma_term s1) + | tBool => tBool + | tTrue => tTrue + | tFalse => tFalse + | tIfte s0 s1 s2 => + tIfte (subst_term sigma_term s0) (subst_term sigma_term s1) (subst_term sigma_term s2) - | tRefl s0 s1 => - tRefl (subst_term sigma_term s0) (subst_term sigma_term s1) - | tIdElim s0 s1 s2 s3 s4 s5 => - tIdElim (subst_term sigma_term s0) (subst_term sigma_term s1) - (subst_term (up_term_term (up_term_term sigma_term)) s2) - (subst_term sigma_term s3) (subst_term sigma_term s4) - (subst_term sigma_term s5) end. Lemma upId_term_term (sigma : nat -> term) (Eq : forall x, sigma x = tRel x) @@ -273,45 +139,13 @@ subst_term sigma_term s = s := | tApp s0 s1 => congr_tApp (idSubst_term sigma_term Eq_term s0) (idSubst_term sigma_term Eq_term s1) - | tNat => congr_tNat - | tZero => congr_tZero - | tSucc s0 => congr_tSucc (idSubst_term sigma_term Eq_term s0) - | tNatElim s0 s1 s2 s3 => - congr_tNatElim - (idSubst_term (up_term_term sigma_term) (upId_term_term _ Eq_term) s0) - (idSubst_term sigma_term Eq_term s1) - (idSubst_term sigma_term Eq_term s2) - (idSubst_term sigma_term Eq_term s3) - | tEmpty => congr_tEmpty - | tEmptyElim s0 s1 => - congr_tEmptyElim - (idSubst_term (up_term_term sigma_term) (upId_term_term _ Eq_term) s0) - (idSubst_term sigma_term Eq_term s1) - | tSig s0 s1 => - congr_tSig (idSubst_term sigma_term Eq_term s0) - (idSubst_term (up_term_term sigma_term) (upId_term_term _ Eq_term) s1) - | tPair s0 s1 s2 s3 => - congr_tPair (idSubst_term sigma_term Eq_term s0) - (idSubst_term (up_term_term sigma_term) (upId_term_term _ Eq_term) s1) - (idSubst_term sigma_term Eq_term s2) - (idSubst_term sigma_term Eq_term s3) - | tFst s0 => congr_tFst (idSubst_term sigma_term Eq_term s0) - | tSnd s0 => congr_tSnd (idSubst_term sigma_term Eq_term s0) - | tId s0 s1 s2 => - congr_tId (idSubst_term sigma_term Eq_term s0) + | tBool => congr_tBool + | tTrue => congr_tTrue + | tFalse => congr_tFalse + | tIfte s0 s1 s2 => + congr_tIfte (idSubst_term sigma_term Eq_term s0) (idSubst_term sigma_term Eq_term s1) (idSubst_term sigma_term Eq_term s2) - | tRefl s0 s1 => - congr_tRefl (idSubst_term sigma_term Eq_term s0) - (idSubst_term sigma_term Eq_term s1) - | tIdElim s0 s1 s2 s3 s4 s5 => - congr_tIdElim (idSubst_term sigma_term Eq_term s0) - (idSubst_term sigma_term Eq_term s1) - (idSubst_term (up_term_term (up_term_term sigma_term)) - (upId_term_term _ (upId_term_term _ Eq_term)) s2) - (idSubst_term sigma_term Eq_term s3) - (idSubst_term sigma_term Eq_term s4) - (idSubst_term sigma_term Eq_term s5) end. Lemma upExtRen_term_term (xi : nat -> nat) (zeta : nat -> nat) @@ -341,50 +175,13 @@ ren_term xi_term s = ren_term zeta_term s := | tApp s0 s1 => congr_tApp (extRen_term xi_term zeta_term Eq_term s0) (extRen_term xi_term zeta_term Eq_term s1) - | tNat => congr_tNat - | tZero => congr_tZero - | tSucc s0 => congr_tSucc (extRen_term xi_term zeta_term Eq_term s0) - | tNatElim s0 s1 s2 s3 => - congr_tNatElim - (extRen_term (upRen_term_term xi_term) (upRen_term_term zeta_term) - (upExtRen_term_term _ _ Eq_term) s0) - (extRen_term xi_term zeta_term Eq_term s1) - (extRen_term xi_term zeta_term Eq_term s2) - (extRen_term xi_term zeta_term Eq_term s3) - | tEmpty => congr_tEmpty - | tEmptyElim s0 s1 => - congr_tEmptyElim - (extRen_term (upRen_term_term xi_term) (upRen_term_term zeta_term) - (upExtRen_term_term _ _ Eq_term) s0) - (extRen_term xi_term zeta_term Eq_term s1) - | tSig s0 s1 => - congr_tSig (extRen_term xi_term zeta_term Eq_term s0) - (extRen_term (upRen_term_term xi_term) (upRen_term_term zeta_term) - (upExtRen_term_term _ _ Eq_term) s1) - | tPair s0 s1 s2 s3 => - congr_tPair (extRen_term xi_term zeta_term Eq_term s0) - (extRen_term (upRen_term_term xi_term) (upRen_term_term zeta_term) - (upExtRen_term_term _ _ Eq_term) s1) - (extRen_term xi_term zeta_term Eq_term s2) - (extRen_term xi_term zeta_term Eq_term s3) - | tFst s0 => congr_tFst (extRen_term xi_term zeta_term Eq_term s0) - | tSnd s0 => congr_tSnd (extRen_term xi_term zeta_term Eq_term s0) - | tId s0 s1 s2 => - congr_tId (extRen_term xi_term zeta_term Eq_term s0) + | tBool => congr_tBool + | tTrue => congr_tTrue + | tFalse => congr_tFalse + | tIfte s0 s1 s2 => + congr_tIfte (extRen_term xi_term zeta_term Eq_term s0) (extRen_term xi_term zeta_term Eq_term s1) (extRen_term xi_term zeta_term Eq_term s2) - | tRefl s0 s1 => - congr_tRefl (extRen_term xi_term zeta_term Eq_term s0) - (extRen_term xi_term zeta_term Eq_term s1) - | tIdElim s0 s1 s2 s3 s4 s5 => - congr_tIdElim (extRen_term xi_term zeta_term Eq_term s0) - (extRen_term xi_term zeta_term Eq_term s1) - (extRen_term (upRen_term_term (upRen_term_term xi_term)) - (upRen_term_term (upRen_term_term zeta_term)) - (upExtRen_term_term _ _ (upExtRen_term_term _ _ Eq_term)) s2) - (extRen_term xi_term zeta_term Eq_term s3) - (extRen_term xi_term zeta_term Eq_term s4) - (extRen_term xi_term zeta_term Eq_term s5) end. Lemma upExt_term_term (sigma : nat -> term) (tau : nat -> term) @@ -415,50 +212,13 @@ subst_term sigma_term s = subst_term tau_term s := | tApp s0 s1 => congr_tApp (ext_term sigma_term tau_term Eq_term s0) (ext_term sigma_term tau_term Eq_term s1) - | tNat => congr_tNat - | tZero => congr_tZero - | tSucc s0 => congr_tSucc (ext_term sigma_term tau_term Eq_term s0) - | tNatElim s0 s1 s2 s3 => - congr_tNatElim - (ext_term (up_term_term sigma_term) (up_term_term tau_term) - (upExt_term_term _ _ Eq_term) s0) - (ext_term sigma_term tau_term Eq_term s1) - (ext_term sigma_term tau_term Eq_term s2) - (ext_term sigma_term tau_term Eq_term s3) - | tEmpty => congr_tEmpty - | tEmptyElim s0 s1 => - congr_tEmptyElim - (ext_term (up_term_term sigma_term) (up_term_term tau_term) - (upExt_term_term _ _ Eq_term) s0) - (ext_term sigma_term tau_term Eq_term s1) - | tSig s0 s1 => - congr_tSig (ext_term sigma_term tau_term Eq_term s0) - (ext_term (up_term_term sigma_term) (up_term_term tau_term) - (upExt_term_term _ _ Eq_term) s1) - | tPair s0 s1 s2 s3 => - congr_tPair (ext_term sigma_term tau_term Eq_term s0) - (ext_term (up_term_term sigma_term) (up_term_term tau_term) - (upExt_term_term _ _ Eq_term) s1) - (ext_term sigma_term tau_term Eq_term s2) - (ext_term sigma_term tau_term Eq_term s3) - | tFst s0 => congr_tFst (ext_term sigma_term tau_term Eq_term s0) - | tSnd s0 => congr_tSnd (ext_term sigma_term tau_term Eq_term s0) - | tId s0 s1 s2 => - congr_tId (ext_term sigma_term tau_term Eq_term s0) + | tBool => congr_tBool + | tTrue => congr_tTrue + | tFalse => congr_tFalse + | tIfte s0 s1 s2 => + congr_tIfte (ext_term sigma_term tau_term Eq_term s0) (ext_term sigma_term tau_term Eq_term s1) (ext_term sigma_term tau_term Eq_term s2) - | tRefl s0 s1 => - congr_tRefl (ext_term sigma_term tau_term Eq_term s0) - (ext_term sigma_term tau_term Eq_term s1) - | tIdElim s0 s1 s2 s3 s4 s5 => - congr_tIdElim (ext_term sigma_term tau_term Eq_term s0) - (ext_term sigma_term tau_term Eq_term s1) - (ext_term (up_term_term (up_term_term sigma_term)) - (up_term_term (up_term_term tau_term)) - (upExt_term_term _ _ (upExt_term_term _ _ Eq_term)) s2) - (ext_term sigma_term tau_term Eq_term s3) - (ext_term sigma_term tau_term Eq_term s4) - (ext_term sigma_term tau_term Eq_term s5) end. Lemma up_ren_ren_term_term (xi : nat -> nat) (zeta : nat -> nat) @@ -490,58 +250,13 @@ Fixpoint compRenRen_term (xi_term : nat -> nat) (zeta_term : nat -> nat) | tApp s0 s1 => congr_tApp (compRenRen_term xi_term zeta_term rho_term Eq_term s0) (compRenRen_term xi_term zeta_term rho_term Eq_term s1) - | tNat => congr_tNat - | tZero => congr_tZero - | tSucc s0 => - congr_tSucc (compRenRen_term xi_term zeta_term rho_term Eq_term s0) - | tNatElim s0 s1 s2 s3 => - congr_tNatElim - (compRenRen_term (upRen_term_term xi_term) - (upRen_term_term zeta_term) (upRen_term_term rho_term) - (up_ren_ren _ _ _ Eq_term) s0) - (compRenRen_term xi_term zeta_term rho_term Eq_term s1) - (compRenRen_term xi_term zeta_term rho_term Eq_term s2) - (compRenRen_term xi_term zeta_term rho_term Eq_term s3) - | tEmpty => congr_tEmpty - | tEmptyElim s0 s1 => - congr_tEmptyElim - (compRenRen_term (upRen_term_term xi_term) - (upRen_term_term zeta_term) (upRen_term_term rho_term) - (up_ren_ren _ _ _ Eq_term) s0) - (compRenRen_term xi_term zeta_term rho_term Eq_term s1) - | tSig s0 s1 => - congr_tSig (compRenRen_term xi_term zeta_term rho_term Eq_term s0) - (compRenRen_term (upRen_term_term xi_term) - (upRen_term_term zeta_term) (upRen_term_term rho_term) - (up_ren_ren _ _ _ Eq_term) s1) - | tPair s0 s1 s2 s3 => - congr_tPair (compRenRen_term xi_term zeta_term rho_term Eq_term s0) - (compRenRen_term (upRen_term_term xi_term) - (upRen_term_term zeta_term) (upRen_term_term rho_term) - (up_ren_ren _ _ _ Eq_term) s1) - (compRenRen_term xi_term zeta_term rho_term Eq_term s2) - (compRenRen_term xi_term zeta_term rho_term Eq_term s3) - | tFst s0 => - congr_tFst (compRenRen_term xi_term zeta_term rho_term Eq_term s0) - | tSnd s0 => - congr_tSnd (compRenRen_term xi_term zeta_term rho_term Eq_term s0) - | tId s0 s1 s2 => - congr_tId (compRenRen_term xi_term zeta_term rho_term Eq_term s0) + | tBool => congr_tBool + | tTrue => congr_tTrue + | tFalse => congr_tFalse + | tIfte s0 s1 s2 => + congr_tIfte (compRenRen_term xi_term zeta_term rho_term Eq_term s0) (compRenRen_term xi_term zeta_term rho_term Eq_term s1) (compRenRen_term xi_term zeta_term rho_term Eq_term s2) - | tRefl s0 s1 => - congr_tRefl (compRenRen_term xi_term zeta_term rho_term Eq_term s0) - (compRenRen_term xi_term zeta_term rho_term Eq_term s1) - | tIdElim s0 s1 s2 s3 s4 s5 => - congr_tIdElim (compRenRen_term xi_term zeta_term rho_term Eq_term s0) - (compRenRen_term xi_term zeta_term rho_term Eq_term s1) - (compRenRen_term (upRen_term_term (upRen_term_term xi_term)) - (upRen_term_term (upRen_term_term zeta_term)) - (upRen_term_term (upRen_term_term rho_term)) - (up_ren_ren _ _ _ (up_ren_ren _ _ _ Eq_term)) s2) - (compRenRen_term xi_term zeta_term rho_term Eq_term s3) - (compRenRen_term xi_term zeta_term rho_term Eq_term s4) - (compRenRen_term xi_term zeta_term rho_term Eq_term s5) end. Lemma up_ren_subst_term_term (xi : nat -> nat) (tau : nat -> term) @@ -578,57 +293,13 @@ subst_term tau_term (ren_term xi_term s) = subst_term theta_term s := | tApp s0 s1 => congr_tApp (compRenSubst_term xi_term tau_term theta_term Eq_term s0) (compRenSubst_term xi_term tau_term theta_term Eq_term s1) - | tNat => congr_tNat - | tZero => congr_tZero - | tSucc s0 => - congr_tSucc (compRenSubst_term xi_term tau_term theta_term Eq_term s0) - | tNatElim s0 s1 s2 s3 => - congr_tNatElim - (compRenSubst_term (upRen_term_term xi_term) (up_term_term tau_term) - (up_term_term theta_term) (up_ren_subst_term_term _ _ _ Eq_term) - s0) (compRenSubst_term xi_term tau_term theta_term Eq_term s1) - (compRenSubst_term xi_term tau_term theta_term Eq_term s2) - (compRenSubst_term xi_term tau_term theta_term Eq_term s3) - | tEmpty => congr_tEmpty - | tEmptyElim s0 s1 => - congr_tEmptyElim - (compRenSubst_term (upRen_term_term xi_term) (up_term_term tau_term) - (up_term_term theta_term) (up_ren_subst_term_term _ _ _ Eq_term) - s0) (compRenSubst_term xi_term tau_term theta_term Eq_term s1) - | tSig s0 s1 => - congr_tSig (compRenSubst_term xi_term tau_term theta_term Eq_term s0) - (compRenSubst_term (upRen_term_term xi_term) (up_term_term tau_term) - (up_term_term theta_term) (up_ren_subst_term_term _ _ _ Eq_term) - s1) - | tPair s0 s1 s2 s3 => - congr_tPair (compRenSubst_term xi_term tau_term theta_term Eq_term s0) - (compRenSubst_term (upRen_term_term xi_term) (up_term_term tau_term) - (up_term_term theta_term) (up_ren_subst_term_term _ _ _ Eq_term) - s1) (compRenSubst_term xi_term tau_term theta_term Eq_term s2) - (compRenSubst_term xi_term tau_term theta_term Eq_term s3) - | tFst s0 => - congr_tFst (compRenSubst_term xi_term tau_term theta_term Eq_term s0) - | tSnd s0 => - congr_tSnd (compRenSubst_term xi_term tau_term theta_term Eq_term s0) - | tId s0 s1 s2 => - congr_tId (compRenSubst_term xi_term tau_term theta_term Eq_term s0) + | tBool => congr_tBool + | tTrue => congr_tTrue + | tFalse => congr_tFalse + | tIfte s0 s1 s2 => + congr_tIfte (compRenSubst_term xi_term tau_term theta_term Eq_term s0) (compRenSubst_term xi_term tau_term theta_term Eq_term s1) (compRenSubst_term xi_term tau_term theta_term Eq_term s2) - | tRefl s0 s1 => - congr_tRefl (compRenSubst_term xi_term tau_term theta_term Eq_term s0) - (compRenSubst_term xi_term tau_term theta_term Eq_term s1) - | tIdElim s0 s1 s2 s3 s4 s5 => - congr_tIdElim - (compRenSubst_term xi_term tau_term theta_term Eq_term s0) - (compRenSubst_term xi_term tau_term theta_term Eq_term s1) - (compRenSubst_term (upRen_term_term (upRen_term_term xi_term)) - (up_term_term (up_term_term tau_term)) - (up_term_term (up_term_term theta_term)) - (up_ren_subst_term_term _ _ _ - (up_ren_subst_term_term _ _ _ Eq_term)) s2) - (compRenSubst_term xi_term tau_term theta_term Eq_term s3) - (compRenSubst_term xi_term tau_term theta_term Eq_term s4) - (compRenSubst_term xi_term tau_term theta_term Eq_term s5) end. Lemma up_subst_ren_term_term (sigma : nat -> term) (zeta_term : nat -> nat) @@ -677,67 +348,14 @@ ren_term zeta_term (subst_term sigma_term s) = subst_term theta_term s := congr_tApp (compSubstRen_term sigma_term zeta_term theta_term Eq_term s0) (compSubstRen_term sigma_term zeta_term theta_term Eq_term s1) - | tNat => congr_tNat - | tZero => congr_tZero - | tSucc s0 => - congr_tSucc - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s0) - | tNatElim s0 s1 s2 s3 => - congr_tNatElim - (compSubstRen_term (up_term_term sigma_term) - (upRen_term_term zeta_term) (up_term_term theta_term) - (up_subst_ren_term_term _ _ _ Eq_term) s0) - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s1) - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s2) - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s3) - | tEmpty => congr_tEmpty - | tEmptyElim s0 s1 => - congr_tEmptyElim - (compSubstRen_term (up_term_term sigma_term) - (upRen_term_term zeta_term) (up_term_term theta_term) - (up_subst_ren_term_term _ _ _ Eq_term) s0) - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s1) - | tSig s0 s1 => - congr_tSig - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s0) - (compSubstRen_term (up_term_term sigma_term) - (upRen_term_term zeta_term) (up_term_term theta_term) - (up_subst_ren_term_term _ _ _ Eq_term) s1) - | tPair s0 s1 s2 s3 => - congr_tPair - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s0) - (compSubstRen_term (up_term_term sigma_term) - (upRen_term_term zeta_term) (up_term_term theta_term) - (up_subst_ren_term_term _ _ _ Eq_term) s1) - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s2) - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s3) - | tFst s0 => - congr_tFst - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s0) - | tSnd s0 => - congr_tSnd - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s0) - | tId s0 s1 s2 => - congr_tId + | tBool => congr_tBool + | tTrue => congr_tTrue + | tFalse => congr_tFalse + | tIfte s0 s1 s2 => + congr_tIfte (compSubstRen_term sigma_term zeta_term theta_term Eq_term s0) (compSubstRen_term sigma_term zeta_term theta_term Eq_term s1) (compSubstRen_term sigma_term zeta_term theta_term Eq_term s2) - | tRefl s0 s1 => - congr_tRefl - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s0) - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s1) - | tIdElim s0 s1 s2 s3 s4 s5 => - congr_tIdElim - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s0) - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s1) - (compSubstRen_term (up_term_term (up_term_term sigma_term)) - (upRen_term_term (upRen_term_term zeta_term)) - (up_term_term (up_term_term theta_term)) - (up_subst_ren_term_term _ _ _ - (up_subst_ren_term_term _ _ _ Eq_term)) s2) - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s3) - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s4) - (compSubstRen_term sigma_term zeta_term theta_term Eq_term s5) end. Lemma up_subst_subst_term_term (sigma : nat -> term) (tau_term : nat -> term) @@ -788,67 +406,14 @@ subst_term tau_term (subst_term sigma_term s) = subst_term theta_term s := congr_tApp (compSubstSubst_term sigma_term tau_term theta_term Eq_term s0) (compSubstSubst_term sigma_term tau_term theta_term Eq_term s1) - | tNat => congr_tNat - | tZero => congr_tZero - | tSucc s0 => - congr_tSucc - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s0) - | tNatElim s0 s1 s2 s3 => - congr_tNatElim - (compSubstSubst_term (up_term_term sigma_term) - (up_term_term tau_term) (up_term_term theta_term) - (up_subst_subst_term_term _ _ _ Eq_term) s0) - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s1) - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s2) - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s3) - | tEmpty => congr_tEmpty - | tEmptyElim s0 s1 => - congr_tEmptyElim - (compSubstSubst_term (up_term_term sigma_term) - (up_term_term tau_term) (up_term_term theta_term) - (up_subst_subst_term_term _ _ _ Eq_term) s0) - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s1) - | tSig s0 s1 => - congr_tSig - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s0) - (compSubstSubst_term (up_term_term sigma_term) - (up_term_term tau_term) (up_term_term theta_term) - (up_subst_subst_term_term _ _ _ Eq_term) s1) - | tPair s0 s1 s2 s3 => - congr_tPair - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s0) - (compSubstSubst_term (up_term_term sigma_term) - (up_term_term tau_term) (up_term_term theta_term) - (up_subst_subst_term_term _ _ _ Eq_term) s1) - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s2) - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s3) - | tFst s0 => - congr_tFst - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s0) - | tSnd s0 => - congr_tSnd - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s0) - | tId s0 s1 s2 => - congr_tId + | tBool => congr_tBool + | tTrue => congr_tTrue + | tFalse => congr_tFalse + | tIfte s0 s1 s2 => + congr_tIfte (compSubstSubst_term sigma_term tau_term theta_term Eq_term s0) (compSubstSubst_term sigma_term tau_term theta_term Eq_term s1) (compSubstSubst_term sigma_term tau_term theta_term Eq_term s2) - | tRefl s0 s1 => - congr_tRefl - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s0) - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s1) - | tIdElim s0 s1 s2 s3 s4 s5 => - congr_tIdElim - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s0) - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s1) - (compSubstSubst_term (up_term_term (up_term_term sigma_term)) - (up_term_term (up_term_term tau_term)) - (up_term_term (up_term_term theta_term)) - (up_subst_subst_term_term _ _ _ - (up_subst_subst_term_term _ _ _ Eq_term)) s2) - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s3) - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s4) - (compSubstSubst_term sigma_term tau_term theta_term Eq_term s5) end. Lemma renRen_term (xi_term : nat -> nat) (zeta_term : nat -> nat) (s : term) @@ -946,50 +511,13 @@ Fixpoint rinst_inst_term (xi_term : nat -> nat) (sigma_term : nat -> term) | tApp s0 s1 => congr_tApp (rinst_inst_term xi_term sigma_term Eq_term s0) (rinst_inst_term xi_term sigma_term Eq_term s1) - | tNat => congr_tNat - | tZero => congr_tZero - | tSucc s0 => congr_tSucc (rinst_inst_term xi_term sigma_term Eq_term s0) - | tNatElim s0 s1 s2 s3 => - congr_tNatElim - (rinst_inst_term (upRen_term_term xi_term) (up_term_term sigma_term) - (rinstInst_up_term_term _ _ Eq_term) s0) - (rinst_inst_term xi_term sigma_term Eq_term s1) - (rinst_inst_term xi_term sigma_term Eq_term s2) - (rinst_inst_term xi_term sigma_term Eq_term s3) - | tEmpty => congr_tEmpty - | tEmptyElim s0 s1 => - congr_tEmptyElim - (rinst_inst_term (upRen_term_term xi_term) (up_term_term sigma_term) - (rinstInst_up_term_term _ _ Eq_term) s0) - (rinst_inst_term xi_term sigma_term Eq_term s1) - | tSig s0 s1 => - congr_tSig (rinst_inst_term xi_term sigma_term Eq_term s0) - (rinst_inst_term (upRen_term_term xi_term) (up_term_term sigma_term) - (rinstInst_up_term_term _ _ Eq_term) s1) - | tPair s0 s1 s2 s3 => - congr_tPair (rinst_inst_term xi_term sigma_term Eq_term s0) - (rinst_inst_term (upRen_term_term xi_term) (up_term_term sigma_term) - (rinstInst_up_term_term _ _ Eq_term) s1) - (rinst_inst_term xi_term sigma_term Eq_term s2) - (rinst_inst_term xi_term sigma_term Eq_term s3) - | tFst s0 => congr_tFst (rinst_inst_term xi_term sigma_term Eq_term s0) - | tSnd s0 => congr_tSnd (rinst_inst_term xi_term sigma_term Eq_term s0) - | tId s0 s1 s2 => - congr_tId (rinst_inst_term xi_term sigma_term Eq_term s0) + | tBool => congr_tBool + | tTrue => congr_tTrue + | tFalse => congr_tFalse + | tIfte s0 s1 s2 => + congr_tIfte (rinst_inst_term xi_term sigma_term Eq_term s0) (rinst_inst_term xi_term sigma_term Eq_term s1) (rinst_inst_term xi_term sigma_term Eq_term s2) - | tRefl s0 s1 => - congr_tRefl (rinst_inst_term xi_term sigma_term Eq_term s0) - (rinst_inst_term xi_term sigma_term Eq_term s1) - | tIdElim s0 s1 s2 s3 s4 s5 => - congr_tIdElim (rinst_inst_term xi_term sigma_term Eq_term s0) - (rinst_inst_term xi_term sigma_term Eq_term s1) - (rinst_inst_term (upRen_term_term (upRen_term_term xi_term)) - (up_term_term (up_term_term sigma_term)) - (rinstInst_up_term_term _ _ (rinstInst_up_term_term _ _ Eq_term)) - s2) (rinst_inst_term xi_term sigma_term Eq_term s3) - (rinst_inst_term xi_term sigma_term Eq_term s4) - (rinst_inst_term xi_term sigma_term Eq_term s5) end. Lemma rinstInst'_term (xi_term : nat -> nat) (s : term) : @@ -1054,13 +582,13 @@ Qed. Class Up_term X Y := up_term : X -> Y. -#[global] Instance Subst_term : (Subst1 _ _ _) := @subst_term. +Instance Subst_term : (Subst1 _ _ _) := @subst_term. -#[global] Instance Up_term_term : (Up_term _ _) := @up_term_term. +Instance Up_term_term : (Up_term _ _) := @up_term_term. -#[global] Instance Ren_term : (Ren1 _ _ _) := @ren_term. +Instance Ren_term : (Ren1 _ _ _) := @ren_term. -#[global] Instance VarInstance_term : (Var _ _) := @tRel. +Instance VarInstance_term : (Var _ _) := @tRel. Notation "[ sigma_term ]" := (subst_term sigma_term) ( at level 1, left associativity, only printing) : fscope. @@ -1086,7 +614,7 @@ Notation "x '__term'" := (@ids _ _ VarInstance_term x) Notation "x '__term'" := (tRel x) ( at level 5, format "x __term") : subst_scope. -#[global] Instance subst_term_morphism : +Instance subst_term_morphism : (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) (@subst_term)). Proof. @@ -1095,14 +623,14 @@ exact (fun f_term g_term Eq_term s t Eq_st => (ext_term f_term g_term Eq_term s) t Eq_st). Qed. -#[global] Instance subst_term_morphism2 : +Instance subst_term_morphism2 : (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq)) (@subst_term)). Proof. exact (fun f_term g_term Eq_term s => ext_term f_term g_term Eq_term s). Qed. -#[global] Instance ren_term_morphism : +Instance ren_term_morphism : (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) (@ren_term)). Proof. @@ -1111,7 +639,7 @@ exact (fun f_term g_term Eq_term s t Eq_st => (extRen_term f_term g_term Eq_term s) t Eq_st). Qed. -#[global] Instance ren_term_morphism2 : +Instance ren_term_morphism2 : (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq)) (@ren_term)). Proof. @@ -1192,39 +720,12 @@ Fixpoint allfv_term (p_term : nat -> Prop) (s : term) {struct s} : Prop := (and (allfv_term (upAllfv_term_term p_term) s1) True) | tApp s0 s1 => and (allfv_term p_term s0) (and (allfv_term p_term s1) True) - | tNat => True - | tZero => True - | tSucc s0 => and (allfv_term p_term s0) True - | tNatElim s0 s1 s2 s3 => - and (allfv_term (upAllfv_term_term p_term) s0) - (and (allfv_term p_term s1) - (and (allfv_term p_term s2) (and (allfv_term p_term s3) True))) - | tEmpty => True - | tEmptyElim s0 s1 => - and (allfv_term (upAllfv_term_term p_term) s0) - (and (allfv_term p_term s1) True) - | tSig s0 s1 => - and (allfv_term p_term s0) - (and (allfv_term (upAllfv_term_term p_term) s1) True) - | tPair s0 s1 s2 s3 => - and (allfv_term p_term s0) - (and (allfv_term (upAllfv_term_term p_term) s1) - (and (allfv_term p_term s2) (and (allfv_term p_term s3) True))) - | tFst s0 => and (allfv_term p_term s0) True - | tSnd s0 => and (allfv_term p_term s0) True - | tId s0 s1 s2 => + | tBool => True + | tTrue => True + | tFalse => True + | tIfte s0 s1 s2 => and (allfv_term p_term s0) (and (allfv_term p_term s1) (and (allfv_term p_term s2) True)) - | tRefl s0 s1 => - and (allfv_term p_term s0) (and (allfv_term p_term s1) True) - | tIdElim s0 s1 s2 s3 s4 s5 => - and (allfv_term p_term s0) - (and (allfv_term p_term s1) - (and - (allfv_term (upAllfv_term_term (upAllfv_term_term p_term)) s2) - (and (allfv_term p_term s3) - (and (allfv_term p_term s4) - (and (allfv_term p_term s5) True))))) end. Lemma upAllfvTriv_term_term {p : nat -> Prop} (H : forall x, p x) : @@ -1254,52 +755,13 @@ Fixpoint allfvTriv_term (p_term : nat -> Prop) (H_term : forall x, p_term x) | tApp s0 s1 => conj (allfvTriv_term p_term H_term s0) (conj (allfvTriv_term p_term H_term s1) I) - | tNat => I - | tZero => I - | tSucc s0 => conj (allfvTriv_term p_term H_term s0) I - | tNatElim s0 s1 s2 s3 => - conj - (allfvTriv_term (upAllfv_term_term p_term) - (upAllfvTriv_term_term H_term) s0) - (conj (allfvTriv_term p_term H_term s1) - (conj (allfvTriv_term p_term H_term s2) - (conj (allfvTriv_term p_term H_term s3) I))) - | tEmpty => I - | tEmptyElim s0 s1 => - conj - (allfvTriv_term (upAllfv_term_term p_term) - (upAllfvTriv_term_term H_term) s0) - (conj (allfvTriv_term p_term H_term s1) I) - | tSig s0 s1 => - conj (allfvTriv_term p_term H_term s0) - (conj - (allfvTriv_term (upAllfv_term_term p_term) - (upAllfvTriv_term_term H_term) s1) I) - | tPair s0 s1 s2 s3 => - conj (allfvTriv_term p_term H_term s0) - (conj - (allfvTriv_term (upAllfv_term_term p_term) - (upAllfvTriv_term_term H_term) s1) - (conj (allfvTriv_term p_term H_term s2) - (conj (allfvTriv_term p_term H_term s3) I))) - | tFst s0 => conj (allfvTriv_term p_term H_term s0) I - | tSnd s0 => conj (allfvTriv_term p_term H_term s0) I - | tId s0 s1 s2 => + | tBool => I + | tTrue => I + | tFalse => I + | tIfte s0 s1 s2 => conj (allfvTriv_term p_term H_term s0) (conj (allfvTriv_term p_term H_term s1) (conj (allfvTriv_term p_term H_term s2) I)) - | tRefl s0 s1 => - conj (allfvTriv_term p_term H_term s0) - (conj (allfvTriv_term p_term H_term s1) I) - | tIdElim s0 s1 s2 s3 s4 s5 => - conj (allfvTriv_term p_term H_term s0) - (conj (allfvTriv_term p_term H_term s1) - (conj - (allfvTriv_term (upAllfv_term_term (upAllfv_term_term p_term)) - (upAllfvTriv_term_term (upAllfvTriv_term_term H_term)) s2) - (conj (allfvTriv_term p_term H_term s3) - (conj (allfvTriv_term p_term H_term s4) - (conj (allfvTriv_term p_term H_term s5) I))))) end. Lemma upAllfvImpl_term_term {p : nat -> Prop} {q : nat -> Prop} @@ -1362,20 +824,13 @@ allfv_term p_term s -> allfv_term q_term s := | conj HP _ => HP end end) I) - | tNat => fun HP => I - | tZero => fun HP => I - | tSucc s0 => + | tBool => fun HP => I + | tTrue => fun HP => I + | tFalse => fun HP => I + | tIfte s0 s1 s2 => fun HP => conj (allfvImpl_term p_term q_term H_term s0 - match HP with - | conj HP _ => HP - end) I - | tNatElim s0 s1 s2 s3 => - fun HP => - conj - (allfvImpl_term (upAllfv_term_term p_term) (upAllfv_term_term q_term) - (upAllfvImpl_term_term H_term) s0 match HP with | conj HP _ => HP end) @@ -1395,350 +850,63 @@ allfv_term p_term s -> allfv_term q_term s := | conj HP _ => HP end end - end) - (conj - (allfvImpl_term p_term q_term H_term s3 - match HP with - | conj _ HP => - match HP with - | conj _ HP => - match HP with - | conj _ HP => - match HP with - | conj HP _ => HP - end - end - end - end) I))) - | tEmpty => fun HP => I - | tEmptyElim s0 s1 => - fun HP => + end) I)) + end. + +Lemma upAllfvRenL_term_term (p : nat -> Prop) (xi : nat -> nat) : + forall x, + upAllfv_term_term p (upRen_term_term xi x) -> + upAllfv_term_term (funcomp p xi) x. +Proof. +exact (fun x => match x with + | S n' => fun i => i + | O => fun H => H + end). +Qed. + +Fixpoint allfvRenL_term (p_term : nat -> Prop) (xi_term : nat -> nat) +(s : term) {struct s} : +allfv_term p_term (ren_term xi_term s) -> +allfv_term (funcomp p_term xi_term) s := + match s with + | tRel s0 => fun H => H + | tSort s0 => fun H => conj I I + | tProd s0 s1 => + fun H => conj - (allfvImpl_term (upAllfv_term_term p_term) (upAllfv_term_term q_term) - (upAllfvImpl_term_term H_term) s0 - match HP with - | conj HP _ => HP - end) + (allfvRenL_term p_term xi_term s0 match H with + | conj H _ => H + end) (conj - (allfvImpl_term p_term q_term H_term s1 - match HP with - | conj _ HP => match HP with - | conj HP _ => HP - end - end) I) - | tSig s0 s1 => - fun HP => + (allfvImpl_term _ _ (upAllfvRenL_term_term p_term xi_term) s1 + (allfvRenL_term (upAllfv_term_term p_term) + (upRen_term_term xi_term) s1 + match H with + | conj _ H => match H with + | conj H _ => H + end + end)) I) + | tLambda s0 s1 => + fun H => conj - (allfvImpl_term p_term q_term H_term s0 - match HP with - | conj HP _ => HP - end) + (allfvRenL_term p_term xi_term s0 match H with + | conj H _ => H + end) (conj - (allfvImpl_term (upAllfv_term_term p_term) - (upAllfv_term_term q_term) (upAllfvImpl_term_term H_term) s1 - match HP with - | conj _ HP => match HP with - | conj HP _ => HP - end - end) I) - | tPair s0 s1 s2 s3 => - fun HP => + (allfvImpl_term _ _ (upAllfvRenL_term_term p_term xi_term) s1 + (allfvRenL_term (upAllfv_term_term p_term) + (upRen_term_term xi_term) s1 + match H with + | conj _ H => match H with + | conj H _ => H + end + end)) I) + | tApp s0 s1 => + fun H => conj - (allfvImpl_term p_term q_term H_term s0 - match HP with - | conj HP _ => HP - end) - (conj - (allfvImpl_term (upAllfv_term_term p_term) - (upAllfv_term_term q_term) (upAllfvImpl_term_term H_term) s1 - match HP with - | conj _ HP => match HP with - | conj HP _ => HP - end - end) - (conj - (allfvImpl_term p_term q_term H_term s2 - match HP with - | conj _ HP => - match HP with - | conj _ HP => match HP with - | conj HP _ => HP - end - end - end) - (conj - (allfvImpl_term p_term q_term H_term s3 - match HP with - | conj _ HP => - match HP with - | conj _ HP => - match HP with - | conj _ HP => - match HP with - | conj HP _ => HP - end - end - end - end) I))) - | tFst s0 => - fun HP => - conj - (allfvImpl_term p_term q_term H_term s0 - match HP with - | conj HP _ => HP - end) I - | tSnd s0 => - fun HP => - conj - (allfvImpl_term p_term q_term H_term s0 - match HP with - | conj HP _ => HP - end) I - | tId s0 s1 s2 => - fun HP => - conj - (allfvImpl_term p_term q_term H_term s0 - match HP with - | conj HP _ => HP - end) - (conj - (allfvImpl_term p_term q_term H_term s1 - match HP with - | conj _ HP => match HP with - | conj HP _ => HP - end - end) - (conj - (allfvImpl_term p_term q_term H_term s2 - match HP with - | conj _ HP => - match HP with - | conj _ HP => match HP with - | conj HP _ => HP - end - end - end) I)) - | tRefl s0 s1 => - fun HP => - conj - (allfvImpl_term p_term q_term H_term s0 - match HP with - | conj HP _ => HP - end) - (conj - (allfvImpl_term p_term q_term H_term s1 - match HP with - | conj _ HP => match HP with - | conj HP _ => HP - end - end) I) - | tIdElim s0 s1 s2 s3 s4 s5 => - fun HP => - conj - (allfvImpl_term p_term q_term H_term s0 - match HP with - | conj HP _ => HP - end) - (conj - (allfvImpl_term p_term q_term H_term s1 - match HP with - | conj _ HP => match HP with - | conj HP _ => HP - end - end) - (conj - (allfvImpl_term (upAllfv_term_term (upAllfv_term_term p_term)) - (upAllfv_term_term (upAllfv_term_term q_term)) - (upAllfvImpl_term_term (upAllfvImpl_term_term H_term)) s2 - match HP with - | conj _ HP => - match HP with - | conj _ HP => match HP with - | conj HP _ => HP - end - end - end) - (conj - (allfvImpl_term p_term q_term H_term s3 - match HP with - | conj _ HP => - match HP with - | conj _ HP => - match HP with - | conj _ HP => - match HP with - | conj HP _ => HP - end - end - end - end) - (conj - (allfvImpl_term p_term q_term H_term s4 - match HP with - | conj _ HP => - match HP with - | conj _ HP => - match HP with - | conj _ HP => - match HP with - | conj _ HP => - match HP with - | conj HP _ => HP - end - end - end - end - end) - (conj - (allfvImpl_term p_term q_term H_term s5 - match HP with - | conj _ HP => - match HP with - | conj _ HP => - match HP with - | conj _ HP => - match HP with - | conj _ HP => - match HP with - | conj _ HP => - match HP with - | conj HP _ => HP - end - end - end - end - end - end) I))))) - end. - -Lemma upAllfvRenL_term_term (p : nat -> Prop) (xi : nat -> nat) : - forall x, - upAllfv_term_term p (upRen_term_term xi x) -> - upAllfv_term_term (funcomp p xi) x. -Proof. -exact (fun x => match x with - | S n' => fun i => i - | O => fun H => H - end). -Qed. - -Lemma upAllfvRenL_term_term2 (p : nat -> Prop) (xi : nat -> nat) : - forall x, - upAllfv_term_term (upAllfv_term_term p) (upRen_term_term (upRen_term_term xi) x) -> - upAllfv_term_term (upAllfv_term_term (funcomp p xi)) x. -Proof. - intros x. - refine (match x with S n' => fun H => upAllfvRenL_term_term p xi _ H | 0 => fun i => i end). -Qed. - - -Fixpoint allfvRenL_term (p_term : nat -> Prop) (xi_term : nat -> nat) -(s : term) {struct s} : -allfv_term p_term (ren_term xi_term s) -> -allfv_term (funcomp p_term xi_term) s := - match s as s return - allfv_term p_term (ren_term xi_term s) -> - allfv_term (funcomp p_term xi_term) s with - | tRel s0 => fun H => H - | tSort s0 => fun H => conj I I - | tProd s0 s1 => - fun H => - conj - (allfvRenL_term p_term xi_term s0 match H with - | conj H _ => H - end) - (conj - (allfvImpl_term _ _ (upAllfvRenL_term_term p_term xi_term) s1 - (allfvRenL_term (upAllfv_term_term p_term) - (upRen_term_term xi_term) s1 - match H with - | conj _ H => match H with - | conj H _ => H - end - end)) I) - | tLambda s0 s1 => - fun H => - conj - (allfvRenL_term p_term xi_term s0 match H with - | conj H _ => H - end) - (conj - (allfvImpl_term _ _ (upAllfvRenL_term_term p_term xi_term) s1 - (allfvRenL_term (upAllfv_term_term p_term) - (upRen_term_term xi_term) s1 - match H with - | conj _ H => match H with - | conj H _ => H - end - end)) I) - | tApp s0 s1 => - fun H => - conj - (allfvRenL_term p_term xi_term s0 match H with - | conj H _ => H - end) - (conj - (allfvRenL_term p_term xi_term s1 - match H with - | conj _ H => match H with - | conj H _ => H - end - end) I) - | tNat => fun H => I - | tZero => fun H => I - | tSucc s0 => - fun H => - conj - (allfvRenL_term p_term xi_term s0 match H with - | conj H _ => H - end) I - | tNatElim s0 s1 s2 s3 => - fun H => - conj - (allfvImpl_term _ _ (upAllfvRenL_term_term p_term xi_term) s0 - (allfvRenL_term (upAllfv_term_term p_term) - (upRen_term_term xi_term) s0 match H with - | conj H _ => H - end)) - (conj - (allfvRenL_term p_term xi_term s1 - match H with - | conj _ H => match H with - | conj H _ => H - end - end) - (conj - (allfvRenL_term p_term xi_term s2 - match H with - | conj _ H => - match H with - | conj _ H => match H with - | conj H _ => H - end - end - end) - (conj - (allfvRenL_term p_term xi_term s3 - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj _ H => match H with - | conj H _ => H - end - end - end - end) I))) - | tEmpty => fun H => I - | tEmptyElim s0 s1 => - fun H => - conj - (allfvImpl_term _ _ (upAllfvRenL_term_term p_term xi_term) s0 - (allfvRenL_term (upAllfv_term_term p_term) - (upRen_term_term xi_term) s0 match H with - | conj H _ => H - end)) + (allfvRenL_term p_term xi_term s0 match H with + | conj H _ => H + end) (conj (allfvRenL_term p_term xi_term s1 match H with @@ -1746,72 +914,10 @@ allfv_term (funcomp p_term xi_term) s := | conj H _ => H end end) I) - | tSig s0 s1 => - fun H => - conj - (allfvRenL_term p_term xi_term s0 match H with - | conj H _ => H - end) - (conj - (allfvImpl_term _ _ (upAllfvRenL_term_term p_term xi_term) s1 - (allfvRenL_term (upAllfv_term_term p_term) - (upRen_term_term xi_term) s1 - match H with - | conj _ H => match H with - | conj H _ => H - end - end)) I) - | tPair s0 s1 s2 s3 => - fun H => - conj - (allfvRenL_term p_term xi_term s0 match H with - | conj H _ => H - end) - (conj - (allfvImpl_term _ _ (upAllfvRenL_term_term p_term xi_term) s1 - (allfvRenL_term (upAllfv_term_term p_term) - (upRen_term_term xi_term) s1 - match H with - | conj _ H => match H with - | conj H _ => H - end - end)) - (conj - (allfvRenL_term p_term xi_term s2 - match H with - | conj _ H => - match H with - | conj _ H => match H with - | conj H _ => H - end - end - end) - (conj - (allfvRenL_term p_term xi_term s3 - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj _ H => match H with - | conj H _ => H - end - end - end - end) I))) - | tFst s0 => - fun H => - conj - (allfvRenL_term p_term xi_term s0 match H with - | conj H _ => H - end) I - | tSnd s0 => - fun H => - conj - (allfvRenL_term p_term xi_term s0 match H with - | conj H _ => H - end) I - | tId s0 s1 s2 => + | tBool => fun H => I + | tTrue => fun H => I + | tFalse => fun H => I + | tIfte s0 s1 s2 => fun H => conj (allfvRenL_term p_term xi_term s0 match H with @@ -1834,95 +940,6 @@ allfv_term (funcomp p_term xi_term) s := end end end) I)) - | tRefl s0 s1 => - fun H => - conj - (allfvRenL_term p_term xi_term s0 match H with - | conj H _ => H - end) - (conj - (allfvRenL_term p_term xi_term s1 - match H with - | conj _ H => match H with - | conj H _ => H - end - end) I) - | tIdElim s0 s1 s2 s3 s4 s5 => - fun H => - conj - (allfvRenL_term p_term xi_term s0 match H with - | conj H _ => H - end) - (conj - (allfvRenL_term p_term xi_term s1 - match H with - | conj _ H => match H with - | conj H _ => H - end - end) - (conj - (allfvImpl_term _ _ (upAllfvRenL_term_term2 p_term xi_term) s2 - (allfvRenL_term - (upAllfv_term_term (upAllfv_term_term p_term)) - (upRen_term_term (upRen_term_term xi_term)) s2 - match H with - | conj _ H => - match H with - | conj _ H => match H with - | conj H _ => H - end - end - end)) - (conj - (allfvRenL_term p_term xi_term s3 - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj _ H => match H with - | conj H _ => H - end - end - end - end) - (conj - (allfvRenL_term p_term xi_term s4 - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj H _ => H - end - end - end - end - end) - (conj - (allfvRenL_term p_term xi_term s5 - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj H _ => H - end - end - end - end - end - end) I))))) end. Lemma upAllfvRenR_term_term (p : nat -> Prop) (xi : nat -> nat) : @@ -1936,27 +953,11 @@ exact (fun x => match x with end). Qed. -Lemma upAllfvRenR_term_term2 (p : nat -> Prop) (xi : nat -> nat) : - forall x, - upAllfv_term_term (upAllfv_term_term (funcomp p xi)) x -> - upAllfv_term_term (upAllfv_term_term p) (upRen_term_term (upRen_term_term xi) x). -Proof. -exact (fun x => match x with - | S n' => fun H => upAllfvRenR_term_term p xi _ H - | O => fun i => i - end). -Qed. - - Fixpoint allfvRenR_term (p_term : nat -> Prop) (xi_term : nat -> nat) (s : term) {struct s} : allfv_term (funcomp p_term xi_term) s -> allfv_term p_term (ren_term xi_term s) := - match s - return -allfv_term (funcomp p_term xi_term) s -> -allfv_term p_term (ren_term xi_term s) - with + match s with | tRel s0 => fun H => H | tSort s0 => fun H => conj I I | tProd s0 s1 => @@ -2002,136 +1003,10 @@ allfv_term p_term (ren_term xi_term s) | conj H _ => H end end) I) - | tNat => fun H => I - | tZero => fun H => I - | tSucc s0 => - fun H => - conj - (allfvRenR_term p_term xi_term s0 match H with - | conj H _ => H - end) I - | tNatElim s0 s1 s2 s3 => - fun H => - conj - (allfvRenR_term (upAllfv_term_term p_term) (upRen_term_term xi_term) - s0 - (allfvImpl_term _ _ (upAllfvRenR_term_term p_term xi_term) s0 - match H with - | conj H _ => H - end)) - (conj - (allfvRenR_term p_term xi_term s1 - match H with - | conj _ H => match H with - | conj H _ => H - end - end) - (conj - (allfvRenR_term p_term xi_term s2 - match H with - | conj _ H => - match H with - | conj _ H => match H with - | conj H _ => H - end - end - end) - (conj - (allfvRenR_term p_term xi_term s3 - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj _ H => match H with - | conj H _ => H - end - end - end - end) I))) - | tEmpty => fun H => I - | tEmptyElim s0 s1 => - fun H => - conj - (allfvRenR_term (upAllfv_term_term p_term) (upRen_term_term xi_term) - s0 - (allfvImpl_term _ _ (upAllfvRenR_term_term p_term xi_term) s0 - match H with - | conj H _ => H - end)) - (conj - (allfvRenR_term p_term xi_term s1 - match H with - | conj _ H => match H with - | conj H _ => H - end - end) I) - | tSig s0 s1 => - fun H => - conj - (allfvRenR_term p_term xi_term s0 match H with - | conj H _ => H - end) - (conj - (allfvRenR_term (upAllfv_term_term p_term) - (upRen_term_term xi_term) s1 - (allfvImpl_term _ _ (upAllfvRenR_term_term p_term xi_term) s1 - match H with - | conj _ H => match H with - | conj H _ => H - end - end)) I) - | tPair s0 s1 s2 s3 => - fun H => - conj - (allfvRenR_term p_term xi_term s0 match H with - | conj H _ => H - end) - (conj - (allfvRenR_term (upAllfv_term_term p_term) - (upRen_term_term xi_term) s1 - (allfvImpl_term _ _ (upAllfvRenR_term_term p_term xi_term) s1 - match H with - | conj _ H => match H with - | conj H _ => H - end - end)) - (conj - (allfvRenR_term p_term xi_term s2 - match H with - | conj _ H => - match H with - | conj _ H => match H with - | conj H _ => H - end - end - end) - (conj - (allfvRenR_term p_term xi_term s3 - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj _ H => match H with - | conj H _ => H - end - end - end - end) I))) - | tFst s0 => - fun H => - conj - (allfvRenR_term p_term xi_term s0 match H with - | conj H _ => H - end) I - | tSnd s0 => - fun H => - conj - (allfvRenR_term p_term xi_term s0 match H with - | conj H _ => H - end) I - | tId s0 s1 s2 => + | tBool => fun H => I + | tTrue => fun H => I + | tFalse => fun H => I + | tIfte s0 s1 s2 => fun H => conj (allfvRenR_term p_term xi_term s0 match H with @@ -2154,95 +1029,6 @@ allfv_term p_term (ren_term xi_term s) end end end) I)) - | tRefl s0 s1 => - fun H => - conj - (allfvRenR_term p_term xi_term s0 match H with - | conj H _ => H - end) - (conj - (allfvRenR_term p_term xi_term s1 - match H with - | conj _ H => match H with - | conj H _ => H - end - end) I) - | tIdElim s0 s1 s2 s3 s4 s5 => - fun H => - conj - (allfvRenR_term p_term xi_term s0 match H with - | conj H _ => H - end) - (conj - (allfvRenR_term p_term xi_term s1 - match H with - | conj _ H => match H with - | conj H _ => H - end - end) - (conj - (allfvRenR_term (upAllfv_term_term (upAllfv_term_term p_term)) - (upRen_term_term (upRen_term_term xi_term)) s2 - (allfvImpl_term _ _ (upAllfvRenR_term_term2 p_term xi_term) - s2 - match H with - | conj _ H => - match H with - | conj _ H => match H with - | conj H _ => H - end - end - end)) - (conj - (allfvRenR_term p_term xi_term s3 - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj _ H => match H with - | conj H _ => H - end - end - end - end) - (conj - (allfvRenR_term p_term xi_term s4 - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj H _ => H - end - end - end - end - end) - (conj - (allfvRenR_term p_term xi_term s5 - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj _ H => - match H with - | conj H _ => H - end - end - end - end - end - end) I))))) end. End Allfv. diff --git a/theories/AutoSubst/unscoped.v b/theories/AutoSubst/unscoped.v index 3b590532..602f8d66 100644 --- a/theories/AutoSubst/unscoped.v +++ b/theories/AutoSubst/unscoped.v @@ -177,6 +177,8 @@ Module UnscopedNotations. Notation "↑" := (shift) : subst_scope. + #[ global ] + Open Scope fscope. #[ global ] Open Scope subst_scope. End UnscopedNotations.