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