diff --git a/Makefile b/Makefile index ef5b76f..972974b 100644 --- a/Makefile +++ b/Makefile @@ -16,12 +16,12 @@ 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 + 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 5d04c05..97ebfb1 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,221 +33,177 @@ 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 - | PBind : BTag -> PTm n_PTm -> PTm (S n_PTm) -> PTm n_PTm - | PUniv : nat -> PTm n_PTm - | PBot : PTm n_PTm - | PNat : PTm n_PTm - | PZero : PTm n_PTm - | PSuc : PTm n_PTm -> PTm n_PTm - | PInd : - PTm (S n_PTm) -> - PTm n_PTm -> PTm n_PTm -> PTm (S (S n_PTm)) -> PTm n_PTm. +Inductive PTm : Type := + | VarPTm : nat -> PTm + | PAbs : PTm -> PTm + | PApp : PTm -> PTm -> PTm + | PPair : PTm -> PTm -> PTm + | PProj : PTag -> PTm -> PTm + | PBind : BTag -> PTm -> PTm -> PTm + | PUniv : nat -> PTm + | PBot : PTm + | PNat : PTm + | PZero : PTm + | PSuc : PTm -> PTm + | PInd : PTm -> PTm -> PTm -> PTm -> 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_PBind {m_PTm : nat} {s0 : BTag} {s1 : PTm m_PTm} - {s2 : PTm (S m_PTm)} {t0 : BTag} {t1 : PTm m_PTm} {t2 : PTm (S m_PTm)} - (H0 : s0 = t0) (H1 : s1 = t1) (H2 : s2 = t2) : - PBind m_PTm s0 s1 s2 = PBind m_PTm t0 t1 t2. +Lemma congr_PBind {s0 : BTag} {s1 : PTm} {s2 : PTm} {t0 : BTag} {t1 : PTm} + {t2 : PTm} (H0 : s0 = t0) (H1 : s1 = t1) (H2 : s2 = t2) : + PBind s0 s1 s2 = PBind t0 t1 t2. Proof. exact (eq_trans - (eq_trans (eq_trans eq_refl (ap (fun x => PBind m_PTm x s1 s2) H0)) - (ap (fun x => PBind m_PTm t0 x s2) H1)) - (ap (fun x => PBind m_PTm t0 t1 x) H2)). + (eq_trans (eq_trans eq_refl (ap (fun x => PBind x s1 s2) H0)) + (ap (fun x => PBind t0 x s2) H1)) + (ap (fun x => PBind t0 t1 x) H2)). 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 congr_PNat {m_PTm : nat} : PNat m_PTm = PNat m_PTm. +Lemma congr_PNat : PNat = PNat. Proof. exact (eq_refl). Qed. -Lemma congr_PZero {m_PTm : nat} : PZero m_PTm = PZero m_PTm. +Lemma congr_PZero : PZero = PZero. Proof. exact (eq_refl). Qed. -Lemma congr_PSuc {m_PTm : nat} {s0 : PTm m_PTm} {t0 : PTm m_PTm} - (H0 : s0 = t0) : PSuc m_PTm s0 = PSuc m_PTm t0. +Lemma congr_PSuc {s0 : PTm} {t0 : PTm} (H0 : s0 = t0) : PSuc s0 = PSuc t0. Proof. -exact (eq_trans eq_refl (ap (fun x => PSuc m_PTm x) H0)). +exact (eq_trans eq_refl (ap (fun x => PSuc x) H0)). Qed. -Lemma congr_PInd {m_PTm : nat} {s0 : PTm (S m_PTm)} {s1 : PTm m_PTm} - {s2 : PTm m_PTm} {s3 : PTm (S (S m_PTm))} {t0 : PTm (S m_PTm)} - {t1 : PTm m_PTm} {t2 : PTm m_PTm} {t3 : PTm (S (S m_PTm))} (H0 : s0 = t0) - (H1 : s1 = t1) (H2 : s2 = t2) (H3 : s3 = t3) : - PInd m_PTm s0 s1 s2 s3 = PInd m_PTm t0 t1 t2 t3. +Lemma congr_PInd {s0 : PTm} {s1 : PTm} {s2 : PTm} {s3 : PTm} {t0 : PTm} + {t1 : PTm} {t2 : PTm} {t3 : PTm} (H0 : s0 = t0) (H1 : s1 = t1) + (H2 : s2 = t2) (H3 : s3 = t3) : PInd s0 s1 s2 s3 = PInd t0 t1 t2 t3. Proof. exact (eq_trans (eq_trans - (eq_trans - (eq_trans eq_refl (ap (fun x => PInd m_PTm x s1 s2 s3) H0)) - (ap (fun x => PInd m_PTm t0 x s2 s3) H1)) - (ap (fun x => PInd m_PTm t0 t1 x s3) H2)) - (ap (fun x => PInd m_PTm t0 t1 t2 x) H3)). + (eq_trans (eq_trans eq_refl (ap (fun x => PInd x s1 s2 s3) H0)) + (ap (fun x => PInd t0 x s2 s3) H1)) + (ap (fun x => PInd t0 t1 x s3) H2)) + (ap (fun x => PInd t0 t1 t2 x) H3)). 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) - | PBind _ s0 s1 s2 => - PBind n_PTm s0 (ren_PTm xi_PTm s1) (ren_PTm (upRen_PTm_PTm xi_PTm) s2) - | PUniv _ s0 => PUniv n_PTm s0 - | PBot _ => PBot n_PTm - | PNat _ => PNat n_PTm - | PZero _ => PZero n_PTm - | PSuc _ s0 => PSuc n_PTm (ren_PTm xi_PTm s0) - | PInd _ s0 s1 s2 s3 => - PInd n_PTm (ren_PTm (upRen_PTm_PTm xi_PTm) s0) (ren_PTm xi_PTm s1) + | 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) + | PBind s0 s1 s2 => + PBind s0 (ren_PTm xi_PTm s1) (ren_PTm (upRen_PTm_PTm xi_PTm) s2) + | PUniv s0 => PUniv s0 + | PBot => PBot + | PNat => PNat + | PZero => PZero + | PSuc s0 => PSuc (ren_PTm xi_PTm s0) + | PInd s0 s1 s2 s3 => + PInd (ren_PTm (upRen_PTm_PTm xi_PTm) s0) (ren_PTm xi_PTm s1) (ren_PTm xi_PTm s2) (ren_PTm (upRen_PTm_PTm (upRen_PTm_PTm xi_PTm)) s3) 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) - | PBind _ s0 s1 s2 => - PBind n_PTm s0 (subst_PTm sigma_PTm s1) - (subst_PTm (up_PTm_PTm sigma_PTm) s2) - | PUniv _ s0 => PUniv n_PTm s0 - | PBot _ => PBot n_PTm - | PNat _ => PNat n_PTm - | PZero _ => PZero n_PTm - | PSuc _ s0 => PSuc n_PTm (subst_PTm sigma_PTm s0) - | PInd _ s0 s1 s2 s3 => - PInd n_PTm (subst_PTm (up_PTm_PTm sigma_PTm) s0) - (subst_PTm sigma_PTm s1) (subst_PTm sigma_PTm s2) + | 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) + | PBind s0 s1 s2 => + PBind s0 (subst_PTm sigma_PTm s1) (subst_PTm (up_PTm_PTm sigma_PTm) s2) + | PUniv s0 => PUniv s0 + | PBot => PBot + | PNat => PNat + | PZero => PZero + | PSuc s0 => PSuc (subst_PTm sigma_PTm s0) + | PInd s0 s1 s2 s3 => + PInd (subst_PTm (up_PTm_PTm sigma_PTm) s0) (subst_PTm sigma_PTm s1) + (subst_PTm sigma_PTm s2) (subst_PTm (up_PTm_PTm (up_PTm_PTm sigma_PTm)) s3) 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) - | PBind _ s0 s1 s2 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1) + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1) (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => congr_PSuc (idSubst_PTm sigma_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (idSubst_PTm sigma_PTm Eq_PTm s0) + | PInd s0 s1 s2 s3 => congr_PInd (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s0) (idSubst_PTm sigma_PTm Eq_PTm s1) (idSubst_PTm sigma_PTm Eq_PTm s2) @@ -255,54 +211,43 @@ Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm) (upId_PTm_PTm _ (upId_PTm_PTm _ Eq_PTm)) s3) 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) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) (upExtRen_PTm_PTm _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => congr_PSuc (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0) + | PInd s0 s1 s2 s3 => congr_PInd (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) (upExtRen_PTm_PTm _ _ Eq_PTm) s0) @@ -313,55 +258,44 @@ ren_PTm xi_PTm s = ren_PTm zeta_PTm s := (upExtRen_PTm_PTm _ _ (upExtRen_PTm_PTm _ _ Eq_PTm)) s3) 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) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) (upExt_PTm_PTm _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => congr_PSuc (ext_PTm sigma_PTm tau_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (ext_PTm sigma_PTm tau_PTm Eq_PTm s0) + | PInd s0 s1 s2 s3 => congr_PInd (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) (upExt_PTm_PTm _ _ Eq_PTm) s0) @@ -372,57 +306,44 @@ subst_PTm sigma_PTm s = subst_PTm tau_PTm s := (upExt_PTm_PTm _ _ (upExt_PTm_PTm _ _ Eq_PTm)) s3) 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) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => - congr_PSuc (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0) + | PInd s0 s1 s2 s3 => congr_PInd (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s0) @@ -434,66 +355,49 @@ Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} (up_ren_ren _ _ _ (up_ren_ren _ _ _ Eq_PTm)) s3) 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) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) (compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm) (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PInd s0 s1 s2 s3 => congr_PInd (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) @@ -506,9 +410,8 @@ Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} s3) 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 = @@ -516,76 +419,51 @@ 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) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) (compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm) (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PInd s0 s1 s2 s3 => congr_PInd (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) @@ -598,9 +476,8 @@ ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := s3) 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 = @@ -608,78 +485,52 @@ 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) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) (compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PInd s0 s1 s2 s3 => congr_PInd (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) @@ -692,126 +543,102 @@ subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := (up_subst_subst_PTm_PTm _ _ _ Eq_PTm)) s3) 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) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm) (rinstInst_up_PTm_PTm _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => congr_PSuc (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0) + | PInd s0 s1 s2 s3 => congr_PInd (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm) (rinstInst_up_PTm_PTm _ _ Eq_PTm) s0) @@ -822,71 +649,61 @@ Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat} (rinstInst_up_PTm_PTm _ _ (rinstInst_up_PTm_PTm _ _ Eq_PTm)) s3) 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. @@ -894,18 +711,14 @@ Qed. Class Up_PTm X Y := up_PTm : X -> Y. -#[global] -Instance Subst_PTm {m_PTm n_PTm : nat}: (Subst1 _ _ _) := - (@subst_PTm m_PTm n_PTm). +#[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_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_PTm ]" := (subst_PTm sigma_PTm) ( at level 1, left associativity, only printing) : fscope. @@ -932,9 +745,9 @@ Notation "x '__PTm'" := (VarPTm x) ( at level 5, format "x __PTm") : subst_scope. #[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') @@ -942,17 +755,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') @@ -960,9 +772,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. @@ -994,9 +806,7 @@ Ltac asimpl' := repeat (first | progress setoid_rewrite rinstId'_PTm | progress setoid_rewrite instId'_PTm_pointwise | progress setoid_rewrite instId'_PTm - | progress - unfold up_list_PTm_PTm, up_PTm_PTm, upRen_list_PTm_PTm, - upRen_PTm_PTm, up_ren + | progress unfold up_PTm_PTm, upRen_PTm_PTm, up_ren | progress cbn[subst_PTm ren_PTm] | progress fsimpl ]). @@ -1021,36 +831,11 @@ End Core. Module Extra. -Import -Core. +Import Core. -Arguments VarPTm {n_PTm}. +#[global] Hint Opaque subst_PTm: rewrite. -Arguments PInd {n_PTm}. - -Arguments PSuc {n_PTm}. - -Arguments PZero {n_PTm}. - -Arguments PNat {n_PTm}. - -Arguments PBot {n_PTm}. - -Arguments PUniv {n_PTm}. - -Arguments PBind {n_PTm}. - -Arguments PProj {n_PTm}. - -Arguments PPair {n_PTm}. - -Arguments PApp {n_PTm}. - -Arguments PAbs {n_PTm}. - -#[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/common.v b/theories/common.v index 282038d..51fad7b 100644 --- a/theories/common.v +++ b/theories/common.v @@ -4,6 +4,7 @@ Import Ltac2.Notations. Import Ltac2.Control. From Hammer Require Import Tactics. + Definition renaming_ok {n m} (Γ : fin n -> PTm n) (Δ : fin m -> PTm m) (ξ : fin m -> fin n) := forall (i : fin m), ren_PTm ξ (Δ i) = Γ (ξ i). diff --git a/theories/executable.v b/theories/executable.v index f773fa6..f7d6707 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -1,58 +1,221 @@ From Equations Require Import Equations. -Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax - common typing preservation admissible fp_red structural soundness. -Require Import algorithmic. -From stdpp Require Import relations (rtc(..), nsteps(..)). -Require Import ssreflect ssrbool. +Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax. +Derive NoConfusion for option sig nat PTag BTag PTm. +Derive EqDec for BTag PTag PTm. +Import Logic (inspect). +Require Import Cdcl.Itauto. -Inductive algo_dom {n} : PTm n -> PTm n -> Prop := +Require Import ssreflect ssrbool. +From Hammer Require Import Tactics. + +Definition ishf (a : PTm) := + match a with + | PPair _ _ => true + | PAbs _ => true + | PUniv _ => true + | PBind _ _ _ => true + | PNat => true + | PSuc _ => true + | PZero => true + | _ => false + end. + +Fixpoint ishne (a : PTm) := + match a with + | VarPTm _ => true + | PApp a _ => ishne a + | PProj _ a => ishne a + | PBot => true + | PInd _ n _ _ => ishne n + | _ => false + end. + +Module HRed. + Inductive R : PTm -> PTm -> Prop := + (****************** Beta ***********************) + | AppAbs a b : + R (PApp (PAbs a) b) (subst_PTm (scons b VarPTm) a) + + | ProjPair p a b : + R (PProj p (PPair a b)) (if p is PL then a else b) + + | IndZero P b c : + R (PInd P PZero b c) b + + | IndSuc P a b c : + R (PInd P (PSuc a) b c) (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) + + (*************** Congruence ********************) + | AppCong a0 a1 b : + R a0 a1 -> + R (PApp a0 b) (PApp a1 b) + | ProjCong p a0 a1 : + R a0 a1 -> + R (PProj p a0) (PProj p a1) + | IndCong P a0 a1 b c : + R a0 a1 -> + R (PInd P a0 b c) (PInd P a1 b c). + + Definition nf a := forall b, ~ R a b. +End HRed. + + +Definition isbind (a : PTm) := if a is PBind _ _ _ then true else false. + +Definition isuniv (a : PTm) := if a is PUniv _ then true else false. + +Definition ispair (a : PTm) := + match a with + | PPair _ _ => true + | _ => false + end. + +Definition isnat (a : PTm) := if a is PNat then true else false. + +Definition iszero (a : PTm) := if a is PZero then true else false. + +Definition issuc (a : PTm) := if a is PSuc _ then true else false. + +Definition isabs (a : PTm) := + match a with + | PAbs _ => true + | _ => false + end. + +Definition tm_nonconf (a b : PTm) : bool := + match a, b with + | PAbs _, _ => ishne b || isabs b + | _, PAbs _ => ishne a + | VarPTm _, VarPTm _ => true + | PPair _ _, _ => ishne b || ispair b + | _, PPair _ _ => ishne a + | PZero, PZero => true + | PSuc _, PSuc _ => true + | PApp _ _, PApp _ _ => ishne a && ishne b + | PProj _ _, PProj _ _ => ishne a && ishne b + | PInd _ _ _ _, PInd _ _ _ _ => ishne a && ishne b + | PNat, PNat => true + | PUniv _, PUniv _ => true + | PBind _ _ _, PBind _ _ _ => true + | _,_=> false + end. + +Definition tm_conf (a b : PTm) := ~~ tm_nonconf a b. + +Inductive eq_view : PTm -> PTm -> Type := +| V_AbsAbs a b : + eq_view (PAbs a) (PAbs b) +| V_AbsNeu a b : + ~~ isabs b -> + eq_view (PAbs a) b +| V_NeuAbs a b : + ~~ isabs a -> + eq_view a (PAbs b) +| V_VarVar i j : + eq_view (VarPTm i) (VarPTm j) +| V_PairPair a0 b0 a1 b1 : + eq_view (PPair a0 b0) (PPair a1 b1) +| V_PairNeu a0 b0 u : + ~~ ispair u -> + eq_view (PPair a0 b0) u +| V_NeuPair u a1 b1 : + ~~ ispair u -> + eq_view u (PPair a1 b1) +| V_ZeroZero : + eq_view PZero PZero +| V_SucSuc a b : + eq_view (PSuc a) (PSuc b) +| V_AppApp u0 b0 u1 b1 : + eq_view (PApp u0 b0) (PApp u1 b1) +| V_ProjProj p0 u0 p1 u1 : + eq_view (PProj p0 u0) (PProj p1 u1) +| V_IndInd P0 u0 b0 c0 P1 u1 b1 c1 : + eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) +| V_NatNat : + eq_view PNat PNat +| V_BindBind p0 A0 B0 p1 A1 B1 : + eq_view (PBind p0 A0 B0) (PBind p1 A1 B1) +| V_UnivUniv i j : + eq_view (PUniv i) (PUniv j) +| V_Others a b : + eq_view a b. + +Equations tm_to_eq_view (a b : PTm) : eq_view a b := + tm_to_eq_view (PAbs a) (PAbs b) := V_AbsAbs a b; + tm_to_eq_view (PAbs a) b := V_AbsNeu a b _; + tm_to_eq_view a (PAbs b) := V_NeuAbs a b _; + tm_to_eq_view (VarPTm i) (VarPTm j) := V_VarVar i j; + tm_to_eq_view (PPair a0 b0) (PPair a1 b1) := V_PairPair a0 b0 a1 b1; + tm_to_eq_view (PPair a0 b0) u := V_PairNeu a0 b0 u _; + tm_to_eq_view u (PPair a1 b1) := V_NeuPair u a1 b1 _; + tm_to_eq_view PZero PZero := V_ZeroZero; + tm_to_eq_view (PSuc a) (PSuc b) := V_SucSuc a b; + tm_to_eq_view (PApp a0 b0) (PApp a1 b1) := V_AppApp a0 b0 a1 b1; + tm_to_eq_view (PProj p0 b0) (PProj p1 b1) := V_ProjProj p0 b0 p1 b1; + tm_to_eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) := V_IndInd P0 u0 b0 c0 P1 u1 b1 c1; + tm_to_eq_view PNat PNat := V_NatNat; + tm_to_eq_view (PUniv i) (PUniv j) := V_UnivUniv i j; + tm_to_eq_view (PBind p0 A0 B0) (PBind p1 A1 B1) := V_BindBind p0 A0 B0 p1 A1 B1; + tm_to_eq_view a b := V_Others a b. + +Inductive algo_dom : PTm -> PTm -> Prop := | A_AbsAbs a b : - algo_dom a b -> + algo_dom_r a b -> (* --------------------- *) algo_dom (PAbs a) (PAbs b) | A_AbsNeu a u : ishne u -> - algo_dom a (PApp (ren_PTm shift u) (VarPTm var_zero)) -> + algo_dom_r a (PApp (ren_PTm shift u) (VarPTm var_zero)) -> (* --------------------- *) algo_dom (PAbs a) u | A_NeuAbs a u : ishne u -> - algo_dom (PApp (ren_PTm shift u) (VarPTm var_zero)) a -> + algo_dom_r (PApp (ren_PTm shift u) (VarPTm var_zero)) a -> (* --------------------- *) algo_dom u (PAbs a) | A_PairPair a0 a1 b0 b1 : - algo_dom a0 a1 -> - algo_dom b0 b1 -> + algo_dom_r a0 a1 -> + algo_dom_r b0 b1 -> (* ---------------------------- *) algo_dom (PPair a0 b0) (PPair a1 b1) | A_PairNeu a0 a1 u : ishne u -> - algo_dom a0 (PProj PL u) -> - algo_dom a1 (PProj PR u) -> + algo_dom_r a0 (PProj PL u) -> + algo_dom_r a1 (PProj PR u) -> (* ----------------------- *) algo_dom (PPair a0 a1) u | A_NeuPair a0 a1 u : ishne u -> - algo_dom (PProj PL u) a0 -> - algo_dom (PProj PR u) a1 -> + algo_dom_r (PProj PL u) a0 -> + algo_dom_r (PProj PR u) a1 -> (* ----------------------- *) algo_dom u (PPair a0 a1) +| A_ZeroZero : + algo_dom PZero PZero + +| A_SucSuc a0 a1 : + algo_dom_r a0 a1 -> + algo_dom (PSuc a0) (PSuc a1) + | A_UnivCong i j : (* -------------------------- *) algo_dom (PUniv i) (PUniv j) | A_BindCong p0 p1 A0 A1 B0 B1 : - algo_dom A0 A1 -> - algo_dom B0 B1 -> + algo_dom_r A0 A1 -> + algo_dom_r B0 B1 -> (* ---------------------------- *) algo_dom (PBind p0 A0 B0) (PBind p1 A1 B1) +| A_NatCong : + algo_dom PNat PNat + | A_VarCong i j : (* -------------------------- *) algo_dom (VarPTm i) (VarPTm j) @@ -68,78 +231,199 @@ Inductive algo_dom {n} : PTm n -> PTm n -> Prop := ishne u0 -> ishne u1 -> algo_dom u0 u1 -> - algo_dom a0 a1 -> + algo_dom_r a0 a1 -> (* ------------------------- *) algo_dom (PApp u0 a0) (PApp u1 a1) +| A_IndCong P0 P1 u0 u1 b0 b1 c0 c1 : + ishne u0 -> + ishne u1 -> + algo_dom_r P0 P1 -> + algo_dom u0 u1 -> + algo_dom_r b0 b1 -> + algo_dom_r c0 c1 -> + algo_dom (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) + +with algo_dom_r : PTm -> PTm -> Prop := +| A_NfNf a b : + algo_dom a b -> + algo_dom_r a b + | A_HRedL a a' b : HRed.R a a' -> - algo_dom a' b -> + algo_dom_r a' b -> (* ----------------------- *) - algo_dom a b + algo_dom_r a b | A_HRedR a b b' : ishne a \/ ishf a -> HRed.R b b' -> - algo_dom a b' -> + algo_dom_r a b' -> (* ----------------------- *) - algo_dom a b. + algo_dom_r a b. - -Definition fin_eq {n} (i j : fin n) : bool. +Lemma algo_dom_hf_hne (a b : PTm) : + algo_dom a b -> + (ishf a \/ ishne a) /\ (ishf b \/ ishne b). Proof. - induction n. - - by exfalso. - - refine (match i , j with - | None, None => true - | Some i, Some j => IHn i j - | _, _ => false - end). -Defined. + induction 1 =>//=; hauto lq:on. +Qed. -Lemma fin_eq_dec {n} (i j : fin n) : - Bool.reflect (i = j) (fin_eq i j). +Lemma hf_no_hred (a b : PTm) : + ishf a -> + HRed.R a b -> + False. +Proof. hauto l:on inv:HRed.R. Qed. + +Lemma hne_no_hred (a b : PTm) : + ishne a -> + HRed.R a b -> + False. +Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed. + +Derive Signature for algo_dom algo_dom_r. + +Fixpoint hred (a : PTm) : option (PTm) := + match a with + | VarPTm i => None + | PAbs a => None + | PApp (PAbs a) b => Some (subst_PTm (scons b VarPTm) a) + | PApp a b => + match hred a with + | Some a => Some (PApp a b) + | None => None + end + | PPair a b => None + | PProj p (PPair a b) => if p is PL then Some a else Some b + | PProj p a => + match hred a with + | Some a => Some (PProj p a) + | None => None + end + | PUniv i => None + | PBind p A B => None + | PBot => None + | PNat => None + | PZero => None + | PSuc a => None + | PInd P PZero b c => Some b + | PInd P (PSuc a) b c => + Some (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) + | PInd P a b c => + match hred a with + | Some a => Some (PInd P a b c) + | None => None + end + end. + +Lemma hred_complete (a b : PTm) : + HRed.R a b -> hred a = Some b. Proof. - revert i j. induction n. - - destruct i. - - destruct i; destruct j. - + specialize (IHn f f0). - inversion IHn; subst. - simpl. rewrite -H. - apply ReflectT. - reflexivity. - simpl. rewrite -H. - apply ReflectF. - injection. tauto. - + by apply ReflectF. - + by apply ReflectF. - + by apply ReflectT. -Defined. + induction 1; hauto lq:on rew:off inv:HRed.R b:on. +Qed. +Lemma hred_sound (a b : PTm): + hred a = Some b -> HRed.R a b. +Proof. + elim : a b; hauto q:on dep:on ctrs:HRed.R. +Qed. -Equations check_equal {n} (a b : PTm n) (h : algo_dom a b) : +Lemma hred_deter (a b0 b1 : PTm) : + HRed.R a b0 -> HRed.R a b1 -> b0 = b1. +Proof. + move /hred_complete => + /hred_complete. congruence. +Qed. + +Ltac check_equal_triv := + intros;subst; + lazymatch goal with + (* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *) + | [h : algo_dom _ _ |- _] => try (inversion h; by subst) + | _ => idtac + end. + +Ltac solve_check_equal := + try solve [intros *; + match goal with + | [|- _ = _] => sauto + | _ => idtac + end]. + +Equations check_equal (a b : PTm) (h : algo_dom a b) : bool by struct h := - check_equal a b h with (@idP (ishne a || ishf a)) := { - | Bool.ReflectT _ _ => _ - | Bool.ReflectF _ _ => _ - }. + check_equal a b h with tm_to_eq_view a b := + check_equal _ _ h (V_VarVar i j) := nat_eqdec i j; + check_equal _ _ h (V_AbsAbs a b) := check_equal_r a b ltac:(check_equal_triv); + check_equal _ _ h (V_AbsNeu a b h') := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv); + check_equal _ _ h (V_NeuAbs a b _) := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv); + check_equal _ _ h (V_PairPair a0 b0 a1 b1) := + check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); + check_equal _ _ h (V_PairNeu a0 b0 u _) := + check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv); + check_equal _ _ h (V_NeuPair u a1 b1 _) := + check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv); + check_equal _ _ h V_NatNat := true; + check_equal _ _ h V_ZeroZero := true; + check_equal _ _ h (V_SucSuc a b) := check_equal_r a b ltac:(check_equal_triv); + check_equal _ _ h (V_ProjProj p0 a p1 b) := + PTag_eqdec p0 p1 && check_equal a b ltac:(check_equal_triv); + check_equal _ _ h (V_AppApp a0 b0 a1 b1) := + check_equal a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); + check_equal _ _ h (V_IndInd P0 u0 b0 c0 P1 u1 b1 c1) := + check_equal_r P0 P1 ltac:(check_equal_triv) && + check_equal u0 u1 ltac:(check_equal_triv) && + check_equal_r b0 b1 ltac:(check_equal_triv) && + check_equal_r c0 c1 ltac:(check_equal_triv); + check_equal _ _ h (V_UnivUniv i j) := Nat.eqb i j; + check_equal _ _ h (V_BindBind p0 A0 B0 p1 A1 B1) := + BTag_eqdec p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv); + check_equal _ _ _ _ := false + (* check_equal a b h := false; *) + with check_equal_r (a b : PTm) (h0 : algo_dom_r a b) : + bool by struct h0 := + check_equal_r a b h with inspect (hred a) := + check_equal_r a b h (exist _ (Some a') k) := check_equal_r a' b _; + check_equal_r a b h (exist _ None k) with inspect (hred b) := + | (exist _ None l) => tm_nonconf a b && check_equal a b _; + | (exist _ (Some b') l) => check_equal_r a b' _. - (* check_equal (VarPTm i) (VarPTm j) h := fin_eq i j; *) - (* check_equal (PAbs a) (PAbs b) h := check_equal a b _; *) - (* check_equal (PPair a0 b0) (PPair a1 b1) h := *) - (* check_equal a0 b0 _ && check_equal a1 b1 _; *) - (* check_equal (PUniv i) (PUniv j) _ := _; *) Next Obligation. - simpl. - intros ih. -Admitted. + intros. + destruct h. + exfalso. apply algo_dom_hf_hne in H. + apply hred_sound in k. + destruct H as [[|] _]. + eauto using hf_no_hred. + eauto using hne_no_hred. + apply hred_sound in k. + assert ( a'0 = a')by eauto using hred_deter. subst. + apply h. + exfalso. + apply hred_sound in k. + destruct H as [|]. + eauto using hne_no_hred. + eauto using hf_no_hred. +Defined. -Search (Bool.reflect (is_true _) _). -Check idP. +Next Obligation. + simpl. intros. + inversion h; subst =>//=. + move {h}. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred, hred_sound. + apply False_ind. hauto l:on use:hred_complete. + assert (b' = b'0) by eauto using hred_deter, hred_sound. + subst. + assumption. +Defined. -Definition metric {n} k (a b : PTm n) := - exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ - nf va /\ nf vb /\ size_PTm va + size_PTm vb + i + j <= k. +Next Obligation. + intros. + inversion h; subst => //=. + exfalso. hauto l:on use:hred_complete. + exfalso. hauto l:on use:hred_complete. +Defined. -Search (nat -> nat -> bool). +Next Obligation. + qauto inv:algo_dom, algo_dom_r. +Defined. +(* Do not step back from here or otherwise equations will cause an error *)