From 145e316a4bcff15bded924ef5f7bedf0e659b4a0 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Wed, 11 Dec 2024 23:52:57 -0500 Subject: [PATCH] Initial commit --- .gitignore | 63 +++ Makefile | 27 ++ _CoqProject | 2 + syntax.sig | 8 + theories/Autosubst2/core.v | 159 +++++++ theories/Autosubst2/fintype.v | 419 ++++++++++++++++++ theories/Autosubst2/syntax.v | 774 ++++++++++++++++++++++++++++++++++ 7 files changed, 1452 insertions(+) create mode 100644 .gitignore create mode 100644 Makefile create mode 100644 _CoqProject create mode 100644 syntax.sig create mode 100644 theories/Autosubst2/core.v create mode 100644 theories/Autosubst2/fintype.v create mode 100644 theories/Autosubst2/syntax.v diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..5894672 --- /dev/null +++ b/.gitignore @@ -0,0 +1,63 @@ +.*.aux +.*.d +*.a +*.cma +*.cmi +*.cmo +*.cmx +*.cmxa +*.cmxs +*.glob +*.ml.d +*.ml4.d +*.mlg.d +*.mli.d +*.mllib.d +*.mlpack.d +*.native +*.o +*.v.d +*.vio +*.vo +*.vok +*.vos +.coq-native +.csdp.cache +.lia.cache +.nia.cache +.nlia.cache +.nra.cache +csdp.cache +lia.cache +nia.cache +nlia.cache +nra.cache +native_compute_profile_*.data + +# generated timing files +*.timing.diff +*.v.after-timing +*.v.before-timing +*.v.timing +time-of-build-after.log +time-of-build-before.log +time-of-build-both.log +time-of-build-pretty.log + +# generated coq files + +# emacs temporary files +*~ + +*.aux +*.bbl +*.blg +*.out +*.log +paper/paper-output.tex +paper/rules.tex +paper/paper-output.pdf +proofs +proofs.zip +CoqMakefile +CoqMakefile.conf \ No newline at end of file diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..ef5b76f --- /dev/null +++ b/Makefile @@ -0,0 +1,27 @@ +COQMAKEFILE=CoqMakefile + +theories: $(COQMAKEFILE) FORCE + $(MAKE) -f $(COQMAKEFILE) + +validate: $(COQMAKEFILE) FORCE + $(MAKE) -f $(COQMAKEFILE) validate + +$(COQMAKEFILE) : theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v + $(COQBIN)coq_makefile -f _CoqProject -o $(COQMAKEFILE) + +install: $(COQMAKEFILE) + $(MAKE) -f $^ install + +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 + +.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 + +FORCE: diff --git a/_CoqProject b/_CoqProject new file mode 100644 index 0000000..24173e2 --- /dev/null +++ b/_CoqProject @@ -0,0 +1,2 @@ +-R theories ImpredIrrel +theories diff --git a/syntax.sig b/syntax.sig new file mode 100644 index 0000000..9c83c4f --- /dev/null +++ b/syntax.sig @@ -0,0 +1,8 @@ +Tm(VarTm) : Type +-- nat : Type + +Abs : (bind Tm in Tm) -> Tm +App : Tm -> Tm -> Tm +Pair : Tm -> Tm -> Tm +Proj1 : Tm -> Tm +Proj2 : Tm -> Tm diff --git a/theories/Autosubst2/core.v b/theories/Autosubst2/core.v new file mode 100644 index 0000000..ec6ba13 --- /dev/null +++ b/theories/Autosubst2/core.v @@ -0,0 +1,159 @@ +(* Function composition *) + +Definition funcomp {X Y Z} (g : Y -> Z) (f : X -> Y) := + fun x => g (f x). + +Lemma funcomp_assoc {W X Y Z} (g: Y -> Z) (f: X -> Y) (h: W -> X) : + funcomp g (funcomp f h) = (funcomp (funcomp g f) h). +Proof. + reflexivity. +Qed. + + +(** ** Functor Instances + +Exemplary functor instances needed to make Autosubst's generation possible for functors. +Two things are important: +1. The names are fixed. +2. For Coq to check termination, also the proofs have to be closed with Defined. + *) + +(** *** List Instance *) +Require Import List. + +Notation "'list_map'" := map. + +Definition list_ext {A B} {f g : A -> B} : + (forall x, f x = g x) -> forall xs, list_map f xs = list_map g xs. + intros H. induction xs. reflexivity. + cbn. f_equal. apply H. apply IHxs. +Defined. + +Definition list_id {A} { f : A -> A} : + (forall x, f x = x) -> forall xs, list_map f xs = xs. +Proof. + intros H. induction xs. reflexivity. + cbn. rewrite H. rewrite IHxs; eauto. +Defined. + +Definition list_comp {A B C} {f: A -> B} {g: B -> C} {h} : + (forall x, (funcomp g f) x = h x) -> forall xs, map g (map f xs) = map h xs. +Proof. + induction xs. reflexivity. + cbn. rewrite <- H. f_equal. apply IHxs. +Defined. + +(** *** Prod Instance *) + +Definition prod_map {A B C D} (f : A -> C) (g : B -> D) (p : A * B) : + C * D. +Proof. + destruct p as [a b]. split. + exact (f a). exact (g b). +Defined. + +Definition prod_id {A B} {f : A -> A} {g : B -> B} : + (forall x, f x = x) -> (forall x, g x = x) -> forall p, prod_map f g p = p. +Proof. + intros H0 H1. destruct p. cbn. f_equal; [ apply H0 | apply H1 ]. +Defined. + +Definition prod_ext {A B C D} {f f' : A -> C} {g g': B -> D} : + (forall x, f x = f' x) -> (forall x, g x = g' x) -> forall p, prod_map f g p = prod_map f' g' p. +Proof. + intros H0 H1. destruct p as [a b]. cbn. f_equal; [ apply H0 | apply H1 ]. +Defined. + +Definition prod_comp {A B C D E F} {f1 : A -> C} {g1 : C -> E} {h1 : A -> E} {f2: B -> D} {g2: D -> F} {h2 : B -> F}: + (forall x, (funcomp g1 f1) x = h1 x) -> (forall x, (funcomp g2 f2) x = h2 x) -> forall p, prod_map g1 g2 (prod_map f1 f2 p) = prod_map h1 h2 p. +Proof. + intros H0 H1. destruct p as [a b]. cbn. f_equal; [ apply H0 | apply H1 ]. +Defined. + +(** *** Option Instance *) + +Definition option_map {A B} (f : A -> B) (p : option A) : + option B := +match p with + | Some a => Some (f a) + | None => None +end. + +Definition option_id {A} {f : A -> A} : + (forall x, f x = x) -> forall p, option_map f p = p. +Proof. + intros H. destruct p ; cbn. + - f_equal. apply H. + - reflexivity. +Defined. + +Definition option_ext {A B} {f f' : A -> B} : + (forall x, f x = f' x) -> forall p, option_map f p = option_map f' p. +Proof. + intros H. destruct p as [a|] ; cbn. + - f_equal. apply H. + - reflexivity. +Defined. + +Definition option_comp {A B C} {f : A -> B} {g : B -> C} {h : A -> C}: + (forall x, (funcomp g f) x = h x) -> + forall p, option_map g (option_map f p) = option_map h p. +Proof. + intros H. destruct p as [a|]; cbn. + - f_equal. apply H. + - reflexivity. +Defined. + +#[export] Hint Rewrite in_map_iff : FunctorInstances. + +(* Declaring the scopes that all our notations will live in *) +Declare Scope fscope. +Declare Scope subst_scope. + +Ltac eta_reduce := + repeat match goal with + | [|- context[fun x => ?f x]] => change (fun x => f x) with f (* eta reduction *) + end. + +Ltac minimize := + repeat match goal with + | [|- context[fun x => ?f x]] => change (fun x => f x) with f (* eta reduction *) + | [|- context[fun x => ?g (?f x)]] => change (fun x => g (f x)) with (funcomp g f) (* funcomp folding *) + end. + +(* had to add this tactic abbreviation because I could not print a setoid_rewrite with the arrow *) +Ltac setoid_rewrite_left t := setoid_rewrite <- t. + +Ltac check_no_evars := + match goal with + | [|- ?x] => assert_fails (has_evar x) + end. + +Require Import Setoid Morphisms. + +Lemma pointwise_forall {X Y:Type} (f g: X -> Y) : + (pointwise_relation _ eq f g) -> forall x, f x = g x. +Proof. + trivial. +Qed. + +#[export] Instance funcomp_morphism {X Y Z} : + Proper (@pointwise_relation Y Z eq ==> @pointwise_relation X Y eq ==> @pointwise_relation X Z eq) funcomp. +Proof. + cbv - [funcomp]. + intros g0 g1 Hg f0 f1 Hf x. + unfold funcomp. rewrite Hf, Hg. + reflexivity. +Qed. + +#[export] Instance funcomp_morphism2 {X Y Z} : + Proper (@pointwise_relation Y Z eq ==> @pointwise_relation X Y eq ==> eq ==> eq) funcomp. +Proof. + intros g0 g1 Hg f0 f1 Hf ? x ->. + unfold funcomp. rewrite Hf, Hg. + reflexivity. +Qed. + +Ltac unfold_funcomp := match goal with + | |- context[(funcomp ?f ?g) ?s] => change ((funcomp f g) s) with (f (g s)) + end. diff --git a/theories/Autosubst2/fintype.v b/theories/Autosubst2/fintype.v new file mode 100644 index 0000000..99508b6 --- /dev/null +++ b/theories/Autosubst2/fintype.v @@ -0,0 +1,419 @@ +(** * 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 new file mode 100644 index 0000000..79e4f87 --- /dev/null +++ b/theories/Autosubst2/syntax.v @@ -0,0 +1,774 @@ +Require Import core fintype. + +Require Import Setoid Morphisms Relation_Definitions. + + +Module Core. + +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 + | Proj1 : Tm n_Tm -> Tm n_Tm + | Proj2 : Tm n_Tm -> Tm n_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. +Proof. +exact (eq_trans eq_refl (ap (fun x => Abs m_Tm 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. +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)). +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. +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)). +Qed. + +Lemma congr_Proj1 {m_Tm : nat} {s0 : Tm m_Tm} {t0 : Tm m_Tm} (H0 : s0 = t0) : + Proj1 m_Tm s0 = Proj1 m_Tm t0. +Proof. +exact (eq_trans eq_refl (ap (fun x => Proj1 m_Tm x) H0)). +Qed. + +Lemma congr_Proj2 {m_Tm : nat} {s0 : Tm m_Tm} {t0 : Tm m_Tm} (H0 : s0 = t0) : + Proj2 m_Tm s0 = Proj2 m_Tm t0. +Proof. +exact (eq_trans eq_refl (ap (fun x => Proj2 m_Tm x) H0)). +Qed. + +Lemma upRen_Tm_Tm {m : nat} {n : nat} (xi : fin m -> fin n) : + fin (S m) -> fin (S n). +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 := + 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) + | Proj1 _ s0 => Proj1 n_Tm (ren_Tm xi_Tm s0) + | Proj2 _ s0 => Proj2 n_Tm (ren_Tm xi_Tm s0) + end. + +Lemma up_Tm_Tm {m : nat} {n_Tm : nat} (sigma : fin m -> Tm n_Tm) : + fin (S m) -> Tm (S n_Tm). +Proof. +exact (scons (VarTm (S n_Tm) 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 := + 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) + | Proj1 _ s0 => Proj1 n_Tm (subst_Tm sigma_Tm s0) + | Proj2 _ s0 => Proj2 n_Tm (subst_Tm sigma_Tm s0) + 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. +Proof. +exact (fun n => + match n with + | Some fin_n => ap (ren_Tm shift) (Eq fin_n) + | None => 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} : +subst_Tm sigma_Tm s = s := + match s with + | 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 => + congr_App (idSubst_Tm sigma_Tm Eq_Tm s0) (idSubst_Tm sigma_Tm Eq_Tm s1) + | Pair _ s0 s1 => + congr_Pair (idSubst_Tm sigma_Tm Eq_Tm s0) + (idSubst_Tm sigma_Tm Eq_Tm s1) + | Proj1 _ s0 => congr_Proj1 (idSubst_Tm sigma_Tm Eq_Tm s0) + | Proj2 _ s0 => congr_Proj2 (idSubst_Tm sigma_Tm Eq_Tm s0) + 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) : + 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). +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 := + match s with + | VarTm _ s0 => ap (VarTm n_Tm) (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 => + congr_App (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0) + (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1) + | Pair _ s0 s1 => + congr_Pair (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0) + (extRen_Tm xi_Tm zeta_Tm Eq_Tm s1) + | Proj1 _ s0 => congr_Proj1 (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0) + | Proj2 _ s0 => congr_Proj2 (extRen_Tm xi_Tm zeta_Tm Eq_Tm s0) + 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) : + 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 + 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 := + match s with + | 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 => + congr_App (ext_Tm sigma_Tm tau_Tm Eq_Tm s0) + (ext_Tm sigma_Tm tau_Tm Eq_Tm s1) + | Pair _ s0 s1 => + congr_Pair (ext_Tm sigma_Tm tau_Tm Eq_Tm s0) + (ext_Tm sigma_Tm tau_Tm Eq_Tm s1) + | Proj1 _ s0 => congr_Proj1 (ext_Tm sigma_Tm tau_Tm Eq_Tm s0) + | Proj2 _ s0 => congr_Proj2 (ext_Tm sigma_Tm tau_Tm Eq_Tm s0) + 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) : + 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 := + match s with + | VarTm _ s0 => ap (VarTm l_Tm) (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 => + 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 => + congr_Pair (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0) + (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s1) + | Proj1 _ s0 => congr_Proj1 (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0) + | Proj2 _ s0 => congr_Proj2 (compRenRen_Tm xi_Tm zeta_Tm rho_Tm Eq_Tm s0) + 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) : + 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 + 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 := + match s with + | 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 => + 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 => + congr_Pair (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0) + (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s1) + | Proj1 _ s0 => + congr_Proj1 (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0) + | Proj2 _ s0 => + congr_Proj2 (compRenSubst_Tm xi_Tm tau_Tm theta_Tm Eq_Tm s0) + 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) + (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 = + up_Tm_Tm theta x. +Proof. +exact (fun n => + match n with + | Some fin_n => + eq_trans + (compRenRen_Tm shift (upRen_Tm_Tm zeta_Tm) + (funcomp shift zeta_Tm) (fun x => eq_refl) (sigma fin_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 + 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} : +ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s := + match s with + | 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 => + 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 => + congr_Pair (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0) + (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s1) + | Proj1 _ s0 => + congr_Proj1 (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0) + | Proj2 _ s0 => + congr_Proj2 (compSubstRen_Tm sigma_Tm zeta_Tm theta_Tm Eq_Tm s0) + 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) + (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 => + eq_trans + (compRenSubst_Tm shift (up_Tm_Tm tau_Tm) + (funcomp (up_Tm_Tm tau_Tm) shift) (fun x => eq_refl) + (sigma fin_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 + 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) +(Eq_Tm : forall x, funcomp (subst_Tm tau_Tm) sigma_Tm x = theta_Tm x) +(s : Tm m_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 => + 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 => + 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 => + congr_Pair (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0) + (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s1) + | Proj1 _ s0 => + congr_Proj1 (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0) + | Proj2 _ s0 => + congr_Proj2 (compSubstSubst_Tm sigma_Tm tau_Tm theta_Tm Eq_Tm s0) + 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) : + 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) : + 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. +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) : + 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) : + 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) : + 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) : + 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) : + 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. +Proof. +exact (fun n => + match n with + | Some fin_n => ap (ren_Tm shift) (Eq fin_n) + | None => 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 := + match s with + | 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 => + 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 => + congr_Pair (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0) + (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s1) + | Proj1 _ s0 => congr_Proj1 (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0) + | Proj2 _ s0 => congr_Proj2 (rinst_inst_Tm xi_Tm sigma_Tm Eq_Tm s0) + 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. +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)). +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. +Proof. +exact (idSubst_Tm (VarTm m_Tm) (fun n => eq_refl) s). +Qed. + +Lemma instId'_Tm_pointwise {m_Tm : nat} : + pointwise_relation _ eq (subst_Tm (VarTm m_Tm)) id. +Proof. +exact (fun s => idSubst_Tm (VarTm m_Tm) (fun n => eq_refl) s). +Qed. + +Lemma rinstId'_Tm {m_Tm : nat} (s : Tm m_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. +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. +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. +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). +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). +Proof. +exact (fun x => eq_refl). +Qed. + +Class Up_Tm X Y := + up_Tm : X -> Y. + +#[global] +Instance Subst_Tm {m_Tm n_Tm : nat}: (Subst1 _ _ _) := (@subst_Tm m_Tm n_Tm). + +#[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). + +Notation "[ sigma_Tm ]" := (subst_Tm sigma_Tm) +( at level 1, left associativity, only printing) : fscope. + +Notation "s [ sigma_Tm ]" := (subst_Tm sigma_Tm s) +( at level 7, left associativity, only printing) : subst_scope. + +Notation "↑__Tm" := up_Tm (only printing) : subst_scope. + +Notation "↑__Tm" := up_Tm_Tm (only printing) : subst_scope. + +Notation "⟨ xi_Tm ⟩" := (ren_Tm xi_Tm) +( at level 1, left associativity, only printing) : fscope. + +Notation "s ⟨ xi_Tm ⟩" := (ren_Tm xi_Tm s) +( at level 7, left associativity, only printing) : subst_scope. + +Notation "'var'" := VarTm ( at level 1, only printing) : subst_scope. + +Notation "x '__Tm'" := (@ids _ _ VarInstance_Tm x) +( at level 5, format "x __Tm", only printing) : subst_scope. + +Notation "x '__Tm'" := (VarTm x) ( at level 5, format "x __Tm") : +subst_scope. + +#[global] +Instance subst_Tm_morphism {m_Tm : nat} {n_Tm : nat}: + (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) + (@subst_Tm m_Tm n_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') + (ext_Tm f_Tm g_Tm Eq_Tm s) t Eq_st). +Qed. + +#[global] +Instance subst_Tm_morphism2 {m_Tm : nat} {n_Tm : nat}: + (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq)) + (@subst_Tm m_Tm n_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)). +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') + (extRen_Tm f_Tm g_Tm Eq_Tm s) t Eq_st). +Qed. + +#[global] +Instance ren_Tm_morphism2 {m_Tm : nat} {n_Tm : nat}: + (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq)) + (@ren_Tm m_Tm n_Tm)). +Proof. +exact (fun f_Tm g_Tm Eq_Tm s => extRen_Tm f_Tm g_Tm Eq_Tm s). +Qed. + +Ltac auto_unfold := repeat + unfold VarInstance_Tm, Var, ids, Ren_Tm, Ren1, ren1, + Up_Tm_Tm, Up_Tm, up_Tm, Subst_Tm, Subst1, subst1. + +Tactic Notation "auto_unfold" "in" "*" := repeat + unfold VarInstance_Tm, Var, ids, + Ren_Tm, Ren1, ren1, Up_Tm_Tm, + Up_Tm, up_Tm, Subst_Tm, Subst1, + subst1 in *. + +Ltac asimpl' := repeat (first + [ progress setoid_rewrite substSubst_Tm_pointwise + | progress setoid_rewrite substSubst_Tm + | progress setoid_rewrite substRen_Tm_pointwise + | progress setoid_rewrite substRen_Tm + | progress setoid_rewrite renSubst_Tm_pointwise + | progress setoid_rewrite renSubst_Tm + | progress setoid_rewrite renRen'_Tm_pointwise + | progress setoid_rewrite renRen_Tm + | progress setoid_rewrite varLRen'_Tm_pointwise + | progress setoid_rewrite varLRen'_Tm + | progress setoid_rewrite varL'_Tm_pointwise + | progress setoid_rewrite varL'_Tm + | progress setoid_rewrite rinstId'_Tm_pointwise + | progress setoid_rewrite rinstId'_Tm + | progress setoid_rewrite instId'_Tm_pointwise + | progress setoid_rewrite instId'_Tm + | progress + unfold up_list_Tm_Tm, up_Tm_Tm, upRen_list_Tm_Tm, + upRen_Tm_Tm, up_ren + | progress cbn[subst_Tm ren_Tm] + | progress fsimpl ]). + +Ltac asimpl := check_no_evars; + repeat + unfold VarInstance_Tm, Var, ids, Ren_Tm, Ren1, ren1, + Up_Tm_Tm, Up_Tm, up_Tm, Subst_Tm, Subst1, subst1 in *; + asimpl'; minimize. + +Tactic Notation "asimpl" "in" hyp(J) := revert J; asimpl; intros J. + +Tactic Notation "auto_case" := auto_case ltac:(asimpl; cbn; eauto). + +Ltac substify := auto_unfold; try setoid_rewrite rinstInst'_Tm_pointwise; + try setoid_rewrite rinstInst'_Tm. + +Ltac renamify := auto_unfold; try setoid_rewrite_left rinstInst'_Tm_pointwise; + try setoid_rewrite_left rinstInst'_Tm. + +End Core. + +Module Extra. + +Import +Core. + +Arguments VarTm {n_Tm}. + +Arguments Proj2 {n_Tm}. + +Arguments Proj1 {n_Tm}. + +Arguments Pair {n_Tm}. + +Arguments App {n_Tm}. + +Arguments Abs {n_Tm}. + +#[global]Hint Opaque subst_Tm: rewrite. + +#[global]Hint Opaque ren_Tm: rewrite. + +End Extra. + +Module interface. + +Export Core. + +Export Extra. + +End interface. + +Export interface. +