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

Add syntax spec

Browse source
This commit is contained in:
Yiyun Liu 2025-04-07 23:35:48 -04:00
commit 5cf82dae12
7 changed files with 984 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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.

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

@ -0,0 +1,517 @@
Require Import core unscoped.
Require Import Setoid Morphisms Relation_Definitions.
Module Core.
Inductive Tm : Type :=
| VarTm : nat -> Tm
| Abs : Tm -> Tm
| App : Tm -> Tm -> Tm.
Lemma congr_Abs {s0 : Tm} {t0 : Tm} (H0 : s0 = t0) : Abs s0 = Abs t0.
Proof.
exact (eq_trans eq_refl (ap (fun x => Abs x) H0)).
Qed.
Lemma congr_App {s0 : Tm} {s1 : Tm} {t0 : Tm} {t1 : Tm} (H0 : s0 = t0)
(H1 : s1 = t1) : App s0 s1 = App t0 t1.
Proof.
exact (eq_trans (eq_trans eq_refl (ap (fun x => App x s1) H0))
(ap (fun x => App t0 x) H1)).
Qed.
Lemma upRen_Tm_Tm (xi : nat -> nat) : nat -> nat.
Proof.
exact (up_ren xi).
Defined.
Fixpoint ren_Tm (xi_Tm : nat -> nat) (s : Tm) {struct s} : Tm :=
match s with
| VarTm s0 => VarTm (xi_Tm s0)
| Abs s0 => Abs (ren_Tm (upRen_Tm_Tm xi_Tm) s0)
| App s0 s1 => App (ren_Tm xi_Tm s0) (ren_Tm xi_Tm s1)
end.
Lemma up_Tm_Tm (sigma : nat -> Tm) : nat -> Tm.
Proof.
exact (scons (VarTm var_zero) (funcomp (ren_Tm shift) sigma)).
Defined.
Fixpoint subst_Tm (sigma_Tm : nat -> Tm) (s : Tm) {struct s} : Tm :=
match s with
| VarTm s0 => sigma_Tm s0
| Abs s0 => Abs (subst_Tm (up_Tm_Tm sigma_Tm) s0)
| App s0 s1 => App (subst_Tm sigma_Tm s0) (subst_Tm sigma_Tm s1)
end.
Lemma upId_Tm_Tm (sigma : nat -> Tm) (Eq : forall x, sigma x = VarTm x) :
forall x, up_Tm_Tm sigma x = VarTm x.
Proof.
exact (fun n =>
match n with
| S n' => ap (ren_Tm shift) (Eq n')
| O => eq_refl
end).
Qed.
Fixpoint idSubst_Tm (sigma_Tm : nat -> Tm)
(Eq_Tm : forall x, sigma_Tm x = VarTm x) (s : Tm) {struct s} :
subst_Tm sigma_Tm s = s :=
match s with
| VarTm s0 => Eq_Tm s0
| Abs s0 =>
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)
end.
Lemma upExtRen_Tm_Tm (xi : nat -> nat) (zeta : nat -> nat)
(Eq : forall x, xi x = zeta x) :
forall x, upRen_Tm_Tm xi x = upRen_Tm_Tm zeta x.
Proof.
exact (fun n => match n with
| S n' => ap shift (Eq n')
| O => eq_refl
end).
Qed.
Fixpoint extRen_Tm (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat)
(Eq_Tm : forall x, xi_Tm x = zeta_Tm x) (s : Tm) {struct s} :
ren_Tm xi_Tm s = ren_Tm zeta_Tm s :=
match s with
| VarTm s0 => ap (VarTm) (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)
end.
Lemma upExt_Tm_Tm (sigma : nat -> Tm) (tau : nat -> Tm)
(Eq : forall x, sigma x = tau x) :
forall x, up_Tm_Tm sigma x = up_Tm_Tm tau x.
Proof.
exact (fun n =>
match n with
| S n' => ap (ren_Tm shift) (Eq n')
| O => eq_refl
end).
Qed.
Fixpoint ext_Tm (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm)
(Eq_Tm : forall x, sigma_Tm x = tau_Tm x) (s : Tm) {struct s} :
subst_Tm sigma_Tm s = subst_Tm tau_Tm s :=
match s with
| VarTm s0 => Eq_Tm s0
| Abs s0 =>
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)
end.
Lemma up_ren_ren_Tm_Tm (xi : nat -> nat) (zeta : nat -> nat)
(rho : nat -> nat) (Eq : forall x, funcomp zeta xi x = rho x) :
forall x, funcomp (upRen_Tm_Tm zeta) (upRen_Tm_Tm xi) x = upRen_Tm_Tm rho x.
Proof.
exact (up_ren_ren xi zeta rho Eq).
Qed.
Fixpoint compRenRen_Tm (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat)
(rho_Tm : nat -> nat) (Eq_Tm : forall x, funcomp zeta_Tm xi_Tm x = rho_Tm x)
(s : Tm) {struct s} : ren_Tm zeta_Tm (ren_Tm xi_Tm s) = ren_Tm rho_Tm s :=
match s with
| VarTm s0 => ap (VarTm) (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)
end.
Lemma up_ren_subst_Tm_Tm (xi : nat -> nat) (tau : nat -> Tm)
(theta : nat -> Tm) (Eq : forall x, funcomp tau xi x = theta x) :
forall x, funcomp (up_Tm_Tm tau) (upRen_Tm_Tm xi) x = up_Tm_Tm theta x.
Proof.
exact (fun n =>
match n with
| S n' => ap (ren_Tm shift) (Eq n')
| O => eq_refl
end).
Qed.
Fixpoint compRenSubst_Tm (xi_Tm : nat -> nat) (tau_Tm : nat -> Tm)
(theta_Tm : nat -> Tm)
(Eq_Tm : forall x, funcomp tau_Tm xi_Tm x = theta_Tm x) (s : Tm) {struct s} :
subst_Tm tau_Tm (ren_Tm xi_Tm s) = subst_Tm theta_Tm s :=
match s with
| VarTm s0 => Eq_Tm s0
| Abs s0 =>
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)
end.
Lemma up_subst_ren_Tm_Tm (sigma : nat -> Tm) (zeta_Tm : nat -> nat)
(theta : nat -> Tm)
(Eq : forall x, funcomp (ren_Tm zeta_Tm) sigma x = theta x) :
forall x,
funcomp (ren_Tm (upRen_Tm_Tm zeta_Tm)) (up_Tm_Tm sigma) x =
up_Tm_Tm theta x.
Proof.
exact (fun n =>
match n with
| S n' =>
eq_trans
(compRenRen_Tm shift (upRen_Tm_Tm zeta_Tm)
(funcomp shift zeta_Tm) (fun x => eq_refl) (sigma n'))
(eq_trans
(eq_sym
(compRenRen_Tm zeta_Tm shift (funcomp shift zeta_Tm)
(fun x => eq_refl) (sigma n')))
(ap (ren_Tm shift) (Eq n')))
| O => eq_refl
end).
Qed.
Fixpoint compSubstRen_Tm (sigma_Tm : nat -> Tm) (zeta_Tm : nat -> nat)
(theta_Tm : nat -> Tm)
(Eq_Tm : forall x, funcomp (ren_Tm zeta_Tm) sigma_Tm x = theta_Tm x)
(s : Tm) {struct s} :
ren_Tm zeta_Tm (subst_Tm sigma_Tm s) = subst_Tm theta_Tm s :=
match s with
| VarTm s0 => Eq_Tm s0
| Abs s0 =>
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)
end.
Lemma up_subst_subst_Tm_Tm (sigma : nat -> Tm) (tau_Tm : nat -> Tm)
(theta : nat -> Tm)
(Eq : forall x, funcomp (subst_Tm tau_Tm) sigma x = theta x) :
forall x,
funcomp (subst_Tm (up_Tm_Tm tau_Tm)) (up_Tm_Tm sigma) x = up_Tm_Tm theta x.
Proof.
exact (fun n =>
match n with
| S n' =>
eq_trans
(compRenSubst_Tm shift (up_Tm_Tm tau_Tm)
(funcomp (up_Tm_Tm tau_Tm) shift) (fun x => eq_refl)
(sigma n'))
(eq_trans
(eq_sym
(compSubstRen_Tm tau_Tm shift
(funcomp (ren_Tm shift) tau_Tm) (fun x => eq_refl)
(sigma n'))) (ap (ren_Tm shift) (Eq n')))
| O => eq_refl
end).
Qed.
Fixpoint compSubstSubst_Tm (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm)
(theta_Tm : nat -> Tm)
(Eq_Tm : forall x, funcomp (subst_Tm tau_Tm) sigma_Tm x = theta_Tm x)
(s : Tm) {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)
end.
Lemma renRen_Tm (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat) (s : Tm) :
ren_Tm zeta_Tm (ren_Tm xi_Tm s) = ren_Tm (funcomp zeta_Tm xi_Tm) s.
Proof.
exact (compRenRen_Tm xi_Tm zeta_Tm _ (fun n => eq_refl) s).
Qed.
Lemma renRen'_Tm_pointwise (xi_Tm : nat -> nat) (zeta_Tm : nat -> nat) :
pointwise_relation _ eq (funcomp (ren_Tm zeta_Tm) (ren_Tm xi_Tm))
(ren_Tm (funcomp zeta_Tm xi_Tm)).
Proof.
exact (fun s => compRenRen_Tm xi_Tm zeta_Tm _ (fun n => eq_refl) s).
Qed.
Lemma renSubst_Tm (xi_Tm : nat -> nat) (tau_Tm : nat -> Tm) (s : Tm) :
subst_Tm tau_Tm (ren_Tm xi_Tm s) = subst_Tm (funcomp tau_Tm xi_Tm) s.
Proof.
exact (compRenSubst_Tm xi_Tm tau_Tm _ (fun n => eq_refl) s).
Qed.
Lemma renSubst_Tm_pointwise (xi_Tm : nat -> nat) (tau_Tm : nat -> Tm) :
pointwise_relation _ eq (funcomp (subst_Tm tau_Tm) (ren_Tm xi_Tm))
(subst_Tm (funcomp tau_Tm xi_Tm)).
Proof.
exact (fun s => compRenSubst_Tm xi_Tm tau_Tm _ (fun n => eq_refl) s).
Qed.
Lemma substRen_Tm (sigma_Tm : nat -> Tm) (zeta_Tm : nat -> nat) (s : Tm) :
ren_Tm zeta_Tm (subst_Tm sigma_Tm s) =
subst_Tm (funcomp (ren_Tm zeta_Tm) sigma_Tm) s.
Proof.
exact (compSubstRen_Tm sigma_Tm zeta_Tm _ (fun n => eq_refl) s).
Qed.
Lemma substRen_Tm_pointwise (sigma_Tm : nat -> Tm) (zeta_Tm : nat -> nat) :
pointwise_relation _ eq (funcomp (ren_Tm zeta_Tm) (subst_Tm sigma_Tm))
(subst_Tm (funcomp (ren_Tm zeta_Tm) sigma_Tm)).
Proof.
exact (fun s => compSubstRen_Tm sigma_Tm zeta_Tm _ (fun n => eq_refl) s).
Qed.
Lemma substSubst_Tm (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm) (s : Tm) :
subst_Tm tau_Tm (subst_Tm sigma_Tm s) =
subst_Tm (funcomp (subst_Tm tau_Tm) sigma_Tm) s.
Proof.
exact (compSubstSubst_Tm sigma_Tm tau_Tm _ (fun n => eq_refl) s).
Qed.
Lemma substSubst_Tm_pointwise (sigma_Tm : nat -> Tm) (tau_Tm : nat -> Tm) :
pointwise_relation _ eq (funcomp (subst_Tm tau_Tm) (subst_Tm sigma_Tm))
(subst_Tm (funcomp (subst_Tm tau_Tm) sigma_Tm)).
Proof.
exact (fun s => compSubstSubst_Tm sigma_Tm tau_Tm _ (fun n => eq_refl) s).
Qed.
Lemma rinstInst_up_Tm_Tm (xi : nat -> nat) (sigma : nat -> Tm)
(Eq : forall x, funcomp (VarTm) xi x = sigma x) :
forall x, funcomp (VarTm) (upRen_Tm_Tm xi) x = up_Tm_Tm sigma x.
Proof.
exact (fun n =>
match n with
| S n' => ap (ren_Tm shift) (Eq n')
| O => eq_refl
end).
Qed.
Fixpoint rinst_inst_Tm (xi_Tm : nat -> nat) (sigma_Tm : nat -> Tm)
(Eq_Tm : forall x, funcomp (VarTm) xi_Tm x = sigma_Tm x) (s : Tm) {struct s}
: ren_Tm xi_Tm s = subst_Tm sigma_Tm s :=
match s with
| VarTm s0 => Eq_Tm s0
| Abs s0 =>
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)
end.
Lemma rinstInst'_Tm (xi_Tm : nat -> nat) (s : Tm) :
ren_Tm xi_Tm s = subst_Tm (funcomp (VarTm) xi_Tm) s.
Proof.
exact (rinst_inst_Tm xi_Tm _ (fun n => eq_refl) s).
Qed.
Lemma rinstInst'_Tm_pointwise (xi_Tm : nat -> nat) :
pointwise_relation _ eq (ren_Tm xi_Tm) (subst_Tm (funcomp (VarTm) xi_Tm)).
Proof.
exact (fun s => rinst_inst_Tm xi_Tm _ (fun n => eq_refl) s).
Qed.
Lemma instId'_Tm (s : Tm) : subst_Tm (VarTm) s = s.
Proof.
exact (idSubst_Tm (VarTm) (fun n => eq_refl) s).
Qed.
Lemma instId'_Tm_pointwise : pointwise_relation _ eq (subst_Tm (VarTm)) id.
Proof.
exact (fun s => idSubst_Tm (VarTm) (fun n => eq_refl) s).
Qed.
Lemma rinstId'_Tm (s : Tm) : ren_Tm id s = s.
Proof.
exact (eq_ind_r (fun t => t = s) (instId'_Tm s) (rinstInst'_Tm id s)).
Qed.
Lemma rinstId'_Tm_pointwise : pointwise_relation _ eq (@ren_Tm id) id.
Proof.
exact (fun s => eq_ind_r (fun t => t = s) (instId'_Tm s) (rinstInst'_Tm id s)).
Qed.
Lemma varL'_Tm (sigma_Tm : nat -> Tm) (x : nat) :
subst_Tm sigma_Tm (VarTm x) = sigma_Tm x.
Proof.
exact (eq_refl).
Qed.
Lemma varL'_Tm_pointwise (sigma_Tm : nat -> Tm) :
pointwise_relation _ eq (funcomp (subst_Tm sigma_Tm) (VarTm)) sigma_Tm.
Proof.
exact (fun x => eq_refl).
Qed.
Lemma varLRen'_Tm (xi_Tm : nat -> nat) (x : nat) :
ren_Tm xi_Tm (VarTm x) = VarTm (xi_Tm x).
Proof.
exact (eq_refl).
Qed.
Lemma varLRen'_Tm_pointwise (xi_Tm : nat -> nat) :
pointwise_relation _ eq (funcomp (ren_Tm xi_Tm) (VarTm))
(funcomp (VarTm) xi_Tm).
Proof.
exact (fun x => eq_refl).
Qed.
Class Up_Tm X Y :=
up_Tm : X -> Y.
#[global] Instance Subst_Tm : (Subst1 _ _ _) := @subst_Tm.
#[global] Instance Up_Tm_Tm : (Up_Tm _ _) := @up_Tm_Tm.
#[global] Instance Ren_Tm : (Ren1 _ _ _) := @ren_Tm.
#[global]
Instance VarInstance_Tm : (Var _ _) := @VarTm.
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 :
(Proper (respectful (pointwise_relation _ eq) (respectful eq eq))
(@subst_Tm)).
Proof.
exact (fun f_Tm g_Tm Eq_Tm s t Eq_st =>
eq_ind s (fun t' => subst_Tm f_Tm s = subst_Tm g_Tm t')
(ext_Tm f_Tm g_Tm Eq_Tm s) t Eq_st).
Qed.
#[global]
Instance subst_Tm_morphism2 :
(Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq))
(@subst_Tm)).
Proof.
exact (fun f_Tm g_Tm Eq_Tm s => ext_Tm f_Tm g_Tm Eq_Tm s).
Qed.
#[global]
Instance ren_Tm_morphism :
(Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) (@ren_Tm)).
Proof.
exact (fun f_Tm g_Tm Eq_Tm s t Eq_st =>
eq_ind s (fun t' => ren_Tm f_Tm s = ren_Tm g_Tm t')
(extRen_Tm f_Tm g_Tm Eq_Tm s) t Eq_st).
Qed.
#[global]
Instance ren_Tm_morphism2 :
(Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq))
(@ren_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_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.
#[global] Hint Opaque subst_Tm: rewrite.
#[global] Hint Opaque ren_Tm: rewrite.
End Extra.
Module interface.
Export Core.
Export Extra.
End interface.
Export interface.

213
theories/Autosubst2/unscoped.v Normal file
View file

@ -0,0 +1,213 @@
(** * Autosubst Header for Unnamed Syntax
Version: December 11, 2019.
*)
(* Adrian:
I changed this library a bit to work better with my generated code.
1. I use nat directly instead of defining fin to be nat and using Some/None as S/O
2. I removed the "s, sigma" notation for scons because it interacts with dependent function types "forall x, A"*)
Require Import core.
Require Import Setoid Morphisms Relation_Definitions.
Definition ap {X Y} (f : X -> Y) {x y : X} (p : x = y) : f x = f y :=
match p with eq_refl => eq_refl end.
Definition apc {X Y} {f g : X -> Y} {x y : X} (p : f = g) (q : x = y) : f x = g y :=
match q with eq_refl => match p with eq_refl => eq_refl end end.
(** ** Primitives of the Sigma Calculus. *)
Definition shift := S.
Definition var_zero := 0.
Definition id {X} := @Datatypes.id X.
Definition scons {X: Type} (x : X) (xi : nat -> X) :=
fun n => match n with
| 0 => x
| S n => xi n
end.
#[ export ]
Hint Opaque scons : rewrite.
(** ** Type Class Instances for Notation
Required to make notation work. *)
(** *** Type classes for renamings. *)
Class Ren1 (X1 : Type) (Y Z : Type) :=
ren1 : X1 -> Y -> Z.
Class Ren2 (X1 X2 : Type) (Y Z : Type) :=
ren2 : X1 -> X2 -> Y -> Z.
Class Ren3 (X1 X2 X3 : Type) (Y Z : Type) :=
ren3 : X1 -> X2 -> X3 -> Y -> Z.
Class Ren4 (X1 X2 X3 X4 : Type) (Y Z : Type) :=
ren4 : X1 -> X2 -> X3 -> X4 -> Y -> Z.
Class Ren5 (X1 X2 X3 X4 X5 : Type) (Y Z : Type) :=
ren5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z.
Module RenNotations.
Notation "s ⟨ xi1 ⟩" := (ren1 xi1 s) (at level 7, left associativity, format "s ⟨ xi1 ⟩") : subst_scope.
Notation "s ⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ⟩") : subst_scope.
Notation "s ⟨ xi1 ; xi2 ; xi3 ⟩" := (ren3 xi1 xi2 xi3 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ⟩") : subst_scope.
Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩" := (ren4 xi1 xi2 xi3 xi4 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩") : subst_scope.
Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩" := (ren5 xi1 xi2 xi3 xi4 xi5 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩") : subst_scope.
Notation "⟨ xi ⟩" := (ren1 xi) (at level 1, left associativity, format "⟨ xi ⟩") : fscope.
Notation "⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2) (at level 1, left associativity, format "⟨ xi1 ; xi2 ⟩") : fscope.
End RenNotations.
(** *** Type Classes for Substiution *)
Class Subst1 (X1 : Type) (Y Z: Type) :=
subst1 : X1 -> Y -> Z.
Class Subst2 (X1 X2 : Type) (Y Z: Type) :=
subst2 : X1 -> X2 -> Y -> Z.
Class Subst3 (X1 X2 X3 : Type) (Y Z: Type) :=
subst3 : X1 -> X2 -> X3 -> Y -> Z.
Class Subst4 (X1 X2 X3 X4: Type) (Y Z: Type) :=
subst4 : X1 -> X2 -> X3 -> X4 -> Y -> Z.
Class Subst5 (X1 X2 X3 X4 X5 : Type) (Y Z: Type) :=
subst5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z.
Module SubstNotations.
Notation "s [ sigma ]" := (subst1 sigma s) (at level 7, left associativity, format "s '/' [ sigma ]") : subst_scope.
Notation "s [ sigma ; tau ]" := (subst2 sigma tau s) (at level 7, left associativity, format "s '/' [ sigma ; '/' tau ]") : subst_scope.
End SubstNotations.
(** *** Type Class for Variables *)
Class Var X Y :=
ids : X -> Y.
#[export] Instance idsRen : Var nat nat := id.
(** ** Proofs for the substitution primitives. *)
Arguments funcomp {X Y Z} (g)%fscope (f)%fscope.
Module CombineNotations.
Notation "f >> g" := (funcomp g f) (at level 50) : fscope.
Notation "s .: sigma" := (scons s sigma) (at level 55, sigma at next level, right associativity) : subst_scope.
#[ global ]
Open Scope fscope.
#[ global ]
Open Scope subst_scope.
End CombineNotations.
Import CombineNotations.
(** A generic lifting of a renaming. *)
Definition up_ren (xi : nat -> nat) :=
0 .: (xi >> S).
(** A generic proof that lifting of renamings composes. *)
Lemma up_ren_ren (xi: nat -> nat) (zeta : nat -> nat) (rho: nat -> nat) (E: forall x, (xi >> zeta) x = rho x) :
forall x, (up_ren xi >> up_ren zeta) x = up_ren rho x.
Proof.
intros [|x].
- reflexivity.
- unfold up_ren. cbn. unfold funcomp. f_equal. apply E.
Qed.
(** Eta laws. *)
Lemma scons_eta' {T} (f : nat -> T) :
pointwise_relation _ eq (f var_zero .: (funcomp f shift)) f.
Proof. intros x. destruct x; reflexivity. Qed.
Lemma scons_eta_id' :
pointwise_relation _ eq (var_zero .: shift) id.
Proof. intros x. destruct x; reflexivity. Qed.
Lemma scons_comp' (T: Type) {U} (s: T) (sigma: nat -> T) (tau: T -> U) :
pointwise_relation _ eq (funcomp tau (s .: sigma)) ((tau s) .: (funcomp tau sigma)).
Proof. intros x. destruct x; reflexivity. Qed.
(* Morphism for Setoid Rewriting. The only morphism that can be defined statically. *)
#[export] Instance scons_morphism {X: Type} :
Proper (eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons X).
Proof.
intros ? t -> sigma tau H.
intros [|x].
cbn. reflexivity.
apply H.
Qed.
#[export] Instance scons_morphism2 {X: Type} :
Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons X).
Proof.
intros ? t -> sigma tau H ? x ->.
destruct x as [|x].
cbn. reflexivity.
apply H.
Qed.
(** ** Generic lifting of an allfv predicate *)
Definition up_allfv (p: nat -> Prop) : nat -> Prop := scons True p.
(** ** Notations for unscoped syntax *)
Module UnscopedNotations.
Include RenNotations.
Include SubstNotations.
Include CombineNotations.
(* Notation "s , sigma" := (scons s sigma) (at level 60, format "s , sigma", right associativity) : subst_scope. *)
Notation "s '..'" := (scons s ids) (at level 1, format "s ..") : subst_scope.
Notation "↑" := (shift) : subst_scope.
#[global]
Open Scope fscope.
#[global]
Open Scope subst_scope.
End UnscopedNotations.
(** ** Tactics for unscoped syntax *)
(** Automatically does a case analysis on a natural number, useful for proofs with context renamings/context morphisms. *)
Tactic Notation "auto_case" tactic(t) := (match goal with
| [|- forall (i : nat), _] => intros []; t
end).
(** Generic fsimpl tactic: simplifies the above primitives in a goal. *)
Ltac fsimpl :=
repeat match goal with
| [|- context[id >> ?f]] => change (id >> f) with f (* AsimplCompIdL *)
| [|- context[?f >> id]] => change (f >> id) with f (* AsimplCompIdR *)
| [|- context [id ?s]] => change (id s) with s
| [|- context[(?f >> ?g) >> ?h]] => change ((f >> g) >> h) with (f >> (g >> h))
| [|- context[(?v .: ?g) var_zero]] => change ((v .: g) var_zero) with v
| [|- context[(?v .: ?g) 0]] => change ((v .: g) 0) with v
| [|- context[(?v .: ?g) (S ?n)]] => change ((v .: g) (S n)) with (g n)
| [|- context[?f >> (?x .: ?g)]] => change (f >> (x .: g)) with g (* f should evaluate to shift *)
| [|- context[var_zero]] => change var_zero with 0
| [|- context[?x2 .: (funcomp ?f shift)]] => change (scons x2 (funcomp f shift)) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite (@scons_eta' _ _ f)
| [|- context[?f var_zero .: ?g]] => change (scons (f var_zero) g) with (scons (f var_zero) (funcomp f shift)); rewrite scons_eta'
| [|- _ = ?h (?f ?s)] => change (h (f s)) with ((f >> h) s)
| [|- ?h (?f ?s) = _] => change (h (f s)) with ((f >> h) s)
(* DONE had to put an underscore as the last argument to scons. This might be an argument against unfolding funcomp *)
| [|- context[funcomp _ (scons _ _)]] => setoid_rewrite scons_comp'; eta_reduce
| [|- context[scons var_zero shift]] => setoid_rewrite scons_eta_id'; eta_reduce
end.