From 9c17ec5cac4f702a69146c86cc244669a82b739e Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Tue, 1 Apr 2025 23:21:39 -0400 Subject: [PATCH] Start refactoring to unscoped syntax --- Makefile | 8 +- theories/Autosubst2/fintype.v | 419 ---------- theories/Autosubst2/syntax.v | 1362 ++++++++++++-------------------- theories/Autosubst2/unscoped.v | 213 +++++ theories/fp_red.v | 84 +- theories/typing.v | 251 ++++++ 6 files changed, 994 insertions(+), 1343 deletions(-) delete mode 100644 theories/Autosubst2/fintype.v create mode 100644 theories/Autosubst2/unscoped.v create mode 100644 theories/typing.v diff --git a/Makefile b/Makefile index ef5b76f..c56e771 100644 --- a/Makefile +++ b/Makefile @@ -6,7 +6,7 @@ theories: $(COQMAKEFILE) FORCE validate: $(COQMAKEFILE) FORCE $(MAKE) -f $(COQMAKEFILE) validate -$(COQMAKEFILE) : theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v +$(COQMAKEFILE) : theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/unscoped.v $(COQBIN)coq_makefile -f _CoqProject -o $(COQMAKEFILE) install: $(COQMAKEFILE) @@ -15,13 +15,13 @@ install: $(COQMAKEFILE) uninstall: $(COQMAKEFILE) $(MAKE) -f $(COQMAKEFILE) uninstall -theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v : syntax.sig - autosubst -f -v ge813 -s coq -o theories/Autosubst2/syntax.v syntax.sig +theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/unscoped.v : syntax.sig + autosubst -f -v ge813 -s ucoq -o theories/Autosubst2/syntax.v syntax.sig .PHONY: clean FORCE clean: test ! -f $(COQMAKEFILE) || ( $(MAKE) -f $(COQMAKEFILE) clean && rm $(COQMAKEFILE) ) - rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v + rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v theories/Autosubst2/unscoped.v FORCE: diff --git a/theories/Autosubst2/fintype.v b/theories/Autosubst2/fintype.v deleted file mode 100644 index 99508b6..0000000 --- a/theories/Autosubst2/fintype.v +++ /dev/null @@ -1,419 +0,0 @@ -(** * Autosubst Header for Scoped Syntax - Our development utilises well-scoped de Bruijn syntax. This means that the de Bruijn indices are taken from finite types. As a consequence, any kind of substitution or environment used in conjunction with well-scoped syntax takes the form of a mapping from some finite type _I^n_. In particular, _renamings_ are mappings _I^n -> I^m_. Here we develop the theory of how these parts interact. - -Version: December 11, 2019. -*) -Require Import core. -Require Import Setoid Morphisms Relation_Definitions. - -Set Implicit Arguments. -Unset Strict Implicit. - -Definition ap {X Y} (f : X -> Y) {x y : X} (p : x = y) : f x = f y := - match p with eq_refl => eq_refl end. - -Definition apc {X Y} {f g : X -> Y} {x y : X} (p : f = g) (q : x = y) : f x = g y := - match q with eq_refl => match p with eq_refl => eq_refl end end. - -(** ** Primitives of the Sigma Calculus - We implement the finite type with _n_ elements, _I^n_, as the _n_-fold iteration of the Option Type. _I^0_ is implemented as the empty type. -*) - -Fixpoint fin (n : nat) : Type := - match n with - | 0 => False - | S m => option (fin m) - end. - -(** Renamings and Injective Renamings - _Renamings_ are mappings between finite types. -*) -Definition ren (m n : nat) : Type := fin m -> fin n. - -Definition id {X} := @Datatypes.id X. - -Definition idren {k: nat} : ren k k := @Datatypes.id (fin k). - -(** We give a special name, to the newest element in a non-empty finite type, as it usually corresponds to a freshly bound variable. *) -Definition var_zero {n : nat} : fin (S n) := None. - -Definition null {T} (i : fin 0) : T := match i with end. - -Definition shift {n : nat} : ren n (S n) := - Some. - -(** Extension of Finite Mappings - Assume we are given a mapping _f_ from _I^n_ to some type _X_, then we can _extend_ this mapping with a new value from _x : X_ to a mapping from _I^n+1_ to _X_. We denote this operation by _x . f_ and define it as follows: -*) -Definition scons {X : Type} {n : nat} (x : X) (f : fin n -> X) (m : fin (S n)) : X := - match m with - | None => x - | Some i => f i - end. - -#[ export ] -Hint Opaque scons : rewrite. - -(** ** Type Class Instances for Notation *) - -(** *** Type classes for renamings. *) - -Class Ren1 (X1 : Type) (Y Z : Type) := - ren1 : X1 -> Y -> Z. - -Class Ren2 (X1 X2 : Type) (Y Z : Type) := - ren2 : X1 -> X2 -> Y -> Z. - -Class Ren3 (X1 X2 X3 : Type) (Y Z : Type) := - ren3 : X1 -> X2 -> X3 -> Y -> Z. - -Class Ren4 (X1 X2 X3 X4 : Type) (Y Z : Type) := - ren4 : X1 -> X2 -> X3 -> X4 -> Y -> Z. - -Class Ren5 (X1 X2 X3 X4 X5 : Type) (Y Z : Type) := - ren5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z. - -Module RenNotations. - Notation "s ⟨ xi1 ⟩" := (ren1 xi1 s) (at level 7, left associativity, format "s ⟨ xi1 ⟩") : subst_scope. - - Notation "s ⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ⟩") : subst_scope. - - Notation "s ⟨ xi1 ; xi2 ; xi3 ⟩" := (ren3 xi1 xi2 xi3 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ⟩") : subst_scope. - - Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩" := (ren4 xi1 xi2 xi3 xi4 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩") : subst_scope. - - Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩" := (ren5 xi1 xi2 xi3 xi4 xi5 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩") : subst_scope. - - Notation "⟨ xi ⟩" := (ren1 xi) (at level 1, left associativity, format "⟨ xi ⟩") : fscope. - - Notation "⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2) (at level 1, left associativity, format "⟨ xi1 ; xi2 ⟩") : fscope. -End RenNotations. - -(** *** Type Classes for Substiution *) - -Class Subst1 (X1 : Type) (Y Z: Type) := - subst1 : X1 -> Y -> Z. - -Class Subst2 (X1 X2 : Type) (Y Z: Type) := - subst2 : X1 -> X2 -> Y -> Z. - -Class Subst3 (X1 X2 X3 : Type) (Y Z: Type) := - subst3 : X1 -> X2 -> X3 -> Y -> Z. - -Class Subst4 (X1 X2 X3 X4: Type) (Y Z: Type) := - subst4 : X1 -> X2 -> X3 -> X4 -> Y -> Z. - -Class Subst5 (X1 X2 X3 X4 X5 : Type) (Y Z: Type) := - subst5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z. - -Module SubstNotations. - Notation "s [ sigma ]" := (subst1 sigma s) (at level 7, left associativity, format "s '/' [ sigma ]") : subst_scope. - - Notation "s [ sigma ; tau ]" := (subst2 sigma tau s) (at level 7, left associativity, format "s '/' [ sigma ; '/' tau ]") : subst_scope. -End SubstNotations. - -(** ** Type Class for Variables *) -Class Var X Y := - ids : X -> Y. - - -(** ** Proofs for substitution primitives *) - -(** Forward Function Composition - Substitutions represented as functions are ubiquitious in this development and we often have to compose them, without talking about their pointwise behaviour. - That is, we are interested in the forward compostion of functions, _f o g_, for which we introduce a convenient notation, "f >> g". The direction of the arrow serves as a reminder of the _forward_ nature of this composition, that is first apply _f_, then _g_. *) - -Arguments funcomp {X Y Z} (g)%fscope (f)%fscope. - -Module CombineNotations. - Notation "f >> g" := (funcomp g f) (at level 50) : fscope. - - Notation "s .: sigma" := (scons s sigma) (at level 55, sigma at next level, right associativity) : subst_scope. - - #[ global ] - Open Scope fscope. - #[ global ] - Open Scope subst_scope. -End CombineNotations. - -Import CombineNotations. - - -(** Generic lifting operation for renamings *) -Definition up_ren {m n} (xi : ren m n) : ren (S m) (S n) := - var_zero .: xi >> shift. - -(** Generic proof that lifting of renamings composes. *) -Lemma up_ren_ren k l m (xi: ren k l) (zeta : ren l m) (rho: ren k m) (E: forall x, (xi >> zeta) x = rho x) : - forall x, (up_ren xi >> up_ren zeta) x = up_ren rho x. -Proof. - intros [x|]. - - cbn. unfold funcomp. now rewrite <- E. - - reflexivity. -Qed. - -Arguments up_ren_ren {k l m} xi zeta rho E. - -Lemma fin_eta {X} (f g : fin 0 -> X) : - pointwise_relation _ eq f g. -Proof. intros []. Qed. - -(** Eta laws *) -Lemma scons_eta' {T} {n : nat} (f : fin (S n) -> T) : - pointwise_relation _ eq (f var_zero .: (funcomp f shift)) f. -Proof. intros x. destruct x; reflexivity. Qed. - -Lemma scons_eta_id' {n : nat} : - pointwise_relation (fin (S n)) eq (var_zero .: shift) id. -Proof. intros x. destruct x; reflexivity. Qed. - -Lemma scons_comp' {T:Type} {U} {m} (s: T) (sigma: fin m -> T) (tau: T -> U) : - pointwise_relation _ eq (funcomp tau (s .: sigma)) ((tau s) .: (funcomp tau sigma)). -Proof. intros x. destruct x; reflexivity. Qed. - -(* Lemma scons_tail'_pointwise {X} {n} (s : X) (f : fin n -> X) : *) -(* pointwise_relation _ eq (funcomp (scons s f) shift) f. *) -(* Proof. *) -(* reflexivity. *) -(* Qed. *) - -(* Lemma scons_tail' {X} {n} (s : X) (f : fin n -> X) x : *) -(* (scons s f (shift x)) = f x. *) -(* Proof. *) -(* reflexivity. *) -(* Qed. *) - -(* Morphism for Setoid Rewriting. The only morphism that can be defined statically. *) -#[export] Instance scons_morphism {X: Type} {n:nat} : - Proper (eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons X n). -Proof. - intros t t' -> sigma tau H. - intros [x|]. - cbn. apply H. - reflexivity. -Qed. - -#[export] Instance scons_morphism2 {X: Type} {n: nat} : - Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons X n). -Proof. - intros ? t -> sigma tau H ? x ->. - destruct x as [x|]. - cbn. apply H. - reflexivity. -Qed. - -(** ** Variadic Substitution Primitives *) - -Fixpoint shift_p (p : nat) {n} : ren n (p + n) := - fun n => match p with - | 0 => n - | S p => Some (shift_p p n) - end. - -Fixpoint scons_p {X: Type} {m : nat} : forall {n} (f : fin m -> X) (g : fin n -> X), fin (m + n) -> X. -Proof. - destruct m. - - intros n f g. exact g. - - intros n f g. cbn. apply scons. - + exact (f var_zero). - + apply scons_p. - * intros z. exact (f (Some z)). - * exact g. -Defined. - -#[export] Hint Opaque scons_p : rewrite. - -#[export] Instance scons_p_morphism {X: Type} {m n:nat} : - Proper (pointwise_relation _ eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons_p X m n). -Proof. - intros sigma sigma' Hsigma tau tau' Htau. - intros x. - induction m. - - cbn. apply Htau. - - cbn. change (fin (S m + n)) with (fin (S (m + n))) in x. - destruct x as [x|]. - + cbn. apply IHm. - intros ?. apply Hsigma. - + cbn. apply Hsigma. -Qed. - -#[export] Instance scons_p_morphism2 {X: Type} {m n:nat} : - Proper (pointwise_relation _ eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons_p X m n). -Proof. - intros sigma sigma' Hsigma tau tau' Htau ? x ->. - induction m. - - cbn. apply Htau. - - cbn. change (fin (S m + n)) with (fin (S (m + n))) in x. - destruct x as [x|]. - + cbn. apply IHm. - intros ?. apply Hsigma. - + cbn. apply Hsigma. -Qed. - -Definition zero_p {m : nat} {n} : fin m -> fin (m + n). -Proof. - induction m. - - intros []. - - intros [x|]. - + exact (shift_p 1 (IHm x)). - + exact var_zero. -Defined. - -Lemma scons_p_head' {X} {m n} (f : fin m -> X) (g : fin n -> X) z: - (scons_p f g) (zero_p z) = f z. -Proof. - induction m. - - inversion z. - - destruct z. - + simpl. simpl. now rewrite IHm. - + reflexivity. -Qed. - -Lemma scons_p_head_pointwise {X} {m n} (f : fin m -> X) (g : fin n -> X) : - pointwise_relation _ eq (funcomp (scons_p f g) zero_p) f. -Proof. - intros z. - unfold funcomp. - induction m. - - inversion z. - - destruct z. - + simpl. now rewrite IHm. - + reflexivity. -Qed. - -Lemma scons_p_tail' X m n (f : fin m -> X) (g : fin n -> X) z : - scons_p f g (shift_p m z) = g z. -Proof. induction m; cbn; eauto. Qed. - -Lemma scons_p_tail_pointwise X m n (f : fin m -> X) (g : fin n -> X) : - pointwise_relation _ eq (funcomp (scons_p f g) (shift_p m)) g. -Proof. intros z. induction m; cbn; eauto. Qed. - -Lemma destruct_fin {m n} (x : fin (m + n)): - (exists x', x = zero_p x') \/ exists x', x = shift_p m x'. -Proof. - induction m; simpl in *. - - right. eauto. - - destruct x as [x|]. - + destruct (IHm x) as [[x' ->] |[x' ->]]. - * left. now exists (Some x'). - * right. eauto. - + left. exists None. eauto. -Qed. - -Lemma scons_p_comp' X Y m n (f : fin m -> X) (g : fin n -> X) (h : X -> Y) : - pointwise_relation _ eq (funcomp h (scons_p f g)) (scons_p (f >> h) (g >> h)). -Proof. - intros x. - destruct (destruct_fin x) as [[x' ->]|[x' ->]]. - (* TODO better way to solve this? *) - - revert x'. - apply pointwise_forall. - change (fun x => (scons_p f g >> h) (zero_p x)) with (zero_p >> scons_p f g >> h). - now setoid_rewrite scons_p_head_pointwise. - - revert x'. - apply pointwise_forall. - change (fun x => (scons_p f g >> h) (shift_p m x)) with (shift_p m >> scons_p f g >> h). - change (fun x => scons_p (f >> h) (g >> h) (shift_p m x)) with (shift_p m >> scons_p (f >> h) (g >> h)). - now rewrite !scons_p_tail_pointwise. -Qed. - - -Lemma scons_p_congr {X} {m n} (f f' : fin m -> X) (g g': fin n -> X) z: - (forall x, f x = f' x) -> (forall x, g x = g' x) -> scons_p f g z = scons_p f' g' z. -Proof. intros H1 H2. induction m; eauto. cbn. destruct z; eauto. Qed. - -(** Generic n-ary lifting operation. *) -Definition upRen_p p { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) : fin (p + m) -> fin (p + n) := - scons_p (zero_p ) (xi >> shift_p _). - -Arguments upRen_p p {m n} xi. - -(** Generic proof for composition of n-ary lifting. *) -Lemma up_ren_ren_p p k l m (xi: ren k l) (zeta : ren l m) (rho: ren k m) (E: forall x, (xi >> zeta) x = rho x) : - forall x, (upRen_p p xi >> upRen_p p zeta) x = upRen_p p rho x. -Proof. - intros x. destruct (destruct_fin x) as [[? ->]|[? ->]]. - - unfold upRen_p. unfold funcomp. now repeat rewrite scons_p_head'. - - unfold upRen_p. unfold funcomp. repeat rewrite scons_p_tail'. - now rewrite <- E. -Qed. - - -Arguments zero_p m {n}. -Arguments scons_p {X} m {n} f g. - -Lemma scons_p_eta {X} {m n} {f : fin m -> X} - {g : fin n -> X} (h: fin (m + n) -> X) {z: fin (m + n)}: - (forall x, g x = h (shift_p m x)) -> (forall x, f x = h (zero_p m x)) -> scons_p m f g z = h z. -Proof. - intros H1 H2. destruct (destruct_fin z) as [[? ->] |[? ->]]. - - rewrite scons_p_head'. eauto. - - rewrite scons_p_tail'. eauto. -Qed. - -Arguments scons_p_eta {X} {m n} {f g} h {z}. -Arguments scons_p_congr {X} {m n} {f f'} {g g'} {z}. - -(** ** Notations for Scoped Syntax *) - -Module ScopedNotations. - Include RenNotations. - Include SubstNotations. - Include CombineNotations. - -(* Notation "s , sigma" := (scons s sigma) (at level 60, format "s , sigma", right associativity) : subst_scope. *) - - Notation "s '..'" := (scons s ids) (at level 1, format "s ..") : subst_scope. - - Notation "↑" := (shift) : subst_scope. - - #[global] - Open Scope fscope. - #[global] - Open Scope subst_scope. -End ScopedNotations. - - -(** ** Tactics for Scoped Syntax *) - -Tactic Notation "auto_case" tactic(t) := (match goal with - | [|- forall (i : fin 0), _] => intros []; t - | [|- forall (i : fin (S (S (S (S _))))), _] => intros [[[[|]|]|]|]; t - | [|- forall (i : fin (S (S (S _)))), _] => intros [[[|]|]|]; t - | [|- forall (i : fin (S (S _))), _] => intros [[?|]|]; t - | [|- forall (i : fin (S _)), _] => intros [?|]; t - end). - -#[export] Hint Rewrite @scons_p_head' @scons_p_tail' : FunctorInstances. - -(** Generic fsimpl tactic: simplifies the above primitives in a goal. *) -Ltac fsimpl := - repeat match goal with - | [|- context[id >> ?f]] => change (id >> f) with f (* AsimplCompIdL *) - | [|- context[?f >> id]] => change (f >> id) with f (* AsimplCompIdR *) - | [|- context [id ?s]] => change (id s) with s - | [|- context[(?f >> ?g) >> ?h]] => change ((f >> g) >> h) with (f >> (g >> h)) (* AsimplComp *) - (* | [|- zero_p >> scons_p ?f ?g] => rewrite scons_p_head *) - | [|- context[(?s .: ?sigma) var_zero]] => change ((s.:sigma) var_zero) with s - | [|- context[(?s .: ?sigma) (shift ?m)]] => change ((s.:sigma) (shift m)) with (sigma m) - (* first [progress setoid_rewrite scons_tail' | progress setoid_rewrite scons_tail'_pointwise ] *) - | [|- context[idren >> ?f]] => change (idren >> f) with f - | [|- context[?f >> idren]] => change (f >> idren) with f - | [|- context[?f >> (?x .: ?g)]] => change (f >> (x .: g)) with g (* f should evaluate to shift *) - | [|- context[?x2 .: (funcomp ?f shift)]] => change (scons x2 (funcomp f shift)) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite (@scons_eta' _ _ f); eta_reduce - | [|- context[?f var_zero .: ?g]] => change (scons (f var_zero) g) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite scons_eta'; eta_reduce - | [|- _ = ?h (?f ?s)] => change (h (f s)) with ((f >> h) s) - | [|- ?h (?f ?s) = _] => change (h (f s)) with ((f >> h) s) - | [|- context[funcomp _ (scons _ _)]] => setoid_rewrite scons_comp'; eta_reduce - | [|- context[funcomp _ (scons_p _ _ _)]] => setoid_rewrite scons_p_comp'; eta_reduce - | [|- context[scons (@var_zero _) shift]] => setoid_rewrite scons_eta_id'; eta_reduce - (* | _ => progress autorewrite with FunctorInstances *) - | [|- context[funcomp (scons_p _ _ _) (zero_p _)]] => - first [progress setoid_rewrite scons_p_head_pointwise | progress setoid_rewrite scons_p_head' ] - | [|- context[scons_p _ _ _ (zero_p _ _)]] => setoid_rewrite scons_p_head' - | [|- context[funcomp (scons_p _ _ _) (shift_p _)]] => - first [progress setoid_rewrite scons_p_tail_pointwise | progress setoid_rewrite scons_p_tail' ] - | [|- context[scons_p _ _ _ (shift_p _ _)]] => setoid_rewrite scons_p_tail' - | _ => first [progress minimize | progress cbn [shift scons scons_p] ] - end. diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v index 75ef645..659d8b0 100644 --- a/theories/Autosubst2/syntax.v +++ b/theories/Autosubst2/syntax.v @@ -1,4 +1,4 @@ -Require Import core fintype. +Require Import core unscoped. Require Import Setoid Morphisms Relation_Definitions. @@ -33,345 +33,257 @@ Proof. exact (eq_refl). Qed. -Inductive PTm (n_PTm : nat) : Type := - | VarPTm : fin n_PTm -> PTm n_PTm - | PAbs : PTm (S n_PTm) -> PTm n_PTm - | PApp : PTm n_PTm -> PTm n_PTm -> PTm n_PTm - | PPair : PTm n_PTm -> PTm n_PTm -> PTm n_PTm - | PProj : PTag -> PTm n_PTm -> PTm n_PTm - | PConst : TTag -> PTm n_PTm - | PUniv : nat -> PTm n_PTm - | PBot : PTm n_PTm. +Inductive PTm : Type := + | VarPTm : nat -> PTm + | PAbs : PTm -> PTm + | PApp : PTm -> PTm -> PTm + | PPair : PTm -> PTm -> PTm + | PProj : PTag -> PTm -> PTm + | PConst : TTag -> PTm + | PUniv : nat -> PTm + | PBot : PTm. -Lemma congr_PAbs {m_PTm : nat} {s0 : PTm (S m_PTm)} {t0 : PTm (S m_PTm)} - (H0 : s0 = t0) : PAbs m_PTm s0 = PAbs m_PTm t0. +Lemma congr_PAbs {s0 : PTm} {t0 : PTm} (H0 : s0 = t0) : PAbs s0 = PAbs t0. Proof. -exact (eq_trans eq_refl (ap (fun x => PAbs m_PTm x) H0)). +exact (eq_trans eq_refl (ap (fun x => PAbs x) H0)). Qed. -Lemma congr_PApp {m_PTm : nat} {s0 : PTm m_PTm} {s1 : PTm m_PTm} - {t0 : PTm m_PTm} {t1 : PTm m_PTm} (H0 : s0 = t0) (H1 : s1 = t1) : - PApp m_PTm s0 s1 = PApp m_PTm t0 t1. +Lemma congr_PApp {s0 : PTm} {s1 : PTm} {t0 : PTm} {t1 : PTm} (H0 : s0 = t0) + (H1 : s1 = t1) : PApp s0 s1 = PApp t0 t1. Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => PApp m_PTm x s1) H0)) - (ap (fun x => PApp m_PTm t0 x) H1)). +exact (eq_trans (eq_trans eq_refl (ap (fun x => PApp x s1) H0)) + (ap (fun x => PApp t0 x) H1)). Qed. -Lemma congr_PPair {m_PTm : nat} {s0 : PTm m_PTm} {s1 : PTm m_PTm} - {t0 : PTm m_PTm} {t1 : PTm m_PTm} (H0 : s0 = t0) (H1 : s1 = t1) : - PPair m_PTm s0 s1 = PPair m_PTm t0 t1. +Lemma congr_PPair {s0 : PTm} {s1 : PTm} {t0 : PTm} {t1 : PTm} (H0 : s0 = t0) + (H1 : s1 = t1) : PPair s0 s1 = PPair t0 t1. Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => PPair m_PTm x s1) H0)) - (ap (fun x => PPair m_PTm t0 x) H1)). +exact (eq_trans (eq_trans eq_refl (ap (fun x => PPair x s1) H0)) + (ap (fun x => PPair t0 x) H1)). Qed. -Lemma congr_PProj {m_PTm : nat} {s0 : PTag} {s1 : PTm m_PTm} {t0 : PTag} - {t1 : PTm m_PTm} (H0 : s0 = t0) (H1 : s1 = t1) : - PProj m_PTm s0 s1 = PProj m_PTm t0 t1. +Lemma congr_PProj {s0 : PTag} {s1 : PTm} {t0 : PTag} {t1 : PTm} + (H0 : s0 = t0) (H1 : s1 = t1) : PProj s0 s1 = PProj t0 t1. Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => PProj m_PTm x s1) H0)) - (ap (fun x => PProj m_PTm t0 x) H1)). +exact (eq_trans (eq_trans eq_refl (ap (fun x => PProj x s1) H0)) + (ap (fun x => PProj t0 x) H1)). Qed. -Lemma congr_PConst {m_PTm : nat} {s0 : TTag} {t0 : TTag} (H0 : s0 = t0) : - PConst m_PTm s0 = PConst m_PTm t0. +Lemma congr_PConst {s0 : TTag} {t0 : TTag} (H0 : s0 = t0) : + PConst s0 = PConst t0. Proof. -exact (eq_trans eq_refl (ap (fun x => PConst m_PTm x) H0)). +exact (eq_trans eq_refl (ap (fun x => PConst x) H0)). Qed. -Lemma congr_PUniv {m_PTm : nat} {s0 : nat} {t0 : nat} (H0 : s0 = t0) : - PUniv m_PTm s0 = PUniv m_PTm t0. +Lemma congr_PUniv {s0 : nat} {t0 : nat} (H0 : s0 = t0) : PUniv s0 = PUniv t0. Proof. -exact (eq_trans eq_refl (ap (fun x => PUniv m_PTm x) H0)). +exact (eq_trans eq_refl (ap (fun x => PUniv x) H0)). Qed. -Lemma congr_PBot {m_PTm : nat} : PBot m_PTm = PBot m_PTm. +Lemma congr_PBot : PBot = PBot. Proof. exact (eq_refl). Qed. -Lemma upRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n) : - fin (S m) -> fin (S n). +Lemma upRen_PTm_PTm (xi : nat -> nat) : nat -> nat. Proof. exact (up_ren xi). Defined. -Lemma upRen_list_PTm_PTm (p : nat) {m : nat} {n : nat} (xi : fin m -> fin n) - : fin (plus p m) -> fin (plus p n). -Proof. -exact (upRen_p p xi). -Defined. - -Fixpoint ren_PTm {m_PTm : nat} {n_PTm : nat} -(xi_PTm : fin m_PTm -> fin n_PTm) (s : PTm m_PTm) {struct s} : PTm n_PTm := +Fixpoint ren_PTm (xi_PTm : nat -> nat) (s : PTm) {struct s} : PTm := match s with - | VarPTm _ s0 => VarPTm n_PTm (xi_PTm s0) - | PAbs _ s0 => PAbs n_PTm (ren_PTm (upRen_PTm_PTm xi_PTm) s0) - | PApp _ s0 s1 => PApp n_PTm (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) - | PPair _ s0 s1 => PPair n_PTm (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) - | PProj _ s0 s1 => PProj n_PTm s0 (ren_PTm xi_PTm s1) - | PConst _ s0 => PConst n_PTm s0 - | PUniv _ s0 => PUniv n_PTm s0 - | PBot _ => PBot n_PTm + | VarPTm s0 => VarPTm (xi_PTm s0) + | PAbs s0 => PAbs (ren_PTm (upRen_PTm_PTm xi_PTm) s0) + | PApp s0 s1 => PApp (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) + | PPair s0 s1 => PPair (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) + | PProj s0 s1 => PProj s0 (ren_PTm xi_PTm s1) + | PConst s0 => PConst s0 + | PUniv s0 => PUniv s0 + | PBot => PBot end. -Lemma up_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) : - fin (S m) -> PTm (S n_PTm). +Lemma up_PTm_PTm (sigma : nat -> PTm) : nat -> PTm. Proof. -exact (scons (VarPTm (S n_PTm) var_zero) (funcomp (ren_PTm shift) sigma)). +exact (scons (VarPTm var_zero) (funcomp (ren_PTm shift) sigma)). Defined. -Lemma up_list_PTm_PTm (p : nat) {m : nat} {n_PTm : nat} - (sigma : fin m -> PTm n_PTm) : fin (plus p m) -> PTm (plus p n_PTm). -Proof. -exact (scons_p p (funcomp (VarPTm (plus p n_PTm)) (zero_p p)) - (funcomp (ren_PTm (shift_p p)) sigma)). -Defined. - -Fixpoint subst_PTm {m_PTm : nat} {n_PTm : nat} -(sigma_PTm : fin m_PTm -> PTm n_PTm) (s : PTm m_PTm) {struct s} : PTm n_PTm -:= +Fixpoint subst_PTm (sigma_PTm : nat -> PTm) (s : PTm) {struct s} : PTm := match s with - | VarPTm _ s0 => sigma_PTm s0 - | PAbs _ s0 => PAbs n_PTm (subst_PTm (up_PTm_PTm sigma_PTm) s0) - | PApp _ s0 s1 => - PApp n_PTm (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1) - | PPair _ s0 s1 => - PPair n_PTm (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1) - | PProj _ s0 s1 => PProj n_PTm s0 (subst_PTm sigma_PTm s1) - | PConst _ s0 => PConst n_PTm s0 - | PUniv _ s0 => PUniv n_PTm s0 - | PBot _ => PBot n_PTm + | VarPTm s0 => sigma_PTm s0 + | PAbs s0 => PAbs (subst_PTm (up_PTm_PTm sigma_PTm) s0) + | PApp s0 s1 => PApp (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1) + | PPair s0 s1 => PPair (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1) + | PProj s0 s1 => PProj s0 (subst_PTm sigma_PTm s1) + | PConst s0 => PConst s0 + | PUniv s0 => PUniv s0 + | PBot => PBot end. -Lemma upId_PTm_PTm {m_PTm : nat} (sigma : fin m_PTm -> PTm m_PTm) - (Eq : forall x, sigma x = VarPTm m_PTm x) : - forall x, up_PTm_PTm sigma x = VarPTm (S m_PTm) x. +Lemma upId_PTm_PTm (sigma : nat -> PTm) (Eq : forall x, sigma x = VarPTm x) : + forall x, up_PTm_PTm sigma x = VarPTm x. Proof. exact (fun n => match n with - | Some fin_n => ap (ren_PTm shift) (Eq fin_n) - | None => eq_refl + | S n' => ap (ren_PTm shift) (Eq n') + | O => eq_refl end). Qed. -Lemma upId_list_PTm_PTm {p : nat} {m_PTm : nat} - (sigma : fin m_PTm -> PTm m_PTm) (Eq : forall x, sigma x = VarPTm m_PTm x) - : forall x, up_list_PTm_PTm p sigma x = VarPTm (plus p m_PTm) x. -Proof. -exact (fun n => - scons_p_eta (VarPTm (plus p m_PTm)) - (fun n => ap (ren_PTm (shift_p p)) (Eq n)) (fun n => eq_refl)). -Qed. - -Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm) -(Eq_PTm : forall x, sigma_PTm x = VarPTm m_PTm x) (s : PTm m_PTm) {struct s} - : subst_PTm sigma_PTm s = s := +Fixpoint idSubst_PTm (sigma_PTm : nat -> PTm) +(Eq_PTm : forall x, sigma_PTm x = VarPTm x) (s : PTm) {struct s} : +subst_PTm sigma_PTm s = s := match s with - | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 => + | VarPTm s0 => Eq_PTm s0 + | PAbs s0 => congr_PAbs (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s0) - | PApp _ s0 s1 => + | PApp s0 s1 => congr_PApp (idSubst_PTm sigma_PTm Eq_PTm s0) (idSubst_PTm sigma_PTm Eq_PTm s1) - | PPair _ s0 s1 => + | PPair s0 s1 => congr_PPair (idSubst_PTm sigma_PTm Eq_PTm s0) (idSubst_PTm sigma_PTm Eq_PTm s1) - | PProj _ s0 s1 => - congr_PProj (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1) - | PConst _ s0 => congr_PConst (eq_refl s0) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot + | PProj s0 s1 => congr_PProj (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1) + | PConst s0 => congr_PConst (eq_refl s0) + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot end. -Lemma upExtRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n) - (zeta : fin m -> fin n) (Eq : forall x, xi x = zeta x) : +Lemma upExtRen_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat) + (Eq : forall x, xi x = zeta x) : forall x, upRen_PTm_PTm xi x = upRen_PTm_PTm zeta x. Proof. -exact (fun n => - match n with - | Some fin_n => ap shift (Eq fin_n) - | None => eq_refl - end). +exact (fun n => match n with + | S n' => ap shift (Eq n') + | O => eq_refl + end). Qed. -Lemma upExtRen_list_PTm_PTm {p : nat} {m : nat} {n : nat} - (xi : fin m -> fin n) (zeta : fin m -> fin n) - (Eq : forall x, xi x = zeta x) : - forall x, upRen_list_PTm_PTm p xi x = upRen_list_PTm_PTm p zeta x. -Proof. -exact (fun n => - scons_p_congr (fun n => eq_refl) (fun n => ap (shift_p p) (Eq n))). -Qed. - -Fixpoint extRen_PTm {m_PTm : nat} {n_PTm : nat} -(xi_PTm : fin m_PTm -> fin n_PTm) (zeta_PTm : fin m_PTm -> fin n_PTm) -(Eq_PTm : forall x, xi_PTm x = zeta_PTm x) (s : PTm m_PTm) {struct s} : +Fixpoint extRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) +(Eq_PTm : forall x, xi_PTm x = zeta_PTm x) (s : PTm) {struct s} : ren_PTm xi_PTm s = ren_PTm zeta_PTm s := match s with - | VarPTm _ s0 => ap (VarPTm n_PTm) (Eq_PTm s0) - | PAbs _ s0 => + | VarPTm s0 => ap (VarPTm) (Eq_PTm s0) + | PAbs s0 => congr_PAbs (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) (upExtRen_PTm_PTm _ _ Eq_PTm) s0) - | PApp _ s0 s1 => + | PApp s0 s1 => congr_PApp (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) - | PPair _ s0 s1 => + | PPair s0 s1 => congr_PPair (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) - | PProj _ s0 s1 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) - | PConst _ s0 => congr_PConst (eq_refl s0) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot + | PConst s0 => congr_PConst (eq_refl s0) + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot end. -Lemma upExt_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) - (tau : fin m -> PTm n_PTm) (Eq : forall x, sigma x = tau x) : +Lemma upExt_PTm_PTm (sigma : nat -> PTm) (tau : nat -> PTm) + (Eq : forall x, sigma x = tau x) : forall x, up_PTm_PTm sigma x = up_PTm_PTm tau x. Proof. exact (fun n => match n with - | Some fin_n => ap (ren_PTm shift) (Eq fin_n) - | None => eq_refl + | S n' => ap (ren_PTm shift) (Eq n') + | O => eq_refl end). Qed. -Lemma upExt_list_PTm_PTm {p : nat} {m : nat} {n_PTm : nat} - (sigma : fin m -> PTm n_PTm) (tau : fin m -> PTm n_PTm) - (Eq : forall x, sigma x = tau x) : - forall x, up_list_PTm_PTm p sigma x = up_list_PTm_PTm p tau x. -Proof. -exact (fun n => - scons_p_congr (fun n => eq_refl) - (fun n => ap (ren_PTm (shift_p p)) (Eq n))). -Qed. - -Fixpoint ext_PTm {m_PTm : nat} {n_PTm : nat} -(sigma_PTm : fin m_PTm -> PTm n_PTm) (tau_PTm : fin m_PTm -> PTm n_PTm) -(Eq_PTm : forall x, sigma_PTm x = tau_PTm x) (s : PTm m_PTm) {struct s} : +Fixpoint ext_PTm (sigma_PTm : nat -> PTm) (tau_PTm : nat -> PTm) +(Eq_PTm : forall x, sigma_PTm x = tau_PTm x) (s : PTm) {struct s} : subst_PTm sigma_PTm s = subst_PTm tau_PTm s := match s with - | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 => + | VarPTm s0 => Eq_PTm s0 + | PAbs s0 => congr_PAbs (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) (upExt_PTm_PTm _ _ Eq_PTm) s0) - | PApp _ s0 s1 => + | PApp s0 s1 => congr_PApp (ext_PTm sigma_PTm tau_PTm Eq_PTm s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) - | PPair _ s0 s1 => + | PPair s0 s1 => congr_PPair (ext_PTm sigma_PTm tau_PTm Eq_PTm s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) - | PProj _ s0 s1 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) - | PConst _ s0 => congr_PConst (eq_refl s0) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot + | PConst s0 => congr_PConst (eq_refl s0) + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot end. -Lemma up_ren_ren_PTm_PTm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l) - (zeta : fin l -> fin m) (rho : fin k -> fin m) - (Eq : forall x, funcomp zeta xi x = rho x) : +Lemma up_ren_ren_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat) + (rho : nat -> nat) (Eq : forall x, funcomp zeta xi x = rho x) : forall x, funcomp (upRen_PTm_PTm zeta) (upRen_PTm_PTm xi) x = upRen_PTm_PTm rho x. Proof. exact (up_ren_ren xi zeta rho Eq). Qed. -Lemma up_ren_ren_list_PTm_PTm {p : nat} {k : nat} {l : nat} {m : nat} - (xi : fin k -> fin l) (zeta : fin l -> fin m) (rho : fin k -> fin m) - (Eq : forall x, funcomp zeta xi x = rho x) : - forall x, - funcomp (upRen_list_PTm_PTm p zeta) (upRen_list_PTm_PTm p xi) x = - upRen_list_PTm_PTm p rho x. -Proof. -exact (up_ren_ren_p Eq). -Qed. - -Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} -(xi_PTm : fin m_PTm -> fin k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) -(rho_PTm : fin m_PTm -> fin l_PTm) -(Eq_PTm : forall x, funcomp zeta_PTm xi_PTm x = rho_PTm x) (s : PTm m_PTm) -{struct s} : ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm rho_PTm s := +Fixpoint compRenRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) +(rho_PTm : nat -> nat) +(Eq_PTm : forall x, funcomp zeta_PTm xi_PTm x = rho_PTm x) (s : PTm) {struct + s} : ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm rho_PTm s := match s with - | VarPTm _ s0 => ap (VarPTm l_PTm) (Eq_PTm s0) - | PAbs _ s0 => + | VarPTm s0 => ap (VarPTm) (Eq_PTm s0) + | PAbs s0 => congr_PAbs (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s0) - | PApp _ s0 s1 => + | PApp s0 s1 => congr_PApp (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0) (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) - | PPair _ s0 s1 => + | PPair s0 s1 => congr_PPair (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0) (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) - | PProj _ s0 s1 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) - | PConst _ s0 => congr_PConst (eq_refl s0) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot + | PConst s0 => congr_PConst (eq_refl s0) + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot end. -Lemma up_ren_subst_PTm_PTm {k : nat} {l : nat} {m_PTm : nat} - (xi : fin k -> fin l) (tau : fin l -> PTm m_PTm) - (theta : fin k -> PTm m_PTm) (Eq : forall x, funcomp tau xi x = theta x) : +Lemma up_ren_subst_PTm_PTm (xi : nat -> nat) (tau : nat -> PTm) + (theta : nat -> PTm) (Eq : forall x, funcomp tau xi x = theta x) : forall x, funcomp (up_PTm_PTm tau) (upRen_PTm_PTm xi) x = up_PTm_PTm theta x. Proof. exact (fun n => match n with - | Some fin_n => ap (ren_PTm shift) (Eq fin_n) - | None => eq_refl + | S n' => ap (ren_PTm shift) (Eq n') + | O => eq_refl end). Qed. -Lemma up_ren_subst_list_PTm_PTm {p : nat} {k : nat} {l : nat} {m_PTm : nat} - (xi : fin k -> fin l) (tau : fin l -> PTm m_PTm) - (theta : fin k -> PTm m_PTm) (Eq : forall x, funcomp tau xi x = theta x) : - forall x, - funcomp (up_list_PTm_PTm p tau) (upRen_list_PTm_PTm p xi) x = - up_list_PTm_PTm p theta x. -Proof. -exact (fun n => - eq_trans (scons_p_comp' _ _ _ n) - (scons_p_congr (fun z => scons_p_head' _ _ z) - (fun z => - eq_trans (scons_p_tail' _ _ (xi z)) - (ap (ren_PTm (shift_p p)) (Eq z))))). -Qed. - -Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} -(xi_PTm : fin m_PTm -> fin k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) -(theta_PTm : fin m_PTm -> PTm l_PTm) -(Eq_PTm : forall x, funcomp tau_PTm xi_PTm x = theta_PTm x) (s : PTm m_PTm) -{struct s} : subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm theta_PTm s := +Fixpoint compRenSubst_PTm (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm) +(theta_PTm : nat -> PTm) +(Eq_PTm : forall x, funcomp tau_PTm xi_PTm x = theta_PTm x) (s : PTm) {struct + s} : subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm theta_PTm s := match s with - | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 => + | VarPTm s0 => Eq_PTm s0 + | PAbs s0 => congr_PAbs (compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm) (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s0) - | PApp _ s0 s1 => + | PApp s0 s1 => congr_PApp (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0) (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) - | PPair _ s0 s1 => + | PPair s0 s1 => congr_PPair (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0) (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) - | PProj _ s0 s1 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) - | PConst _ s0 => congr_PConst (eq_refl s0) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot + | PConst s0 => congr_PConst (eq_refl s0) + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot end. -Lemma up_subst_ren_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat} - (sigma : fin k -> PTm l_PTm) (zeta_PTm : fin l_PTm -> fin m_PTm) - (theta : fin k -> PTm m_PTm) +Lemma up_subst_ren_PTm_PTm (sigma : nat -> PTm) (zeta_PTm : nat -> nat) + (theta : nat -> PTm) (Eq : forall x, funcomp (ren_PTm zeta_PTm) sigma x = theta x) : forall x, funcomp (ren_PTm (upRen_PTm_PTm zeta_PTm)) (up_PTm_PTm sigma) x = @@ -379,72 +291,46 @@ Lemma up_subst_ren_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat} Proof. exact (fun n => match n with - | Some fin_n => + | S n' => eq_trans (compRenRen_PTm shift (upRen_PTm_PTm zeta_PTm) - (funcomp shift zeta_PTm) (fun x => eq_refl) (sigma fin_n)) + (funcomp shift zeta_PTm) (fun x => eq_refl) (sigma n')) (eq_trans (eq_sym (compRenRen_PTm zeta_PTm shift (funcomp shift zeta_PTm) - (fun x => eq_refl) (sigma fin_n))) - (ap (ren_PTm shift) (Eq fin_n))) - | None => eq_refl + (fun x => eq_refl) (sigma n'))) + (ap (ren_PTm shift) (Eq n'))) + | O => eq_refl end). Qed. -Lemma up_subst_ren_list_PTm_PTm {p : nat} {k : nat} {l_PTm : nat} - {m_PTm : nat} (sigma : fin k -> PTm l_PTm) - (zeta_PTm : fin l_PTm -> fin m_PTm) (theta : fin k -> PTm m_PTm) - (Eq : forall x, funcomp (ren_PTm zeta_PTm) sigma x = theta x) : - forall x, - funcomp (ren_PTm (upRen_list_PTm_PTm p zeta_PTm)) (up_list_PTm_PTm p sigma) - x = up_list_PTm_PTm p theta x. -Proof. -exact (fun n => - eq_trans (scons_p_comp' _ _ _ n) - (scons_p_congr - (fun x => ap (VarPTm (plus p m_PTm)) (scons_p_head' _ _ x)) - (fun n => - eq_trans - (compRenRen_PTm (shift_p p) (upRen_list_PTm_PTm p zeta_PTm) - (funcomp (shift_p p) zeta_PTm) - (fun x => scons_p_tail' _ _ x) (sigma n)) - (eq_trans - (eq_sym - (compRenRen_PTm zeta_PTm (shift_p p) - (funcomp (shift_p p) zeta_PTm) (fun x => eq_refl) - (sigma n))) (ap (ren_PTm (shift_p p)) (Eq n)))))). -Qed. - -Fixpoint compSubstRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} -(sigma_PTm : fin m_PTm -> PTm k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) -(theta_PTm : fin m_PTm -> PTm l_PTm) +Fixpoint compSubstRen_PTm (sigma_PTm : nat -> PTm) (zeta_PTm : nat -> nat) +(theta_PTm : nat -> PTm) (Eq_PTm : forall x, funcomp (ren_PTm zeta_PTm) sigma_PTm x = theta_PTm x) -(s : PTm m_PTm) {struct s} : +(s : PTm) {struct s} : ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := match s with - | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 => + | VarPTm s0 => Eq_PTm s0 + | PAbs s0 => congr_PAbs (compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm) (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s0) - | PApp _ s0 s1 => + | PApp s0 s1 => congr_PApp (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0) (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) - | PPair _ s0 s1 => + | PPair s0 s1 => congr_PPair (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0) (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) - | PProj _ s0 s1 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) - | PConst _ s0 => congr_PConst (eq_refl s0) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot + | PConst s0 => congr_PConst (eq_refl s0) + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot end. -Lemma up_subst_subst_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat} - (sigma : fin k -> PTm l_PTm) (tau_PTm : fin l_PTm -> PTm m_PTm) - (theta : fin k -> PTm m_PTm) +Lemma up_subst_subst_PTm_PTm (sigma : nat -> PTm) (tau_PTm : nat -> PTm) + (theta : nat -> PTm) (Eq : forall x, funcomp (subst_PTm tau_PTm) sigma x = theta x) : forall x, funcomp (subst_PTm (up_PTm_PTm tau_PTm)) (up_PTm_PTm sigma) x = @@ -452,649 +338,501 @@ Lemma up_subst_subst_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat} Proof. exact (fun n => match n with - | Some fin_n => + | S n' => eq_trans (compRenSubst_PTm shift (up_PTm_PTm tau_PTm) (funcomp (up_PTm_PTm tau_PTm) shift) (fun x => eq_refl) - (sigma fin_n)) + (sigma n')) (eq_trans (eq_sym (compSubstRen_PTm tau_PTm shift (funcomp (ren_PTm shift) tau_PTm) (fun x => eq_refl) - (sigma fin_n))) (ap (ren_PTm shift) (Eq fin_n))) - | None => eq_refl + (sigma n'))) (ap (ren_PTm shift) (Eq n'))) + | O => eq_refl end). Qed. -Lemma up_subst_subst_list_PTm_PTm {p : nat} {k : nat} {l_PTm : nat} - {m_PTm : nat} (sigma : fin k -> PTm l_PTm) - (tau_PTm : fin l_PTm -> PTm m_PTm) (theta : fin k -> PTm m_PTm) - (Eq : forall x, funcomp (subst_PTm tau_PTm) sigma x = theta x) : - forall x, - funcomp (subst_PTm (up_list_PTm_PTm p tau_PTm)) (up_list_PTm_PTm p sigma) x = - up_list_PTm_PTm p theta x. -Proof. -exact (fun n => - eq_trans - (scons_p_comp' (funcomp (VarPTm (plus p l_PTm)) (zero_p p)) _ _ n) - (scons_p_congr - (fun x => scons_p_head' _ (fun z => ren_PTm (shift_p p) _) x) - (fun n => - eq_trans - (compRenSubst_PTm (shift_p p) (up_list_PTm_PTm p tau_PTm) - (funcomp (up_list_PTm_PTm p tau_PTm) (shift_p p)) - (fun x => eq_refl) (sigma n)) - (eq_trans - (eq_sym - (compSubstRen_PTm tau_PTm (shift_p p) _ - (fun x => eq_sym (scons_p_tail' _ _ x)) (sigma n))) - (ap (ren_PTm (shift_p p)) (Eq n)))))). -Qed. - -Fixpoint compSubstSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} -(sigma_PTm : fin m_PTm -> PTm k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) -(theta_PTm : fin m_PTm -> PTm l_PTm) +Fixpoint compSubstSubst_PTm (sigma_PTm : nat -> PTm) (tau_PTm : nat -> PTm) +(theta_PTm : nat -> PTm) (Eq_PTm : forall x, funcomp (subst_PTm tau_PTm) sigma_PTm x = theta_PTm x) -(s : PTm m_PTm) {struct s} : +(s : PTm) {struct s} : subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := match s with - | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 => + | VarPTm s0 => Eq_PTm s0 + | PAbs s0 => congr_PAbs (compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s0) - | PApp _ s0 s1 => + | PApp s0 s1 => congr_PApp (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0) (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) - | PPair _ s0 s1 => + | PPair s0 s1 => congr_PPair (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0) (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) - | PProj _ s0 s1 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) - | PConst _ s0 => congr_PConst (eq_refl s0) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot + | PConst s0 => congr_PConst (eq_refl s0) + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot end. -Lemma renRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} - (xi_PTm : fin m_PTm -> fin k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) - (s : PTm m_PTm) : +Lemma renRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) (s : PTm) : ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm (funcomp zeta_PTm xi_PTm) s. Proof. exact (compRenRen_PTm xi_PTm zeta_PTm _ (fun n => eq_refl) s). Qed. -Lemma renRen'_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} - (xi_PTm : fin m_PTm -> fin k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) : +Lemma renRen'_PTm_pointwise (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) : pointwise_relation _ eq (funcomp (ren_PTm zeta_PTm) (ren_PTm xi_PTm)) (ren_PTm (funcomp zeta_PTm xi_PTm)). Proof. exact (fun s => compRenRen_PTm xi_PTm zeta_PTm _ (fun n => eq_refl) s). Qed. -Lemma renSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} - (xi_PTm : fin m_PTm -> fin k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) - (s : PTm m_PTm) : +Lemma renSubst_PTm (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm) (s : PTm) : subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm (funcomp tau_PTm xi_PTm) s. Proof. exact (compRenSubst_PTm xi_PTm tau_PTm _ (fun n => eq_refl) s). Qed. -Lemma renSubst_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} - (xi_PTm : fin m_PTm -> fin k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) : +Lemma renSubst_PTm_pointwise (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm) : pointwise_relation _ eq (funcomp (subst_PTm tau_PTm) (ren_PTm xi_PTm)) (subst_PTm (funcomp tau_PTm xi_PTm)). Proof. exact (fun s => compRenSubst_PTm xi_PTm tau_PTm _ (fun n => eq_refl) s). Qed. -Lemma substRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} - (sigma_PTm : fin m_PTm -> PTm k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) - (s : PTm m_PTm) : +Lemma substRen_PTm (sigma_PTm : nat -> PTm) (zeta_PTm : nat -> nat) (s : PTm) + : ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm (funcomp (ren_PTm zeta_PTm) sigma_PTm) s. Proof. exact (compSubstRen_PTm sigma_PTm zeta_PTm _ (fun n => eq_refl) s). Qed. -Lemma substRen_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} - (sigma_PTm : fin m_PTm -> PTm k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) : +Lemma substRen_PTm_pointwise (sigma_PTm : nat -> PTm) (zeta_PTm : nat -> nat) + : pointwise_relation _ eq (funcomp (ren_PTm zeta_PTm) (subst_PTm sigma_PTm)) (subst_PTm (funcomp (ren_PTm zeta_PTm) sigma_PTm)). Proof. exact (fun s => compSubstRen_PTm sigma_PTm zeta_PTm _ (fun n => eq_refl) s). Qed. -Lemma substSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} - (sigma_PTm : fin m_PTm -> PTm k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) - (s : PTm m_PTm) : +Lemma substSubst_PTm (sigma_PTm : nat -> PTm) (tau_PTm : nat -> PTm) + (s : PTm) : subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm (funcomp (subst_PTm tau_PTm) sigma_PTm) s. Proof. exact (compSubstSubst_PTm sigma_PTm tau_PTm _ (fun n => eq_refl) s). Qed. -Lemma substSubst_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} - (sigma_PTm : fin m_PTm -> PTm k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) : +Lemma substSubst_PTm_pointwise (sigma_PTm : nat -> PTm) + (tau_PTm : nat -> PTm) : pointwise_relation _ eq (funcomp (subst_PTm tau_PTm) (subst_PTm sigma_PTm)) (subst_PTm (funcomp (subst_PTm tau_PTm) sigma_PTm)). Proof. exact (fun s => compSubstSubst_PTm sigma_PTm tau_PTm _ (fun n => eq_refl) s). Qed. -Lemma rinstInst_up_PTm_PTm {m : nat} {n_PTm : nat} (xi : fin m -> fin n_PTm) - (sigma : fin m -> PTm n_PTm) - (Eq : forall x, funcomp (VarPTm n_PTm) xi x = sigma x) : - forall x, - funcomp (VarPTm (S n_PTm)) (upRen_PTm_PTm xi) x = up_PTm_PTm sigma x. +Lemma rinstInst_up_PTm_PTm (xi : nat -> nat) (sigma : nat -> PTm) + (Eq : forall x, funcomp (VarPTm) xi x = sigma x) : + forall x, funcomp (VarPTm) (upRen_PTm_PTm xi) x = up_PTm_PTm sigma x. Proof. exact (fun n => match n with - | Some fin_n => ap (ren_PTm shift) (Eq fin_n) - | None => eq_refl + | S n' => ap (ren_PTm shift) (Eq n') + | O => eq_refl end). Qed. -Lemma rinstInst_up_list_PTm_PTm {p : nat} {m : nat} {n_PTm : nat} - (xi : fin m -> fin n_PTm) (sigma : fin m -> PTm n_PTm) - (Eq : forall x, funcomp (VarPTm n_PTm) xi x = sigma x) : - forall x, - funcomp (VarPTm (plus p n_PTm)) (upRen_list_PTm_PTm p xi) x = - up_list_PTm_PTm p sigma x. -Proof. -exact (fun n => - eq_trans (scons_p_comp' _ _ (VarPTm (plus p n_PTm)) n) - (scons_p_congr (fun z => eq_refl) - (fun n => ap (ren_PTm (shift_p p)) (Eq n)))). -Qed. - -Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat} -(xi_PTm : fin m_PTm -> fin n_PTm) (sigma_PTm : fin m_PTm -> PTm n_PTm) -(Eq_PTm : forall x, funcomp (VarPTm n_PTm) xi_PTm x = sigma_PTm x) -(s : PTm m_PTm) {struct s} : ren_PTm xi_PTm s = subst_PTm sigma_PTm s := +Fixpoint rinst_inst_PTm (xi_PTm : nat -> nat) (sigma_PTm : nat -> PTm) +(Eq_PTm : forall x, funcomp (VarPTm) xi_PTm x = sigma_PTm x) (s : PTm) +{struct s} : ren_PTm xi_PTm s = subst_PTm sigma_PTm s := match s with - | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 => + | VarPTm s0 => Eq_PTm s0 + | PAbs s0 => congr_PAbs (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm) (rinstInst_up_PTm_PTm _ _ Eq_PTm) s0) - | PApp _ s0 s1 => + | PApp s0 s1 => congr_PApp (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) - | PPair _ s0 s1 => + | PPair s0 s1 => congr_PPair (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) - | PProj _ s0 s1 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) - | PConst _ s0 => congr_PConst (eq_refl s0) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot + | PConst s0 => congr_PConst (eq_refl s0) + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot end. -Lemma rinstInst'_PTm {m_PTm : nat} {n_PTm : nat} - (xi_PTm : fin m_PTm -> fin n_PTm) (s : PTm m_PTm) : - ren_PTm xi_PTm s = subst_PTm (funcomp (VarPTm n_PTm) xi_PTm) s. +Lemma rinstInst'_PTm (xi_PTm : nat -> nat) (s : PTm) : + ren_PTm xi_PTm s = subst_PTm (funcomp (VarPTm) xi_PTm) s. Proof. exact (rinst_inst_PTm xi_PTm _ (fun n => eq_refl) s). Qed. -Lemma rinstInst'_PTm_pointwise {m_PTm : nat} {n_PTm : nat} - (xi_PTm : fin m_PTm -> fin n_PTm) : +Lemma rinstInst'_PTm_pointwise (xi_PTm : nat -> nat) : pointwise_relation _ eq (ren_PTm xi_PTm) - (subst_PTm (funcomp (VarPTm n_PTm) xi_PTm)). + (subst_PTm (funcomp (VarPTm) xi_PTm)). Proof. exact (fun s => rinst_inst_PTm xi_PTm _ (fun n => eq_refl) s). Qed. -Lemma instId'_PTm {m_PTm : nat} (s : PTm m_PTm) : - subst_PTm (VarPTm m_PTm) s = s. +Lemma instId'_PTm (s : PTm) : subst_PTm (VarPTm) s = s. Proof. -exact (idSubst_PTm (VarPTm m_PTm) (fun n => eq_refl) s). +exact (idSubst_PTm (VarPTm) (fun n => eq_refl) s). Qed. -Lemma instId'_PTm_pointwise {m_PTm : nat} : - pointwise_relation _ eq (subst_PTm (VarPTm m_PTm)) id. +Lemma instId'_PTm_pointwise : pointwise_relation _ eq (subst_PTm (VarPTm)) id. Proof. -exact (fun s => idSubst_PTm (VarPTm m_PTm) (fun n => eq_refl) s). +exact (fun s => idSubst_PTm (VarPTm) (fun n => eq_refl) s). Qed. -Lemma rinstId'_PTm {m_PTm : nat} (s : PTm m_PTm) : ren_PTm id s = s. +Lemma rinstId'_PTm (s : PTm) : ren_PTm id s = s. Proof. exact (eq_ind_r (fun t => t = s) (instId'_PTm s) (rinstInst'_PTm id s)). Qed. -Lemma rinstId'_PTm_pointwise {m_PTm : nat} : - pointwise_relation _ eq (@ren_PTm m_PTm m_PTm id) id. +Lemma rinstId'_PTm_pointwise : pointwise_relation _ eq (@ren_PTm id) id. Proof. exact (fun s => eq_ind_r (fun t => t = s) (instId'_PTm s) (rinstInst'_PTm id s)). Qed. -Lemma varL'_PTm {m_PTm : nat} {n_PTm : nat} - (sigma_PTm : fin m_PTm -> PTm n_PTm) (x : fin m_PTm) : - subst_PTm sigma_PTm (VarPTm m_PTm x) = sigma_PTm x. +Lemma varL'_PTm (sigma_PTm : nat -> PTm) (x : nat) : + subst_PTm sigma_PTm (VarPTm x) = sigma_PTm x. Proof. exact (eq_refl). Qed. -Lemma varL'_PTm_pointwise {m_PTm : nat} {n_PTm : nat} - (sigma_PTm : fin m_PTm -> PTm n_PTm) : - pointwise_relation _ eq (funcomp (subst_PTm sigma_PTm) (VarPTm m_PTm)) - sigma_PTm. +Lemma varL'_PTm_pointwise (sigma_PTm : nat -> PTm) : + pointwise_relation _ eq (funcomp (subst_PTm sigma_PTm) (VarPTm)) sigma_PTm. Proof. exact (fun x => eq_refl). Qed. -Lemma varLRen'_PTm {m_PTm : nat} {n_PTm : nat} - (xi_PTm : fin m_PTm -> fin n_PTm) (x : fin m_PTm) : - ren_PTm xi_PTm (VarPTm m_PTm x) = VarPTm n_PTm (xi_PTm x). +Lemma varLRen'_PTm (xi_PTm : nat -> nat) (x : nat) : + ren_PTm xi_PTm (VarPTm x) = VarPTm (xi_PTm x). Proof. exact (eq_refl). Qed. -Lemma varLRen'_PTm_pointwise {m_PTm : nat} {n_PTm : nat} - (xi_PTm : fin m_PTm -> fin n_PTm) : - pointwise_relation _ eq (funcomp (ren_PTm xi_PTm) (VarPTm m_PTm)) - (funcomp (VarPTm n_PTm) xi_PTm). +Lemma varLRen'_PTm_pointwise (xi_PTm : nat -> nat) : + pointwise_relation _ eq (funcomp (ren_PTm xi_PTm) (VarPTm)) + (funcomp (VarPTm) xi_PTm). Proof. exact (fun x => eq_refl). Qed. -Inductive Tm (n_Tm : nat) : Type := - | VarTm : fin n_Tm -> Tm n_Tm - | Abs : Tm (S n_Tm) -> Tm n_Tm - | App : Tm n_Tm -> Tm n_Tm -> Tm n_Tm - | Pair : Tm n_Tm -> Tm n_Tm -> Tm n_Tm - | Proj : PTag -> Tm n_Tm -> Tm n_Tm - | TBind : TTag -> Tm n_Tm -> Tm (S n_Tm) -> Tm n_Tm - | Univ : nat -> Tm n_Tm - | BVal : bool -> Tm n_Tm - | Bool : Tm n_Tm - | If : Tm n_Tm -> Tm n_Tm -> Tm n_Tm -> Tm n_Tm. +Inductive Tm : Type := + | VarTm : nat -> Tm + | Abs : Tm -> Tm + | App : Tm -> Tm -> Tm + | Pair : Tm -> Tm -> Tm + | Proj : PTag -> Tm -> Tm + | TBind : TTag -> Tm -> Tm -> Tm + | Univ : nat -> Tm + | BVal : bool -> Tm + | Bool : Tm + | If : Tm -> Tm -> Tm -> Tm. -Lemma congr_Abs {m_Tm : nat} {s0 : Tm (S m_Tm)} {t0 : Tm (S m_Tm)} - (H0 : s0 = t0) : Abs m_Tm s0 = Abs m_Tm t0. +Lemma congr_Abs {s0 : Tm} {t0 : Tm} (H0 : s0 = t0) : Abs s0 = Abs t0. Proof. -exact (eq_trans eq_refl (ap (fun x => Abs m_Tm x) H0)). +exact (eq_trans eq_refl (ap (fun x => Abs x) H0)). Qed. -Lemma congr_App {m_Tm : nat} {s0 : Tm m_Tm} {s1 : Tm m_Tm} {t0 : Tm m_Tm} - {t1 : Tm m_Tm} (H0 : s0 = t0) (H1 : s1 = t1) : - App m_Tm s0 s1 = App m_Tm t0 t1. +Lemma congr_App {s0 : Tm} {s1 : Tm} {t0 : Tm} {t1 : Tm} (H0 : s0 = t0) + (H1 : s1 = t1) : App s0 s1 = App t0 t1. Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => App m_Tm x s1) H0)) - (ap (fun x => App m_Tm t0 x) H1)). +exact (eq_trans (eq_trans eq_refl (ap (fun x => App x s1) H0)) + (ap (fun x => App t0 x) H1)). Qed. -Lemma congr_Pair {m_Tm : nat} {s0 : Tm m_Tm} {s1 : Tm m_Tm} {t0 : Tm m_Tm} - {t1 : Tm m_Tm} (H0 : s0 = t0) (H1 : s1 = t1) : - Pair m_Tm s0 s1 = Pair m_Tm t0 t1. +Lemma congr_Pair {s0 : Tm} {s1 : Tm} {t0 : Tm} {t1 : Tm} (H0 : s0 = t0) + (H1 : s1 = t1) : Pair s0 s1 = Pair t0 t1. Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => Pair m_Tm x s1) H0)) - (ap (fun x => Pair m_Tm t0 x) H1)). +exact (eq_trans (eq_trans eq_refl (ap (fun x => Pair x s1) H0)) + (ap (fun x => Pair t0 x) H1)). Qed. -Lemma congr_Proj {m_Tm : nat} {s0 : PTag} {s1 : Tm m_Tm} {t0 : PTag} - {t1 : Tm m_Tm} (H0 : s0 = t0) (H1 : s1 = t1) : - Proj m_Tm s0 s1 = Proj m_Tm t0 t1. +Lemma congr_Proj {s0 : PTag} {s1 : Tm} {t0 : PTag} {t1 : Tm} (H0 : s0 = t0) + (H1 : s1 = t1) : Proj s0 s1 = Proj t0 t1. Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => Proj m_Tm x s1) H0)) - (ap (fun x => Proj m_Tm t0 x) H1)). +exact (eq_trans (eq_trans eq_refl (ap (fun x => Proj x s1) H0)) + (ap (fun x => Proj t0 x) H1)). Qed. -Lemma congr_TBind {m_Tm : nat} {s0 : TTag} {s1 : Tm m_Tm} {s2 : Tm (S m_Tm)} - {t0 : TTag} {t1 : Tm m_Tm} {t2 : Tm (S m_Tm)} (H0 : s0 = t0) (H1 : s1 = t1) - (H2 : s2 = t2) : TBind m_Tm s0 s1 s2 = TBind m_Tm t0 t1 t2. +Lemma congr_TBind {s0 : TTag} {s1 : Tm} {s2 : Tm} {t0 : TTag} {t1 : Tm} + {t2 : Tm} (H0 : s0 = t0) (H1 : s1 = t1) (H2 : s2 = t2) : + TBind s0 s1 s2 = TBind t0 t1 t2. Proof. exact (eq_trans - (eq_trans (eq_trans eq_refl (ap (fun x => TBind m_Tm x s1 s2) H0)) - (ap (fun x => TBind m_Tm t0 x s2) H1)) - (ap (fun x => TBind m_Tm t0 t1 x) H2)). + (eq_trans (eq_trans eq_refl (ap (fun x => TBind x s1 s2) H0)) + (ap (fun x => TBind t0 x s2) H1)) + (ap (fun x => TBind t0 t1 x) H2)). Qed. -Lemma congr_Univ {m_Tm : nat} {s0 : nat} {t0 : nat} (H0 : s0 = t0) : - Univ m_Tm s0 = Univ m_Tm t0. +Lemma congr_Univ {s0 : nat} {t0 : nat} (H0 : s0 = t0) : Univ s0 = Univ t0. Proof. -exact (eq_trans eq_refl (ap (fun x => Univ m_Tm x) H0)). +exact (eq_trans eq_refl (ap (fun x => Univ x) H0)). Qed. -Lemma congr_BVal {m_Tm : nat} {s0 : bool} {t0 : bool} (H0 : s0 = t0) : - BVal m_Tm s0 = BVal m_Tm t0. +Lemma congr_BVal {s0 : bool} {t0 : bool} (H0 : s0 = t0) : BVal s0 = BVal t0. Proof. -exact (eq_trans eq_refl (ap (fun x => BVal m_Tm x) H0)). +exact (eq_trans eq_refl (ap (fun x => BVal x) H0)). Qed. -Lemma congr_Bool {m_Tm : nat} : Bool m_Tm = Bool m_Tm. +Lemma congr_Bool : Bool = Bool. Proof. exact (eq_refl). Qed. -Lemma congr_If {m_Tm : nat} {s0 : Tm m_Tm} {s1 : Tm m_Tm} {s2 : Tm m_Tm} - {t0 : Tm m_Tm} {t1 : Tm m_Tm} {t2 : Tm m_Tm} (H0 : s0 = t0) (H1 : s1 = t1) - (H2 : s2 = t2) : If m_Tm s0 s1 s2 = If m_Tm t0 t1 t2. +Lemma congr_If {s0 : Tm} {s1 : Tm} {s2 : Tm} {t0 : Tm} {t1 : Tm} {t2 : Tm} + (H0 : s0 = t0) (H1 : s1 = t1) (H2 : s2 = t2) : If s0 s1 s2 = If t0 t1 t2. Proof. exact (eq_trans - (eq_trans (eq_trans eq_refl (ap (fun x => If m_Tm x s1 s2) H0)) - (ap (fun x => If m_Tm t0 x s2) H1)) - (ap (fun x => If m_Tm t0 t1 x) H2)). + (eq_trans (eq_trans eq_refl (ap (fun x => If x s1 s2) H0)) + (ap (fun x => If t0 x s2) H1)) (ap (fun x => If t0 t1 x) H2)). Qed. -Lemma upRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n) : - fin (S m) -> fin (S n). +Lemma upRen_Tm_Tm (xi : nat -> nat) : nat -> nat. Proof. exact (up_ren xi). Defined. -Lemma upRen_list_Tm_Tm (p : nat) {m : nat} {n : nat} (xi : fin m -> fin n) : - fin (plus p m) -> fin (plus p n). -Proof. -exact (upRen_p p xi). -Defined. - -Fixpoint ren_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm) -(s : Tm m_Tm) {struct s} : Tm n_Tm := +Fixpoint ren_Tm (xi_Tm : nat -> nat) (s : Tm) {struct s} : Tm := match s with - | VarTm _ s0 => VarTm n_Tm (xi_Tm s0) - | Abs _ s0 => Abs n_Tm (ren_Tm (upRen_Tm_Tm xi_Tm) s0) - | App _ s0 s1 => App n_Tm (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1) - | Pair _ s0 s1 => Pair n_Tm (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1) - | Proj _ s0 s1 => Proj n_Tm s0 (ren_Tm xi_Tm s1) - | TBind _ s0 s1 s2 => - TBind n_Tm s0 (ren_Tm xi_Tm s1) (ren_Tm (upRen_Tm_Tm xi_Tm) s2) - | Univ _ s0 => Univ n_Tm s0 - | BVal _ s0 => BVal n_Tm s0 - | Bool _ => Bool n_Tm - | If _ s0 s1 s2 => - If n_Tm (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1) (ren_Tm xi_Tm s2) + | VarTm s0 => VarTm (xi_Tm s0) + | Abs s0 => Abs (ren_Tm (upRen_Tm_Tm xi_Tm) s0) + | App s0 s1 => App (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1) + | Pair s0 s1 => Pair (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1) + | Proj s0 s1 => Proj s0 (ren_Tm xi_Tm s1) + | TBind s0 s1 s2 => + TBind s0 (ren_Tm xi_Tm s1) (ren_Tm (upRen_Tm_Tm xi_Tm) s2) + | Univ s0 => Univ s0 + | BVal s0 => BVal s0 + | Bool => Bool + | If s0 s1 s2 => If (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1) (ren_Tm xi_Tm s2) end. -Lemma up_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm) : - fin (S m) -> Tm (S n_Tm). +Lemma up_Tm_Tm (sigma : nat -> Tm) : nat -> Tm. Proof. -exact (scons (VarTm (S n_Tm) var_zero) (funcomp (ren_Tm shift) sigma)). +exact (scons (VarTm var_zero) (funcomp (ren_Tm shift) sigma)). Defined. -Lemma up_list_Tm_Tm (p : nat) {m : nat} {n_Tm : nat} - (sigma : fin m -> Tm n_Tm) : fin (plus p m) -> Tm (plus p n_Tm). -Proof. -exact (scons_p p (funcomp (VarTm (plus p n_Tm)) (zero_p p)) - (funcomp (ren_Tm (shift_p p)) sigma)). -Defined. - -Fixpoint subst_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm) -(s : Tm m_Tm) {struct s} : Tm n_Tm := +Fixpoint subst_Tm (sigma_Tm : nat -> Tm) (s : Tm) {struct s} : Tm := match s with - | VarTm _ s0 => sigma_Tm s0 - | Abs _ s0 => Abs n_Tm (subst_Tm (up_Tm_Tm sigma_Tm) s0) - | App _ s0 s1 => App n_Tm (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1) - | Pair _ s0 s1 => Pair n_Tm (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1) - | Proj _ s0 s1 => Proj n_Tm s0 (subst_Tm sigma_Tm s1) - | TBind _ s0 s1 s2 => - TBind n_Tm s0 (subst_Tm sigma_Tm s1) (subst_Tm (up_Tm_Tm sigma_Tm) s2) - | Univ _ s0 => Univ n_Tm s0 - | BVal _ s0 => BVal n_Tm s0 - | Bool _ => Bool n_Tm - | If _ s0 s1 s2 => - If n_Tm (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1) - (subst_Tm sigma_Tm s2) + | VarTm s0 => sigma_Tm s0 + | Abs s0 => Abs (subst_Tm (up_Tm_Tm sigma_Tm) s0) + | App s0 s1 => App (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1) + | Pair s0 s1 => Pair (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1) + | Proj s0 s1 => Proj s0 (subst_Tm sigma_Tm s1) + | TBind s0 s1 s2 => + TBind s0 (subst_Tm sigma_Tm s1) (subst_Tm (up_Tm_Tm sigma_Tm) s2) + | Univ s0 => Univ s0 + | BVal s0 => BVal s0 + | Bool => Bool + | If s0 s1 s2 => + If (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1) (subst_Tm sigma_Tm s2) end. -Lemma upId_Tm_Tm {m_Tm : nat} (sigma : fin m_Tm -> Tm m_Tm) - (Eq : forall x, sigma x = VarTm m_Tm x) : - forall x, up_Tm_Tm sigma x = VarTm (S m_Tm) x. +Lemma upId_Tm_Tm (sigma : nat -> Tm) (Eq : forall x, sigma x = VarTm x) : + forall x, up_Tm_Tm sigma x = VarTm x. Proof. exact (fun n => match n with - | Some fin_n => ap (ren_Tm shift) (Eq fin_n) - | None => eq_refl + | S n' => ap (ren_Tm shift) (Eq n') + | O => eq_refl end). Qed. -Lemma upId_list_Tm_Tm {p : nat} {m_Tm : nat} (sigma : fin m_Tm -> Tm m_Tm) - (Eq : forall x, sigma x = VarTm m_Tm x) : - forall x, up_list_Tm_Tm p sigma x = VarTm (plus p m_Tm) x. -Proof. -exact (fun n => - scons_p_eta (VarTm (plus p m_Tm)) - (fun n => ap (ren_Tm (shift_p p)) (Eq n)) (fun n => eq_refl)). -Qed. - -Fixpoint idSubst_Tm {m_Tm : nat} (sigma_Tm : fin m_Tm -> Tm m_Tm) -(Eq_Tm : forall x, sigma_Tm x = VarTm m_Tm x) (s : Tm m_Tm) {struct s} : +Fixpoint idSubst_Tm (sigma_Tm : nat -> Tm) +(Eq_Tm : forall x, sigma_Tm x = VarTm x) (s : Tm) {struct s} : subst_Tm sigma_Tm s = s := match s with - | VarTm _ s0 => Eq_Tm s0 - | Abs _ s0 => + | VarTm s0 => Eq_Tm s0 + | Abs s0 => congr_Abs (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s0) - | App _ s0 s1 => + | App s0 s1 => congr_App (idSubst_Tm sigma_Tm Eq_Tm s0) (idSubst_Tm sigma_Tm Eq_Tm s1) - | Pair _ s0 s1 => + | Pair s0 s1 => congr_Pair (idSubst_Tm sigma_Tm Eq_Tm s0) (idSubst_Tm sigma_Tm Eq_Tm s1) - | Proj _ s0 s1 => congr_Proj (eq_refl s0) (idSubst_Tm sigma_Tm Eq_Tm s1) - | TBind _ s0 s1 s2 => + | Proj s0 s1 => congr_Proj (eq_refl s0) (idSubst_Tm sigma_Tm Eq_Tm s1) + | TBind s0 s1 s2 => congr_TBind (eq_refl s0) (idSubst_Tm sigma_Tm Eq_Tm s1) (idSubst_Tm (up_Tm_Tm sigma_Tm) (upId_Tm_Tm _ Eq_Tm) s2) - | Univ _ s0 => congr_Univ (eq_refl s0) - | BVal _ s0 => congr_BVal (eq_refl s0) - | Bool _ => congr_Bool - | If _ s0 s1 s2 => + | Univ s0 => congr_Univ (eq_refl s0) + | BVal s0 => congr_BVal (eq_refl s0) + | Bool => congr_Bool + | If s0 s1 s2 => congr_If (idSubst_Tm sigma_Tm Eq_Tm s0) (idSubst_Tm sigma_Tm Eq_Tm s1) (idSubst_Tm sigma_Tm Eq_Tm s2) end. -Lemma upExtRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n) - (zeta : fin m -> fin n) (Eq : forall x, xi x = zeta x) : +Lemma upExtRen_Tm_Tm (xi : nat -> nat) (zeta : nat -> nat) + (Eq : forall x, xi x = zeta x) : forall x, upRen_Tm_Tm xi x = upRen_Tm_Tm zeta x. Proof. -exact (fun n => - match n with - | Some fin_n => ap shift (Eq fin_n) - | None => eq_refl - end). +exact (fun n => match n with + | S n' => ap shift (Eq n') + | O => eq_refl + end). Qed. -Lemma upExtRen_list_Tm_Tm {p : nat} {m : nat} {n : nat} (xi : fin m -> fin n) - (zeta : fin m -> fin n) (Eq : forall x, xi x = zeta x) : - forall x, upRen_list_Tm_Tm p xi x = upRen_list_Tm_Tm p zeta x. -Proof. -exact (fun n => - scons_p_congr (fun n => eq_refl) (fun n => ap (shift_p p) (Eq n))). -Qed. - -Fixpoint extRen_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm) -(zeta_Tm : fin m_Tm -> fin n_Tm) (Eq_Tm : forall x, xi_Tm x = zeta_Tm x) -(s : Tm m_Tm) {struct s} : ren_Tm xi_Tm s = ren_Tm zeta_Tm s := +Fixpoint extRen_Tm (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat) +(Eq_Tm : forall x, xi_Tm x = zeta_Tm x) (s : Tm) {struct s} : +ren_Tm xi_Tm s = ren_Tm zeta_Tm s := match s with - | VarTm _ s0 => ap (VarTm n_Tm) (Eq_Tm s0) - | Abs _ s0 => + | VarTm s0 => ap (VarTm) (Eq_Tm s0) + | Abs s0 => congr_Abs (extRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm) (upExtRen_Tm_Tm _ _ Eq_Tm) s0) - | App _ s0 s1 => + | App s0 s1 => congr_App (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1) - | Pair _ s0 s1 => + | Pair s0 s1 => congr_Pair (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1) - | Proj _ s0 s1 => - congr_Proj (eq_refl s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1) - | TBind _ s0 s1 s2 => + | Proj s0 s1 => congr_Proj (eq_refl s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1) + | TBind s0 s1 s2 => congr_TBind (eq_refl s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1) (extRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm) (upExtRen_Tm_Tm _ _ Eq_Tm) s2) - | Univ _ s0 => congr_Univ (eq_refl s0) - | BVal _ s0 => congr_BVal (eq_refl s0) - | Bool _ => congr_Bool - | If _ s0 s1 s2 => + | Univ s0 => congr_Univ (eq_refl s0) + | BVal s0 => congr_BVal (eq_refl s0) + | Bool => congr_Bool + | If s0 s1 s2 => congr_If (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1) (extRen_Tm xi_Tm zeta_Tm Eq_Tm s2) end. -Lemma upExt_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm) - (tau : fin m -> Tm n_Tm) (Eq : forall x, sigma x = tau x) : +Lemma upExt_Tm_Tm (sigma : nat -> Tm) (tau : nat -> Tm) + (Eq : forall x, sigma x = tau x) : forall x, up_Tm_Tm sigma x = up_Tm_Tm tau x. Proof. exact (fun n => match n with - | Some fin_n => ap (ren_Tm shift) (Eq fin_n) - | None => eq_refl + | S n' => ap (ren_Tm shift) (Eq n') + | O => eq_refl end). Qed. -Lemma upExt_list_Tm_Tm {p : nat} {m : nat} {n_Tm : nat} - (sigma : fin m -> Tm n_Tm) (tau : fin m -> Tm n_Tm) - (Eq : forall x, sigma x = tau x) : - forall x, up_list_Tm_Tm p sigma x = up_list_Tm_Tm p tau x. -Proof. -exact (fun n => - scons_p_congr (fun n => eq_refl) - (fun n => ap (ren_Tm (shift_p p)) (Eq n))). -Qed. - -Fixpoint ext_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm) -(tau_Tm : fin m_Tm -> Tm n_Tm) (Eq_Tm : forall x, sigma_Tm x = tau_Tm x) -(s : Tm m_Tm) {struct s} : subst_Tm sigma_Tm s = subst_Tm tau_Tm s := +Fixpoint ext_Tm (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm) +(Eq_Tm : forall x, sigma_Tm x = tau_Tm x) (s : Tm) {struct s} : +subst_Tm sigma_Tm s = subst_Tm tau_Tm s := match s with - | VarTm _ s0 => Eq_Tm s0 - | Abs _ s0 => + | VarTm s0 => Eq_Tm s0 + | Abs s0 => congr_Abs (ext_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (upExt_Tm_Tm _ _ Eq_Tm) s0) - | App _ s0 s1 => + | App s0 s1 => congr_App (ext_Tm sigma_Tm tau_Tm Eq_Tm s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1) - | Pair _ s0 s1 => + | Pair s0 s1 => congr_Pair (ext_Tm sigma_Tm tau_Tm Eq_Tm s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1) - | Proj _ s0 s1 => congr_Proj (eq_refl s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1) - | TBind _ s0 s1 s2 => + | Proj s0 s1 => congr_Proj (eq_refl s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1) + | TBind s0 s1 s2 => congr_TBind (eq_refl s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1) (ext_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (upExt_Tm_Tm _ _ Eq_Tm) s2) - | Univ _ s0 => congr_Univ (eq_refl s0) - | BVal _ s0 => congr_BVal (eq_refl s0) - | Bool _ => congr_Bool - | If _ s0 s1 s2 => + | Univ s0 => congr_Univ (eq_refl s0) + | BVal s0 => congr_BVal (eq_refl s0) + | Bool => congr_Bool + | If s0 s1 s2 => congr_If (ext_Tm sigma_Tm tau_Tm Eq_Tm s0) (ext_Tm sigma_Tm tau_Tm Eq_Tm s1) (ext_Tm sigma_Tm tau_Tm Eq_Tm s2) end. -Lemma up_ren_ren_Tm_Tm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l) - (zeta : fin l -> fin m) (rho : fin k -> fin m) - (Eq : forall x, funcomp zeta xi x = rho x) : +Lemma up_ren_ren_Tm_Tm (xi : nat -> nat) (zeta : nat -> nat) + (rho : nat -> nat) (Eq : forall x, funcomp zeta xi x = rho x) : forall x, funcomp (upRen_Tm_Tm zeta) (upRen_Tm_Tm xi) x = upRen_Tm_Tm rho x. Proof. exact (up_ren_ren xi zeta rho Eq). Qed. -Lemma up_ren_ren_list_Tm_Tm {p : nat} {k : nat} {l : nat} {m : nat} - (xi : fin k -> fin l) (zeta : fin l -> fin m) (rho : fin k -> fin m) - (Eq : forall x, funcomp zeta xi x = rho x) : - forall x, - funcomp (upRen_list_Tm_Tm p zeta) (upRen_list_Tm_Tm p xi) x = - upRen_list_Tm_Tm p rho x. -Proof. -exact (up_ren_ren_p Eq). -Qed. - -Fixpoint compRenRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} -(xi_Tm : fin m_Tm -> fin k_Tm) (zeta_Tm : fin k_Tm -> fin l_Tm) -(rho_Tm : fin m_Tm -> fin l_Tm) -(Eq_Tm : forall x, funcomp zeta_Tm xi_Tm x = rho_Tm x) (s : Tm m_Tm) {struct - s} : ren_Tm zeta_Tm (ren_Tm xi_Tm s) = ren_Tm rho_Tm s := +Fixpoint compRenRen_Tm (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat) +(rho_Tm : nat -> nat) (Eq_Tm : forall x, funcomp zeta_Tm xi_Tm x = rho_Tm x) +(s : Tm) {struct s} : ren_Tm zeta_Tm (ren_Tm xi_Tm s) = ren_Tm rho_Tm s := match s with - | VarTm _ s0 => ap (VarTm l_Tm) (Eq_Tm s0) - | Abs _ s0 => + | VarTm s0 => ap (VarTm) (Eq_Tm s0) + | Abs s0 => congr_Abs (compRenRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm) (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s0) - | App _ s0 s1 => + | App s0 s1 => congr_App (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1) - | Pair _ s0 s1 => + | Pair s0 s1 => congr_Pair (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1) - | Proj _ s0 s1 => + | Proj s0 s1 => congr_Proj (eq_refl s0) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1) - | TBind _ s0 s1 s2 => + | TBind s0 s1 s2 => congr_TBind (eq_refl s0) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1) (compRenRen_Tm (upRen_Tm_Tm xi_Tm) (upRen_Tm_Tm zeta_Tm) (upRen_Tm_Tm rho_Tm) (up_ren_ren _ _ _ Eq_Tm) s2) - | Univ _ s0 => congr_Univ (eq_refl s0) - | BVal _ s0 => congr_BVal (eq_refl s0) - | Bool _ => congr_Bool - | If _ s0 s1 s2 => + | Univ s0 => congr_Univ (eq_refl s0) + | BVal s0 => congr_BVal (eq_refl s0) + | Bool => congr_Bool + | If s0 s1 s2 => congr_If (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1) (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s2) end. -Lemma up_ren_subst_Tm_Tm {k : nat} {l : nat} {m_Tm : nat} - (xi : fin k -> fin l) (tau : fin l -> Tm m_Tm) (theta : fin k -> Tm m_Tm) - (Eq : forall x, funcomp tau xi x = theta x) : +Lemma up_ren_subst_Tm_Tm (xi : nat -> nat) (tau : nat -> Tm) + (theta : nat -> Tm) (Eq : forall x, funcomp tau xi x = theta x) : forall x, funcomp (up_Tm_Tm tau) (upRen_Tm_Tm xi) x = up_Tm_Tm theta x. Proof. exact (fun n => match n with - | Some fin_n => ap (ren_Tm shift) (Eq fin_n) - | None => eq_refl + | S n' => ap (ren_Tm shift) (Eq n') + | O => eq_refl end). Qed. -Lemma up_ren_subst_list_Tm_Tm {p : nat} {k : nat} {l : nat} {m_Tm : nat} - (xi : fin k -> fin l) (tau : fin l -> Tm m_Tm) (theta : fin k -> Tm m_Tm) - (Eq : forall x, funcomp tau xi x = theta x) : - forall x, - funcomp (up_list_Tm_Tm p tau) (upRen_list_Tm_Tm p xi) x = - up_list_Tm_Tm p theta x. -Proof. -exact (fun n => - eq_trans (scons_p_comp' _ _ _ n) - (scons_p_congr (fun z => scons_p_head' _ _ z) - (fun z => - eq_trans (scons_p_tail' _ _ (xi z)) - (ap (ren_Tm (shift_p p)) (Eq z))))). -Qed. - -Fixpoint compRenSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} -(xi_Tm : fin m_Tm -> fin k_Tm) (tau_Tm : fin k_Tm -> Tm l_Tm) -(theta_Tm : fin m_Tm -> Tm l_Tm) -(Eq_Tm : forall x, funcomp tau_Tm xi_Tm x = theta_Tm x) (s : Tm m_Tm) {struct - s} : subst_Tm tau_Tm (ren_Tm xi_Tm s) = subst_Tm theta_Tm s := +Fixpoint compRenSubst_Tm (xi_Tm : nat -> nat) (tau_Tm : nat -> Tm) +(theta_Tm : nat -> Tm) +(Eq_Tm : forall x, funcomp tau_Tm xi_Tm x = theta_Tm x) (s : Tm) {struct s} : +subst_Tm tau_Tm (ren_Tm xi_Tm s) = subst_Tm theta_Tm s := match s with - | VarTm _ s0 => Eq_Tm s0 - | Abs _ s0 => + | VarTm s0 => Eq_Tm s0 + | Abs s0 => congr_Abs (compRenSubst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm tau_Tm) (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s0) - | App _ s0 s1 => + | App s0 s1 => congr_App (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0) (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1) - | Pair _ s0 s1 => + | Pair s0 s1 => congr_Pair (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0) (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1) - | Proj _ s0 s1 => + | Proj s0 s1 => congr_Proj (eq_refl s0) (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1) - | TBind _ s0 s1 s2 => + | TBind s0 s1 s2 => congr_TBind (eq_refl s0) (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1) (compRenSubst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm tau_Tm) (up_Tm_Tm theta_Tm) (up_ren_subst_Tm_Tm _ _ _ Eq_Tm) s2) - | Univ _ s0 => congr_Univ (eq_refl s0) - | BVal _ s0 => congr_BVal (eq_refl s0) - | Bool _ => congr_Bool - | If _ s0 s1 s2 => + | Univ s0 => congr_Univ (eq_refl s0) + | BVal s0 => congr_BVal (eq_refl s0) + | Bool => congr_Bool + | If s0 s1 s2 => congr_If (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0) (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1) (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s2) end. -Lemma up_subst_ren_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat} - (sigma : fin k -> Tm l_Tm) (zeta_Tm : fin l_Tm -> fin m_Tm) - (theta : fin k -> Tm m_Tm) +Lemma up_subst_ren_Tm_Tm (sigma : nat -> Tm) (zeta_Tm : nat -> nat) + (theta : nat -> Tm) (Eq : forall x, funcomp (ren_Tm zeta_Tm) sigma x = theta x) : forall x, funcomp (ren_Tm (upRen_Tm_Tm zeta_Tm)) (up_Tm_Tm sigma) x = @@ -1102,341 +840,257 @@ Lemma up_subst_ren_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat} Proof. exact (fun n => match n with - | Some fin_n => + | S n' => eq_trans (compRenRen_Tm shift (upRen_Tm_Tm zeta_Tm) - (funcomp shift zeta_Tm) (fun x => eq_refl) (sigma fin_n)) + (funcomp shift zeta_Tm) (fun x => eq_refl) (sigma n')) (eq_trans (eq_sym (compRenRen_Tm zeta_Tm shift (funcomp shift zeta_Tm) - (fun x => eq_refl) (sigma fin_n))) - (ap (ren_Tm shift) (Eq fin_n))) - | None => eq_refl + (fun x => eq_refl) (sigma n'))) + (ap (ren_Tm shift) (Eq n'))) + | O => eq_refl end). Qed. -Lemma up_subst_ren_list_Tm_Tm {p : nat} {k : nat} {l_Tm : nat} {m_Tm : nat} - (sigma : fin k -> Tm l_Tm) (zeta_Tm : fin l_Tm -> fin m_Tm) - (theta : fin k -> Tm m_Tm) - (Eq : forall x, funcomp (ren_Tm zeta_Tm) sigma x = theta x) : - forall x, - funcomp (ren_Tm (upRen_list_Tm_Tm p zeta_Tm)) (up_list_Tm_Tm p sigma) x = - up_list_Tm_Tm p theta x. -Proof. -exact (fun n => - eq_trans (scons_p_comp' _ _ _ n) - (scons_p_congr - (fun x => ap (VarTm (plus p m_Tm)) (scons_p_head' _ _ x)) - (fun n => - eq_trans - (compRenRen_Tm (shift_p p) (upRen_list_Tm_Tm p zeta_Tm) - (funcomp (shift_p p) zeta_Tm) - (fun x => scons_p_tail' _ _ x) (sigma n)) - (eq_trans - (eq_sym - (compRenRen_Tm zeta_Tm (shift_p p) - (funcomp (shift_p p) zeta_Tm) (fun x => eq_refl) - (sigma n))) (ap (ren_Tm (shift_p p)) (Eq n)))))). -Qed. - -Fixpoint compSubstRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} -(sigma_Tm : fin m_Tm -> Tm k_Tm) (zeta_Tm : fin k_Tm -> fin l_Tm) -(theta_Tm : fin m_Tm -> Tm l_Tm) -(Eq_Tm : forall x, funcomp (ren_Tm zeta_Tm) sigma_Tm x = theta_Tm x) -(s : Tm m_Tm) {struct s} : +Fixpoint compSubstRen_Tm (sigma_Tm : nat -> Tm) (zeta_Tm : nat -> nat) +(theta_Tm : nat -> Tm) +(Eq_Tm : forall x, funcomp (ren_Tm zeta_Tm) sigma_Tm x = theta_Tm x) +(s : Tm) {struct s} : ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s := match s with - | VarTm _ s0 => Eq_Tm s0 - | Abs _ s0 => + | VarTm s0 => Eq_Tm s0 + | Abs s0 => congr_Abs (compSubstRen_Tm (up_Tm_Tm sigma_Tm) (upRen_Tm_Tm zeta_Tm) (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s0) - | App _ s0 s1 => + | App s0 s1 => congr_App (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0) (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1) - | Pair _ s0 s1 => + | Pair s0 s1 => congr_Pair (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0) (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1) - | Proj _ s0 s1 => + | Proj s0 s1 => congr_Proj (eq_refl s0) (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1) - | TBind _ s0 s1 s2 => + | TBind s0 s1 s2 => congr_TBind (eq_refl s0) (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1) (compSubstRen_Tm (up_Tm_Tm sigma_Tm) (upRen_Tm_Tm zeta_Tm) (up_Tm_Tm theta_Tm) (up_subst_ren_Tm_Tm _ _ _ Eq_Tm) s2) - | Univ _ s0 => congr_Univ (eq_refl s0) - | BVal _ s0 => congr_BVal (eq_refl s0) - | Bool _ => congr_Bool - | If _ s0 s1 s2 => + | Univ s0 => congr_Univ (eq_refl s0) + | BVal s0 => congr_BVal (eq_refl s0) + | Bool => congr_Bool + | If s0 s1 s2 => congr_If (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0) (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1) (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s2) end. -Lemma up_subst_subst_Tm_Tm {k : nat} {l_Tm : nat} {m_Tm : nat} - (sigma : fin k -> Tm l_Tm) (tau_Tm : fin l_Tm -> Tm m_Tm) - (theta : fin k -> Tm m_Tm) +Lemma up_subst_subst_Tm_Tm (sigma : nat -> Tm) (tau_Tm : nat -> Tm) + (theta : nat -> Tm) (Eq : forall x, funcomp (subst_Tm tau_Tm) sigma x = theta x) : forall x, funcomp (subst_Tm (up_Tm_Tm tau_Tm)) (up_Tm_Tm sigma) x = up_Tm_Tm theta x. Proof. exact (fun n => match n with - | Some fin_n => + | S n' => eq_trans (compRenSubst_Tm shift (up_Tm_Tm tau_Tm) (funcomp (up_Tm_Tm tau_Tm) shift) (fun x => eq_refl) - (sigma fin_n)) + (sigma n')) (eq_trans (eq_sym (compSubstRen_Tm tau_Tm shift (funcomp (ren_Tm shift) tau_Tm) (fun x => eq_refl) - (sigma fin_n))) (ap (ren_Tm shift) (Eq fin_n))) - | None => eq_refl + (sigma n'))) (ap (ren_Tm shift) (Eq n'))) + | O => eq_refl end). Qed. -Lemma up_subst_subst_list_Tm_Tm {p : nat} {k : nat} {l_Tm : nat} {m_Tm : nat} - (sigma : fin k -> Tm l_Tm) (tau_Tm : fin l_Tm -> Tm m_Tm) - (theta : fin k -> Tm m_Tm) - (Eq : forall x, funcomp (subst_Tm tau_Tm) sigma x = theta x) : - forall x, - funcomp (subst_Tm (up_list_Tm_Tm p tau_Tm)) (up_list_Tm_Tm p sigma) x = - up_list_Tm_Tm p theta x. -Proof. -exact (fun n => - eq_trans - (scons_p_comp' (funcomp (VarTm (plus p l_Tm)) (zero_p p)) _ _ n) - (scons_p_congr - (fun x => scons_p_head' _ (fun z => ren_Tm (shift_p p) _) x) - (fun n => - eq_trans - (compRenSubst_Tm (shift_p p) (up_list_Tm_Tm p tau_Tm) - (funcomp (up_list_Tm_Tm p tau_Tm) (shift_p p)) - (fun x => eq_refl) (sigma n)) - (eq_trans - (eq_sym - (compSubstRen_Tm tau_Tm (shift_p p) _ - (fun x => eq_sym (scons_p_tail' _ _ x)) (sigma n))) - (ap (ren_Tm (shift_p p)) (Eq n)))))). -Qed. - -Fixpoint compSubstSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} -(sigma_Tm : fin m_Tm -> Tm k_Tm) (tau_Tm : fin k_Tm -> Tm l_Tm) -(theta_Tm : fin m_Tm -> Tm l_Tm) +Fixpoint compSubstSubst_Tm (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm) +(theta_Tm : nat -> Tm) (Eq_Tm : forall x, funcomp (subst_Tm tau_Tm) sigma_Tm x = theta_Tm x) -(s : Tm m_Tm) {struct s} : +(s : Tm) {struct s} : subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s := match s with - | VarTm _ s0 => Eq_Tm s0 - | Abs _ s0 => + | VarTm s0 => Eq_Tm s0 + | Abs s0 => congr_Abs (compSubstSubst_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s0) - | App _ s0 s1 => + | App s0 s1 => congr_App (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0) (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1) - | Pair _ s0 s1 => + | Pair s0 s1 => congr_Pair (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0) (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1) - | Proj _ s0 s1 => + | Proj s0 s1 => congr_Proj (eq_refl s0) (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1) - | TBind _ s0 s1 s2 => + | TBind s0 s1 s2 => congr_TBind (eq_refl s0) (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1) (compSubstSubst_Tm (up_Tm_Tm sigma_Tm) (up_Tm_Tm tau_Tm) (up_Tm_Tm theta_Tm) (up_subst_subst_Tm_Tm _ _ _ Eq_Tm) s2) - | Univ _ s0 => congr_Univ (eq_refl s0) - | BVal _ s0 => congr_BVal (eq_refl s0) - | Bool _ => congr_Bool - | If _ s0 s1 s2 => + | Univ s0 => congr_Univ (eq_refl s0) + | BVal s0 => congr_BVal (eq_refl s0) + | Bool => congr_Bool + | If s0 s1 s2 => congr_If (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0) (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1) (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s2) end. -Lemma renRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} - (xi_Tm : fin m_Tm -> fin k_Tm) (zeta_Tm : fin k_Tm -> fin l_Tm) - (s : Tm m_Tm) : +Lemma renRen_Tm (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat) (s : Tm) : ren_Tm zeta_Tm (ren_Tm xi_Tm s) = ren_Tm (funcomp zeta_Tm xi_Tm) s. Proof. exact (compRenRen_Tm xi_Tm zeta_Tm _ (fun n => eq_refl) s). Qed. -Lemma renRen'_Tm_pointwise {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} - (xi_Tm : fin m_Tm -> fin k_Tm) (zeta_Tm : fin k_Tm -> fin l_Tm) : +Lemma renRen'_Tm_pointwise (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat) : pointwise_relation _ eq (funcomp (ren_Tm zeta_Tm) (ren_Tm xi_Tm)) (ren_Tm (funcomp zeta_Tm xi_Tm)). Proof. exact (fun s => compRenRen_Tm xi_Tm zeta_Tm _ (fun n => eq_refl) s). Qed. -Lemma renSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} - (xi_Tm : fin m_Tm -> fin k_Tm) (tau_Tm : fin k_Tm -> Tm l_Tm) (s : Tm m_Tm) - : subst_Tm tau_Tm (ren_Tm xi_Tm s) = subst_Tm (funcomp tau_Tm xi_Tm) s. +Lemma renSubst_Tm (xi_Tm : nat -> nat) (tau_Tm : nat -> Tm) (s : Tm) : + subst_Tm tau_Tm (ren_Tm xi_Tm s) = subst_Tm (funcomp tau_Tm xi_Tm) s. Proof. exact (compRenSubst_Tm xi_Tm tau_Tm _ (fun n => eq_refl) s). Qed. -Lemma renSubst_Tm_pointwise {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} - (xi_Tm : fin m_Tm -> fin k_Tm) (tau_Tm : fin k_Tm -> Tm l_Tm) : +Lemma renSubst_Tm_pointwise (xi_Tm : nat -> nat) (tau_Tm : nat -> Tm) : pointwise_relation _ eq (funcomp (subst_Tm tau_Tm) (ren_Tm xi_Tm)) (subst_Tm (funcomp tau_Tm xi_Tm)). Proof. exact (fun s => compRenSubst_Tm xi_Tm tau_Tm _ (fun n => eq_refl) s). Qed. -Lemma substRen_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} - (sigma_Tm : fin m_Tm -> Tm k_Tm) (zeta_Tm : fin k_Tm -> fin l_Tm) - (s : Tm m_Tm) : +Lemma substRen_Tm (sigma_Tm : nat -> Tm) (zeta_Tm : nat -> nat) (s : Tm) : ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm (funcomp (ren_Tm zeta_Tm) sigma_Tm) s. Proof. exact (compSubstRen_Tm sigma_Tm zeta_Tm _ (fun n => eq_refl) s). Qed. -Lemma substRen_Tm_pointwise {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} - (sigma_Tm : fin m_Tm -> Tm k_Tm) (zeta_Tm : fin k_Tm -> fin l_Tm) : +Lemma substRen_Tm_pointwise (sigma_Tm : nat -> Tm) (zeta_Tm : nat -> nat) : pointwise_relation _ eq (funcomp (ren_Tm zeta_Tm) (subst_Tm sigma_Tm)) (subst_Tm (funcomp (ren_Tm zeta_Tm) sigma_Tm)). Proof. exact (fun s => compSubstRen_Tm sigma_Tm zeta_Tm _ (fun n => eq_refl) s). Qed. -Lemma substSubst_Tm {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} - (sigma_Tm : fin m_Tm -> Tm k_Tm) (tau_Tm : fin k_Tm -> Tm l_Tm) - (s : Tm m_Tm) : +Lemma substSubst_Tm (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm) (s : Tm) : subst_Tm tau_Tm (subst_Tm sigma_Tm s) = subst_Tm (funcomp (subst_Tm tau_Tm) sigma_Tm) s. Proof. exact (compSubstSubst_Tm sigma_Tm tau_Tm _ (fun n => eq_refl) s). Qed. -Lemma substSubst_Tm_pointwise {k_Tm : nat} {l_Tm : nat} {m_Tm : nat} - (sigma_Tm : fin m_Tm -> Tm k_Tm) (tau_Tm : fin k_Tm -> Tm l_Tm) : +Lemma substSubst_Tm_pointwise (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm) : pointwise_relation _ eq (funcomp (subst_Tm tau_Tm) (subst_Tm sigma_Tm)) (subst_Tm (funcomp (subst_Tm tau_Tm) sigma_Tm)). Proof. exact (fun s => compSubstSubst_Tm sigma_Tm tau_Tm _ (fun n => eq_refl) s). Qed. -Lemma rinstInst_up_Tm_Tm {m : nat} {n_Tm : nat} (xi : fin m -> fin n_Tm) - (sigma : fin m -> Tm n_Tm) - (Eq : forall x, funcomp (VarTm n_Tm) xi x = sigma x) : - forall x, funcomp (VarTm (S n_Tm)) (upRen_Tm_Tm xi) x = up_Tm_Tm sigma x. +Lemma rinstInst_up_Tm_Tm (xi : nat -> nat) (sigma : nat -> Tm) + (Eq : forall x, funcomp (VarTm) xi x = sigma x) : + forall x, funcomp (VarTm) (upRen_Tm_Tm xi) x = up_Tm_Tm sigma x. Proof. exact (fun n => match n with - | Some fin_n => ap (ren_Tm shift) (Eq fin_n) - | None => eq_refl + | S n' => ap (ren_Tm shift) (Eq n') + | O => eq_refl end). Qed. -Lemma rinstInst_up_list_Tm_Tm {p : nat} {m : nat} {n_Tm : nat} - (xi : fin m -> fin n_Tm) (sigma : fin m -> Tm n_Tm) - (Eq : forall x, funcomp (VarTm n_Tm) xi x = sigma x) : - forall x, - funcomp (VarTm (plus p n_Tm)) (upRen_list_Tm_Tm p xi) x = - up_list_Tm_Tm p sigma x. -Proof. -exact (fun n => - eq_trans (scons_p_comp' _ _ (VarTm (plus p n_Tm)) n) - (scons_p_congr (fun z => eq_refl) - (fun n => ap (ren_Tm (shift_p p)) (Eq n)))). -Qed. - -Fixpoint rinst_inst_Tm {m_Tm : nat} {n_Tm : nat} -(xi_Tm : fin m_Tm -> fin n_Tm) (sigma_Tm : fin m_Tm -> Tm n_Tm) -(Eq_Tm : forall x, funcomp (VarTm n_Tm) xi_Tm x = sigma_Tm x) (s : Tm m_Tm) -{struct s} : ren_Tm xi_Tm s = subst_Tm sigma_Tm s := +Fixpoint rinst_inst_Tm (xi_Tm : nat -> nat) (sigma_Tm : nat -> Tm) +(Eq_Tm : forall x, funcomp (VarTm) xi_Tm x = sigma_Tm x) (s : Tm) {struct s} + : ren_Tm xi_Tm s = subst_Tm sigma_Tm s := match s with - | VarTm _ s0 => Eq_Tm s0 - | Abs _ s0 => + | VarTm s0 => Eq_Tm s0 + | Abs s0 => congr_Abs (rinst_inst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm sigma_Tm) (rinstInst_up_Tm_Tm _ _ Eq_Tm) s0) - | App _ s0 s1 => + | App s0 s1 => congr_App (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1) - | Pair _ s0 s1 => + | Pair s0 s1 => congr_Pair (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1) - | Proj _ s0 s1 => + | Proj s0 s1 => congr_Proj (eq_refl s0) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1) - | TBind _ s0 s1 s2 => + | TBind s0 s1 s2 => congr_TBind (eq_refl s0) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1) (rinst_inst_Tm (upRen_Tm_Tm xi_Tm) (up_Tm_Tm sigma_Tm) (rinstInst_up_Tm_Tm _ _ Eq_Tm) s2) - | Univ _ s0 => congr_Univ (eq_refl s0) - | BVal _ s0 => congr_BVal (eq_refl s0) - | Bool _ => congr_Bool - | If _ s0 s1 s2 => + | Univ s0 => congr_Univ (eq_refl s0) + | BVal s0 => congr_BVal (eq_refl s0) + | Bool => congr_Bool + | If s0 s1 s2 => congr_If (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1) (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s2) end. -Lemma rinstInst'_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm) - (s : Tm m_Tm) : ren_Tm xi_Tm s = subst_Tm (funcomp (VarTm n_Tm) xi_Tm) s. +Lemma rinstInst'_Tm (xi_Tm : nat -> nat) (s : Tm) : + ren_Tm xi_Tm s = subst_Tm (funcomp (VarTm) xi_Tm) s. Proof. exact (rinst_inst_Tm xi_Tm _ (fun n => eq_refl) s). Qed. -Lemma rinstInst'_Tm_pointwise {m_Tm : nat} {n_Tm : nat} - (xi_Tm : fin m_Tm -> fin n_Tm) : - pointwise_relation _ eq (ren_Tm xi_Tm) - (subst_Tm (funcomp (VarTm n_Tm) xi_Tm)). +Lemma rinstInst'_Tm_pointwise (xi_Tm : nat -> nat) : + pointwise_relation _ eq (ren_Tm xi_Tm) (subst_Tm (funcomp (VarTm) xi_Tm)). Proof. exact (fun s => rinst_inst_Tm xi_Tm _ (fun n => eq_refl) s). Qed. -Lemma instId'_Tm {m_Tm : nat} (s : Tm m_Tm) : subst_Tm (VarTm m_Tm) s = s. +Lemma instId'_Tm (s : Tm) : subst_Tm (VarTm) s = s. Proof. -exact (idSubst_Tm (VarTm m_Tm) (fun n => eq_refl) s). +exact (idSubst_Tm (VarTm) (fun n => eq_refl) s). Qed. -Lemma instId'_Tm_pointwise {m_Tm : nat} : - pointwise_relation _ eq (subst_Tm (VarTm m_Tm)) id. +Lemma instId'_Tm_pointwise : pointwise_relation _ eq (subst_Tm (VarTm)) id. Proof. -exact (fun s => idSubst_Tm (VarTm m_Tm) (fun n => eq_refl) s). +exact (fun s => idSubst_Tm (VarTm) (fun n => eq_refl) s). Qed. -Lemma rinstId'_Tm {m_Tm : nat} (s : Tm m_Tm) : ren_Tm id s = s. +Lemma rinstId'_Tm (s : Tm) : ren_Tm id s = s. Proof. exact (eq_ind_r (fun t => t = s) (instId'_Tm s) (rinstInst'_Tm id s)). Qed. -Lemma rinstId'_Tm_pointwise {m_Tm : nat} : - pointwise_relation _ eq (@ren_Tm m_Tm m_Tm id) id. +Lemma rinstId'_Tm_pointwise : pointwise_relation _ eq (@ren_Tm id) id. Proof. exact (fun s => eq_ind_r (fun t => t = s) (instId'_Tm s) (rinstInst'_Tm id s)). Qed. -Lemma varL'_Tm {m_Tm : nat} {n_Tm : nat} (sigma_Tm : fin m_Tm -> Tm n_Tm) - (x : fin m_Tm) : subst_Tm sigma_Tm (VarTm m_Tm x) = sigma_Tm x. +Lemma varL'_Tm (sigma_Tm : nat -> Tm) (x : nat) : + subst_Tm sigma_Tm (VarTm x) = sigma_Tm x. Proof. exact (eq_refl). Qed. -Lemma varL'_Tm_pointwise {m_Tm : nat} {n_Tm : nat} - (sigma_Tm : fin m_Tm -> Tm n_Tm) : - pointwise_relation _ eq (funcomp (subst_Tm sigma_Tm) (VarTm m_Tm)) sigma_Tm. +Lemma varL'_Tm_pointwise (sigma_Tm : nat -> Tm) : + pointwise_relation _ eq (funcomp (subst_Tm sigma_Tm) (VarTm)) sigma_Tm. Proof. exact (fun x => eq_refl). Qed. -Lemma varLRen'_Tm {m_Tm : nat} {n_Tm : nat} (xi_Tm : fin m_Tm -> fin n_Tm) - (x : fin m_Tm) : ren_Tm xi_Tm (VarTm m_Tm x) = VarTm n_Tm (xi_Tm x). +Lemma varLRen'_Tm (xi_Tm : nat -> nat) (x : nat) : + ren_Tm xi_Tm (VarTm x) = VarTm (xi_Tm x). Proof. exact (eq_refl). Qed. -Lemma varLRen'_Tm_pointwise {m_Tm : nat} {n_Tm : nat} - (xi_Tm : fin m_Tm -> fin n_Tm) : - pointwise_relation _ eq (funcomp (ren_Tm xi_Tm) (VarTm m_Tm)) - (funcomp (VarTm n_Tm) xi_Tm). +Lemma varLRen'_Tm_pointwise (xi_Tm : nat -> nat) : + pointwise_relation _ eq (funcomp (ren_Tm xi_Tm) (VarTm)) + (funcomp (VarTm) xi_Tm). Proof. exact (fun x => eq_refl). Qed. @@ -1447,30 +1101,22 @@ Class Up_Tm X Y := Class Up_PTm X Y := up_PTm : X -> Y. -#[global] -Instance Subst_Tm {m_Tm n_Tm : nat}: (Subst1 _ _ _) := (@subst_Tm m_Tm n_Tm). +#[global] Instance Subst_Tm : (Subst1 _ _ _) := @subst_Tm. + +#[global] Instance Up_Tm_Tm : (Up_Tm _ _) := @up_Tm_Tm. + +#[global] Instance Ren_Tm : (Ren1 _ _ _) := @ren_Tm. + +#[global] Instance VarInstance_Tm : (Var _ _) := @VarTm. + +#[global] Instance Subst_PTm : (Subst1 _ _ _) := @subst_PTm. + +#[global] Instance Up_PTm_PTm : (Up_PTm _ _) := @up_PTm_PTm. + +#[global] Instance Ren_PTm : (Ren1 _ _ _) := @ren_PTm. #[global] -Instance Up_Tm_Tm {m n_Tm : nat}: (Up_Tm _ _) := (@up_Tm_Tm m n_Tm). - -#[global] -Instance Ren_Tm {m_Tm n_Tm : nat}: (Ren1 _ _ _) := (@ren_Tm m_Tm n_Tm). - -#[global] -Instance VarInstance_Tm {n_Tm : nat}: (Var _ _) := (@VarTm n_Tm). - -#[global] -Instance Subst_PTm {m_PTm n_PTm : nat}: (Subst1 _ _ _) := - (@subst_PTm m_PTm n_PTm). - -#[global] -Instance Up_PTm_PTm {m n_PTm : nat}: (Up_PTm _ _) := (@up_PTm_PTm m n_PTm). - -#[global] -Instance Ren_PTm {m_PTm n_PTm : nat}: (Ren1 _ _ _) := (@ren_PTm m_PTm n_PTm). - -#[global] -Instance VarInstance_PTm {n_PTm : nat}: (Var _ _) := (@VarPTm n_PTm). +Instance VarInstance_PTm : (Var _ _) := @VarPTm. Notation "[ sigma_Tm ]" := (subst_Tm sigma_Tm) ( at level 1, left associativity, only printing) : fscope. @@ -1521,9 +1167,9 @@ Notation "x '__PTm'" := (VarPTm x) ( at level 5, format "x __PTm") : subst_scope. #[global] -Instance subst_Tm_morphism {m_Tm : nat} {n_Tm : nat}: +Instance subst_Tm_morphism : (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) - (@subst_Tm m_Tm n_Tm)). + (@subst_Tm)). Proof. exact (fun f_Tm g_Tm Eq_Tm s t Eq_st => eq_ind s (fun t' => subst_Tm f_Tm s = subst_Tm g_Tm t') @@ -1531,17 +1177,16 @@ exact (fun f_Tm g_Tm Eq_Tm s t Eq_st => Qed. #[global] -Instance subst_Tm_morphism2 {m_Tm : nat} {n_Tm : nat}: +Instance subst_Tm_morphism2 : (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq)) - (@subst_Tm m_Tm n_Tm)). + (@subst_Tm)). Proof. exact (fun f_Tm g_Tm Eq_Tm s => ext_Tm f_Tm g_Tm Eq_Tm s). Qed. #[global] -Instance ren_Tm_morphism {m_Tm : nat} {n_Tm : nat}: - (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) - (@ren_Tm m_Tm n_Tm)). +Instance ren_Tm_morphism : + (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) (@ren_Tm)). Proof. exact (fun f_Tm g_Tm Eq_Tm s t Eq_st => eq_ind s (fun t' => ren_Tm f_Tm s = ren_Tm g_Tm t') @@ -1549,17 +1194,17 @@ exact (fun f_Tm g_Tm Eq_Tm s t Eq_st => Qed. #[global] -Instance ren_Tm_morphism2 {m_Tm : nat} {n_Tm : nat}: +Instance ren_Tm_morphism2 : (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq)) - (@ren_Tm m_Tm n_Tm)). + (@ren_Tm)). Proof. exact (fun f_Tm g_Tm Eq_Tm s => extRen_Tm f_Tm g_Tm Eq_Tm s). Qed. #[global] -Instance subst_PTm_morphism {m_PTm : nat} {n_PTm : nat}: +Instance subst_PTm_morphism : (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) - (@subst_PTm m_PTm n_PTm)). + (@subst_PTm)). Proof. exact (fun f_PTm g_PTm Eq_PTm s t Eq_st => eq_ind s (fun t' => subst_PTm f_PTm s = subst_PTm g_PTm t') @@ -1567,17 +1212,16 @@ exact (fun f_PTm g_PTm Eq_PTm s t Eq_st => Qed. #[global] -Instance subst_PTm_morphism2 {m_PTm : nat} {n_PTm : nat}: +Instance subst_PTm_morphism2 : (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq)) - (@subst_PTm m_PTm n_PTm)). + (@subst_PTm)). Proof. exact (fun f_PTm g_PTm Eq_PTm s => ext_PTm f_PTm g_PTm Eq_PTm s). Qed. #[global] -Instance ren_PTm_morphism {m_PTm : nat} {n_PTm : nat}: - (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) - (@ren_PTm m_PTm n_PTm)). +Instance ren_PTm_morphism : + (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) (@ren_PTm)). Proof. exact (fun f_PTm g_PTm Eq_PTm s t Eq_st => eq_ind s (fun t' => ren_PTm f_PTm s = ren_PTm g_PTm t') @@ -1585,9 +1229,9 @@ exact (fun f_PTm g_PTm Eq_PTm s t Eq_st => Qed. #[global] -Instance ren_PTm_morphism2 {m_PTm : nat} {n_PTm : nat}: +Instance ren_PTm_morphism2 : (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq)) - (@ren_PTm m_PTm n_PTm)). + (@ren_PTm)). Proof. exact (fun f_PTm g_PTm Eq_PTm s => extRen_PTm f_PTm g_PTm Eq_PTm s). Qed. @@ -1641,9 +1285,8 @@ Ltac asimpl' := repeat (first | progress setoid_rewrite instId'_PTm_pointwise | progress setoid_rewrite instId'_PTm | progress - unfold up_list_Tm_Tm, up_Tm_Tm, upRen_list_Tm_Tm, - upRen_Tm_Tm, up_list_PTm_PTm, up_PTm_PTm, - upRen_list_PTm_PTm, upRen_PTm_PTm, up_ren + unfold up_Tm_Tm, upRen_Tm_Tm, up_PTm_PTm, upRen_PTm_PTm, + up_ren | progress cbn[subst_Tm ren_Tm subst_PTm ren_PTm] | progress fsimpl ]). @@ -1673,52 +1316,15 @@ End Core. Module Extra. -Import -Core. +Import Core. -Arguments VarTm {n_Tm}. +#[global] Hint Opaque subst_Tm: rewrite. -Arguments If {n_Tm}. +#[global] Hint Opaque ren_Tm: rewrite. -Arguments Bool {n_Tm}. +#[global] Hint Opaque subst_PTm: rewrite. -Arguments BVal {n_Tm}. - -Arguments Univ {n_Tm}. - -Arguments TBind {n_Tm}. - -Arguments Proj {n_Tm}. - -Arguments Pair {n_Tm}. - -Arguments App {n_Tm}. - -Arguments Abs {n_Tm}. - -Arguments VarPTm {n_PTm}. - -Arguments PBot {n_PTm}. - -Arguments PUniv {n_PTm}. - -Arguments PConst {n_PTm}. - -Arguments PProj {n_PTm}. - -Arguments PPair {n_PTm}. - -Arguments PApp {n_PTm}. - -Arguments PAbs {n_PTm}. - -#[global]Hint Opaque subst_Tm: rewrite. - -#[global]Hint Opaque ren_Tm: rewrite. - -#[global]Hint Opaque subst_PTm: rewrite. - -#[global]Hint Opaque ren_PTm: rewrite. +#[global] Hint Opaque ren_PTm: rewrite. End Extra. diff --git a/theories/Autosubst2/unscoped.v b/theories/Autosubst2/unscoped.v new file mode 100644 index 0000000..55f8172 --- /dev/null +++ b/theories/Autosubst2/unscoped.v @@ -0,0 +1,213 @@ +(** * Autosubst Header for Unnamed Syntax + +Version: December 11, 2019. + *) + +(* Adrian: + I changed this library a bit to work better with my generated code. + 1. I use nat directly instead of defining fin to be nat and using Some/None as S/O + 2. I removed the "s, sigma" notation for scons because it interacts with dependent function types "forall x, A"*) +Require Import core. +Require Import Setoid Morphisms Relation_Definitions. + +Definition ap {X Y} (f : X -> Y) {x y : X} (p : x = y) : f x = f y := + match p with eq_refl => eq_refl end. + +Definition apc {X Y} {f g : X -> Y} {x y : X} (p : f = g) (q : x = y) : f x = g y := + match q with eq_refl => match p with eq_refl => eq_refl end end. + +(** ** Primitives of the Sigma Calculus. *) + +Definition shift := S. + +Definition var_zero := 0. + +Definition id {X} := @Datatypes.id X. + +Definition scons {X: Type} (x : X) (xi : nat -> X) := + fun n => match n with + | 0 => x + | S n => xi n + end. + +#[ export ] +Hint Opaque scons : rewrite. + +(** ** Type Class Instances for Notation +Required to make notation work. *) + +(** *** Type classes for renamings. *) + +Class Ren1 (X1 : Type) (Y Z : Type) := + ren1 : X1 -> Y -> Z. + +Class Ren2 (X1 X2 : Type) (Y Z : Type) := + ren2 : X1 -> X2 -> Y -> Z. + +Class Ren3 (X1 X2 X3 : Type) (Y Z : Type) := + ren3 : X1 -> X2 -> X3 -> Y -> Z. + +Class Ren4 (X1 X2 X3 X4 : Type) (Y Z : Type) := + ren4 : X1 -> X2 -> X3 -> X4 -> Y -> Z. + +Class Ren5 (X1 X2 X3 X4 X5 : Type) (Y Z : Type) := + ren5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z. + +Module RenNotations. + Notation "s ⟨ xi1 ⟩" := (ren1 xi1 s) (at level 7, left associativity, format "s ⟨ xi1 ⟩") : subst_scope. + + Notation "s ⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ⟩") : subst_scope. + + Notation "s ⟨ xi1 ; xi2 ; xi3 ⟩" := (ren3 xi1 xi2 xi3 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ⟩") : subst_scope. + + Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩" := (ren4 xi1 xi2 xi3 xi4 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩") : subst_scope. + + Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩" := (ren5 xi1 xi2 xi3 xi4 xi5 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩") : subst_scope. + + Notation "⟨ xi ⟩" := (ren1 xi) (at level 1, left associativity, format "⟨ xi ⟩") : fscope. + + Notation "⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2) (at level 1, left associativity, format "⟨ xi1 ; xi2 ⟩") : fscope. +End RenNotations. + +(** *** Type Classes for Substiution *) + +Class Subst1 (X1 : Type) (Y Z: Type) := + subst1 : X1 -> Y -> Z. + +Class Subst2 (X1 X2 : Type) (Y Z: Type) := + subst2 : X1 -> X2 -> Y -> Z. + +Class Subst3 (X1 X2 X3 : Type) (Y Z: Type) := + subst3 : X1 -> X2 -> X3 -> Y -> Z. + +Class Subst4 (X1 X2 X3 X4: Type) (Y Z: Type) := + subst4 : X1 -> X2 -> X3 -> X4 -> Y -> Z. + +Class Subst5 (X1 X2 X3 X4 X5 : Type) (Y Z: Type) := + subst5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z. + +Module SubstNotations. + Notation "s [ sigma ]" := (subst1 sigma s) (at level 7, left associativity, format "s '/' [ sigma ]") : subst_scope. + + Notation "s [ sigma ; tau ]" := (subst2 sigma tau s) (at level 7, left associativity, format "s '/' [ sigma ; '/' tau ]") : subst_scope. +End SubstNotations. + +(** *** Type Class for Variables *) + +Class Var X Y := + ids : X -> Y. + +#[export] Instance idsRen : Var nat nat := id. + +(** ** Proofs for the substitution primitives. *) + +Arguments funcomp {X Y Z} (g)%fscope (f)%fscope. + +Module CombineNotations. + Notation "f >> g" := (funcomp g f) (at level 50) : fscope. + + Notation "s .: sigma" := (scons s sigma) (at level 55, sigma at next level, right associativity) : subst_scope. + + #[ global ] + Open Scope fscope. + #[ global ] + Open Scope subst_scope. +End CombineNotations. + +Import CombineNotations. + + +(** A generic lifting of a renaming. *) +Definition up_ren (xi : nat -> nat) := + 0 .: (xi >> S). + +(** A generic proof that lifting of renamings composes. *) +Lemma up_ren_ren (xi: nat -> nat) (zeta : nat -> nat) (rho: nat -> nat) (E: forall x, (xi >> zeta) x = rho x) : + forall x, (up_ren xi >> up_ren zeta) x = up_ren rho x. +Proof. + intros [|x]. + - reflexivity. + - unfold up_ren. cbn. unfold funcomp. f_equal. apply E. +Qed. + +(** Eta laws. *) +Lemma scons_eta' {T} (f : nat -> T) : + pointwise_relation _ eq (f var_zero .: (funcomp f shift)) f. +Proof. intros x. destruct x; reflexivity. Qed. + +Lemma scons_eta_id' : + pointwise_relation _ eq (var_zero .: shift) id. +Proof. intros x. destruct x; reflexivity. Qed. + +Lemma scons_comp' (T: Type) {U} (s: T) (sigma: nat -> T) (tau: T -> U) : + pointwise_relation _ eq (funcomp tau (s .: sigma)) ((tau s) .: (funcomp tau sigma)). +Proof. intros x. destruct x; reflexivity. Qed. + +(* Morphism for Setoid Rewriting. The only morphism that can be defined statically. *) +#[export] Instance scons_morphism {X: Type} : + Proper (eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons X). +Proof. + intros ? t -> sigma tau H. + intros [|x]. + cbn. reflexivity. + apply H. +Qed. + +#[export] Instance scons_morphism2 {X: Type} : + Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons X). +Proof. + intros ? t -> sigma tau H ? x ->. + destruct x as [|x]. + cbn. reflexivity. + apply H. +Qed. + +(** ** Generic lifting of an allfv predicate *) +Definition up_allfv (p: nat -> Prop) : nat -> Prop := scons True p. + +(** ** Notations for unscoped syntax *) +Module UnscopedNotations. + Include RenNotations. + Include SubstNotations. + Include CombineNotations. + + (* Notation "s , sigma" := (scons s sigma) (at level 60, format "s , sigma", right associativity) : subst_scope. *) + + Notation "s '..'" := (scons s ids) (at level 1, format "s ..") : subst_scope. + + Notation "↑" := (shift) : subst_scope. + + #[global] + Open Scope fscope. + #[global] + Open Scope subst_scope. +End UnscopedNotations. + +(** ** Tactics for unscoped syntax *) + +(** Automatically does a case analysis on a natural number, useful for proofs with context renamings/context morphisms. *) +Tactic Notation "auto_case" tactic(t) := (match goal with + | [|- forall (i : nat), _] => intros []; t + end). + + +(** Generic fsimpl tactic: simplifies the above primitives in a goal. *) +Ltac fsimpl := + repeat match goal with + | [|- context[id >> ?f]] => change (id >> f) with f (* AsimplCompIdL *) + | [|- context[?f >> id]] => change (f >> id) with f (* AsimplCompIdR *) + | [|- context [id ?s]] => change (id s) with s + | [|- context[(?f >> ?g) >> ?h]] => change ((f >> g) >> h) with (f >> (g >> h)) + | [|- context[(?v .: ?g) var_zero]] => change ((v .: g) var_zero) with v + | [|- context[(?v .: ?g) 0]] => change ((v .: g) 0) with v + | [|- context[(?v .: ?g) (S ?n)]] => change ((v .: g) (S n)) with (g n) + | [|- context[?f >> (?x .: ?g)]] => change (f >> (x .: g)) with g (* f should evaluate to shift *) + | [|- context[var_zero]] => change var_zero with 0 + | [|- context[?x2 .: (funcomp ?f shift)]] => change (scons x2 (funcomp f shift)) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite (@scons_eta' _ _ f) + | [|- context[?f var_zero .: ?g]] => change (scons (f var_zero) g) with (scons (f var_zero) (funcomp f shift)); rewrite scons_eta' + | [|- _ = ?h (?f ?s)] => change (h (f s)) with ((f >> h) s) + | [|- ?h (?f ?s) = _] => change (h (f s)) with ((f >> h) s) + (* DONE had to put an underscore as the last argument to scons. This might be an argument against unfolding funcomp *) + | [|- context[funcomp _ (scons _ _)]] => setoid_rewrite scons_comp'; eta_reduce + | [|- context[scons var_zero shift]] => setoid_rewrite scons_eta_id'; eta_reduce + end. \ No newline at end of file diff --git a/theories/fp_red.v b/theories/fp_red.v index bbe58d9..f9abc08 100644 --- a/theories/fp_red.v +++ b/theories/fp_red.v @@ -7,7 +7,7 @@ Require Import Arith.Wf_nat. Require Import Psatz. From stdpp Require Import relations (rtc (..), rtc_once, rtc_r). From Hammer Require Import Tactics. -Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax. +Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax. Ltac2 spec_refl () := List.iter @@ -22,7 +22,7 @@ Ltac spec_refl := ltac2:(spec_refl ()). (* Trying my best to not write C style module_funcname *) Module Par. - Inductive R {n} : PTm n -> PTm n -> Prop := + Inductive R : PTm -> PTm -> Prop := (***************** Beta ***********************) | AppAbs a0 a1 b0 b1 : R a0 a1 -> @@ -72,35 +72,35 @@ Module Par. | Bot : R PBot PBot. - Lemma refl n (a : PTm n) : R a a. - elim : n /a; hauto ctrs:R. + Lemma refl (a : PTm) : R a a. + elim : a; hauto ctrs:R. Qed. - Lemma AppAbs' n a0 a1 (b0 b1 t : PTm n) : + Lemma AppAbs' a0 a1 (b0 b1 t : PTm) : t = subst_PTm (scons b1 VarPTm) a1 -> R a0 a1 -> R b0 b1 -> R (PApp (PAbs a0) b0) t. Proof. move => ->. apply AppAbs. Qed. - Lemma ProjPair' n p (a0 a1 b0 b1 : PTm n) t : + Lemma ProjPair' p (a0 a1 b0 b1 : PTm) t : t = (if p is PL then a1 else b1) -> R a0 a1 -> R b0 b1 -> R (PProj p (PPair a0 b0)) t. Proof. move => > ->. apply ProjPair. Qed. - Lemma AppEta' n (a0 a1 b : PTm n) : + Lemma AppEta' (a0 a1 b : PTm) : b = (PAbs (PApp (ren_PTm shift a1) (VarPTm var_zero))) -> R a0 a1 -> R a0 b. Proof. move => ->; apply AppEta. Qed. - Lemma renaming n m (a b : PTm n) (ξ : fin n -> fin m) : + Lemma renaming (a b : PTm) (ξ : nat -> nat) : R a b -> R (ren_PTm ξ a) (ren_PTm ξ b). Proof. - move => h. move : m ξ. - elim : n a b /h. + move => h. move : ξ. + elim : a b /h. move => *; apply : AppAbs'; eauto; by asimpl. all : match goal with | [ |- context[var_zero]] => move => *; apply : AppEta'; eauto; by asimpl @@ -109,23 +109,23 @@ Module Par. Qed. - Lemma morphing n m (a b : PTm n) (ρ0 ρ1 : fin n -> PTm m) : + Lemma morphing (a b : PTm) (ρ0 ρ1 : nat -> PTm) : (forall i, R (ρ0 i) (ρ1 i)) -> R a b -> R (subst_PTm ρ0 a) (subst_PTm ρ1 b). Proof. - move => + h. move : m ρ0 ρ1. elim : n a b/h. - - move => n a0 a1 b0 b1 ha iha hb ihb m ρ0 ρ1 hρ /=. + move => + h. move : ρ0 ρ1. elim : a b/h. + - move => a0 a1 b0 b1 ha iha hb ihb ρ0 ρ1 hρ /=. eapply AppAbs' with (a1 := subst_PTm (up_PTm_PTm ρ1) a1); eauto. by asimpl. - hauto l:on use:renaming inv:option. + hauto l:on use:renaming inv:nat. - hauto lq:on rew:off ctrs:R. - - hauto l:on inv:option use:renaming ctrs:R. + - hauto l:on inv:nat use:renaming ctrs:R. - hauto lq:on use:ProjPair'. - - move => n a0 a1 ha iha m ρ0 ρ1 hρ /=. + - move => a0 a1 ha iha ρ0 ρ1 hρ /=. apply : AppEta'; eauto. by asimpl. - hauto lq:on ctrs:R. - sfirstorder. - - hauto l:on inv:option ctrs:R use:renaming. + - hauto l:on inv:nat ctrs:R use:renaming. - hauto q:on ctrs:R. - qauto l:on ctrs:R. - qauto l:on ctrs:R. @@ -134,16 +134,16 @@ Module Par. - qauto l:on ctrs:R. Qed. - Lemma substing n m (a b : PTm n) (ρ : fin n -> PTm m) : + Lemma substing (a b : PTm) (ρ : nat -> PTm) : R a b -> R (subst_PTm ρ a) (subst_PTm ρ b). Proof. hauto l:on use:morphing, refl. Qed. - Lemma antirenaming n m (a : PTm n) (b : PTm m) (ξ : fin n -> fin m) : + Lemma antirenaming (a : PTm) (b : PTm) (ξ : nat -> nat) : R (ren_PTm ξ a) b -> exists b0, R a b0 /\ ren_PTm ξ b0 = b. Proof. move E : (ren_PTm ξ a) => u h. - move : n ξ a E. elim : m u b/h. - - move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//=. + move : ξ a E. elim : u b/h. + - move => a0 a1 b0 b1 ha iha hb ihb ξ []//=. move => c c0 [+ ?]. subst. case : c => //=. move => c [?]. subst. @@ -153,7 +153,7 @@ Module Par. eexists. split. apply AppAbs; eauto. by asimpl. - - move => n a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc m ξ []//=. + - move => a0 a1 b0 b1 c0 c1 ha iha hb ihb hc ihc ξ []//=. move => []//= t t0 t1 [*]. subst. spec_refl. move : iha => [? [*]]. @@ -162,43 +162,43 @@ Module Par. eexists. split. apply AppPair; hauto. subst. by asimpl. - - move => n p a0 a1 ha iha m ξ []//= p0 []//= t [*]. subst. + - move => p a0 a1 ha iha ξ []//= p0 []//= t [*]. subst. spec_refl. move : iha => [b0 [? ?]]. subst. eexists. split. apply ProjAbs; eauto. by asimpl. - - move => n p a0 a1 b0 b1 ha iha hb ihb m ξ []//= p0 []//= t t0[*]. + - move => p a0 a1 b0 b1 ha iha hb ihb ξ []//= p0 []//= t t0[*]. subst. spec_refl. move : iha => [b0 [? ?]]. move : ihb => [c0 [? ?]]. subst. eexists. split. by eauto using ProjPair. hauto q:on. - - move => n a0 a1 ha iha m ξ a ?. subst. + - move => a0 a1 ha iha ξ a ?. subst. spec_refl. move : iha => [a0 [? ?]]. subst. eexists. split. apply AppEta; eauto. by asimpl. - - move => n a0 a1 ha iha m ξ a ?. subst. + - move => a0 a1 ha iha ξ a ?. subst. spec_refl. move : iha => [b0 [? ?]]. subst. eexists. split. apply PairEta; eauto. by asimpl. - - move => n i m ξ []//=. + - move => i ξ []//=. hauto l:on. - - move => n a0 a1 ha iha m ξ []//= t [*]. subst. + - move => a0 a1 ha iha ξ []//= t [*]. subst. spec_refl. move :iha => [b0 [? ?]]. subst. eexists. split. by apply AbsCong; eauto. done. - - move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//= t t0 [*]. subst. + - move => a0 a1 b0 b1 ha iha hb ihb ξ []//= t t0 [*]. subst. spec_refl. move : iha => [b0 [? ?]]. subst. move : ihb => [c0 [? ?]]. subst. eexists. split. by apply AppCong; eauto. done. - - move => n a0 a1 b0 b1 ha iha hb ihb m ξ []//= t t0[*]. subst. + - move => a0 a1 b0 b1 ha iha hb ihb ξ []//= t t0[*]. subst. spec_refl. move : iha => [b0 [? ?]]. subst. move : ihb => [c0 [? ?]]. subst. eexists. split=>/=. by apply PairCong; eauto. done. - - move => n p a0 a1 ha iha m ξ []//= p0 t [*]. subst. + - move => p a0 a1 ha iha ξ []//= p0 t [*]. subst. spec_refl. move : iha => [b0 [? ?]]. subst. eexists. split. by apply ProjCong; eauto. @@ -359,7 +359,7 @@ Module RPar. R a b -> (forall i, R (ρ0 i) (ρ1 i)) -> (forall i, R ((scons a ρ0) i) ((scons b ρ1) i)). - Proof. hauto q:on inv:option. Qed. + Proof. hauto q:on inv:nat. Qed. Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) : (forall i, R (ρ0 i) (ρ1 i)) -> @@ -399,7 +399,7 @@ Module RPar. R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons d VarPTm) b). Proof. move => h0 h1. apply morphing => //=. - qauto l:on ctrs:R inv:option. + qauto l:on ctrs:R inv:nat. Qed. Lemma var_or_const_imp {n} (a b : PTm n) : @@ -595,7 +595,7 @@ Module RPar'. R a b -> (forall i, R (ρ0 i) (ρ1 i)) -> (forall i, R ((scons a ρ0) i) ((scons b ρ1) i)). - Proof. hauto q:on inv:option. Qed. + Proof. hauto q:on inv:nat. Qed. Lemma morphing_up n m (ρ0 ρ1 : fin n -> PTm m) : (forall i, R (ρ0 i) (ρ1 i)) -> @@ -633,7 +633,7 @@ Module RPar'. R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons d VarPTm) b). Proof. move => h0 h1. apply morphing => //=. - qauto l:on ctrs:R inv:option. + qauto l:on ctrs:R inv:nat. Qed. Lemma var_or_const_imp {n} (a b : PTm n) : @@ -786,7 +786,7 @@ Module ERed. move => h. move : m ρ. elim : n a b / h => n. move => a m ρ /=. apply : AppEta'; eauto. by asimpl. - all : hauto ctrs:R inv:option use:renaming. + all : hauto ctrs:R inv:nat use:renaming. Qed. End ERed. @@ -892,11 +892,11 @@ Module EPar. apply : AppEta'; eauto. by asimpl. - hauto lq:on ctrs:R. - hauto lq:on ctrs:R. - - hauto l:on ctrs:R use:renaming inv:option. + - hauto l:on ctrs:R use:renaming inv:nat. - hauto q:on ctrs:R. - hauto q:on ctrs:R. - hauto q:on ctrs:R. - - hauto l:on ctrs:R use:renaming inv:option. + - hauto l:on ctrs:R use:renaming inv:nat. - hauto lq:on ctrs:R. - hauto lq:on ctrs:R. Qed. @@ -907,7 +907,7 @@ Module EPar. R (subst_PTm (scons b0 VarPTm) a0) (subst_PTm (scons b1 VarPTm) a1). Proof. move => h0 h1. apply morphing => //. - hauto lq:on ctrs:R inv:option. + hauto lq:on ctrs:R inv:nat. Qed. End EPar. @@ -1018,7 +1018,7 @@ Module RPars. Lemma substing n (a b : PTm (S n)) c : rtc RPar.R a b -> rtc RPar.R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons c VarPTm) b). - Proof. hauto lq:on use:morphing inv:option. Qed. + Proof. hauto lq:on use:morphing inv:nat. Qed. Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) : (forall i, var_or_const (ρ i)) -> @@ -1099,7 +1099,7 @@ Module RPars'. Lemma substing n (a b : PTm (S n)) c : rtc RPar'.R a b -> rtc RPar'.R (subst_PTm (scons c VarPTm) a) (subst_PTm (scons c VarPTm) b). - Proof. hauto lq:on use:morphing inv:option. Qed. + Proof. hauto lq:on use:morphing inv:nat. Qed. Lemma antirenaming n m (a : PTm n) (b : PTm m) (ρ : fin n -> PTm m) : (forall i, var_or_const (ρ i)) -> @@ -2328,7 +2328,7 @@ Proof. have : wn (subst_PTm (scons (PBot) VarPTm) a3) by sfirstorder. move => h. apply wn_abs. move : h. apply wn_antirenaming. - hauto lq:on rew:off inv:option. + hauto lq:on rew:off inv:nat. + hauto q:on inv:RPar'.R ctrs:rtc b:on. Qed. diff --git a/theories/typing.v b/theories/typing.v new file mode 100644 index 0000000..d41facd --- /dev/null +++ b/theories/typing.v @@ -0,0 +1,251 @@ +Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax. + +Reserved Notation "Γ ⊢ a ∈ A" (at level 70). +Reserved Notation "Γ ⊢ a ≡ b ∈ A" (at level 70). +Reserved Notation "Γ ⊢ A ≲ B" (at level 70). +Reserved Notation "⊢ Γ" (at level 70). +Inductive Wt : list PTm -> PTm -> PTm -> Prop := +| T_Var i Γ A : + ⊢ Γ -> + lookup i Γ A -> + Γ ⊢ VarPTm i ∈ A + +| T_Bind Γ i p (A : PTm) (B : PTm) : + Γ ⊢ A ∈ PUniv i -> + cons A Γ ⊢ B ∈ PUniv i -> + Γ ⊢ PBind p A B ∈ PUniv i + +| T_Abs Γ (a : PTm) A B i : + Γ ⊢ PBind PPi A B ∈ (PUniv i) -> + (cons A Γ) ⊢ a ∈ B -> + Γ ⊢ PAbs a ∈ PBind PPi A B + +| T_App Γ (b a : PTm) A B : + Γ ⊢ b ∈ PBind PPi A B -> + Γ ⊢ a ∈ A -> + Γ ⊢ PApp b a ∈ subst_PTm (scons a VarPTm) B + +| T_Pair Γ (a b : PTm) A B i : + Γ ⊢ PBind PSig A B ∈ (PUniv i) -> + Γ ⊢ a ∈ A -> + Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B -> + Γ ⊢ PPair a b ∈ PBind PSig A B + +| T_Proj1 Γ (a : PTm) A B : + Γ ⊢ a ∈ PBind PSig A B -> + Γ ⊢ PProj PL a ∈ A + +| T_Proj2 Γ (a : PTm) A B : + Γ ⊢ a ∈ PBind PSig A B -> + Γ ⊢ PProj PR a ∈ subst_PTm (scons (PProj PL a) VarPTm) B + +| T_Univ Γ i : + ⊢ Γ -> + Γ ⊢ PUniv i ∈ PUniv (S i) + +| T_Nat Γ i : + ⊢ Γ -> + Γ ⊢ PNat ∈ PUniv i + +| T_Zero Γ : + ⊢ Γ -> + Γ ⊢ PZero ∈ PNat + +| T_Suc Γ (a : PTm) : + Γ ⊢ a ∈ PNat -> + Γ ⊢ PSuc a ∈ PNat + +| T_Ind Γ P (a : PTm) b c i : + cons PNat Γ ⊢ P ∈ PUniv i -> + Γ ⊢ a ∈ PNat -> + Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P -> + (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) -> + Γ ⊢ PInd P a b c ∈ subst_PTm (scons a VarPTm) P + +| T_Conv Γ (a : PTm) A B : + Γ ⊢ a ∈ A -> + Γ ⊢ A ≲ B -> + Γ ⊢ a ∈ B + +with Eq : list PTm -> PTm -> PTm -> PTm -> Prop := +(* Structural *) +| E_Refl Γ (a : PTm ) A : + Γ ⊢ a ∈ A -> + Γ ⊢ a ≡ a ∈ A + +| E_Symmetric Γ (a b : PTm) A : + Γ ⊢ a ≡ b ∈ A -> + Γ ⊢ b ≡ a ∈ A + +| E_Transitive Γ (a b c : PTm) A : + Γ ⊢ a ≡ b ∈ A -> + Γ ⊢ b ≡ c ∈ A -> + Γ ⊢ a ≡ c ∈ A + +(* Congruence *) +| E_Bind Γ i p (A0 A1 : PTm) B0 B1 : + Γ ⊢ A0 ∈ PUniv i -> + Γ ⊢ A0 ≡ A1 ∈ PUniv i -> + (cons A0 Γ) ⊢ B0 ≡ B1 ∈ PUniv i -> + Γ ⊢ PBind p A0 B0 ≡ PBind p A1 B1 ∈ PUniv i + +| E_Abs Γ (a b : PTm) A B i : + Γ ⊢ PBind PPi A B ∈ (PUniv i) -> + (cons A Γ) ⊢ a ≡ b ∈ B -> + Γ ⊢ PAbs a ≡ PAbs b ∈ PBind PPi A B + +| E_App Γ i (b0 b1 a0 a1 : PTm) A B : + Γ ⊢ PBind PPi A B ∈ (PUniv i) -> + Γ ⊢ b0 ≡ b1 ∈ PBind PPi A B -> + Γ ⊢ a0 ≡ a1 ∈ A -> + Γ ⊢ PApp b0 a0 ≡ PApp b1 a1 ∈ subst_PTm (scons a0 VarPTm) B + +| E_Pair Γ (a0 a1 b0 b1 : PTm) A B i : + Γ ⊢ PBind PSig A B ∈ (PUniv i) -> + Γ ⊢ a0 ≡ a1 ∈ A -> + Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons a0 VarPTm) B -> + Γ ⊢ PPair a0 b0 ≡ PPair a1 b1 ∈ PBind PSig A B + +| E_Proj1 Γ (a b : PTm) A B : + Γ ⊢ a ≡ b ∈ PBind PSig A B -> + Γ ⊢ PProj PL a ≡ PProj PL b ∈ A + +| E_Proj2 Γ i (a b : PTm) A B : + Γ ⊢ PBind PSig A B ∈ (PUniv i) -> + Γ ⊢ a ≡ b ∈ PBind PSig A B -> + Γ ⊢ PProj PR a ≡ PProj PR b ∈ subst_PTm (scons (PProj PL a) VarPTm) B + +| E_IndCong Γ P0 P1 (a0 a1 : PTm) b0 b1 c0 c1 i : + (cons PNat Γ) ⊢ P0 ∈ PUniv i -> + (cons PNat Γ) ⊢ P0 ≡ P1 ∈ PUniv i -> + Γ ⊢ a0 ≡ a1 ∈ PNat -> + Γ ⊢ b0 ≡ b1 ∈ subst_PTm (scons PZero VarPTm) P0 -> + (cons P0 ((cons PNat Γ))) ⊢ c0 ≡ c1 ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P0) -> + Γ ⊢ PInd P0 a0 b0 c0 ≡ PInd P1 a1 b1 c1 ∈ subst_PTm (scons a0 VarPTm) P0 + +| E_SucCong Γ (a b : PTm) : + Γ ⊢ a ≡ b ∈ PNat -> + Γ ⊢ PSuc a ≡ PSuc b ∈ PNat + +| E_Conv Γ (a b : PTm) A B : + Γ ⊢ a ≡ b ∈ A -> + Γ ⊢ A ≲ B -> + Γ ⊢ a ≡ b ∈ B + +(* Beta *) +| E_AppAbs Γ (a : PTm) b A B i: + Γ ⊢ PBind PPi A B ∈ PUniv i -> + Γ ⊢ b ∈ A -> + (cons A Γ) ⊢ a ∈ B -> + Γ ⊢ PApp (PAbs a) b ≡ subst_PTm (scons b VarPTm) a ∈ subst_PTm (scons b VarPTm ) B + +| E_ProjPair1 Γ (a b : PTm) A B i : + Γ ⊢ PBind PSig A B ∈ (PUniv i) -> + Γ ⊢ a ∈ A -> + Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B -> + Γ ⊢ PProj PL (PPair a b) ≡ a ∈ A + +| E_ProjPair2 Γ (a b : PTm) A B i : + Γ ⊢ PBind PSig A B ∈ (PUniv i) -> + Γ ⊢ a ∈ A -> + Γ ⊢ b ∈ subst_PTm (scons a VarPTm) B -> + Γ ⊢ PProj PR (PPair a b) ≡ b ∈ subst_PTm (scons a VarPTm) B + +| E_IndZero Γ P i (b : PTm) c : + (cons PNat Γ) ⊢ P ∈ PUniv i -> + Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P -> + (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) -> + Γ ⊢ PInd P PZero b c ≡ b ∈ subst_PTm (scons PZero VarPTm) P + +| E_IndSuc Γ P (a : PTm) b c i : + (cons PNat Γ) ⊢ P ∈ PUniv i -> + Γ ⊢ a ∈ PNat -> + Γ ⊢ b ∈ subst_PTm (scons PZero VarPTm) P -> + (cons P (cons PNat Γ)) ⊢ c ∈ ren_PTm shift (subst_PTm (scons (PSuc (VarPTm var_zero)) (funcomp VarPTm shift) ) P) -> + Γ ⊢ PInd P (PSuc a) b c ≡ (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) ∈ subst_PTm (scons (PSuc a) VarPTm) P + +(* Eta *) +| E_AppEta Γ (b : PTm) A B i : + Γ ⊢ PBind PPi A B ∈ (PUniv i) -> + Γ ⊢ b ∈ PBind PPi A B -> + Γ ⊢ PAbs (PApp (ren_PTm shift b) (VarPTm var_zero)) ≡ b ∈ PBind PPi A B + +| E_PairEta Γ (a : PTm ) A B i : + Γ ⊢ PBind PSig A B ∈ (PUniv i) -> + Γ ⊢ a ∈ PBind PSig A B -> + Γ ⊢ a ≡ PPair (PProj PL a) (PProj PR a) ∈ PBind PSig A B + +with LEq : list PTm -> PTm -> PTm -> Prop := +(* Structural *) +| Su_Transitive Γ (A B C : PTm) : + Γ ⊢ A ≲ B -> + Γ ⊢ B ≲ C -> + Γ ⊢ A ≲ C + +(* Congruence *) +| Su_Univ Γ i j : + ⊢ Γ -> + i <= j -> + Γ ⊢ PUniv i ≲ PUniv j + +| Su_Pi Γ (A0 A1 : PTm) B0 B1 i : + Γ ⊢ A0 ∈ PUniv i -> + Γ ⊢ A1 ≲ A0 -> + (cons A0 Γ) ⊢ B0 ≲ B1 -> + Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 + +| Su_Sig Γ (A0 A1 : PTm) B0 B1 i : + Γ ⊢ A1 ∈ PUniv i -> + Γ ⊢ A0 ≲ A1 -> + (cons A1 Γ) ⊢ B0 ≲ B1 -> + Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 + +(* Injecting from equalities *) +| Su_Eq Γ (A : PTm) B i : + Γ ⊢ A ≡ B ∈ PUniv i -> + Γ ⊢ A ≲ B + +(* Projection axioms *) +| Su_Pi_Proj1 Γ (A0 A1 : PTm) B0 B1 : + Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 -> + Γ ⊢ A1 ≲ A0 + +| Su_Sig_Proj1 Γ (A0 A1 : PTm) B0 B1 : + Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 -> + Γ ⊢ A0 ≲ A1 + +| Su_Pi_Proj2 Γ (a0 a1 A0 A1 : PTm ) B0 B1 : + Γ ⊢ PBind PPi A0 B0 ≲ PBind PPi A1 B1 -> + Γ ⊢ a0 ≡ a1 ∈ A1 -> + Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≲ subst_PTm (scons a1 VarPTm) B1 + +| Su_Sig_Proj2 Γ (a0 a1 A0 A1 : PTm) B0 B1 : + Γ ⊢ PBind PSig A0 B0 ≲ PBind PSig A1 B1 -> + Γ ⊢ a0 ≡ a1 ∈ A0 -> + Γ ⊢ subst_PTm (scons a0 VarPTm) B0 ≲ subst_PTm (scons a1 VarPTm) B1 + +with Wff : list PTm -> Prop := +| Wff_Nil : + ⊢ nil +| Wff_Cons Γ (A : PTm) i : + ⊢ Γ -> + Γ ⊢ A ∈ PUniv i -> + (* -------------------------------- *) + ⊢ (cons A Γ) + +where +"Γ ⊢ a ∈ A" := (Wt Γ a A) and "⊢ Γ" := (Wff Γ) and "Γ ⊢ a ≡ b ∈ A" := (Eq Γ a b A) and "Γ ⊢ A ≲ B" := (LEq Γ A B). + +Scheme wf_ind := Induction for Wff Sort Prop + with wt_ind := Induction for Wt Sort Prop + with eq_ind := Induction for Eq Sort Prop + with le_ind := Induction for LEq Sort Prop. + +Combined Scheme wt_mutual from wf_ind, wt_ind, eq_ind, le_ind. + +(* Lemma lem : *) +(* (forall n (Γ : fin n -> PTm n), ⊢ Γ -> ...) /\ *) +(* (forall n Γ (a A : PTm n), Γ ⊢ a ∈ A -> ...) /\ *) +(* (forall n Γ (a b A : PTm n), Γ ⊢ a ≡ b ∈ A -> ...) /\ *) +(* (forall n Γ (A B : PTm n), Γ ⊢ A ≲ B -> ...). *) +(* Proof. apply wt_mutual. ... *)