yiyunliu/sp-eta-postpone
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add a mostly finished eta postponement proof

Browse source
This commit is contained in:
Yiyun Liu 2025-01-25 16:08:21 -07:00
commit 2f04bcc75c
8 changed files with 4231 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

63
.gitignore vendored Normal file
View file

@ -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

27
Makefile Normal file
View file

@ -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:

2
_CoqProject Normal file
View file

@ -0,0 +1,2 @@
-R theories ImpredIrrel
theories

15
syntax.sig Normal file
View file

@ -0,0 +1,15 @@
PTm(VarPTm) : Type
PTag : Type
Ty : Type
Fun : Ty -> Ty -> Ty
Prod : Ty -> Ty -> Ty
Void : Ty
PL : PTag
PR : PTag
PAbs : Ty -> (bind PTm in PTm) -> PTm
PApp : PTm -> PTm -> PTm
PPair : PTm -> PTm -> PTm
PProj : PTag -> PTm -> PTm

159
theories/Autosubst2/core.v Normal file
View file

@ -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.

419
theories/Autosubst2/fintype.v Normal file
View file

@ -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.

824
theories/Autosubst2/syntax.v Normal file
View file

@ -0,0 +1,824 @@
Require Import core fintype.
Require Import Setoid Morphisms Relation_Definitions.
Module Core.
Inductive PTag : Type :=
| PL : PTag
| PR : PTag.
Lemma congr_PL : PL = PL.
Proof.
exact (eq_refl).
Qed.
Lemma congr_PR : PR = PR.
Proof.
exact (eq_refl).
Qed.
Inductive Ty : Type :=
| Fun : Ty -> Ty -> Ty
| Prod : Ty -> Ty -> Ty
| Void : Ty.
Lemma congr_Fun {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0)
(H1 : s1 = t1) : Fun s0 s1 = Fun t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => Fun x s1) H0))
(ap (fun x => Fun t0 x) H1)).
Qed.
Lemma congr_Prod {s0 : Ty} {s1 : Ty} {t0 : Ty} {t1 : Ty} (H0 : s0 = t0)
(H1 : s1 = t1) : Prod s0 s1 = Prod t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => Prod x s1) H0))
(ap (fun x => Prod t0 x) H1)).
Qed.
Lemma congr_Void : Void = Void.
Proof.
exact (eq_refl).
Qed.
Inductive PTm (n_PTm : nat) : Type :=
| VarPTm : fin n_PTm -> PTm n_PTm
| PAbs : Ty -> 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.
Lemma congr_PAbs {m_PTm : nat} {s0 : Ty} {s1 : PTm (S m_PTm)} {t0 : Ty}
{t1 : PTm (S m_PTm)} (H0 : s0 = t0) (H1 : s1 = t1) :
PAbs m_PTm s0 s1 = PAbs m_PTm t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => PAbs m_PTm x s1) H0))
(ap (fun x => PAbs m_PTm t0 x) H1)).
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.
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)).
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.
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)).
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.
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)).
Qed.
Lemma upRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n) :
fin (S m) -> fin (S n).
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 :=
match s with
| VarPTm _ s0 => VarPTm n_PTm (xi_PTm s0)
| PAbs _ s0 s1 => PAbs n_PTm s0 (ren_PTm (upRen_PTm_PTm xi_PTm) s1)
| 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)
end.
Lemma up_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) :
fin (S m) -> PTm (S n_PTm).
Proof.
exact (scons (VarPTm (S n_PTm) 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
:=
match s with
| VarPTm _ s0 => sigma_PTm s0
| PAbs _ s0 s1 => PAbs n_PTm s0 (subst_PTm (up_PTm_PTm sigma_PTm) s1)
| 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)
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.
Proof.
exact (fun n =>
match n with
| Some fin_n => ap (ren_PTm shift) (Eq fin_n)
| None => 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 :=
match s with
| VarPTm _ s0 => Eq_PTm s0
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
(idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s1)
| PApp _ s0 s1 =>
congr_PApp (idSubst_PTm sigma_PTm Eq_PTm s0)
(idSubst_PTm sigma_PTm Eq_PTm 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)
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) :
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).
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} :
ren_PTm xi_PTm s = ren_PTm zeta_PTm s :=
match s with
| VarPTm _ s0 => ap (VarPTm n_PTm) (Eq_PTm s0)
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
(extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
(upExtRen_PTm_PTm _ _ Eq_PTm) 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 =>
congr_PPair (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0)
(extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
| PProj _ s0 s1 =>
congr_PProj (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1)
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) :
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
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} :
subst_PTm sigma_PTm s = subst_PTm tau_PTm s :=
match s with
| VarPTm _ s0 => Eq_PTm s0
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
(ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
(upExt_PTm_PTm _ _ Eq_PTm) 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 =>
congr_PPair (ext_PTm sigma_PTm tau_PTm Eq_PTm s0)
(ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
| PProj _ s0 s1 =>
congr_PProj (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1)
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) :
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 :=
match s with
| VarPTm _ s0 => ap (VarPTm l_PTm) (Eq_PTm s0)
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
(compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm)
(upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) 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 =>
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 =>
congr_PProj (eq_refl s0)
(compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1)
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) :
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
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 :=
match s with
| VarPTm _ s0 => Eq_PTm s0
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
(compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm)
(up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) 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 =>
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 =>
congr_PProj (eq_refl s0)
(compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1)
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)
(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 =
up_PTm_PTm theta x.
Proof.
exact (fun n =>
match n with
| Some fin_n =>
eq_trans
(compRenRen_PTm shift (upRen_PTm_PTm zeta_PTm)
(funcomp shift zeta_PTm) (fun x => eq_refl) (sigma fin_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
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)
(Eq_PTm : forall x, funcomp (ren_PTm zeta_PTm) sigma_PTm x = theta_PTm x)
(s : PTm m_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 s1 =>
congr_PAbs (eq_refl s0)
(compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm)
(up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) 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 =>
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 =>
congr_PProj (eq_refl s0)
(compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1)
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)
(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 =
up_PTm_PTm theta x.
Proof.
exact (fun n =>
match n with
| Some fin_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))
(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
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)
(Eq_PTm : forall x, funcomp (subst_PTm tau_PTm) sigma_PTm x = theta_PTm x)
(s : PTm m_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 s1 =>
congr_PAbs (eq_refl s0)
(compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm)
(up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) 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 =>
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 =>
congr_PProj (eq_refl s0)
(compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1)
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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.
Proof.
exact (fun n =>
match n with
| Some fin_n => ap (ren_PTm shift) (Eq fin_n)
| None => 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 :=
match s with
| VarPTm _ s0 => Eq_PTm s0
| PAbs _ s0 s1 =>
congr_PAbs (eq_refl s0)
(rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm)
(rinstInst_up_PTm_PTm _ _ Eq_PTm) 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 =>
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 =>
congr_PProj (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1)
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.
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) :
pointwise_relation _ eq (ren_PTm xi_PTm)
(subst_PTm (funcomp (VarPTm n_PTm) 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.
Proof.
exact (idSubst_PTm (VarPTm m_PTm) (fun n => eq_refl) s).
Qed.
Lemma instId'_PTm_pointwise {m_PTm : nat} :
pointwise_relation _ eq (subst_PTm (VarPTm m_PTm)) id.
Proof.
exact (fun s => idSubst_PTm (VarPTm m_PTm) (fun n => eq_refl) s).
Qed.
Lemma rinstId'_PTm {m_PTm : nat} (s : PTm m_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.
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.
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.
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).
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).
Proof.
exact (fun x => eq_refl).
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 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).
Notation "[ sigma_PTm ]" := (subst_PTm sigma_PTm)
( at level 1, left associativity, only printing) : fscope.
Notation "s [ sigma_PTm ]" := (subst_PTm sigma_PTm s)
( at level 7, left associativity, only printing) : subst_scope.
Notation "↑__PTm" := up_PTm (only printing) : subst_scope.
Notation "↑__PTm" := up_PTm_PTm (only printing) : subst_scope.
Notation "⟨ xi_PTm ⟩" := (ren_PTm xi_PTm)
( at level 1, left associativity, only printing) : fscope.
Notation "s ⟨ xi_PTm ⟩" := (ren_PTm xi_PTm s)
( at level 7, left associativity, only printing) : subst_scope.
Notation "'var'" := VarPTm ( at level 1, only printing) : subst_scope.
Notation "x '__PTm'" := (@ids _ _ VarInstance_PTm x)
( at level 5, format "x __PTm", only printing) : subst_scope.
Notation "x '__PTm'" := (VarPTm x) ( at level 5, format "x __PTm") :
subst_scope.
#[global]
Instance subst_PTm_morphism {m_PTm : nat} {n_PTm : nat}:
(Proper (respectful (pointwise_relation _ eq) (respectful eq eq))
(@subst_PTm m_PTm n_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')
(ext_PTm f_PTm g_PTm Eq_PTm s) t Eq_st).
Qed.
#[global]
Instance subst_PTm_morphism2 {m_PTm : nat} {n_PTm : nat}:
(Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq))
(@subst_PTm m_PTm n_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)).
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')
(extRen_PTm f_PTm g_PTm Eq_PTm s) t Eq_st).
Qed.
#[global]
Instance ren_PTm_morphism2 {m_PTm : nat} {n_PTm : nat}:
(Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq))
(@ren_PTm m_PTm n_PTm)).
Proof.
exact (fun f_PTm g_PTm Eq_PTm s => extRen_PTm f_PTm g_PTm Eq_PTm s).
Qed.
Ltac auto_unfold := repeat
unfold VarInstance_PTm, Var, ids, Ren_PTm, Ren1, ren1,
Up_PTm_PTm, Up_PTm, up_PTm, Subst_PTm, Subst1, subst1.
Tactic Notation "auto_unfold" "in" "*" := repeat
unfold VarInstance_PTm, Var, ids,
Ren_PTm, Ren1, ren1, Up_PTm_PTm,
Up_PTm, up_PTm, Subst_PTm,
Subst1, subst1 in *.
Ltac asimpl' := repeat (first
[ progress setoid_rewrite substSubst_PTm_pointwise
| progress setoid_rewrite substSubst_PTm
| progress setoid_rewrite substRen_PTm_pointwise
| progress setoid_rewrite substRen_PTm
| progress setoid_rewrite renSubst_PTm_pointwise
| progress setoid_rewrite renSubst_PTm
| progress setoid_rewrite renRen'_PTm_pointwise
| progress setoid_rewrite renRen_PTm
| progress setoid_rewrite varLRen'_PTm_pointwise
| progress setoid_rewrite varLRen'_PTm
| progress setoid_rewrite varL'_PTm_pointwise
| progress setoid_rewrite varL'_PTm
| progress setoid_rewrite rinstId'_PTm_pointwise
| 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 cbn[subst_PTm ren_PTm]
| progress fsimpl ]).
Ltac asimpl := check_no_evars;
repeat
unfold VarInstance_PTm, Var, ids, Ren_PTm, Ren1, ren1,
Up_PTm_PTm, Up_PTm, up_PTm, Subst_PTm, 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'_PTm_pointwise;
try setoid_rewrite rinstInst'_PTm.
Ltac renamify := auto_unfold;
try setoid_rewrite_left rinstInst'_PTm_pointwise;
try setoid_rewrite_left rinstInst'_PTm.
End Core.
Module Extra.
Import
Core.
Arguments VarPTm {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.
End Extra.
Module interface.
Export Core.
Export Extra.
End interface.
Export interface.

2722
theories/fp_red.v Normal file
View file

File diff suppressed because it is too large Load diff