From 875db75955fa54829e51cfe9756ffaaeb21c4542 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 27 Feb 2025 20:39:55 -0500 Subject: [PATCH 01/10] Add equations for check_equal --- theories/executable.v | 226 ++++++++++++++++++++++++++++++++++++------ 1 file changed, 197 insertions(+), 29 deletions(-) diff --git a/theories/executable.v b/theories/executable.v index f773fa6..144979d 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -4,42 +4,44 @@ Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax Require Import algorithmic. From stdpp Require Import relations (rtc(..), nsteps(..)). Require Import ssreflect ssrbool. +From Hammer Require Import Tactics. + Inductive algo_dom {n} : PTm n -> PTm n -> Prop := | A_AbsAbs a b : - algo_dom a b -> + algo_dom_r a b -> (* --------------------- *) algo_dom (PAbs a) (PAbs b) | A_AbsNeu a u : ishne u -> - algo_dom a (PApp (ren_PTm shift u) (VarPTm var_zero)) -> + algo_dom_r a (PApp (ren_PTm shift u) (VarPTm var_zero)) -> (* --------------------- *) algo_dom (PAbs a) u | A_NeuAbs a u : ishne u -> - algo_dom (PApp (ren_PTm shift u) (VarPTm var_zero)) a -> + algo_dom_r (PApp (ren_PTm shift u) (VarPTm var_zero)) a -> (* --------------------- *) algo_dom u (PAbs a) | A_PairPair a0 a1 b0 b1 : - algo_dom a0 a1 -> - algo_dom b0 b1 -> + algo_dom_r a0 a1 -> + algo_dom_r b0 b1 -> (* ---------------------------- *) algo_dom (PPair a0 b0) (PPair a1 b1) | A_PairNeu a0 a1 u : ishne u -> - algo_dom a0 (PProj PL u) -> - algo_dom a1 (PProj PR u) -> + algo_dom_r a0 (PProj PL u) -> + algo_dom_r a1 (PProj PR u) -> (* ----------------------- *) algo_dom (PPair a0 a1) u | A_NeuPair a0 a1 u : ishne u -> - algo_dom (PProj PL u) a0 -> - algo_dom (PProj PR u) a1 -> + algo_dom_r (PProj PL u) a0 -> + algo_dom_r (PProj PR u) a1 -> (* ----------------------- *) algo_dom u (PPair a0 a1) @@ -48,8 +50,8 @@ Inductive algo_dom {n} : PTm n -> PTm n -> Prop := algo_dom (PUniv i) (PUniv j) | A_BindCong p0 p1 A0 A1 B0 B1 : - algo_dom A0 A1 -> - algo_dom B0 B1 -> + algo_dom_r A0 A1 -> + algo_dom_r B0 B1 -> (* ---------------------------- *) algo_dom (PBind p0 A0 B0) (PBind p1 A1 B1) @@ -68,25 +70,53 @@ Inductive algo_dom {n} : PTm n -> PTm n -> Prop := ishne u0 -> ishne u1 -> algo_dom u0 u1 -> - algo_dom a0 a1 -> + algo_dom_r a0 a1 -> (* ------------------------- *) algo_dom (PApp u0 a0) (PApp u1 a1) +with algo_dom_r {n} : PTm n -> PTm n -> Prop := +| A_NfNf a b : + algo_dom a b -> + algo_dom_r a b + | A_HRedL a a' b : HRed.R a a' -> - algo_dom a' b -> + algo_dom_r a' b -> (* ----------------------- *) - algo_dom a b + algo_dom_r a b | A_HRedR a b b' : ishne a \/ ishf a -> HRed.R b b' -> - algo_dom a b' -> + algo_dom_r a b' -> (* ----------------------- *) - algo_dom a b. + algo_dom_r a b. + +Derive Signature for algo_dom algo_dom_r. -Definition fin_eq {n} (i j : fin n) : bool. +Derive Dependent Inversion adom_inv with (forall n (a b : PTm n), algo_dom a b) Sort Prop. + +Lemma algo_dom_hf_hne n (a b : PTm n) : + algo_dom a b -> + (ishf a \/ ishne a) /\ (ishf b \/ ishne b). +Proof. + induction 1 =>//=; hauto lq:on. +Qed. + +Lemma hf_no_hred n (a b : PTm n) : + ishf a -> + HRed.R a b -> + False. +Proof. hauto l:on inv:HRed.R. Qed. + +Lemma hne_no_hred n (a b : PTm n) : + ishne a -> + HRed.R a b -> + False. +Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed. + +Definition fin_beq {n} (i j : fin n) : bool. Proof. induction n. - by exfalso. @@ -98,7 +128,7 @@ Proof. Defined. Lemma fin_eq_dec {n} (i j : fin n) : - Bool.reflect (i = j) (fin_eq i j). + Bool.reflect (i = j) (fin_beq i j). Proof. revert i j. induction n. - destruct i. @@ -116,24 +146,162 @@ Proof. + by apply ReflectT. Defined. +Scheme Equality for PTag. +Scheme Equality for BTag. + +(* Fixpoint PTm_eqb {n} (a b : PTm n) := *) +(* match a, b with *) +(* | VarPTm i, VarPTm j => fin_eq i j *) +(* | PAbs a, PAbs b => PTm_eqb a b *) +(* | PApp a0 b0, PApp a1 b1 => PTm_eqb a0 a1 && PTm_eqb b0 b1 *) +(* | PBind p0 A0 B0, PBind p1 A1 B1 => BTag_beq p0 p1 && PTm_eqb A0 A1 && PTm_eqb B0 B1 *) +(* | PPair a0 b0, PPair a1 b1 => PTm_eqb a0 a1 && PTm_eqb b0 b1 *) +(* | *) + +(* Lemma hred {n} (a : PTm n) : (relations.nf HRed.R a) + {x | HRed.R a x}. *) +(* Proof. *) +(* induction a. *) +(* - hauto lq:on inv:HRed.R unfold:relations.nf. *) +(* - hauto lq:on inv:HRed.R unfold:relations.nf. *) +(* - clear IHa2. *) +(* destruct IHa1. *) +(* destruct a1. *) + +Fixpoint hred {n} (a : PTm n) : option (PTm n) := + match a with + | VarPTm i => None + | PAbs a => None + | PApp (PAbs a) b => Some (subst_PTm (scons b VarPTm) a) + | PApp a b => + match hred a with + | Some a => Some (PApp a b) + | None => None + end + | PPair a b => None + | PProj p (PPair a b) => if p is PL then Some a else Some b + | PProj p a => + match hred a with + | Some a => Some (PProj p a) + | None => None + end + | PUniv i => None + | PBind p A B => None + | PBot => None + | PNat => None + | PZero => None + | PSuc a => None + | PInd P PZero b c => Some b + | PInd P (PSuc a) b c => + Some (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) + | PInd P a b c => + match hred a with + | Some a => Some (PInd P a b c) + | None => None + end + end. + +Lemma hred_complete n (a b : PTm n) : + HRed.R a b -> hred a = Some b. +Proof. + induction 1; hauto lq:on rew:off inv:HRed.R b:on. +Qed. + +Lemma hred_sound n (a b : PTm n): + hred a = Some b -> HRed.R a b. +Proof. + elim : a b; hauto q:on dep:on ctrs:HRed.R. +Qed. + +Lemma hred_deter n (a b0 b1 : PTm n) : + HRed.R a b0 -> HRed.R a b1 -> b0 = b1. +Proof. + move /hred_complete => + /hred_complete. congruence. +Qed. + +Definition hred_fancy n (a : PTm n) : + relations.nf HRed.R a + {x | HRed.R a x}. +Proof. + destruct (hred a) as [a'|] eqn:eq . + - right. exists a'. hauto q:on use:hred_sound. + - left. + move => [a' h]. + move /hred_complete in h. + congruence. +Defined. + +Ltac check_equal_triv := + lazymatch goal with + (* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *) + | [h : algo_dom _ _ |- _] => try inversion h; by subst + | _ => idtac + end. + +Lemma algo_dom_hne_abs_inv n (a : PTm n) b : + ishne a -> + algo_dom a (PAbs b) -> + algo_dom_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b. +Proof. + remember (PAbs b) as u. + destruct 2; try (exfalso; simpl in *; congruence). + injection Hequ. move => <-. + apply H1. +Defined. Equations check_equal {n} (a b : PTm n) (h : algo_dom a b) : bool by struct h := - check_equal a b h with (@idP (ishne a || ishf a)) := { - | Bool.ReflectT _ _ => _ - | Bool.ReflectF _ _ => _ - }. + check_equal (VarPTm i) (VarPTm j) h := fin_beq i j; + check_equal (PAbs a) (PAbs b) h := check_equal_r a b ltac:(check_equal_triv); + check_equal (PAbs a) b h := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv); + check_equal a (PAbs b) h := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv); + check_equal (PPair a0 b0) (PPair a1 b1) h := + check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); + check_equal (PPair a0 b0) u h := + check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv); + check_equal u (PPair a1 b1) h := + check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv); + check_equal (PBind p0 A0 B0) (PBind p1 A1 B1) h := + BTag_beq p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv); + check_equal PNat PNat _ := true; + check_equal PZero PZero _ := true; + check_equal (PSuc a) (PSuc b) h := check_equal_r a b ltac:(check_equal_triv); + check_equal (PUniv i) (PUniv j) _ := Nat.eqb i j; + check_equal a b h := false; + with check_equal_r {n} (a b : PTm n) (h : algo_dom_r a b) : + bool by struct h := + check_equal_r a b h with hred_fancy _ a => + { check_equal_r a b h (inr a') := check_equal_r (proj1_sig a') b _; + check_equal_r a b h (inl _) with hred_fancy _ b => + { check_equal_r a b h (inl _) (inl _) := check_equal a b _; + check_equal_r a b h (inl _) (inr b') := check_equal_r a (proj1_sig b') _}} . - (* check_equal (VarPTm i) (VarPTm j) h := fin_eq i j; *) - (* check_equal (PAbs a) (PAbs b) h := check_equal a b _; *) - (* check_equal (PPair a0 b0) (PPair a1 b1) h := *) - (* check_equal a0 b0 _ && check_equal a1 b1 _; *) - (* check_equal (PUniv i) (PUniv j) _ := _; *) +Next Obligation. + move => /= ih ihr n a nfa b nfb. + inversion 1; subst=>//=. + exfalso. sfirstorder. + exfalso. sfirstorder. +Defined. + Next Obligation. simpl. - intros ih. -Admitted. + move => /= ih ihr n a nfa b [b' hb']. + inversion 1; subst =>//=. + exfalso. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred. + exfalso. sfirstorder. + have ? : b' = b'0 by eauto using hred_deter. + subst. + assumption. +Defined. + +Next Obligation. + simpl => ih ihr n a [a' ha'] b. + inversion 1; subst => //=. + exfalso. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred. + suff ? : a'0 = a' by subst; assumption. + by eauto using hred_deter. + exfalso. hauto lq:on use:hf_no_hred, hne_no_hred. +Defined. + Search (Bool.reflect (is_true _) _). Check idP. From 6c11f5560db3ba1b043430d9815d3e68691754ac Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 27 Feb 2025 20:56:01 -0500 Subject: [PATCH 02/10] Need noconfusion? --- theories/executable.v | 30 +++++++++++++++++++----------- 1 file changed, 19 insertions(+), 11 deletions(-) diff --git a/theories/executable.v b/theories/executable.v index 144979d..dd7d2aa 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -93,7 +93,11 @@ with algo_dom_r {n} : PTm n -> PTm n -> Prop := algo_dom_r a b. Derive Signature for algo_dom algo_dom_r. - +Derive NoConfusion for PTm. +Next Obligation. +Admitted. +Next Obligation. +Admitted. Derive Dependent Inversion adom_inv with (forall n (a b : PTm n), algo_dom a b) Sort Prop. @@ -230,22 +234,26 @@ Proof. Defined. Ltac check_equal_triv := + intros;subst; lazymatch goal with (* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *) | [h : algo_dom _ _ |- _] => try inversion h; by subst | _ => idtac end. -Lemma algo_dom_hne_abs_inv n (a : PTm n) b : - ishne a -> - algo_dom a (PAbs b) -> - algo_dom_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b. -Proof. - remember (PAbs b) as u. - destruct 2; try (exfalso; simpl in *; congruence). - injection Hequ. move => <-. - apply H1. -Defined. +(* Program Fixpoint check_equal {n} (a b : PTm n) (h : algo_dom a b) {struct h} : bool := *) +(* match a, b with *) +(* | VarPTm i, VarPTm j => fin_beq i j *) +(* | PAbs a, PAbs b => check_equal_r a b ltac:(check_equal_triv) *) +(* | _, _ => false *) +(* end *) +(* with check_equal_r {n} (a b : PTm n) (h : algo_dom_r a b) {struct h} : bool := *) +(* match hred_fancy _ a with *) +(* | inr a' => check_equal_r (proj1_sig a') b _ *) +(* | _ => false *) +(* end. *) +(* Next Obligation. *) +(* simpl. *) Equations check_equal {n} (a b : PTm n) (h : algo_dom a b) : bool by struct h := From 7503dea251bdba7aabf005f89c57fe0a28f90741 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 27 Feb 2025 21:33:25 -0500 Subject: [PATCH 03/10] Seems to work but takes a million years to type check --- Makefile | 2 +- theories/Autosubst2/syntax.v | 789 ++++++++++++--------------------- theories/Autosubst2/unscoped.v | 213 +++++++++ theories/common.v | 1 + theories/executable.v | 147 +++--- 5 files changed, 580 insertions(+), 572 deletions(-) create mode 100644 theories/Autosubst2/unscoped.v diff --git a/Makefile b/Makefile index ef5b76f..3c879f6 100644 --- a/Makefile +++ b/Makefile @@ -16,7 +16,7 @@ uninstall: $(COQMAKEFILE) $(MAKE) -f $(COQMAKEFILE) uninstall theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v : syntax.sig - autosubst -f -v ge813 -s coq -o theories/Autosubst2/syntax.v syntax.sig + autosubst -f -v ge813 -s ucoq -o theories/Autosubst2/syntax.v syntax.sig .PHONY: clean FORCE diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v index 5d04c05..3d1e1f6 100644 --- a/theories/Autosubst2/syntax.v +++ b/theories/Autosubst2/syntax.v @@ -1,4 +1,4 @@ -Require Import core fintype. +Require Import core unscoped. Require Import Setoid Morphisms Relation_Definitions. @@ -33,221 +33,177 @@ Proof. exact (eq_refl). Qed. -Inductive PTm (n_PTm : nat) : Type := - | VarPTm : fin n_PTm -> PTm n_PTm - | PAbs : PTm (S n_PTm) -> PTm n_PTm - | PApp : PTm n_PTm -> PTm n_PTm -> PTm n_PTm - | PPair : PTm n_PTm -> PTm n_PTm -> PTm n_PTm - | PProj : PTag -> PTm n_PTm -> PTm n_PTm - | PBind : BTag -> PTm n_PTm -> PTm (S n_PTm) -> PTm n_PTm - | PUniv : nat -> PTm n_PTm - | PBot : PTm n_PTm - | PNat : PTm n_PTm - | PZero : PTm n_PTm - | PSuc : PTm n_PTm -> PTm n_PTm - | PInd : - PTm (S n_PTm) -> - PTm n_PTm -> PTm n_PTm -> PTm (S (S n_PTm)) -> PTm n_PTm. +Inductive PTm : Type := + | VarPTm : nat -> PTm + | PAbs : PTm -> PTm + | PApp : PTm -> PTm -> PTm + | PPair : PTm -> PTm -> PTm + | PProj : PTag -> PTm -> PTm + | PBind : BTag -> PTm -> PTm -> PTm + | PUniv : nat -> PTm + | PBot : PTm + | PNat : PTm + | PZero : PTm + | PSuc : PTm -> PTm + | PInd : PTm -> PTm -> PTm -> PTm -> PTm. -Lemma congr_PAbs {m_PTm : nat} {s0 : PTm (S m_PTm)} {t0 : PTm (S m_PTm)} - (H0 : s0 = t0) : PAbs m_PTm s0 = PAbs m_PTm t0. +Lemma congr_PAbs {s0 : PTm} {t0 : PTm} (H0 : s0 = t0) : PAbs s0 = PAbs t0. Proof. -exact (eq_trans eq_refl (ap (fun x => PAbs m_PTm x) H0)). +exact (eq_trans eq_refl (ap (fun x => PAbs x) H0)). Qed. -Lemma congr_PApp {m_PTm : nat} {s0 : PTm m_PTm} {s1 : PTm m_PTm} - {t0 : PTm m_PTm} {t1 : PTm m_PTm} (H0 : s0 = t0) (H1 : s1 = t1) : - PApp m_PTm s0 s1 = PApp m_PTm t0 t1. +Lemma congr_PApp {s0 : PTm} {s1 : PTm} {t0 : PTm} {t1 : PTm} (H0 : s0 = t0) + (H1 : s1 = t1) : PApp s0 s1 = PApp t0 t1. Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => PApp m_PTm x s1) H0)) - (ap (fun x => PApp m_PTm t0 x) H1)). +exact (eq_trans (eq_trans eq_refl (ap (fun x => PApp x s1) H0)) + (ap (fun x => PApp t0 x) H1)). Qed. -Lemma congr_PPair {m_PTm : nat} {s0 : PTm m_PTm} {s1 : PTm m_PTm} - {t0 : PTm m_PTm} {t1 : PTm m_PTm} (H0 : s0 = t0) (H1 : s1 = t1) : - PPair m_PTm s0 s1 = PPair m_PTm t0 t1. +Lemma congr_PPair {s0 : PTm} {s1 : PTm} {t0 : PTm} {t1 : PTm} (H0 : s0 = t0) + (H1 : s1 = t1) : PPair s0 s1 = PPair t0 t1. Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => PPair m_PTm x s1) H0)) - (ap (fun x => PPair m_PTm t0 x) H1)). +exact (eq_trans (eq_trans eq_refl (ap (fun x => PPair x s1) H0)) + (ap (fun x => PPair t0 x) H1)). Qed. -Lemma congr_PProj {m_PTm : nat} {s0 : PTag} {s1 : PTm m_PTm} {t0 : PTag} - {t1 : PTm m_PTm} (H0 : s0 = t0) (H1 : s1 = t1) : - PProj m_PTm s0 s1 = PProj m_PTm t0 t1. +Lemma congr_PProj {s0 : PTag} {s1 : PTm} {t0 : PTag} {t1 : PTm} + (H0 : s0 = t0) (H1 : s1 = t1) : PProj s0 s1 = PProj t0 t1. Proof. -exact (eq_trans (eq_trans eq_refl (ap (fun x => PProj m_PTm x s1) H0)) - (ap (fun x => PProj m_PTm t0 x) H1)). +exact (eq_trans (eq_trans eq_refl (ap (fun x => PProj x s1) H0)) + (ap (fun x => PProj t0 x) H1)). Qed. -Lemma congr_PBind {m_PTm : nat} {s0 : BTag} {s1 : PTm m_PTm} - {s2 : PTm (S m_PTm)} {t0 : BTag} {t1 : PTm m_PTm} {t2 : PTm (S m_PTm)} - (H0 : s0 = t0) (H1 : s1 = t1) (H2 : s2 = t2) : - PBind m_PTm s0 s1 s2 = PBind m_PTm t0 t1 t2. +Lemma congr_PBind {s0 : BTag} {s1 : PTm} {s2 : PTm} {t0 : BTag} {t1 : PTm} + {t2 : PTm} (H0 : s0 = t0) (H1 : s1 = t1) (H2 : s2 = t2) : + PBind s0 s1 s2 = PBind t0 t1 t2. Proof. exact (eq_trans - (eq_trans (eq_trans eq_refl (ap (fun x => PBind m_PTm x s1 s2) H0)) - (ap (fun x => PBind m_PTm t0 x s2) H1)) - (ap (fun x => PBind m_PTm t0 t1 x) H2)). + (eq_trans (eq_trans eq_refl (ap (fun x => PBind x s1 s2) H0)) + (ap (fun x => PBind t0 x s2) H1)) + (ap (fun x => PBind t0 t1 x) H2)). Qed. -Lemma congr_PUniv {m_PTm : nat} {s0 : nat} {t0 : nat} (H0 : s0 = t0) : - PUniv m_PTm s0 = PUniv m_PTm t0. +Lemma congr_PUniv {s0 : nat} {t0 : nat} (H0 : s0 = t0) : PUniv s0 = PUniv t0. Proof. -exact (eq_trans eq_refl (ap (fun x => PUniv m_PTm x) H0)). +exact (eq_trans eq_refl (ap (fun x => PUniv x) H0)). Qed. -Lemma congr_PBot {m_PTm : nat} : PBot m_PTm = PBot m_PTm. +Lemma congr_PBot : PBot = PBot. Proof. exact (eq_refl). Qed. -Lemma congr_PNat {m_PTm : nat} : PNat m_PTm = PNat m_PTm. +Lemma congr_PNat : PNat = PNat. Proof. exact (eq_refl). Qed. -Lemma congr_PZero {m_PTm : nat} : PZero m_PTm = PZero m_PTm. +Lemma congr_PZero : PZero = PZero. Proof. exact (eq_refl). Qed. -Lemma congr_PSuc {m_PTm : nat} {s0 : PTm m_PTm} {t0 : PTm m_PTm} - (H0 : s0 = t0) : PSuc m_PTm s0 = PSuc m_PTm t0. +Lemma congr_PSuc {s0 : PTm} {t0 : PTm} (H0 : s0 = t0) : PSuc s0 = PSuc t0. Proof. -exact (eq_trans eq_refl (ap (fun x => PSuc m_PTm x) H0)). +exact (eq_trans eq_refl (ap (fun x => PSuc x) H0)). Qed. -Lemma congr_PInd {m_PTm : nat} {s0 : PTm (S m_PTm)} {s1 : PTm m_PTm} - {s2 : PTm m_PTm} {s3 : PTm (S (S m_PTm))} {t0 : PTm (S m_PTm)} - {t1 : PTm m_PTm} {t2 : PTm m_PTm} {t3 : PTm (S (S m_PTm))} (H0 : s0 = t0) - (H1 : s1 = t1) (H2 : s2 = t2) (H3 : s3 = t3) : - PInd m_PTm s0 s1 s2 s3 = PInd m_PTm t0 t1 t2 t3. +Lemma congr_PInd {s0 : PTm} {s1 : PTm} {s2 : PTm} {s3 : PTm} {t0 : PTm} + {t1 : PTm} {t2 : PTm} {t3 : PTm} (H0 : s0 = t0) (H1 : s1 = t1) + (H2 : s2 = t2) (H3 : s3 = t3) : PInd s0 s1 s2 s3 = PInd t0 t1 t2 t3. Proof. exact (eq_trans (eq_trans - (eq_trans - (eq_trans eq_refl (ap (fun x => PInd m_PTm x s1 s2 s3) H0)) - (ap (fun x => PInd m_PTm t0 x s2 s3) H1)) - (ap (fun x => PInd m_PTm t0 t1 x s3) H2)) - (ap (fun x => PInd m_PTm t0 t1 t2 x) H3)). + (eq_trans (eq_trans eq_refl (ap (fun x => PInd x s1 s2 s3) H0)) + (ap (fun x => PInd t0 x s2 s3) H1)) + (ap (fun x => PInd t0 t1 x s3) H2)) + (ap (fun x => PInd t0 t1 t2 x) H3)). Qed. -Lemma upRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n) : - fin (S m) -> fin (S n). +Lemma upRen_PTm_PTm (xi : nat -> nat) : nat -> nat. Proof. exact (up_ren xi). Defined. -Lemma upRen_list_PTm_PTm (p : nat) {m : nat} {n : nat} (xi : fin m -> fin n) - : fin (plus p m) -> fin (plus p n). -Proof. -exact (upRen_p p xi). -Defined. - -Fixpoint ren_PTm {m_PTm : nat} {n_PTm : nat} -(xi_PTm : fin m_PTm -> fin n_PTm) (s : PTm m_PTm) {struct s} : PTm n_PTm := +Fixpoint ren_PTm (xi_PTm : nat -> nat) (s : PTm) {struct s} : PTm := match s with - | VarPTm _ s0 => VarPTm n_PTm (xi_PTm s0) - | PAbs _ s0 => PAbs n_PTm (ren_PTm (upRen_PTm_PTm xi_PTm) s0) - | PApp _ s0 s1 => PApp n_PTm (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) - | PPair _ s0 s1 => PPair n_PTm (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) - | PProj _ s0 s1 => PProj n_PTm s0 (ren_PTm xi_PTm s1) - | PBind _ s0 s1 s2 => - PBind n_PTm s0 (ren_PTm xi_PTm s1) (ren_PTm (upRen_PTm_PTm xi_PTm) s2) - | PUniv _ s0 => PUniv n_PTm s0 - | PBot _ => PBot n_PTm - | PNat _ => PNat n_PTm - | PZero _ => PZero n_PTm - | PSuc _ s0 => PSuc n_PTm (ren_PTm xi_PTm s0) - | PInd _ s0 s1 s2 s3 => - PInd n_PTm (ren_PTm (upRen_PTm_PTm xi_PTm) s0) (ren_PTm xi_PTm s1) + | VarPTm s0 => VarPTm (xi_PTm s0) + | PAbs s0 => PAbs (ren_PTm (upRen_PTm_PTm xi_PTm) s0) + | PApp s0 s1 => PApp (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) + | PPair s0 s1 => PPair (ren_PTm xi_PTm s0) (ren_PTm xi_PTm s1) + | PProj s0 s1 => PProj s0 (ren_PTm xi_PTm s1) + | PBind s0 s1 s2 => + PBind s0 (ren_PTm xi_PTm s1) (ren_PTm (upRen_PTm_PTm xi_PTm) s2) + | PUniv s0 => PUniv s0 + | PBot => PBot + | PNat => PNat + | PZero => PZero + | PSuc s0 => PSuc (ren_PTm xi_PTm s0) + | PInd s0 s1 s2 s3 => + PInd (ren_PTm (upRen_PTm_PTm xi_PTm) s0) (ren_PTm xi_PTm s1) (ren_PTm xi_PTm s2) (ren_PTm (upRen_PTm_PTm (upRen_PTm_PTm xi_PTm)) s3) end. -Lemma up_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) : - fin (S m) -> PTm (S n_PTm). +Lemma up_PTm_PTm (sigma : nat -> PTm) : nat -> PTm. Proof. -exact (scons (VarPTm (S n_PTm) var_zero) (funcomp (ren_PTm shift) sigma)). +exact (scons (VarPTm var_zero) (funcomp (ren_PTm shift) sigma)). Defined. -Lemma up_list_PTm_PTm (p : nat) {m : nat} {n_PTm : nat} - (sigma : fin m -> PTm n_PTm) : fin (plus p m) -> PTm (plus p n_PTm). -Proof. -exact (scons_p p (funcomp (VarPTm (plus p n_PTm)) (zero_p p)) - (funcomp (ren_PTm (shift_p p)) sigma)). -Defined. - -Fixpoint subst_PTm {m_PTm : nat} {n_PTm : nat} -(sigma_PTm : fin m_PTm -> PTm n_PTm) (s : PTm m_PTm) {struct s} : PTm n_PTm -:= +Fixpoint subst_PTm (sigma_PTm : nat -> PTm) (s : PTm) {struct s} : PTm := match s with - | VarPTm _ s0 => sigma_PTm s0 - | PAbs _ s0 => PAbs n_PTm (subst_PTm (up_PTm_PTm sigma_PTm) s0) - | PApp _ s0 s1 => - PApp n_PTm (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1) - | PPair _ s0 s1 => - PPair n_PTm (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1) - | PProj _ s0 s1 => PProj n_PTm s0 (subst_PTm sigma_PTm s1) - | PBind _ s0 s1 s2 => - PBind n_PTm s0 (subst_PTm sigma_PTm s1) - (subst_PTm (up_PTm_PTm sigma_PTm) s2) - | PUniv _ s0 => PUniv n_PTm s0 - | PBot _ => PBot n_PTm - | PNat _ => PNat n_PTm - | PZero _ => PZero n_PTm - | PSuc _ s0 => PSuc n_PTm (subst_PTm sigma_PTm s0) - | PInd _ s0 s1 s2 s3 => - PInd n_PTm (subst_PTm (up_PTm_PTm sigma_PTm) s0) - (subst_PTm sigma_PTm s1) (subst_PTm sigma_PTm s2) + | VarPTm s0 => sigma_PTm s0 + | PAbs s0 => PAbs (subst_PTm (up_PTm_PTm sigma_PTm) s0) + | PApp s0 s1 => PApp (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1) + | PPair s0 s1 => PPair (subst_PTm sigma_PTm s0) (subst_PTm sigma_PTm s1) + | PProj s0 s1 => PProj s0 (subst_PTm sigma_PTm s1) + | PBind s0 s1 s2 => + PBind s0 (subst_PTm sigma_PTm s1) (subst_PTm (up_PTm_PTm sigma_PTm) s2) + | PUniv s0 => PUniv s0 + | PBot => PBot + | PNat => PNat + | PZero => PZero + | PSuc s0 => PSuc (subst_PTm sigma_PTm s0) + | PInd s0 s1 s2 s3 => + PInd (subst_PTm (up_PTm_PTm sigma_PTm) s0) (subst_PTm sigma_PTm s1) + (subst_PTm sigma_PTm s2) (subst_PTm (up_PTm_PTm (up_PTm_PTm sigma_PTm)) s3) end. -Lemma upId_PTm_PTm {m_PTm : nat} (sigma : fin m_PTm -> PTm m_PTm) - (Eq : forall x, sigma x = VarPTm m_PTm x) : - forall x, up_PTm_PTm sigma x = VarPTm (S m_PTm) x. +Lemma upId_PTm_PTm (sigma : nat -> PTm) (Eq : forall x, sigma x = VarPTm x) : + forall x, up_PTm_PTm sigma x = VarPTm x. Proof. exact (fun n => match n with - | Some fin_n => ap (ren_PTm shift) (Eq fin_n) - | None => eq_refl + | S n' => ap (ren_PTm shift) (Eq n') + | O => eq_refl end). Qed. -Lemma upId_list_PTm_PTm {p : nat} {m_PTm : nat} - (sigma : fin m_PTm -> PTm m_PTm) (Eq : forall x, sigma x = VarPTm m_PTm x) - : forall x, up_list_PTm_PTm p sigma x = VarPTm (plus p m_PTm) x. -Proof. -exact (fun n => - scons_p_eta (VarPTm (plus p m_PTm)) - (fun n => ap (ren_PTm (shift_p p)) (Eq n)) (fun n => eq_refl)). -Qed. - -Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm) -(Eq_PTm : forall x, sigma_PTm x = VarPTm m_PTm x) (s : PTm m_PTm) {struct s} - : subst_PTm sigma_PTm s = s := +Fixpoint idSubst_PTm (sigma_PTm : nat -> PTm) +(Eq_PTm : forall x, sigma_PTm x = VarPTm x) (s : PTm) {struct s} : +subst_PTm sigma_PTm s = s := match s with - | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 => + | VarPTm s0 => Eq_PTm s0 + | PAbs s0 => congr_PAbs (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s0) - | PApp _ s0 s1 => + | PApp s0 s1 => congr_PApp (idSubst_PTm sigma_PTm Eq_PTm s0) (idSubst_PTm sigma_PTm Eq_PTm s1) - | PPair _ s0 s1 => + | PPair s0 s1 => congr_PPair (idSubst_PTm sigma_PTm Eq_PTm s0) (idSubst_PTm sigma_PTm Eq_PTm s1) - | PProj _ s0 s1 => - congr_PProj (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1) - | PBind _ s0 s1 s2 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1) + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (idSubst_PTm sigma_PTm Eq_PTm s1) (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => congr_PSuc (idSubst_PTm sigma_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (idSubst_PTm sigma_PTm Eq_PTm s0) + | PInd s0 s1 s2 s3 => congr_PInd (idSubst_PTm (up_PTm_PTm sigma_PTm) (upId_PTm_PTm _ Eq_PTm) s0) (idSubst_PTm sigma_PTm Eq_PTm s1) (idSubst_PTm sigma_PTm Eq_PTm s2) @@ -255,54 +211,43 @@ Fixpoint idSubst_PTm {m_PTm : nat} (sigma_PTm : fin m_PTm -> PTm m_PTm) (upId_PTm_PTm _ (upId_PTm_PTm _ Eq_PTm)) s3) end. -Lemma upExtRen_PTm_PTm {m : nat} {n : nat} (xi : fin m -> fin n) - (zeta : fin m -> fin n) (Eq : forall x, xi x = zeta x) : +Lemma upExtRen_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat) + (Eq : forall x, xi x = zeta x) : forall x, upRen_PTm_PTm xi x = upRen_PTm_PTm zeta x. Proof. -exact (fun n => - match n with - | Some fin_n => ap shift (Eq fin_n) - | None => eq_refl - end). +exact (fun n => match n with + | S n' => ap shift (Eq n') + | O => eq_refl + end). Qed. -Lemma upExtRen_list_PTm_PTm {p : nat} {m : nat} {n : nat} - (xi : fin m -> fin n) (zeta : fin m -> fin n) - (Eq : forall x, xi x = zeta x) : - forall x, upRen_list_PTm_PTm p xi x = upRen_list_PTm_PTm p zeta x. -Proof. -exact (fun n => - scons_p_congr (fun n => eq_refl) (fun n => ap (shift_p p) (Eq n))). -Qed. - -Fixpoint extRen_PTm {m_PTm : nat} {n_PTm : nat} -(xi_PTm : fin m_PTm -> fin n_PTm) (zeta_PTm : fin m_PTm -> fin n_PTm) -(Eq_PTm : forall x, xi_PTm x = zeta_PTm x) (s : PTm m_PTm) {struct s} : +Fixpoint extRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) +(Eq_PTm : forall x, xi_PTm x = zeta_PTm x) (s : PTm) {struct s} : ren_PTm xi_PTm s = ren_PTm zeta_PTm s := match s with - | VarPTm _ s0 => ap (VarPTm n_PTm) (Eq_PTm s0) - | PAbs _ s0 => + | VarPTm s0 => ap (VarPTm) (Eq_PTm s0) + | PAbs s0 => congr_PAbs (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) (upExtRen_PTm_PTm _ _ Eq_PTm) s0) - | PApp _ s0 s1 => + | PApp s0 s1 => congr_PApp (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) - | PPair _ s0 s1 => + | PPair s0 s1 => congr_PPair (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) - | PProj _ s0 s1 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (extRen_PTm xi_PTm zeta_PTm Eq_PTm s1) (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) (upExtRen_PTm_PTm _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => congr_PSuc (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (extRen_PTm xi_PTm zeta_PTm Eq_PTm s0) + | PInd s0 s1 s2 s3 => congr_PInd (extRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) (upExtRen_PTm_PTm _ _ Eq_PTm) s0) @@ -313,55 +258,44 @@ ren_PTm xi_PTm s = ren_PTm zeta_PTm s := (upExtRen_PTm_PTm _ _ (upExtRen_PTm_PTm _ _ Eq_PTm)) s3) end. -Lemma upExt_PTm_PTm {m : nat} {n_PTm : nat} (sigma : fin m -> PTm n_PTm) - (tau : fin m -> PTm n_PTm) (Eq : forall x, sigma x = tau x) : +Lemma upExt_PTm_PTm (sigma : nat -> PTm) (tau : nat -> PTm) + (Eq : forall x, sigma x = tau x) : forall x, up_PTm_PTm sigma x = up_PTm_PTm tau x. Proof. exact (fun n => match n with - | Some fin_n => ap (ren_PTm shift) (Eq fin_n) - | None => eq_refl + | S n' => ap (ren_PTm shift) (Eq n') + | O => eq_refl end). Qed. -Lemma upExt_list_PTm_PTm {p : nat} {m : nat} {n_PTm : nat} - (sigma : fin m -> PTm n_PTm) (tau : fin m -> PTm n_PTm) - (Eq : forall x, sigma x = tau x) : - forall x, up_list_PTm_PTm p sigma x = up_list_PTm_PTm p tau x. -Proof. -exact (fun n => - scons_p_congr (fun n => eq_refl) - (fun n => ap (ren_PTm (shift_p p)) (Eq n))). -Qed. - -Fixpoint ext_PTm {m_PTm : nat} {n_PTm : nat} -(sigma_PTm : fin m_PTm -> PTm n_PTm) (tau_PTm : fin m_PTm -> PTm n_PTm) -(Eq_PTm : forall x, sigma_PTm x = tau_PTm x) (s : PTm m_PTm) {struct s} : +Fixpoint ext_PTm (sigma_PTm : nat -> PTm) (tau_PTm : nat -> PTm) +(Eq_PTm : forall x, sigma_PTm x = tau_PTm x) (s : PTm) {struct s} : subst_PTm sigma_PTm s = subst_PTm tau_PTm s := match s with - | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 => + | VarPTm s0 => Eq_PTm s0 + | PAbs s0 => congr_PAbs (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) (upExt_PTm_PTm _ _ Eq_PTm) s0) - | PApp _ s0 s1 => + | PApp s0 s1 => congr_PApp (ext_PTm sigma_PTm tau_PTm Eq_PTm s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) - | PPair _ s0 s1 => + | PPair s0 s1 => congr_PPair (ext_PTm sigma_PTm tau_PTm Eq_PTm s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) - | PProj _ s0 s1 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (ext_PTm sigma_PTm tau_PTm Eq_PTm s1) (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) (upExt_PTm_PTm _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => congr_PSuc (ext_PTm sigma_PTm tau_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (ext_PTm sigma_PTm tau_PTm Eq_PTm s0) + | PInd s0 s1 s2 s3 => congr_PInd (ext_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) (upExt_PTm_PTm _ _ Eq_PTm) s0) @@ -372,57 +306,44 @@ subst_PTm sigma_PTm s = subst_PTm tau_PTm s := (upExt_PTm_PTm _ _ (upExt_PTm_PTm _ _ Eq_PTm)) s3) end. -Lemma up_ren_ren_PTm_PTm {k : nat} {l : nat} {m : nat} (xi : fin k -> fin l) - (zeta : fin l -> fin m) (rho : fin k -> fin m) - (Eq : forall x, funcomp zeta xi x = rho x) : +Lemma up_ren_ren_PTm_PTm (xi : nat -> nat) (zeta : nat -> nat) + (rho : nat -> nat) (Eq : forall x, funcomp zeta xi x = rho x) : forall x, funcomp (upRen_PTm_PTm zeta) (upRen_PTm_PTm xi) x = upRen_PTm_PTm rho x. Proof. exact (up_ren_ren xi zeta rho Eq). Qed. -Lemma up_ren_ren_list_PTm_PTm {p : nat} {k : nat} {l : nat} {m : nat} - (xi : fin k -> fin l) (zeta : fin l -> fin m) (rho : fin k -> fin m) - (Eq : forall x, funcomp zeta xi x = rho x) : - forall x, - funcomp (upRen_list_PTm_PTm p zeta) (upRen_list_PTm_PTm p xi) x = - upRen_list_PTm_PTm p rho x. -Proof. -exact (up_ren_ren_p Eq). -Qed. - -Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} -(xi_PTm : fin m_PTm -> fin k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) -(rho_PTm : fin m_PTm -> fin l_PTm) -(Eq_PTm : forall x, funcomp zeta_PTm xi_PTm x = rho_PTm x) (s : PTm m_PTm) -{struct s} : ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm rho_PTm s := +Fixpoint compRenRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) +(rho_PTm : nat -> nat) +(Eq_PTm : forall x, funcomp zeta_PTm xi_PTm x = rho_PTm x) (s : PTm) {struct + s} : ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm rho_PTm s := match s with - | VarPTm _ s0 => ap (VarPTm l_PTm) (Eq_PTm s0) - | PAbs _ s0 => + | VarPTm s0 => ap (VarPTm) (Eq_PTm s0) + | PAbs s0 => congr_PAbs (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s0) - | PApp _ s0 s1 => + | PApp s0 s1 => congr_PApp (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0) (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) - | PPair _ s0 s1 => + | PPair s0 s1 => congr_PPair (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0) (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) - | PProj _ s0 s1 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s1) (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => - congr_PSuc (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (compRenRen_PTm xi_PTm zeta_PTm rho_PTm Eq_PTm s0) + | PInd s0 s1 s2 s3 => congr_PInd (compRenRen_PTm (upRen_PTm_PTm xi_PTm) (upRen_PTm_PTm zeta_PTm) (upRen_PTm_PTm rho_PTm) (up_ren_ren _ _ _ Eq_PTm) s0) @@ -434,66 +355,49 @@ Fixpoint compRenRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} (up_ren_ren _ _ _ (up_ren_ren _ _ _ Eq_PTm)) s3) end. -Lemma up_ren_subst_PTm_PTm {k : nat} {l : nat} {m_PTm : nat} - (xi : fin k -> fin l) (tau : fin l -> PTm m_PTm) - (theta : fin k -> PTm m_PTm) (Eq : forall x, funcomp tau xi x = theta x) : +Lemma up_ren_subst_PTm_PTm (xi : nat -> nat) (tau : nat -> PTm) + (theta : nat -> PTm) (Eq : forall x, funcomp tau xi x = theta x) : forall x, funcomp (up_PTm_PTm tau) (upRen_PTm_PTm xi) x = up_PTm_PTm theta x. Proof. exact (fun n => match n with - | Some fin_n => ap (ren_PTm shift) (Eq fin_n) - | None => eq_refl + | S n' => ap (ren_PTm shift) (Eq n') + | O => eq_refl end). Qed. -Lemma up_ren_subst_list_PTm_PTm {p : nat} {k : nat} {l : nat} {m_PTm : nat} - (xi : fin k -> fin l) (tau : fin l -> PTm m_PTm) - (theta : fin k -> PTm m_PTm) (Eq : forall x, funcomp tau xi x = theta x) : - forall x, - funcomp (up_list_PTm_PTm p tau) (upRen_list_PTm_PTm p xi) x = - up_list_PTm_PTm p theta x. -Proof. -exact (fun n => - eq_trans (scons_p_comp' _ _ _ n) - (scons_p_congr (fun z => scons_p_head' _ _ z) - (fun z => - eq_trans (scons_p_tail' _ _ (xi z)) - (ap (ren_PTm (shift_p p)) (Eq z))))). -Qed. - -Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} -(xi_PTm : fin m_PTm -> fin k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) -(theta_PTm : fin m_PTm -> PTm l_PTm) -(Eq_PTm : forall x, funcomp tau_PTm xi_PTm x = theta_PTm x) (s : PTm m_PTm) -{struct s} : subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm theta_PTm s := +Fixpoint compRenSubst_PTm (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm) +(theta_PTm : nat -> PTm) +(Eq_PTm : forall x, funcomp tau_PTm xi_PTm x = theta_PTm x) (s : PTm) {struct + s} : subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm theta_PTm s := match s with - | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 => + | VarPTm s0 => Eq_PTm s0 + | PAbs s0 => congr_PAbs (compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm) (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s0) - | PApp _ s0 s1 => + | PApp s0 s1 => congr_PApp (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0) (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) - | PPair _ s0 s1 => + | PPair s0 s1 => congr_PPair (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0) (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) - | PProj _ s0 s1 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s1) (compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm) (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (compRenSubst_PTm xi_PTm tau_PTm theta_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PInd s0 s1 s2 s3 => congr_PInd (compRenSubst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm tau_PTm) (up_PTm_PTm theta_PTm) (up_ren_subst_PTm_PTm _ _ _ Eq_PTm) s0) @@ -506,9 +410,8 @@ Fixpoint compRenSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} s3) end. -Lemma up_subst_ren_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat} - (sigma : fin k -> PTm l_PTm) (zeta_PTm : fin l_PTm -> fin m_PTm) - (theta : fin k -> PTm m_PTm) +Lemma up_subst_ren_PTm_PTm (sigma : nat -> PTm) (zeta_PTm : nat -> nat) + (theta : nat -> PTm) (Eq : forall x, funcomp (ren_PTm zeta_PTm) sigma x = theta x) : forall x, funcomp (ren_PTm (upRen_PTm_PTm zeta_PTm)) (up_PTm_PTm sigma) x = @@ -516,76 +419,51 @@ Lemma up_subst_ren_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat} Proof. exact (fun n => match n with - | Some fin_n => + | S n' => eq_trans (compRenRen_PTm shift (upRen_PTm_PTm zeta_PTm) - (funcomp shift zeta_PTm) (fun x => eq_refl) (sigma fin_n)) + (funcomp shift zeta_PTm) (fun x => eq_refl) (sigma n')) (eq_trans (eq_sym (compRenRen_PTm zeta_PTm shift (funcomp shift zeta_PTm) - (fun x => eq_refl) (sigma fin_n))) - (ap (ren_PTm shift) (Eq fin_n))) - | None => eq_refl + (fun x => eq_refl) (sigma n'))) + (ap (ren_PTm shift) (Eq n'))) + | O => eq_refl end). Qed. -Lemma up_subst_ren_list_PTm_PTm {p : nat} {k : nat} {l_PTm : nat} - {m_PTm : nat} (sigma : fin k -> PTm l_PTm) - (zeta_PTm : fin l_PTm -> fin m_PTm) (theta : fin k -> PTm m_PTm) - (Eq : forall x, funcomp (ren_PTm zeta_PTm) sigma x = theta x) : - forall x, - funcomp (ren_PTm (upRen_list_PTm_PTm p zeta_PTm)) (up_list_PTm_PTm p sigma) - x = up_list_PTm_PTm p theta x. -Proof. -exact (fun n => - eq_trans (scons_p_comp' _ _ _ n) - (scons_p_congr - (fun x => ap (VarPTm (plus p m_PTm)) (scons_p_head' _ _ x)) - (fun n => - eq_trans - (compRenRen_PTm (shift_p p) (upRen_list_PTm_PTm p zeta_PTm) - (funcomp (shift_p p) zeta_PTm) - (fun x => scons_p_tail' _ _ x) (sigma n)) - (eq_trans - (eq_sym - (compRenRen_PTm zeta_PTm (shift_p p) - (funcomp (shift_p p) zeta_PTm) (fun x => eq_refl) - (sigma n))) (ap (ren_PTm (shift_p p)) (Eq n)))))). -Qed. - -Fixpoint compSubstRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} -(sigma_PTm : fin m_PTm -> PTm k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) -(theta_PTm : fin m_PTm -> PTm l_PTm) +Fixpoint compSubstRen_PTm (sigma_PTm : nat -> PTm) (zeta_PTm : nat -> nat) +(theta_PTm : nat -> PTm) (Eq_PTm : forall x, funcomp (ren_PTm zeta_PTm) sigma_PTm x = theta_PTm x) -(s : PTm m_PTm) {struct s} : +(s : PTm) {struct s} : ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := match s with - | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 => + | VarPTm s0 => Eq_PTm s0 + | PAbs s0 => congr_PAbs (compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm) (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s0) - | PApp _ s0 s1 => + | PApp s0 s1 => congr_PApp (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0) (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) - | PPair _ s0 s1 => + | PPair s0 s1 => congr_PPair (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0) (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) - | PProj _ s0 s1 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s1) (compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm) (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (compSubstRen_PTm sigma_PTm zeta_PTm theta_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PInd s0 s1 s2 s3 => congr_PInd (compSubstRen_PTm (up_PTm_PTm sigma_PTm) (upRen_PTm_PTm zeta_PTm) (up_PTm_PTm theta_PTm) (up_subst_ren_PTm_PTm _ _ _ Eq_PTm) s0) @@ -598,9 +476,8 @@ ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := s3) end. -Lemma up_subst_subst_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat} - (sigma : fin k -> PTm l_PTm) (tau_PTm : fin l_PTm -> PTm m_PTm) - (theta : fin k -> PTm m_PTm) +Lemma up_subst_subst_PTm_PTm (sigma : nat -> PTm) (tau_PTm : nat -> PTm) + (theta : nat -> PTm) (Eq : forall x, funcomp (subst_PTm tau_PTm) sigma x = theta x) : forall x, funcomp (subst_PTm (up_PTm_PTm tau_PTm)) (up_PTm_PTm sigma) x = @@ -608,78 +485,52 @@ Lemma up_subst_subst_PTm_PTm {k : nat} {l_PTm : nat} {m_PTm : nat} Proof. exact (fun n => match n with - | Some fin_n => + | S n' => eq_trans (compRenSubst_PTm shift (up_PTm_PTm tau_PTm) (funcomp (up_PTm_PTm tau_PTm) shift) (fun x => eq_refl) - (sigma fin_n)) + (sigma n')) (eq_trans (eq_sym (compSubstRen_PTm tau_PTm shift (funcomp (ren_PTm shift) tau_PTm) (fun x => eq_refl) - (sigma fin_n))) (ap (ren_PTm shift) (Eq fin_n))) - | None => eq_refl + (sigma n'))) (ap (ren_PTm shift) (Eq n'))) + | O => eq_refl end). Qed. -Lemma up_subst_subst_list_PTm_PTm {p : nat} {k : nat} {l_PTm : nat} - {m_PTm : nat} (sigma : fin k -> PTm l_PTm) - (tau_PTm : fin l_PTm -> PTm m_PTm) (theta : fin k -> PTm m_PTm) - (Eq : forall x, funcomp (subst_PTm tau_PTm) sigma x = theta x) : - forall x, - funcomp (subst_PTm (up_list_PTm_PTm p tau_PTm)) (up_list_PTm_PTm p sigma) x = - up_list_PTm_PTm p theta x. -Proof. -exact (fun n => - eq_trans - (scons_p_comp' (funcomp (VarPTm (plus p l_PTm)) (zero_p p)) _ _ n) - (scons_p_congr - (fun x => scons_p_head' _ (fun z => ren_PTm (shift_p p) _) x) - (fun n => - eq_trans - (compRenSubst_PTm (shift_p p) (up_list_PTm_PTm p tau_PTm) - (funcomp (up_list_PTm_PTm p tau_PTm) (shift_p p)) - (fun x => eq_refl) (sigma n)) - (eq_trans - (eq_sym - (compSubstRen_PTm tau_PTm (shift_p p) _ - (fun x => eq_sym (scons_p_tail' _ _ x)) (sigma n))) - (ap (ren_PTm (shift_p p)) (Eq n)))))). -Qed. - -Fixpoint compSubstSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} -(sigma_PTm : fin m_PTm -> PTm k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) -(theta_PTm : fin m_PTm -> PTm l_PTm) +Fixpoint compSubstSubst_PTm (sigma_PTm : nat -> PTm) (tau_PTm : nat -> PTm) +(theta_PTm : nat -> PTm) (Eq_PTm : forall x, funcomp (subst_PTm tau_PTm) sigma_PTm x = theta_PTm x) -(s : PTm m_PTm) {struct s} : +(s : PTm) {struct s} : subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := match s with - | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 => + | VarPTm s0 => Eq_PTm s0 + | PAbs s0 => congr_PAbs (compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s0) - | PApp _ s0 s1 => + | PApp s0 s1 => congr_PApp (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0) (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) - | PPair _ s0 s1 => + | PPair s0 s1 => congr_PPair (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0) (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) - | PProj _ s0 s1 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s1) (compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (compSubstSubst_PTm sigma_PTm tau_PTm theta_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PInd s0 s1 s2 s3 => congr_PInd (compSubstSubst_PTm (up_PTm_PTm sigma_PTm) (up_PTm_PTm tau_PTm) (up_PTm_PTm theta_PTm) (up_subst_subst_PTm_PTm _ _ _ Eq_PTm) s0) @@ -692,126 +543,102 @@ subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm theta_PTm s := (up_subst_subst_PTm_PTm _ _ _ Eq_PTm)) s3) end. -Lemma renRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} - (xi_PTm : fin m_PTm -> fin k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) - (s : PTm m_PTm) : +Lemma renRen_PTm (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) (s : PTm) : ren_PTm zeta_PTm (ren_PTm xi_PTm s) = ren_PTm (funcomp zeta_PTm xi_PTm) s. Proof. exact (compRenRen_PTm xi_PTm zeta_PTm _ (fun n => eq_refl) s). Qed. -Lemma renRen'_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} - (xi_PTm : fin m_PTm -> fin k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) : +Lemma renRen'_PTm_pointwise (xi_PTm : nat -> nat) (zeta_PTm : nat -> nat) : pointwise_relation _ eq (funcomp (ren_PTm zeta_PTm) (ren_PTm xi_PTm)) (ren_PTm (funcomp zeta_PTm xi_PTm)). Proof. exact (fun s => compRenRen_PTm xi_PTm zeta_PTm _ (fun n => eq_refl) s). Qed. -Lemma renSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} - (xi_PTm : fin m_PTm -> fin k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) - (s : PTm m_PTm) : +Lemma renSubst_PTm (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm) (s : PTm) : subst_PTm tau_PTm (ren_PTm xi_PTm s) = subst_PTm (funcomp tau_PTm xi_PTm) s. Proof. exact (compRenSubst_PTm xi_PTm tau_PTm _ (fun n => eq_refl) s). Qed. -Lemma renSubst_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} - (xi_PTm : fin m_PTm -> fin k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) : +Lemma renSubst_PTm_pointwise (xi_PTm : nat -> nat) (tau_PTm : nat -> PTm) : pointwise_relation _ eq (funcomp (subst_PTm tau_PTm) (ren_PTm xi_PTm)) (subst_PTm (funcomp tau_PTm xi_PTm)). Proof. exact (fun s => compRenSubst_PTm xi_PTm tau_PTm _ (fun n => eq_refl) s). Qed. -Lemma substRen_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} - (sigma_PTm : fin m_PTm -> PTm k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) - (s : PTm m_PTm) : +Lemma substRen_PTm (sigma_PTm : nat -> PTm) (zeta_PTm : nat -> nat) (s : PTm) + : ren_PTm zeta_PTm (subst_PTm sigma_PTm s) = subst_PTm (funcomp (ren_PTm zeta_PTm) sigma_PTm) s. Proof. exact (compSubstRen_PTm sigma_PTm zeta_PTm _ (fun n => eq_refl) s). Qed. -Lemma substRen_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} - (sigma_PTm : fin m_PTm -> PTm k_PTm) (zeta_PTm : fin k_PTm -> fin l_PTm) : +Lemma substRen_PTm_pointwise (sigma_PTm : nat -> PTm) (zeta_PTm : nat -> nat) + : pointwise_relation _ eq (funcomp (ren_PTm zeta_PTm) (subst_PTm sigma_PTm)) (subst_PTm (funcomp (ren_PTm zeta_PTm) sigma_PTm)). Proof. exact (fun s => compSubstRen_PTm sigma_PTm zeta_PTm _ (fun n => eq_refl) s). Qed. -Lemma substSubst_PTm {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} - (sigma_PTm : fin m_PTm -> PTm k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) - (s : PTm m_PTm) : +Lemma substSubst_PTm (sigma_PTm : nat -> PTm) (tau_PTm : nat -> PTm) + (s : PTm) : subst_PTm tau_PTm (subst_PTm sigma_PTm s) = subst_PTm (funcomp (subst_PTm tau_PTm) sigma_PTm) s. Proof. exact (compSubstSubst_PTm sigma_PTm tau_PTm _ (fun n => eq_refl) s). Qed. -Lemma substSubst_PTm_pointwise {k_PTm : nat} {l_PTm : nat} {m_PTm : nat} - (sigma_PTm : fin m_PTm -> PTm k_PTm) (tau_PTm : fin k_PTm -> PTm l_PTm) : +Lemma substSubst_PTm_pointwise (sigma_PTm : nat -> PTm) + (tau_PTm : nat -> PTm) : pointwise_relation _ eq (funcomp (subst_PTm tau_PTm) (subst_PTm sigma_PTm)) (subst_PTm (funcomp (subst_PTm tau_PTm) sigma_PTm)). Proof. exact (fun s => compSubstSubst_PTm sigma_PTm tau_PTm _ (fun n => eq_refl) s). Qed. -Lemma rinstInst_up_PTm_PTm {m : nat} {n_PTm : nat} (xi : fin m -> fin n_PTm) - (sigma : fin m -> PTm n_PTm) - (Eq : forall x, funcomp (VarPTm n_PTm) xi x = sigma x) : - forall x, - funcomp (VarPTm (S n_PTm)) (upRen_PTm_PTm xi) x = up_PTm_PTm sigma x. +Lemma rinstInst_up_PTm_PTm (xi : nat -> nat) (sigma : nat -> PTm) + (Eq : forall x, funcomp (VarPTm) xi x = sigma x) : + forall x, funcomp (VarPTm) (upRen_PTm_PTm xi) x = up_PTm_PTm sigma x. Proof. exact (fun n => match n with - | Some fin_n => ap (ren_PTm shift) (Eq fin_n) - | None => eq_refl + | S n' => ap (ren_PTm shift) (Eq n') + | O => eq_refl end). Qed. -Lemma rinstInst_up_list_PTm_PTm {p : nat} {m : nat} {n_PTm : nat} - (xi : fin m -> fin n_PTm) (sigma : fin m -> PTm n_PTm) - (Eq : forall x, funcomp (VarPTm n_PTm) xi x = sigma x) : - forall x, - funcomp (VarPTm (plus p n_PTm)) (upRen_list_PTm_PTm p xi) x = - up_list_PTm_PTm p sigma x. -Proof. -exact (fun n => - eq_trans (scons_p_comp' _ _ (VarPTm (plus p n_PTm)) n) - (scons_p_congr (fun z => eq_refl) - (fun n => ap (ren_PTm (shift_p p)) (Eq n)))). -Qed. - -Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat} -(xi_PTm : fin m_PTm -> fin n_PTm) (sigma_PTm : fin m_PTm -> PTm n_PTm) -(Eq_PTm : forall x, funcomp (VarPTm n_PTm) xi_PTm x = sigma_PTm x) -(s : PTm m_PTm) {struct s} : ren_PTm xi_PTm s = subst_PTm sigma_PTm s := +Fixpoint rinst_inst_PTm (xi_PTm : nat -> nat) (sigma_PTm : nat -> PTm) +(Eq_PTm : forall x, funcomp (VarPTm) xi_PTm x = sigma_PTm x) (s : PTm) +{struct s} : ren_PTm xi_PTm s = subst_PTm sigma_PTm s := match s with - | VarPTm _ s0 => Eq_PTm s0 - | PAbs _ s0 => + | VarPTm s0 => Eq_PTm s0 + | PAbs s0 => congr_PAbs (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm) (rinstInst_up_PTm_PTm _ _ Eq_PTm) s0) - | PApp _ s0 s1 => + | PApp s0 s1 => congr_PApp (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) - | PPair _ s0 s1 => + | PPair s0 s1 => congr_PPair (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) - | PProj _ s0 s1 => + | PProj s0 s1 => congr_PProj (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) - | PBind _ s0 s1 s2 => + | PBind s0 s1 s2 => congr_PBind (eq_refl s0) (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s1) (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm) (rinstInst_up_PTm_PTm _ _ Eq_PTm) s2) - | PUniv _ s0 => congr_PUniv (eq_refl s0) - | PBot _ => congr_PBot - | PNat _ => congr_PNat - | PZero _ => congr_PZero - | PSuc _ s0 => congr_PSuc (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0) - | PInd _ s0 s1 s2 s3 => + | PUniv s0 => congr_PUniv (eq_refl s0) + | PBot => congr_PBot + | PNat => congr_PNat + | PZero => congr_PZero + | PSuc s0 => congr_PSuc (rinst_inst_PTm xi_PTm sigma_PTm Eq_PTm s0) + | PInd s0 s1 s2 s3 => congr_PInd (rinst_inst_PTm (upRen_PTm_PTm xi_PTm) (up_PTm_PTm sigma_PTm) (rinstInst_up_PTm_PTm _ _ Eq_PTm) s0) @@ -822,71 +649,61 @@ Fixpoint rinst_inst_PTm {m_PTm : nat} {n_PTm : nat} (rinstInst_up_PTm_PTm _ _ (rinstInst_up_PTm_PTm _ _ Eq_PTm)) s3) end. -Lemma rinstInst'_PTm {m_PTm : nat} {n_PTm : nat} - (xi_PTm : fin m_PTm -> fin n_PTm) (s : PTm m_PTm) : - ren_PTm xi_PTm s = subst_PTm (funcomp (VarPTm n_PTm) xi_PTm) s. +Lemma rinstInst'_PTm (xi_PTm : nat -> nat) (s : PTm) : + ren_PTm xi_PTm s = subst_PTm (funcomp (VarPTm) xi_PTm) s. Proof. exact (rinst_inst_PTm xi_PTm _ (fun n => eq_refl) s). Qed. -Lemma rinstInst'_PTm_pointwise {m_PTm : nat} {n_PTm : nat} - (xi_PTm : fin m_PTm -> fin n_PTm) : +Lemma rinstInst'_PTm_pointwise (xi_PTm : nat -> nat) : pointwise_relation _ eq (ren_PTm xi_PTm) - (subst_PTm (funcomp (VarPTm n_PTm) xi_PTm)). + (subst_PTm (funcomp (VarPTm) xi_PTm)). Proof. exact (fun s => rinst_inst_PTm xi_PTm _ (fun n => eq_refl) s). Qed. -Lemma instId'_PTm {m_PTm : nat} (s : PTm m_PTm) : - subst_PTm (VarPTm m_PTm) s = s. +Lemma instId'_PTm (s : PTm) : subst_PTm (VarPTm) s = s. Proof. -exact (idSubst_PTm (VarPTm m_PTm) (fun n => eq_refl) s). +exact (idSubst_PTm (VarPTm) (fun n => eq_refl) s). Qed. -Lemma instId'_PTm_pointwise {m_PTm : nat} : - pointwise_relation _ eq (subst_PTm (VarPTm m_PTm)) id. +Lemma instId'_PTm_pointwise : pointwise_relation _ eq (subst_PTm (VarPTm)) id. Proof. -exact (fun s => idSubst_PTm (VarPTm m_PTm) (fun n => eq_refl) s). +exact (fun s => idSubst_PTm (VarPTm) (fun n => eq_refl) s). Qed. -Lemma rinstId'_PTm {m_PTm : nat} (s : PTm m_PTm) : ren_PTm id s = s. +Lemma rinstId'_PTm (s : PTm) : ren_PTm id s = s. Proof. exact (eq_ind_r (fun t => t = s) (instId'_PTm s) (rinstInst'_PTm id s)). Qed. -Lemma rinstId'_PTm_pointwise {m_PTm : nat} : - pointwise_relation _ eq (@ren_PTm m_PTm m_PTm id) id. +Lemma rinstId'_PTm_pointwise : pointwise_relation _ eq (@ren_PTm id) id. Proof. exact (fun s => eq_ind_r (fun t => t = s) (instId'_PTm s) (rinstInst'_PTm id s)). Qed. -Lemma varL'_PTm {m_PTm : nat} {n_PTm : nat} - (sigma_PTm : fin m_PTm -> PTm n_PTm) (x : fin m_PTm) : - subst_PTm sigma_PTm (VarPTm m_PTm x) = sigma_PTm x. +Lemma varL'_PTm (sigma_PTm : nat -> PTm) (x : nat) : + subst_PTm sigma_PTm (VarPTm x) = sigma_PTm x. Proof. exact (eq_refl). Qed. -Lemma varL'_PTm_pointwise {m_PTm : nat} {n_PTm : nat} - (sigma_PTm : fin m_PTm -> PTm n_PTm) : - pointwise_relation _ eq (funcomp (subst_PTm sigma_PTm) (VarPTm m_PTm)) - sigma_PTm. +Lemma varL'_PTm_pointwise (sigma_PTm : nat -> PTm) : + pointwise_relation _ eq (funcomp (subst_PTm sigma_PTm) (VarPTm)) sigma_PTm. Proof. exact (fun x => eq_refl). Qed. -Lemma varLRen'_PTm {m_PTm : nat} {n_PTm : nat} - (xi_PTm : fin m_PTm -> fin n_PTm) (x : fin m_PTm) : - ren_PTm xi_PTm (VarPTm m_PTm x) = VarPTm n_PTm (xi_PTm x). +Lemma varLRen'_PTm (xi_PTm : nat -> nat) (x : nat) : + ren_PTm xi_PTm (VarPTm x) = VarPTm (xi_PTm x). Proof. exact (eq_refl). Qed. -Lemma varLRen'_PTm_pointwise {m_PTm : nat} {n_PTm : nat} - (xi_PTm : fin m_PTm -> fin n_PTm) : - pointwise_relation _ eq (funcomp (ren_PTm xi_PTm) (VarPTm m_PTm)) - (funcomp (VarPTm n_PTm) xi_PTm). +Lemma varLRen'_PTm_pointwise (xi_PTm : nat -> nat) : + pointwise_relation _ eq (funcomp (ren_PTm xi_PTm) (VarPTm)) + (funcomp (VarPTm) xi_PTm). Proof. exact (fun x => eq_refl). Qed. @@ -894,18 +711,14 @@ Qed. Class Up_PTm X Y := up_PTm : X -> Y. -#[global] -Instance Subst_PTm {m_PTm n_PTm : nat}: (Subst1 _ _ _) := - (@subst_PTm m_PTm n_PTm). +#[global]Instance Subst_PTm : (Subst1 _ _ _) := @subst_PTm. + +#[global]Instance Up_PTm_PTm : (Up_PTm _ _) := @up_PTm_PTm. + +#[global]Instance Ren_PTm : (Ren1 _ _ _) := @ren_PTm. #[global] -Instance Up_PTm_PTm {m n_PTm : nat}: (Up_PTm _ _) := (@up_PTm_PTm m n_PTm). - -#[global] -Instance Ren_PTm {m_PTm n_PTm : nat}: (Ren1 _ _ _) := (@ren_PTm m_PTm n_PTm). - -#[global] -Instance VarInstance_PTm {n_PTm : nat}: (Var _ _) := (@VarPTm n_PTm). +Instance VarInstance_PTm : (Var _ _) := @VarPTm. Notation "[ sigma_PTm ]" := (subst_PTm sigma_PTm) ( at level 1, left associativity, only printing) : fscope. @@ -932,9 +745,9 @@ Notation "x '__PTm'" := (VarPTm x) ( at level 5, format "x __PTm") : subst_scope. #[global] -Instance subst_PTm_morphism {m_PTm : nat} {n_PTm : nat}: +Instance subst_PTm_morphism : (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) - (@subst_PTm m_PTm n_PTm)). + (@subst_PTm)). Proof. exact (fun f_PTm g_PTm Eq_PTm s t Eq_st => eq_ind s (fun t' => subst_PTm f_PTm s = subst_PTm g_PTm t') @@ -942,17 +755,16 @@ exact (fun f_PTm g_PTm Eq_PTm s t Eq_st => Qed. #[global] -Instance subst_PTm_morphism2 {m_PTm : nat} {n_PTm : nat}: +Instance subst_PTm_morphism2 : (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq)) - (@subst_PTm m_PTm n_PTm)). + (@subst_PTm)). Proof. exact (fun f_PTm g_PTm Eq_PTm s => ext_PTm f_PTm g_PTm Eq_PTm s). Qed. #[global] -Instance ren_PTm_morphism {m_PTm : nat} {n_PTm : nat}: - (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) - (@ren_PTm m_PTm n_PTm)). +Instance ren_PTm_morphism : + (Proper (respectful (pointwise_relation _ eq) (respectful eq eq)) (@ren_PTm)). Proof. exact (fun f_PTm g_PTm Eq_PTm s t Eq_st => eq_ind s (fun t' => ren_PTm f_PTm s = ren_PTm g_PTm t') @@ -960,9 +772,9 @@ exact (fun f_PTm g_PTm Eq_PTm s t Eq_st => Qed. #[global] -Instance ren_PTm_morphism2 {m_PTm : nat} {n_PTm : nat}: +Instance ren_PTm_morphism2 : (Proper (respectful (pointwise_relation _ eq) (pointwise_relation _ eq)) - (@ren_PTm m_PTm n_PTm)). + (@ren_PTm)). Proof. exact (fun f_PTm g_PTm Eq_PTm s => extRen_PTm f_PTm g_PTm Eq_PTm s). Qed. @@ -994,9 +806,7 @@ Ltac asimpl' := repeat (first | progress setoid_rewrite rinstId'_PTm | progress setoid_rewrite instId'_PTm_pointwise | progress setoid_rewrite instId'_PTm - | progress - unfold up_list_PTm_PTm, up_PTm_PTm, upRen_list_PTm_PTm, - upRen_PTm_PTm, up_ren + | progress unfold up_PTm_PTm, upRen_PTm_PTm, up_ren | progress cbn[subst_PTm ren_PTm] | progress fsimpl ]). @@ -1021,32 +831,7 @@ End Core. Module Extra. -Import -Core. - -Arguments VarPTm {n_PTm}. - -Arguments PInd {n_PTm}. - -Arguments PSuc {n_PTm}. - -Arguments PZero {n_PTm}. - -Arguments PNat {n_PTm}. - -Arguments PBot {n_PTm}. - -Arguments PUniv {n_PTm}. - -Arguments PBind {n_PTm}. - -Arguments PProj {n_PTm}. - -Arguments PPair {n_PTm}. - -Arguments PApp {n_PTm}. - -Arguments PAbs {n_PTm}. +Import Core. #[global]Hint Opaque subst_PTm: rewrite. diff --git a/theories/Autosubst2/unscoped.v b/theories/Autosubst2/unscoped.v new file mode 100644 index 0000000..55f8172 --- /dev/null +++ b/theories/Autosubst2/unscoped.v @@ -0,0 +1,213 @@ +(** * Autosubst Header for Unnamed Syntax + +Version: December 11, 2019. + *) + +(* Adrian: + I changed this library a bit to work better with my generated code. + 1. I use nat directly instead of defining fin to be nat and using Some/None as S/O + 2. I removed the "s, sigma" notation for scons because it interacts with dependent function types "forall x, A"*) +Require Import core. +Require Import Setoid Morphisms Relation_Definitions. + +Definition ap {X Y} (f : X -> Y) {x y : X} (p : x = y) : f x = f y := + match p with eq_refl => eq_refl end. + +Definition apc {X Y} {f g : X -> Y} {x y : X} (p : f = g) (q : x = y) : f x = g y := + match q with eq_refl => match p with eq_refl => eq_refl end end. + +(** ** Primitives of the Sigma Calculus. *) + +Definition shift := S. + +Definition var_zero := 0. + +Definition id {X} := @Datatypes.id X. + +Definition scons {X: Type} (x : X) (xi : nat -> X) := + fun n => match n with + | 0 => x + | S n => xi n + end. + +#[ export ] +Hint Opaque scons : rewrite. + +(** ** Type Class Instances for Notation +Required to make notation work. *) + +(** *** Type classes for renamings. *) + +Class Ren1 (X1 : Type) (Y Z : Type) := + ren1 : X1 -> Y -> Z. + +Class Ren2 (X1 X2 : Type) (Y Z : Type) := + ren2 : X1 -> X2 -> Y -> Z. + +Class Ren3 (X1 X2 X3 : Type) (Y Z : Type) := + ren3 : X1 -> X2 -> X3 -> Y -> Z. + +Class Ren4 (X1 X2 X3 X4 : Type) (Y Z : Type) := + ren4 : X1 -> X2 -> X3 -> X4 -> Y -> Z. + +Class Ren5 (X1 X2 X3 X4 X5 : Type) (Y Z : Type) := + ren5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z. + +Module RenNotations. + Notation "s ⟨ xi1 ⟩" := (ren1 xi1 s) (at level 7, left associativity, format "s ⟨ xi1 ⟩") : subst_scope. + + Notation "s ⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ⟩") : subst_scope. + + Notation "s ⟨ xi1 ; xi2 ; xi3 ⟩" := (ren3 xi1 xi2 xi3 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ⟩") : subst_scope. + + Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩" := (ren4 xi1 xi2 xi3 xi4 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩") : subst_scope. + + Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩" := (ren5 xi1 xi2 xi3 xi4 xi5 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩") : subst_scope. + + Notation "⟨ xi ⟩" := (ren1 xi) (at level 1, left associativity, format "⟨ xi ⟩") : fscope. + + Notation "⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2) (at level 1, left associativity, format "⟨ xi1 ; xi2 ⟩") : fscope. +End RenNotations. + +(** *** Type Classes for Substiution *) + +Class Subst1 (X1 : Type) (Y Z: Type) := + subst1 : X1 -> Y -> Z. + +Class Subst2 (X1 X2 : Type) (Y Z: Type) := + subst2 : X1 -> X2 -> Y -> Z. + +Class Subst3 (X1 X2 X3 : Type) (Y Z: Type) := + subst3 : X1 -> X2 -> X3 -> Y -> Z. + +Class Subst4 (X1 X2 X3 X4: Type) (Y Z: Type) := + subst4 : X1 -> X2 -> X3 -> X4 -> Y -> Z. + +Class Subst5 (X1 X2 X3 X4 X5 : Type) (Y Z: Type) := + subst5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z. + +Module SubstNotations. + Notation "s [ sigma ]" := (subst1 sigma s) (at level 7, left associativity, format "s '/' [ sigma ]") : subst_scope. + + Notation "s [ sigma ; tau ]" := (subst2 sigma tau s) (at level 7, left associativity, format "s '/' [ sigma ; '/' tau ]") : subst_scope. +End SubstNotations. + +(** *** Type Class for Variables *) + +Class Var X Y := + ids : X -> Y. + +#[export] Instance idsRen : Var nat nat := id. + +(** ** Proofs for the substitution primitives. *) + +Arguments funcomp {X Y Z} (g)%fscope (f)%fscope. + +Module CombineNotations. + Notation "f >> g" := (funcomp g f) (at level 50) : fscope. + + Notation "s .: sigma" := (scons s sigma) (at level 55, sigma at next level, right associativity) : subst_scope. + + #[ global ] + Open Scope fscope. + #[ global ] + Open Scope subst_scope. +End CombineNotations. + +Import CombineNotations. + + +(** A generic lifting of a renaming. *) +Definition up_ren (xi : nat -> nat) := + 0 .: (xi >> S). + +(** A generic proof that lifting of renamings composes. *) +Lemma up_ren_ren (xi: nat -> nat) (zeta : nat -> nat) (rho: nat -> nat) (E: forall x, (xi >> zeta) x = rho x) : + forall x, (up_ren xi >> up_ren zeta) x = up_ren rho x. +Proof. + intros [|x]. + - reflexivity. + - unfold up_ren. cbn. unfold funcomp. f_equal. apply E. +Qed. + +(** Eta laws. *) +Lemma scons_eta' {T} (f : nat -> T) : + pointwise_relation _ eq (f var_zero .: (funcomp f shift)) f. +Proof. intros x. destruct x; reflexivity. Qed. + +Lemma scons_eta_id' : + pointwise_relation _ eq (var_zero .: shift) id. +Proof. intros x. destruct x; reflexivity. Qed. + +Lemma scons_comp' (T: Type) {U} (s: T) (sigma: nat -> T) (tau: T -> U) : + pointwise_relation _ eq (funcomp tau (s .: sigma)) ((tau s) .: (funcomp tau sigma)). +Proof. intros x. destruct x; reflexivity. Qed. + +(* Morphism for Setoid Rewriting. The only morphism that can be defined statically. *) +#[export] Instance scons_morphism {X: Type} : + Proper (eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons X). +Proof. + intros ? t -> sigma tau H. + intros [|x]. + cbn. reflexivity. + apply H. +Qed. + +#[export] Instance scons_morphism2 {X: Type} : + Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons X). +Proof. + intros ? t -> sigma tau H ? x ->. + destruct x as [|x]. + cbn. reflexivity. + apply H. +Qed. + +(** ** Generic lifting of an allfv predicate *) +Definition up_allfv (p: nat -> Prop) : nat -> Prop := scons True p. + +(** ** Notations for unscoped syntax *) +Module UnscopedNotations. + Include RenNotations. + Include SubstNotations. + Include CombineNotations. + + (* Notation "s , sigma" := (scons s sigma) (at level 60, format "s , sigma", right associativity) : subst_scope. *) + + Notation "s '..'" := (scons s ids) (at level 1, format "s ..") : subst_scope. + + Notation "↑" := (shift) : subst_scope. + + #[global] + Open Scope fscope. + #[global] + Open Scope subst_scope. +End UnscopedNotations. + +(** ** Tactics for unscoped syntax *) + +(** Automatically does a case analysis on a natural number, useful for proofs with context renamings/context morphisms. *) +Tactic Notation "auto_case" tactic(t) := (match goal with + | [|- forall (i : nat), _] => intros []; t + end). + + +(** Generic fsimpl tactic: simplifies the above primitives in a goal. *) +Ltac fsimpl := + repeat match goal with + | [|- context[id >> ?f]] => change (id >> f) with f (* AsimplCompIdL *) + | [|- context[?f >> id]] => change (f >> id) with f (* AsimplCompIdR *) + | [|- context [id ?s]] => change (id s) with s + | [|- context[(?f >> ?g) >> ?h]] => change ((f >> g) >> h) with (f >> (g >> h)) + | [|- context[(?v .: ?g) var_zero]] => change ((v .: g) var_zero) with v + | [|- context[(?v .: ?g) 0]] => change ((v .: g) 0) with v + | [|- context[(?v .: ?g) (S ?n)]] => change ((v .: g) (S n)) with (g n) + | [|- context[?f >> (?x .: ?g)]] => change (f >> (x .: g)) with g (* f should evaluate to shift *) + | [|- context[var_zero]] => change var_zero with 0 + | [|- context[?x2 .: (funcomp ?f shift)]] => change (scons x2 (funcomp f shift)) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite (@scons_eta' _ _ f) + | [|- context[?f var_zero .: ?g]] => change (scons (f var_zero) g) with (scons (f var_zero) (funcomp f shift)); rewrite scons_eta' + | [|- _ = ?h (?f ?s)] => change (h (f s)) with ((f >> h) s) + | [|- ?h (?f ?s) = _] => change (h (f s)) with ((f >> h) s) + (* DONE had to put an underscore as the last argument to scons. This might be an argument against unfolding funcomp *) + | [|- context[funcomp _ (scons _ _)]] => setoid_rewrite scons_comp'; eta_reduce + | [|- context[scons var_zero shift]] => setoid_rewrite scons_eta_id'; eta_reduce + end. \ No newline at end of file diff --git a/theories/common.v b/theories/common.v index 282038d..51fad7b 100644 --- a/theories/common.v +++ b/theories/common.v @@ -4,6 +4,7 @@ Import Ltac2.Notations. Import Ltac2.Control. From Hammer Require Import Tactics. + Definition renaming_ok {n m} (Γ : fin n -> PTm n) (Δ : fin m -> PTm m) (ξ : fin m -> fin n) := forall (i : fin m), ren_PTm ξ (Δ i) = Γ (ξ i). diff --git a/theories/executable.v b/theories/executable.v index dd7d2aa..04ab661 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -1,13 +1,64 @@ From Equations Require Import Equations. -Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax - common typing preservation admissible fp_red structural soundness. -Require Import algorithmic. -From stdpp Require Import relations (rtc(..), nsteps(..)). +Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax. +Derive NoConfusion for nat PTag BTag PTm. + Require Import ssreflect ssrbool. From Hammer Require Import Tactics. -Inductive algo_dom {n} : PTm n -> PTm n -> Prop := +Definition ishf (a : PTm) := + match a with + | PPair _ _ => true + | PAbs _ => true + | PUniv _ => true + | PBind _ _ _ => true + | PNat => true + | PSuc _ => true + | PZero => true + | _ => false + end. + +Fixpoint ishne (a : PTm) := + match a with + | VarPTm _ => true + | PApp a _ => ishne a + | PProj _ a => ishne a + | PBot => true + | PInd _ n _ _ => ishne n + | _ => false + end. + +Module HRed. + Inductive R : PTm -> PTm -> Prop := + (****************** Beta ***********************) + | AppAbs a b : + R (PApp (PAbs a) b) (subst_PTm (scons b VarPTm) a) + + | ProjPair p a b : + R (PProj p (PPair a b)) (if p is PL then a else b) + + | IndZero P b c : + R (PInd P PZero b c) b + + | IndSuc P a b c : + R (PInd P (PSuc a) b c) (subst_PTm (scons (PInd P a b c) (scons a VarPTm)) c) + + (*************** Congruence ********************) + | AppCong a0 a1 b : + R a0 a1 -> + R (PApp a0 b) (PApp a1 b) + | ProjCong p a0 a1 : + R a0 a1 -> + R (PProj p a0) (PProj p a1) + | IndCong P a0 a1 b c : + R a0 a1 -> + R (PInd P a0 b c) (PInd P a1 b c). + + Definition nf a := forall b, ~ R a b. +End HRed. + + +Inductive algo_dom : PTm -> PTm -> Prop := | A_AbsAbs a b : algo_dom_r a b -> (* --------------------- *) @@ -74,7 +125,7 @@ Inductive algo_dom {n} : PTm n -> PTm n -> Prop := (* ------------------------- *) algo_dom (PApp u0 a0) (PApp u1 a1) -with algo_dom_r {n} : PTm n -> PTm n -> Prop := +with algo_dom_r : PTm -> PTm -> Prop := | A_NfNf a b : algo_dom a b -> algo_dom_r a b @@ -92,67 +143,26 @@ with algo_dom_r {n} : PTm n -> PTm n -> Prop := (* ----------------------- *) algo_dom_r a b. -Derive Signature for algo_dom algo_dom_r. -Derive NoConfusion for PTm. -Next Obligation. -Admitted. -Next Obligation. -Admitted. - -Derive Dependent Inversion adom_inv with (forall n (a b : PTm n), algo_dom a b) Sort Prop. - -Lemma algo_dom_hf_hne n (a b : PTm n) : +Lemma algo_dom_hf_hne (a b : PTm) : algo_dom a b -> (ishf a \/ ishne a) /\ (ishf b \/ ishne b). Proof. induction 1 =>//=; hauto lq:on. Qed. -Lemma hf_no_hred n (a b : PTm n) : +Lemma hf_no_hred (a b : PTm) : ishf a -> HRed.R a b -> False. Proof. hauto l:on inv:HRed.R. Qed. -Lemma hne_no_hred n (a b : PTm n) : +Lemma hne_no_hred (a b : PTm) : ishne a -> HRed.R a b -> False. Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed. -Definition fin_beq {n} (i j : fin n) : bool. -Proof. - induction n. - - by exfalso. - - refine (match i , j with - | None, None => true - | Some i, Some j => IHn i j - | _, _ => false - end). -Defined. - -Lemma fin_eq_dec {n} (i j : fin n) : - Bool.reflect (i = j) (fin_beq i j). -Proof. - revert i j. induction n. - - destruct i. - - destruct i; destruct j. - + specialize (IHn f f0). - inversion IHn; subst. - simpl. rewrite -H. - apply ReflectT. - reflexivity. - simpl. rewrite -H. - apply ReflectF. - injection. tauto. - + by apply ReflectF. - + by apply ReflectF. - + by apply ReflectT. -Defined. - -Scheme Equality for PTag. -Scheme Equality for BTag. - +Derive Signature for algo_dom. (* Fixpoint PTm_eqb {n} (a b : PTm n) := *) (* match a, b with *) (* | VarPTm i, VarPTm j => fin_eq i j *) @@ -171,7 +181,7 @@ Scheme Equality for BTag. (* destruct IHa1. *) (* destruct a1. *) -Fixpoint hred {n} (a : PTm n) : option (PTm n) := +Fixpoint hred (a : PTm) : option (PTm) := match a with | VarPTm i => None | PAbs a => None @@ -204,31 +214,31 @@ Fixpoint hred {n} (a : PTm n) : option (PTm n) := end end. -Lemma hred_complete n (a b : PTm n) : +Lemma hred_complete (a b : PTm) : HRed.R a b -> hred a = Some b. Proof. induction 1; hauto lq:on rew:off inv:HRed.R b:on. Qed. -Lemma hred_sound n (a b : PTm n): +Lemma hred_sound (a b : PTm): hred a = Some b -> HRed.R a b. Proof. elim : a b; hauto q:on dep:on ctrs:HRed.R. Qed. -Lemma hred_deter n (a b0 b1 : PTm n) : +Lemma hred_deter (a b0 b1 : PTm) : HRed.R a b0 -> HRed.R a b1 -> b0 = b1. Proof. move /hred_complete => + /hred_complete. congruence. Qed. -Definition hred_fancy n (a : PTm n) : - relations.nf HRed.R a + {x | HRed.R a x}. +Definition hred_fancy (a : PTm) : + HRed.nf a + {x | HRed.R a x}. Proof. destruct (hred a) as [a'|] eqn:eq . - right. exists a'. hauto q:on use:hred_sound. - left. - move => [a' h]. + move => a' h. move /hred_complete in h. congruence. Defined. @@ -241,6 +251,8 @@ Ltac check_equal_triv := | _ => idtac end. +Scheme Equality for nat. Scheme Equality for PTag. +Scheme Equality for BTag. Scheme Equality for PTm. (* Program Fixpoint check_equal {n} (a b : PTm n) (h : algo_dom a b) {struct h} : bool := *) (* match a, b with *) (* | VarPTm i, VarPTm j => fin_beq i j *) @@ -255,9 +267,9 @@ Ltac check_equal_triv := (* Next Obligation. *) (* simpl. *) -Equations check_equal {n} (a b : PTm n) (h : algo_dom a b) : +Equations check_equal (a b : PTm) (h : algo_dom a b) : bool by struct h := - check_equal (VarPTm i) (VarPTm j) h := fin_beq i j; + check_equal (VarPTm i) (VarPTm j) h := nat_beq i j; check_equal (PAbs a) (PAbs b) h := check_equal_r a b ltac:(check_equal_triv); check_equal (PAbs a) b h := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv); check_equal a (PAbs b) h := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv); @@ -274,26 +286,24 @@ Equations check_equal {n} (a b : PTm n) (h : algo_dom a b) : check_equal (PSuc a) (PSuc b) h := check_equal_r a b ltac:(check_equal_triv); check_equal (PUniv i) (PUniv j) _ := Nat.eqb i j; check_equal a b h := false; - with check_equal_r {n} (a b : PTm n) (h : algo_dom_r a b) : + with check_equal_r (a b : PTm) (h : algo_dom_r a b) : bool by struct h := - check_equal_r a b h with hred_fancy _ a => + check_equal_r a b h with hred_fancy a => { check_equal_r a b h (inr a') := check_equal_r (proj1_sig a') b _; - check_equal_r a b h (inl _) with hred_fancy _ b => + check_equal_r a b h (inl _) with hred_fancy b => { check_equal_r a b h (inl _) (inl _) := check_equal a b _; check_equal_r a b h (inl _) (inr b') := check_equal_r a (proj1_sig b') _}} . Next Obligation. - move => /= ih ihr n a nfa b nfb. - inversion 1; subst=>//=. + inversion h; subst=>//=. exfalso. sfirstorder. exfalso. sfirstorder. Defined. Next Obligation. simpl. - move => /= ih ihr n a nfa b [b' hb']. - inversion 1; subst =>//=. + inversion h; subst =>//=. exfalso. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred. exfalso. sfirstorder. have ? : b' = b'0 by eauto using hred_deter. @@ -302,8 +312,7 @@ Next Obligation. Defined. Next Obligation. - simpl => ih ihr n a [a' ha'] b. - inversion 1; subst => //=. + inversion h; subst => //=. exfalso. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred. suff ? : a'0 = a' by subst; assumption. by eauto using hred_deter. From 757f050d92c4a4108b10397386d706268b7c8fb5 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Thu, 27 Feb 2025 22:27:16 -0500 Subject: [PATCH 04/10] The definition is semi-working --- theories/executable.v | 91 +++++++++++++++++++++++-------------------- 1 file changed, 48 insertions(+), 43 deletions(-) diff --git a/theories/executable.v b/theories/executable.v index 04ab661..b4dcfbe 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -1,6 +1,7 @@ From Equations Require Import Equations. Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax. -Derive NoConfusion for nat PTag BTag PTm. +Derive NoConfusion for sig option nat PTag BTag PTm. +Import Logic (inspect). Require Import ssreflect ssrbool. From Hammer Require Import Tactics. @@ -162,7 +163,7 @@ Lemma hne_no_hred (a b : PTm) : False. Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed. -Derive Signature for algo_dom. +Derive Signature for algo_dom algo_dom_r. (* Fixpoint PTm_eqb {n} (a b : PTm n) := *) (* match a, b with *) (* | VarPTm i, VarPTm j => fin_eq i j *) @@ -232,6 +233,16 @@ Proof. move /hred_complete => + /hred_complete. congruence. Qed. +(* Equations hred_fancy (a : PTm ) : *) +(* HRed.nf a + {x | HRed.R a x} := *) +(* hred_fancy a with hra => { *) +(* hred_fancy a None := inl _; *) +(* hred_fancy a (Some b) := inr (exist _ b _) *) +(* } *) +(* with hra := hred a. *) +(* Next Obligation. *) + + Definition hred_fancy (a : PTm) : HRed.nf a + {x | HRed.R a x}. Proof. @@ -269,62 +280,56 @@ Scheme Equality for BTag. Scheme Equality for PTm. Equations check_equal (a b : PTm) (h : algo_dom a b) : bool by struct h := - check_equal (VarPTm i) (VarPTm j) h := nat_beq i j; - check_equal (PAbs a) (PAbs b) h := check_equal_r a b ltac:(check_equal_triv); - check_equal (PAbs a) b h := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv); - check_equal a (PAbs b) h := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv); - check_equal (PPair a0 b0) (PPair a1 b1) h := - check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); - check_equal (PPair a0 b0) u h := - check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv); - check_equal u (PPair a1 b1) h := - check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv); - check_equal (PBind p0 A0 B0) (PBind p1 A1 B1) h := - BTag_beq p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv); - check_equal PNat PNat _ := true; - check_equal PZero PZero _ := true; - check_equal (PSuc a) (PSuc b) h := check_equal_r a b ltac:(check_equal_triv); - check_equal (PUniv i) (PUniv j) _ := Nat.eqb i j; + (* check_equal (VarPTm i) (VarPTm j) h := nat_beq i j; *) + (* check_equal (PAbs a) (PAbs b) h := check_equal_r a b ltac:(check_equal_triv); *) + (* check_equal (PAbs a) b h := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv); *) + (* check_equal a (PAbs b) h := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv); *) + (* check_equal (PPair a0 b0) (PPair a1 b1) h := *) + (* check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); *) + (* check_equal (PPair a0 b0) u h := *) + (* check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv); *) + (* check_equal u (PPair a1 b1) h := *) + (* check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv); *) + (* check_equal (PBind p0 A0 B0) (PBind p1 A1 B1) h := *) + (* BTag_beq p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv); *) + (* check_equal PNat PNat _ := true; *) + (* check_equal PZero PZero _ := true; *) + (* check_equal (PSuc a) (PSuc b) h := check_equal_r a b ltac:(check_equal_triv); *) + (* check_equal (PUniv i) (PUniv j) _ := Nat.eqb i j; *) check_equal a b h := false; with check_equal_r (a b : PTm) (h : algo_dom_r a b) : bool by struct h := - check_equal_r a b h with hred_fancy a => - { check_equal_r a b h (inr a') := check_equal_r (proj1_sig a') b _; - check_equal_r a b h (inl _) with hred_fancy b => - { check_equal_r a b h (inl _) (inl _) := check_equal a b _; - check_equal_r a b h (inl _) (inr b') := check_equal_r a (proj1_sig b') _}} . - + check_equal_r a b h with inspect (hred a) := + { check_equal_r a b h (exist _ (Some a') k) := check_equal_r a' b _; + check_equal_r a b h (exist _ None k) with inspect (hred b) := + { | (exist _ None l) => check_equal a b _; + | (exist _ (Some b') l) => check_equal_r a b' _}} . Next Obligation. - inversion h; subst=>//=. - exfalso. sfirstorder. - exfalso. sfirstorder. + simpl. + inversion h; subst =>//=. + exfalso. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred, hred_sound. + suff ? : a'0 = a' by subst; assumption. + by eauto using hred_deter, hred_sound. + exfalso. hauto lq:on use:hf_no_hred, hne_no_hred, hred_sound. Defined. Next Obligation. simpl. inversion h; subst =>//=. - exfalso. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred. - exfalso. sfirstorder. - have ? : b' = b'0 by eauto using hred_deter. + exfalso. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred, hred_sound. + exfalso. hauto l:on use:hred_complete. + have ? : b' = b'0 by eauto using hred_deter, hred_sound. subst. assumption. Defined. Next Obligation. inversion h; subst => //=. - exfalso. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred. - suff ? : a'0 = a' by subst; assumption. - by eauto using hred_deter. - exfalso. hauto lq:on use:hf_no_hred, hne_no_hred. + exfalso. hauto l:on use:hred_complete. + exfalso. hauto l:on use:hred_complete. Defined. - -Search (Bool.reflect (is_true _) _). -Check idP. - -Definition metric {n} k (a b : PTm n) := - exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\ - nf va /\ nf vb /\ size_PTm va + size_PTm vb + i + j <= k. - -Search (nat -> nat -> bool). +Next Obligation. + sauto lq:on. +Defined. From 11bfed2d17f48715b7a442f6bccd52b2a75b54a9 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 28 Feb 2025 00:30:02 -0500 Subject: [PATCH 05/10] Finish defining the algorithm --- Makefile | 2 +- theories/Autosubst2/fintype.v | 419 ---------------------------------- theories/Autosubst2/syntax.v | 10 +- theories/executable.v | 125 ++++++---- 4 files changed, 84 insertions(+), 472 deletions(-) delete mode 100644 theories/Autosubst2/fintype.v diff --git a/Makefile b/Makefile index 3c879f6..972974b 100644 --- a/Makefile +++ b/Makefile @@ -22,6 +22,6 @@ theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fint clean: test ! -f $(COQMAKEFILE) || ( $(MAKE) -f $(COQMAKEFILE) clean && rm $(COQMAKEFILE) ) - rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v + rm -f theories/Autosubst2/syntax.v theories/Autosubst2/core.v theories/Autosubst2/fintype.v theories/Autosubst2/unscoped.v FORCE: diff --git a/theories/Autosubst2/fintype.v b/theories/Autosubst2/fintype.v deleted file mode 100644 index 99508b6..0000000 --- a/theories/Autosubst2/fintype.v +++ /dev/null @@ -1,419 +0,0 @@ -(** * Autosubst Header for Scoped Syntax - Our development utilises well-scoped de Bruijn syntax. This means that the de Bruijn indices are taken from finite types. As a consequence, any kind of substitution or environment used in conjunction with well-scoped syntax takes the form of a mapping from some finite type _I^n_. In particular, _renamings_ are mappings _I^n -> I^m_. Here we develop the theory of how these parts interact. - -Version: December 11, 2019. -*) -Require Import core. -Require Import Setoid Morphisms Relation_Definitions. - -Set Implicit Arguments. -Unset Strict Implicit. - -Definition ap {X Y} (f : X -> Y) {x y : X} (p : x = y) : f x = f y := - match p with eq_refl => eq_refl end. - -Definition apc {X Y} {f g : X -> Y} {x y : X} (p : f = g) (q : x = y) : f x = g y := - match q with eq_refl => match p with eq_refl => eq_refl end end. - -(** ** Primitives of the Sigma Calculus - We implement the finite type with _n_ elements, _I^n_, as the _n_-fold iteration of the Option Type. _I^0_ is implemented as the empty type. -*) - -Fixpoint fin (n : nat) : Type := - match n with - | 0 => False - | S m => option (fin m) - end. - -(** Renamings and Injective Renamings - _Renamings_ are mappings between finite types. -*) -Definition ren (m n : nat) : Type := fin m -> fin n. - -Definition id {X} := @Datatypes.id X. - -Definition idren {k: nat} : ren k k := @Datatypes.id (fin k). - -(** We give a special name, to the newest element in a non-empty finite type, as it usually corresponds to a freshly bound variable. *) -Definition var_zero {n : nat} : fin (S n) := None. - -Definition null {T} (i : fin 0) : T := match i with end. - -Definition shift {n : nat} : ren n (S n) := - Some. - -(** Extension of Finite Mappings - Assume we are given a mapping _f_ from _I^n_ to some type _X_, then we can _extend_ this mapping with a new value from _x : X_ to a mapping from _I^n+1_ to _X_. We denote this operation by _x . f_ and define it as follows: -*) -Definition scons {X : Type} {n : nat} (x : X) (f : fin n -> X) (m : fin (S n)) : X := - match m with - | None => x - | Some i => f i - end. - -#[ export ] -Hint Opaque scons : rewrite. - -(** ** Type Class Instances for Notation *) - -(** *** Type classes for renamings. *) - -Class Ren1 (X1 : Type) (Y Z : Type) := - ren1 : X1 -> Y -> Z. - -Class Ren2 (X1 X2 : Type) (Y Z : Type) := - ren2 : X1 -> X2 -> Y -> Z. - -Class Ren3 (X1 X2 X3 : Type) (Y Z : Type) := - ren3 : X1 -> X2 -> X3 -> Y -> Z. - -Class Ren4 (X1 X2 X3 X4 : Type) (Y Z : Type) := - ren4 : X1 -> X2 -> X3 -> X4 -> Y -> Z. - -Class Ren5 (X1 X2 X3 X4 X5 : Type) (Y Z : Type) := - ren5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z. - -Module RenNotations. - Notation "s ⟨ xi1 ⟩" := (ren1 xi1 s) (at level 7, left associativity, format "s ⟨ xi1 ⟩") : subst_scope. - - Notation "s ⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ⟩") : subst_scope. - - Notation "s ⟨ xi1 ; xi2 ; xi3 ⟩" := (ren3 xi1 xi2 xi3 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ⟩") : subst_scope. - - Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩" := (ren4 xi1 xi2 xi3 xi4 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ⟩") : subst_scope. - - Notation "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩" := (ren5 xi1 xi2 xi3 xi4 xi5 s) (at level 7, left associativity, format "s ⟨ xi1 ; xi2 ; xi3 ; xi4 ; xi5 ⟩") : subst_scope. - - Notation "⟨ xi ⟩" := (ren1 xi) (at level 1, left associativity, format "⟨ xi ⟩") : fscope. - - Notation "⟨ xi1 ; xi2 ⟩" := (ren2 xi1 xi2) (at level 1, left associativity, format "⟨ xi1 ; xi2 ⟩") : fscope. -End RenNotations. - -(** *** Type Classes for Substiution *) - -Class Subst1 (X1 : Type) (Y Z: Type) := - subst1 : X1 -> Y -> Z. - -Class Subst2 (X1 X2 : Type) (Y Z: Type) := - subst2 : X1 -> X2 -> Y -> Z. - -Class Subst3 (X1 X2 X3 : Type) (Y Z: Type) := - subst3 : X1 -> X2 -> X3 -> Y -> Z. - -Class Subst4 (X1 X2 X3 X4: Type) (Y Z: Type) := - subst4 : X1 -> X2 -> X3 -> X4 -> Y -> Z. - -Class Subst5 (X1 X2 X3 X4 X5 : Type) (Y Z: Type) := - subst5 : X1 -> X2 -> X3 -> X4 -> X5 -> Y -> Z. - -Module SubstNotations. - Notation "s [ sigma ]" := (subst1 sigma s) (at level 7, left associativity, format "s '/' [ sigma ]") : subst_scope. - - Notation "s [ sigma ; tau ]" := (subst2 sigma tau s) (at level 7, left associativity, format "s '/' [ sigma ; '/' tau ]") : subst_scope. -End SubstNotations. - -(** ** Type Class for Variables *) -Class Var X Y := - ids : X -> Y. - - -(** ** Proofs for substitution primitives *) - -(** Forward Function Composition - Substitutions represented as functions are ubiquitious in this development and we often have to compose them, without talking about their pointwise behaviour. - That is, we are interested in the forward compostion of functions, _f o g_, for which we introduce a convenient notation, "f >> g". The direction of the arrow serves as a reminder of the _forward_ nature of this composition, that is first apply _f_, then _g_. *) - -Arguments funcomp {X Y Z} (g)%fscope (f)%fscope. - -Module CombineNotations. - Notation "f >> g" := (funcomp g f) (at level 50) : fscope. - - Notation "s .: sigma" := (scons s sigma) (at level 55, sigma at next level, right associativity) : subst_scope. - - #[ global ] - Open Scope fscope. - #[ global ] - Open Scope subst_scope. -End CombineNotations. - -Import CombineNotations. - - -(** Generic lifting operation for renamings *) -Definition up_ren {m n} (xi : ren m n) : ren (S m) (S n) := - var_zero .: xi >> shift. - -(** Generic proof that lifting of renamings composes. *) -Lemma up_ren_ren k l m (xi: ren k l) (zeta : ren l m) (rho: ren k m) (E: forall x, (xi >> zeta) x = rho x) : - forall x, (up_ren xi >> up_ren zeta) x = up_ren rho x. -Proof. - intros [x|]. - - cbn. unfold funcomp. now rewrite <- E. - - reflexivity. -Qed. - -Arguments up_ren_ren {k l m} xi zeta rho E. - -Lemma fin_eta {X} (f g : fin 0 -> X) : - pointwise_relation _ eq f g. -Proof. intros []. Qed. - -(** Eta laws *) -Lemma scons_eta' {T} {n : nat} (f : fin (S n) -> T) : - pointwise_relation _ eq (f var_zero .: (funcomp f shift)) f. -Proof. intros x. destruct x; reflexivity. Qed. - -Lemma scons_eta_id' {n : nat} : - pointwise_relation (fin (S n)) eq (var_zero .: shift) id. -Proof. intros x. destruct x; reflexivity. Qed. - -Lemma scons_comp' {T:Type} {U} {m} (s: T) (sigma: fin m -> T) (tau: T -> U) : - pointwise_relation _ eq (funcomp tau (s .: sigma)) ((tau s) .: (funcomp tau sigma)). -Proof. intros x. destruct x; reflexivity. Qed. - -(* Lemma scons_tail'_pointwise {X} {n} (s : X) (f : fin n -> X) : *) -(* pointwise_relation _ eq (funcomp (scons s f) shift) f. *) -(* Proof. *) -(* reflexivity. *) -(* Qed. *) - -(* Lemma scons_tail' {X} {n} (s : X) (f : fin n -> X) x : *) -(* (scons s f (shift x)) = f x. *) -(* Proof. *) -(* reflexivity. *) -(* Qed. *) - -(* Morphism for Setoid Rewriting. The only morphism that can be defined statically. *) -#[export] Instance scons_morphism {X: Type} {n:nat} : - Proper (eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons X n). -Proof. - intros t t' -> sigma tau H. - intros [x|]. - cbn. apply H. - reflexivity. -Qed. - -#[export] Instance scons_morphism2 {X: Type} {n: nat} : - Proper (eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons X n). -Proof. - intros ? t -> sigma tau H ? x ->. - destruct x as [x|]. - cbn. apply H. - reflexivity. -Qed. - -(** ** Variadic Substitution Primitives *) - -Fixpoint shift_p (p : nat) {n} : ren n (p + n) := - fun n => match p with - | 0 => n - | S p => Some (shift_p p n) - end. - -Fixpoint scons_p {X: Type} {m : nat} : forall {n} (f : fin m -> X) (g : fin n -> X), fin (m + n) -> X. -Proof. - destruct m. - - intros n f g. exact g. - - intros n f g. cbn. apply scons. - + exact (f var_zero). - + apply scons_p. - * intros z. exact (f (Some z)). - * exact g. -Defined. - -#[export] Hint Opaque scons_p : rewrite. - -#[export] Instance scons_p_morphism {X: Type} {m n:nat} : - Proper (pointwise_relation _ eq ==> pointwise_relation _ eq ==> pointwise_relation _ eq) (@scons_p X m n). -Proof. - intros sigma sigma' Hsigma tau tau' Htau. - intros x. - induction m. - - cbn. apply Htau. - - cbn. change (fin (S m + n)) with (fin (S (m + n))) in x. - destruct x as [x|]. - + cbn. apply IHm. - intros ?. apply Hsigma. - + cbn. apply Hsigma. -Qed. - -#[export] Instance scons_p_morphism2 {X: Type} {m n:nat} : - Proper (pointwise_relation _ eq ==> pointwise_relation _ eq ==> eq ==> eq) (@scons_p X m n). -Proof. - intros sigma sigma' Hsigma tau tau' Htau ? x ->. - induction m. - - cbn. apply Htau. - - cbn. change (fin (S m + n)) with (fin (S (m + n))) in x. - destruct x as [x|]. - + cbn. apply IHm. - intros ?. apply Hsigma. - + cbn. apply Hsigma. -Qed. - -Definition zero_p {m : nat} {n} : fin m -> fin (m + n). -Proof. - induction m. - - intros []. - - intros [x|]. - + exact (shift_p 1 (IHm x)). - + exact var_zero. -Defined. - -Lemma scons_p_head' {X} {m n} (f : fin m -> X) (g : fin n -> X) z: - (scons_p f g) (zero_p z) = f z. -Proof. - induction m. - - inversion z. - - destruct z. - + simpl. simpl. now rewrite IHm. - + reflexivity. -Qed. - -Lemma scons_p_head_pointwise {X} {m n} (f : fin m -> X) (g : fin n -> X) : - pointwise_relation _ eq (funcomp (scons_p f g) zero_p) f. -Proof. - intros z. - unfold funcomp. - induction m. - - inversion z. - - destruct z. - + simpl. now rewrite IHm. - + reflexivity. -Qed. - -Lemma scons_p_tail' X m n (f : fin m -> X) (g : fin n -> X) z : - scons_p f g (shift_p m z) = g z. -Proof. induction m; cbn; eauto. Qed. - -Lemma scons_p_tail_pointwise X m n (f : fin m -> X) (g : fin n -> X) : - pointwise_relation _ eq (funcomp (scons_p f g) (shift_p m)) g. -Proof. intros z. induction m; cbn; eauto. Qed. - -Lemma destruct_fin {m n} (x : fin (m + n)): - (exists x', x = zero_p x') \/ exists x', x = shift_p m x'. -Proof. - induction m; simpl in *. - - right. eauto. - - destruct x as [x|]. - + destruct (IHm x) as [[x' ->] |[x' ->]]. - * left. now exists (Some x'). - * right. eauto. - + left. exists None. eauto. -Qed. - -Lemma scons_p_comp' X Y m n (f : fin m -> X) (g : fin n -> X) (h : X -> Y) : - pointwise_relation _ eq (funcomp h (scons_p f g)) (scons_p (f >> h) (g >> h)). -Proof. - intros x. - destruct (destruct_fin x) as [[x' ->]|[x' ->]]. - (* TODO better way to solve this? *) - - revert x'. - apply pointwise_forall. - change (fun x => (scons_p f g >> h) (zero_p x)) with (zero_p >> scons_p f g >> h). - now setoid_rewrite scons_p_head_pointwise. - - revert x'. - apply pointwise_forall. - change (fun x => (scons_p f g >> h) (shift_p m x)) with (shift_p m >> scons_p f g >> h). - change (fun x => scons_p (f >> h) (g >> h) (shift_p m x)) with (shift_p m >> scons_p (f >> h) (g >> h)). - now rewrite !scons_p_tail_pointwise. -Qed. - - -Lemma scons_p_congr {X} {m n} (f f' : fin m -> X) (g g': fin n -> X) z: - (forall x, f x = f' x) -> (forall x, g x = g' x) -> scons_p f g z = scons_p f' g' z. -Proof. intros H1 H2. induction m; eauto. cbn. destruct z; eauto. Qed. - -(** Generic n-ary lifting operation. *) -Definition upRen_p p { m : nat } { n : nat } (xi : (fin) (m) -> (fin) (n)) : fin (p + m) -> fin (p + n) := - scons_p (zero_p ) (xi >> shift_p _). - -Arguments upRen_p p {m n} xi. - -(** Generic proof for composition of n-ary lifting. *) -Lemma up_ren_ren_p p k l m (xi: ren k l) (zeta : ren l m) (rho: ren k m) (E: forall x, (xi >> zeta) x = rho x) : - forall x, (upRen_p p xi >> upRen_p p zeta) x = upRen_p p rho x. -Proof. - intros x. destruct (destruct_fin x) as [[? ->]|[? ->]]. - - unfold upRen_p. unfold funcomp. now repeat rewrite scons_p_head'. - - unfold upRen_p. unfold funcomp. repeat rewrite scons_p_tail'. - now rewrite <- E. -Qed. - - -Arguments zero_p m {n}. -Arguments scons_p {X} m {n} f g. - -Lemma scons_p_eta {X} {m n} {f : fin m -> X} - {g : fin n -> X} (h: fin (m + n) -> X) {z: fin (m + n)}: - (forall x, g x = h (shift_p m x)) -> (forall x, f x = h (zero_p m x)) -> scons_p m f g z = h z. -Proof. - intros H1 H2. destruct (destruct_fin z) as [[? ->] |[? ->]]. - - rewrite scons_p_head'. eauto. - - rewrite scons_p_tail'. eauto. -Qed. - -Arguments scons_p_eta {X} {m n} {f g} h {z}. -Arguments scons_p_congr {X} {m n} {f f'} {g g'} {z}. - -(** ** Notations for Scoped Syntax *) - -Module ScopedNotations. - Include RenNotations. - Include SubstNotations. - Include CombineNotations. - -(* Notation "s , sigma" := (scons s sigma) (at level 60, format "s , sigma", right associativity) : subst_scope. *) - - Notation "s '..'" := (scons s ids) (at level 1, format "s ..") : subst_scope. - - Notation "↑" := (shift) : subst_scope. - - #[global] - Open Scope fscope. - #[global] - Open Scope subst_scope. -End ScopedNotations. - - -(** ** Tactics for Scoped Syntax *) - -Tactic Notation "auto_case" tactic(t) := (match goal with - | [|- forall (i : fin 0), _] => intros []; t - | [|- forall (i : fin (S (S (S (S _))))), _] => intros [[[[|]|]|]|]; t - | [|- forall (i : fin (S (S (S _)))), _] => intros [[[|]|]|]; t - | [|- forall (i : fin (S (S _))), _] => intros [[?|]|]; t - | [|- forall (i : fin (S _)), _] => intros [?|]; t - end). - -#[export] Hint Rewrite @scons_p_head' @scons_p_tail' : FunctorInstances. - -(** Generic fsimpl tactic: simplifies the above primitives in a goal. *) -Ltac fsimpl := - repeat match goal with - | [|- context[id >> ?f]] => change (id >> f) with f (* AsimplCompIdL *) - | [|- context[?f >> id]] => change (f >> id) with f (* AsimplCompIdR *) - | [|- context [id ?s]] => change (id s) with s - | [|- context[(?f >> ?g) >> ?h]] => change ((f >> g) >> h) with (f >> (g >> h)) (* AsimplComp *) - (* | [|- zero_p >> scons_p ?f ?g] => rewrite scons_p_head *) - | [|- context[(?s .: ?sigma) var_zero]] => change ((s.:sigma) var_zero) with s - | [|- context[(?s .: ?sigma) (shift ?m)]] => change ((s.:sigma) (shift m)) with (sigma m) - (* first [progress setoid_rewrite scons_tail' | progress setoid_rewrite scons_tail'_pointwise ] *) - | [|- context[idren >> ?f]] => change (idren >> f) with f - | [|- context[?f >> idren]] => change (f >> idren) with f - | [|- context[?f >> (?x .: ?g)]] => change (f >> (x .: g)) with g (* f should evaluate to shift *) - | [|- context[?x2 .: (funcomp ?f shift)]] => change (scons x2 (funcomp f shift)) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite (@scons_eta' _ _ f); eta_reduce - | [|- context[?f var_zero .: ?g]] => change (scons (f var_zero) g) with (scons (f var_zero) (funcomp f shift)); setoid_rewrite scons_eta'; eta_reduce - | [|- _ = ?h (?f ?s)] => change (h (f s)) with ((f >> h) s) - | [|- ?h (?f ?s) = _] => change (h (f s)) with ((f >> h) s) - | [|- context[funcomp _ (scons _ _)]] => setoid_rewrite scons_comp'; eta_reduce - | [|- context[funcomp _ (scons_p _ _ _)]] => setoid_rewrite scons_p_comp'; eta_reduce - | [|- context[scons (@var_zero _) shift]] => setoid_rewrite scons_eta_id'; eta_reduce - (* | _ => progress autorewrite with FunctorInstances *) - | [|- context[funcomp (scons_p _ _ _) (zero_p _)]] => - first [progress setoid_rewrite scons_p_head_pointwise | progress setoid_rewrite scons_p_head' ] - | [|- context[scons_p _ _ _ (zero_p _ _)]] => setoid_rewrite scons_p_head' - | [|- context[funcomp (scons_p _ _ _) (shift_p _)]] => - first [progress setoid_rewrite scons_p_tail_pointwise | progress setoid_rewrite scons_p_tail' ] - | [|- context[scons_p _ _ _ (shift_p _ _)]] => setoid_rewrite scons_p_tail' - | _ => first [progress minimize | progress cbn [shift scons scons_p] ] - end. diff --git a/theories/Autosubst2/syntax.v b/theories/Autosubst2/syntax.v index 3d1e1f6..97ebfb1 100644 --- a/theories/Autosubst2/syntax.v +++ b/theories/Autosubst2/syntax.v @@ -711,11 +711,11 @@ Qed. Class Up_PTm X Y := up_PTm : X -> Y. -#[global]Instance Subst_PTm : (Subst1 _ _ _) := @subst_PTm. +#[global] Instance Subst_PTm : (Subst1 _ _ _) := @subst_PTm. -#[global]Instance Up_PTm_PTm : (Up_PTm _ _) := @up_PTm_PTm. +#[global] Instance Up_PTm_PTm : (Up_PTm _ _) := @up_PTm_PTm. -#[global]Instance Ren_PTm : (Ren1 _ _ _) := @ren_PTm. +#[global] Instance Ren_PTm : (Ren1 _ _ _) := @ren_PTm. #[global] Instance VarInstance_PTm : (Var _ _) := @VarPTm. @@ -833,9 +833,9 @@ Module Extra. Import Core. -#[global]Hint Opaque subst_PTm: rewrite. +#[global] Hint Opaque subst_PTm: rewrite. -#[global]Hint Opaque ren_PTm: rewrite. +#[global] Hint Opaque ren_PTm: rewrite. End Extra. diff --git a/theories/executable.v b/theories/executable.v index b4dcfbe..69e6d78 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -1,6 +1,7 @@ From Equations Require Import Equations. Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax. -Derive NoConfusion for sig option nat PTag BTag PTm. +Derive NoConfusion for sig nat PTag BTag PTm. +Derive EqDec for BTag PTag PTm. Import Logic (inspect). Require Import ssreflect ssrbool. @@ -97,6 +98,13 @@ Inductive algo_dom : PTm -> PTm -> Prop := (* ----------------------- *) algo_dom u (PPair a0 a1) +| A_ZeroZero : + algo_dom PZero PZero + +| A_SucSuc a0 a1 : + algo_dom_r a0 a1 -> + algo_dom (PSuc a0) (PSuc a1) + | A_UnivCong i j : (* -------------------------- *) algo_dom (PUniv i) (PUniv j) @@ -107,6 +115,9 @@ Inductive algo_dom : PTm -> PTm -> Prop := (* ---------------------------- *) algo_dom (PBind p0 A0 B0) (PBind p1 A1 B1) +| A_NatCong : + algo_dom PNat PNat + | A_VarCong i j : (* -------------------------- *) algo_dom (VarPTm i) (VarPTm j) @@ -126,6 +137,15 @@ Inductive algo_dom : PTm -> PTm -> Prop := (* ------------------------- *) algo_dom (PApp u0 a0) (PApp u1 a1) +| A_IndCong P0 P1 u0 u1 b0 b1 c0 c1 : + ishne u0 -> + ishne u1 -> + algo_dom_r P0 P1 -> + algo_dom u0 u1 -> + algo_dom_r b0 b1 -> + algo_dom_r c0 c1 -> + algo_dom (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) + with algo_dom_r : PTm -> PTm -> Prop := | A_NfNf a b : algo_dom a b -> @@ -164,23 +184,6 @@ Lemma hne_no_hred (a b : PTm) : Proof. elim : a b => //=; hauto l:on inv:HRed.R. Qed. Derive Signature for algo_dom algo_dom_r. -(* Fixpoint PTm_eqb {n} (a b : PTm n) := *) -(* match a, b with *) -(* | VarPTm i, VarPTm j => fin_eq i j *) -(* | PAbs a, PAbs b => PTm_eqb a b *) -(* | PApp a0 b0, PApp a1 b1 => PTm_eqb a0 a1 && PTm_eqb b0 b1 *) -(* | PBind p0 A0 B0, PBind p1 A1 B1 => BTag_beq p0 p1 && PTm_eqb A0 A1 && PTm_eqb B0 B1 *) -(* | PPair a0 b0, PPair a1 b1 => PTm_eqb a0 a1 && PTm_eqb b0 b1 *) -(* | *) - -(* Lemma hred {n} (a : PTm n) : (relations.nf HRed.R a) + {x | HRed.R a x}. *) -(* Proof. *) -(* induction a. *) -(* - hauto lq:on inv:HRed.R unfold:relations.nf. *) -(* - hauto lq:on inv:HRed.R unfold:relations.nf. *) -(* - clear IHa2. *) -(* destruct IHa1. *) -(* destruct a1. *) Fixpoint hred (a : PTm) : option (PTm) := match a with @@ -262,8 +265,6 @@ Ltac check_equal_triv := | _ => idtac end. -Scheme Equality for nat. Scheme Equality for PTag. -Scheme Equality for BTag. Scheme Equality for PTm. (* Program Fixpoint check_equal {n} (a b : PTm n) (h : algo_dom a b) {struct h} : bool := *) (* match a, b with *) (* | VarPTm i, VarPTm j => fin_beq i j *) @@ -278,24 +279,44 @@ Scheme Equality for BTag. Scheme Equality for PTm. (* Next Obligation. *) (* simpl. *) + +Ltac solve_check_equal := + try solve [intros *; + match goal with + | [|- _ = _] => sauto + | _ => idtac + end]. + +(* #[export,global] Obligation Tactic := idtac "fiewof". *) + + Equations check_equal (a b : PTm) (h : algo_dom a b) : bool by struct h := - (* check_equal (VarPTm i) (VarPTm j) h := nat_beq i j; *) - (* check_equal (PAbs a) (PAbs b) h := check_equal_r a b ltac:(check_equal_triv); *) - (* check_equal (PAbs a) b h := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv); *) - (* check_equal a (PAbs b) h := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv); *) - (* check_equal (PPair a0 b0) (PPair a1 b1) h := *) - (* check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); *) - (* check_equal (PPair a0 b0) u h := *) - (* check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv); *) - (* check_equal u (PPair a1 b1) h := *) - (* check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv); *) - (* check_equal (PBind p0 A0 B0) (PBind p1 A1 B1) h := *) - (* BTag_beq p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv); *) - (* check_equal PNat PNat _ := true; *) - (* check_equal PZero PZero _ := true; *) - (* check_equal (PSuc a) (PSuc b) h := check_equal_r a b ltac:(check_equal_triv); *) - (* check_equal (PUniv i) (PUniv j) _ := Nat.eqb i j; *) + check_equal (VarPTm i) (VarPTm j) h := nat_eqdec i j; + check_equal (PAbs a) (PAbs b) h := check_equal_r a b ltac:(check_equal_triv); + check_equal (PAbs a) b h := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv); + check_equal a (PAbs b) h := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv); + check_equal (PPair a0 b0) (PPair a1 b1) h := + check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); + check_equal (PPair a0 b0) u h := + check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv); + check_equal u (PPair a1 b1) h := + check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv); + check_equal PNat PNat _ := true; + check_equal PZero PZero _ := true; + check_equal (PSuc a) (PSuc b) h := check_equal_r a b ltac:(check_equal_triv); + check_equal (PProj p0 a) (PProj p1 b) h := + PTag_eqdec p0 p1 && check_equal a b ltac:(check_equal_triv); + check_equal (PApp a0 b0) (PApp a1 b1) h := + check_equal a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); + check_equal (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) h := + check_equal_r P0 P1 ltac:(check_equal_triv) && + check_equal u0 u1 ltac:(check_equal_triv) && + check_equal_r b0 b1 ltac:(check_equal_triv) && + check_equal_r c0 c1 ltac:(check_equal_triv); + check_equal (PUniv i) (PUniv j) _ := Nat.eqb i j; + check_equal (PBind p0 A0 B0) (PBind p1 A1 B1) h := + BTag_eqdec p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv); check_equal a b h := false; with check_equal_r (a b : PTm) (h : algo_dom_r a b) : bool by struct h := @@ -306,30 +327,40 @@ Equations check_equal (a b : PTm) (h : algo_dom a b) : | (exist _ (Some b') l) => check_equal_r a b' _}} . Next Obligation. - simpl. - inversion h; subst =>//=. - exfalso. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred, hred_sound. - suff ? : a'0 = a' by subst; assumption. - by eauto using hred_deter, hred_sound. - exfalso. hauto lq:on use:hf_no_hred, hne_no_hred, hred_sound. + intros. + destruct h. + exfalso. apply algo_dom_hf_hne in H. + apply hred_sound in k. + destruct H as [[|] _]. + eauto using hf_no_hred. + eauto using hne_no_hred. + apply hred_sound in k. + assert ( a'0 = a')by eauto using hred_deter. subst. + apply h. + exfalso. + apply hred_sound in k. + destruct H as [|]. + eauto using hne_no_hred. + eauto using hf_no_hred. Defined. Next Obligation. - simpl. + simpl. intros. inversion h; subst =>//=. - exfalso. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred, hred_sound. - exfalso. hauto l:on use:hred_complete. - have ? : b' = b'0 by eauto using hred_deter, hred_sound. + move {h}. hauto lq:on use:algo_dom_hf_hne, hf_no_hred, hne_no_hred, hred_sound. + apply False_ind. hauto l:on use:hred_complete. + assert (b' = b'0) by eauto using hred_deter, hred_sound. subst. assumption. Defined. Next Obligation. + intros. inversion h; subst => //=. exfalso. hauto l:on use:hred_complete. exfalso. hauto l:on use:hred_complete. Defined. Next Obligation. - sauto lq:on. + sauto. Defined. From 44ba3e6575cc52266b5aeb435fcaf8716c4928dc Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 28 Feb 2025 14:05:26 -0500 Subject: [PATCH 06/10] Add view --- theories/executable.v | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/theories/executable.v b/theories/executable.v index 69e6d78..93be579 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -289,6 +289,49 @@ Ltac solve_check_equal := (* #[export,global] Obligation Tactic := idtac "fiewof". *) +Definition isbind (a : PTm) := if a is PBind _ _ _ then true else false. + +Definition isuniv (a : PTm) := if a is PUniv _ then true else false. + +Definition ispair (a : PTm) := + match a with + | PPair _ _ => true + | _ => false + end. + +Definition isnat (a : PTm) := if a is PNat then true else false. + +Definition iszero (a : PTm) := if a is PZero then true else false. + +Definition issuc (a : PTm) := if a is PSuc _ then true else false. + +Definition isabs (a : PTm) := + match a with + | PAbs _ => true + | _ => false + end. + +Inductive eq_view : PTm -> PTm -> Type := +| V_AbsAbs a b : + eq_view (PAbs a) (PAbs b) +| V_AbsNeu a b : + ~~ isabs b -> + eq_view (PAbs a) b +(* | V_NeuAbs a b : *) +(* ~~ isabs a -> *) +(* eq_view a (PAbs b) *) +(* | V_VarVar i j : *) +(* eq_view (VarPTm i) (VarPTm j) *) +(* | V_PairPair a0 b0 a1 b1 : *) +(* eq_view (PPair a0 b0) (PPair a1 b1) *) +| V_Others a b : + eq_view a b. + +Equations tm_to_eq_view (a b : PTm) : eq_view a b := + tm_to_eq_view (PAbs a) (PAbs b) := V_AbsAbs a b; + tm_to_eq_view (PAbs a) b := V_AbsNeu a b _; + (* tm_to_eq_view a (PAbs b) := V_NeuAbs a b _; *) + tm_to_eq_view a b := V_Others a b. Equations check_equal (a b : PTm) (h : algo_dom a b) : bool by struct h := From ca73b5eac6e73f74da869d1e0d5c51e271993ab4 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 28 Feb 2025 14:42:40 -0500 Subject: [PATCH 07/10] Add more cases to tm_to_eq --- theories/executable.v | 163 ++++++++++++++++++++++-------------------- 1 file changed, 86 insertions(+), 77 deletions(-) diff --git a/theories/executable.v b/theories/executable.v index 93be579..52b9759 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -1,6 +1,6 @@ From Equations Require Import Equations. Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax. -Derive NoConfusion for sig nat PTag BTag PTm. +Derive NoConfusion for option sig nat PTag BTag PTm. Derive EqDec for BTag PTag PTm. Import Logic (inspect). @@ -236,27 +236,6 @@ Proof. move /hred_complete => + /hred_complete. congruence. Qed. -(* Equations hred_fancy (a : PTm ) : *) -(* HRed.nf a + {x | HRed.R a x} := *) -(* hred_fancy a with hra => { *) -(* hred_fancy a None := inl _; *) -(* hred_fancy a (Some b) := inr (exist _ b _) *) -(* } *) -(* with hra := hred a. *) -(* Next Obligation. *) - - -Definition hred_fancy (a : PTm) : - HRed.nf a + {x | HRed.R a x}. -Proof. - destruct (hred a) as [a'|] eqn:eq . - - right. exists a'. hauto q:on use:hred_sound. - - left. - move => a' h. - move /hred_complete in h. - congruence. -Defined. - Ltac check_equal_triv := intros;subst; lazymatch goal with @@ -265,20 +244,6 @@ Ltac check_equal_triv := | _ => idtac end. -(* Program Fixpoint check_equal {n} (a b : PTm n) (h : algo_dom a b) {struct h} : bool := *) -(* match a, b with *) -(* | VarPTm i, VarPTm j => fin_beq i j *) -(* | PAbs a, PAbs b => check_equal_r a b ltac:(check_equal_triv) *) -(* | _, _ => false *) -(* end *) -(* with check_equal_r {n} (a b : PTm n) (h : algo_dom_r a b) {struct h} : bool := *) -(* match hred_fancy _ a with *) -(* | inr a' => check_equal_r (proj1_sig a') b _ *) -(* | _ => false *) -(* end. *) -(* Next Obligation. *) -(* simpl. *) - Ltac solve_check_equal := try solve [intros *; @@ -317,57 +282,101 @@ Inductive eq_view : PTm -> PTm -> Type := | V_AbsNeu a b : ~~ isabs b -> eq_view (PAbs a) b -(* | V_NeuAbs a b : *) -(* ~~ isabs a -> *) -(* eq_view a (PAbs b) *) -(* | V_VarVar i j : *) -(* eq_view (VarPTm i) (VarPTm j) *) -(* | V_PairPair a0 b0 a1 b1 : *) -(* eq_view (PPair a0 b0) (PPair a1 b1) *) +| V_NeuAbs a b : + ~~ isabs a -> + eq_view a (PAbs b) +| V_VarVar i j : + eq_view (VarPTm i) (VarPTm j) +| V_PairPair a0 b0 a1 b1 : + eq_view (PPair a0 b0) (PPair a1 b1) +| V_PairNeu a0 b0 u : + ~~ ispair u -> + eq_view (PPair a0 b0) u +| V_NeuPair u a1 b1 : + ~~ ispair u -> + eq_view u (PPair a1 b1) +| V_ZeroZero : + eq_view PZero PZero +| V_SucSuc a b : + eq_view (PSuc a) (PSuc b) +| V_AppApp u0 b0 u1 b1 : + eq_view (PApp u0 b0) (PApp u1 b1) +| V_ProjProj p0 u0 p1 u1 : + eq_view (PProj p0 u0) (PProj p1 u1) +| V_IndInd P0 u0 b0 c0 P1 u1 b1 c1 : + eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) +| V_NatNat : + eq_view PNat PNat +| V_BindBind p0 A0 B0 p1 A1 B1 : + eq_view (PBind p0 A0 B0) (PBind p1 A1 B1) +| V_UnivUniv i j : + eq_view (PUniv i) (PUniv j) | V_Others a b : eq_view a b. Equations tm_to_eq_view (a b : PTm) : eq_view a b := tm_to_eq_view (PAbs a) (PAbs b) := V_AbsAbs a b; tm_to_eq_view (PAbs a) b := V_AbsNeu a b _; - (* tm_to_eq_view a (PAbs b) := V_NeuAbs a b _; *) + tm_to_eq_view a (PAbs b) := V_NeuAbs a b _; + tm_to_eq_view (VarPTm i) (VarPTm j) := V_VarVar i j; + tm_to_eq_view (PPair a0 b0) (PPair a1 b1) := V_PairPair a0 b0 a1 b1; + tm_to_eq_view (PPair a0 b0) u := V_PairNeu a0 b0 u _; + tm_to_eq_view u (PPair a1 b1) := V_NeuPair u a1 b1 _; + tm_to_eq_view PZero PZero := V_ZeroZero; + tm_to_eq_view (PSuc a) (PSuc b) := V_SucSuc a b; + tm_to_eq_view (PApp a0 b0) (PApp a1 b1) := V_AppApp a0 b0 a1 b1; + tm_to_eq_view (PProj p0 b0) (PProj p1 b1) := V_ProjProj p0 b0 p1 b1; + tm_to_eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) := V_IndInd P0 u0 b0 c0 P1 u1 b1 c1; + tm_to_eq_view PNat PNat := V_NatNat; + tm_to_eq_view (PUniv i) (PUniv j) := V_UnivUniv i j; + tm_to_eq_view (PBind p0 A0 B0) (PBind p1 A1 B1) := V_BindBind p0 A0 B0 p1 A1 B1; tm_to_eq_view a b := V_Others a b. +Set Transparent Obligations. + +Equations hred' (a : PTm) : option PTm := + hred' (VarPTm i) := None; + hred' (PAbs a) := None; + hred' _ := None. + Equations check_equal (a b : PTm) (h : algo_dom a b) : bool by struct h := - check_equal (VarPTm i) (VarPTm j) h := nat_eqdec i j; - check_equal (PAbs a) (PAbs b) h := check_equal_r a b ltac:(check_equal_triv); - check_equal (PAbs a) b h := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv); - check_equal a (PAbs b) h := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv); - check_equal (PPair a0 b0) (PPair a1 b1) h := - check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); - check_equal (PPair a0 b0) u h := - check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv); - check_equal u (PPair a1 b1) h := - check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv); - check_equal PNat PNat _ := true; - check_equal PZero PZero _ := true; - check_equal (PSuc a) (PSuc b) h := check_equal_r a b ltac:(check_equal_triv); - check_equal (PProj p0 a) (PProj p1 b) h := - PTag_eqdec p0 p1 && check_equal a b ltac:(check_equal_triv); - check_equal (PApp a0 b0) (PApp a1 b1) h := - check_equal a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); - check_equal (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) h := - check_equal_r P0 P1 ltac:(check_equal_triv) && - check_equal u0 u1 ltac:(check_equal_triv) && - check_equal_r b0 b1 ltac:(check_equal_triv) && - check_equal_r c0 c1 ltac:(check_equal_triv); - check_equal (PUniv i) (PUniv j) _ := Nat.eqb i j; - check_equal (PBind p0 A0 B0) (PBind p1 A1 B1) h := - BTag_eqdec p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv); - check_equal a b h := false; - with check_equal_r (a b : PTm) (h : algo_dom_r a b) : - bool by struct h := + check_equal a b h with tm_to_eq_view a b := + check_equal _ _ h (V_AbsAbs a b) := check_equal_r a b ltac:(check_equal_triv); + check_equal a b h _ := false + (* check_equal (VarPTm i) (VarPTm j) h := nat_eqdec i j; *) + (* check_equal (PAbs a) (PAbs b) h := check_equal_r a b ltac:(check_equal_triv); *) + (* check_equal (PAbs a) b h := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv); *) + (* check_equal a (PAbs b) h := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv); *) + (* check_equal (PPair a0 b0) (PPair a1 b1) h := *) + (* check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); *) + (* check_equal (PPair a0 b0) u h := *) + (* check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv); *) + (* check_equal u (PPair a1 b1) h := *) + (* check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv); *) + (* check_equal PNat PNat _ := true; *) + (* check_equal PZero PZero _ := true; *) + (* check_equal (PSuc a) (PSuc b) h := check_equal_r a b ltac:(check_equal_triv); *) + (* check_equal (PProj p0 a) (PProj p1 b) h := *) + (* PTag_eqdec p0 p1 && check_equal a b ltac:(check_equal_triv); *) + (* check_equal (PApp a0 b0) (PApp a1 b1) h := *) + (* check_equal a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); *) + (* check_equal (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) h := *) + (* check_equal_r P0 P1 ltac:(check_equal_triv) && *) + (* check_equal u0 u1 ltac:(check_equal_triv) && *) + (* check_equal_r b0 b1 ltac:(check_equal_triv) && *) + (* check_equal_r c0 c1 ltac:(check_equal_triv); *) + (* check_equal (PUniv i) (PUniv j) _ := Nat.eqb i j; *) + (* check_equal (PBind p0 A0 B0) (PBind p1 A1 B1) h := *) + (* BTag_eqdec p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv); *) + (* check_equal a b h := false; *) + with check_equal_r (a b : PTm) (h0 : algo_dom_r a b) : + bool by struct h0 := check_equal_r a b h with inspect (hred a) := - { check_equal_r a b h (exist _ (Some a') k) := check_equal_r a' b _; - check_equal_r a b h (exist _ None k) with inspect (hred b) := - { | (exist _ None l) => check_equal a b _; - | (exist _ (Some b') l) => check_equal_r a b' _}} . + check_equal_r a b h (exist _ (Some a') k) := check_equal_r a' b _; + check_equal_r a b h (exist _ None k) with inspect (hred b) := + | (exist _ None l) => check_equal a b _; + | (exist _ (Some b') l) => check_equal_r a b' _. Next Obligation. intros. @@ -405,5 +414,5 @@ Next Obligation. Defined. Next Obligation. - sauto. + qauto inv:algo_dom, algo_dom_r. Defined. From 816c73cb7104b54c93f2a503c74dc08c4af7dbf9 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 28 Feb 2025 14:50:42 -0500 Subject: [PATCH 08/10] Switch to view pattern --- theories/executable.v | 57 ++++++++++++++++++++----------------------- 1 file changed, 26 insertions(+), 31 deletions(-) diff --git a/theories/executable.v b/theories/executable.v index 52b9759..955ef1d 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -334,41 +334,36 @@ Equations tm_to_eq_view (a b : PTm) : eq_view a b := Set Transparent Obligations. -Equations hred' (a : PTm) : option PTm := - hred' (VarPTm i) := None; - hred' (PAbs a) := None; - hred' _ := None. - Equations check_equal (a b : PTm) (h : algo_dom a b) : bool by struct h := check_equal a b h with tm_to_eq_view a b := + check_equal _ _ h (V_VarVar i j) := nat_eqdec i j; check_equal _ _ h (V_AbsAbs a b) := check_equal_r a b ltac:(check_equal_triv); - check_equal a b h _ := false - (* check_equal (VarPTm i) (VarPTm j) h := nat_eqdec i j; *) - (* check_equal (PAbs a) (PAbs b) h := check_equal_r a b ltac:(check_equal_triv); *) - (* check_equal (PAbs a) b h := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv); *) - (* check_equal a (PAbs b) h := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv); *) - (* check_equal (PPair a0 b0) (PPair a1 b1) h := *) - (* check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); *) - (* check_equal (PPair a0 b0) u h := *) - (* check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv); *) - (* check_equal u (PPair a1 b1) h := *) - (* check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv); *) - (* check_equal PNat PNat _ := true; *) - (* check_equal PZero PZero _ := true; *) - (* check_equal (PSuc a) (PSuc b) h := check_equal_r a b ltac:(check_equal_triv); *) - (* check_equal (PProj p0 a) (PProj p1 b) h := *) - (* PTag_eqdec p0 p1 && check_equal a b ltac:(check_equal_triv); *) - (* check_equal (PApp a0 b0) (PApp a1 b1) h := *) - (* check_equal a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); *) - (* check_equal (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) h := *) - (* check_equal_r P0 P1 ltac:(check_equal_triv) && *) - (* check_equal u0 u1 ltac:(check_equal_triv) && *) - (* check_equal_r b0 b1 ltac:(check_equal_triv) && *) - (* check_equal_r c0 c1 ltac:(check_equal_triv); *) - (* check_equal (PUniv i) (PUniv j) _ := Nat.eqb i j; *) - (* check_equal (PBind p0 A0 B0) (PBind p1 A1 B1) h := *) - (* BTag_eqdec p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv); *) + check_equal _ _ h (V_AbsNeu a b _) := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv); + check_equal _ _ h (V_NeuAbs a b _) := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv); + check_equal _ _ h (V_PairPair a0 b0 a1 b1) := + check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); + check_equal _ _ h (V_PairNeu a0 b0 u _) := + check_equal_r a0 (PProj PL u) ltac:(check_equal_triv) && check_equal_r b0 (PProj PR u) ltac:(check_equal_triv); + check_equal _ _ h (V_NeuPair u a1 b1 _) := + check_equal_r (PProj PL u) a1 ltac:(check_equal_triv) && check_equal_r (PProj PR u) b1 ltac:(check_equal_triv); + check_equal _ _ h V_NatNat := true; + check_equal _ _ h V_ZeroZero := true; + check_equal _ _ h (V_SucSuc a b) := check_equal_r a b ltac:(check_equal_triv); + check_equal _ _ h (V_ProjProj p0 a p1 b) := + PTag_eqdec p0 p1 && check_equal a b ltac:(check_equal_triv); + check_equal _ _ h (V_AppApp a0 b0 a1 b1) := + check_equal a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); + check_equal _ _ h (V_IndInd P0 u0 b0 c0 P1 u1 b1 c1) := + check_equal_r P0 P1 ltac:(check_equal_triv) && + check_equal u0 u1 ltac:(check_equal_triv) && + check_equal_r b0 b1 ltac:(check_equal_triv) && + check_equal_r c0 c1 ltac:(check_equal_triv); + check_equal _ _ h (V_UnivUniv i j) := Nat.eqb i j; + check_equal _ _ h (V_BindBind p0 A0 B0 p1 A1 B1) := + BTag_eqdec p0 p1 && check_equal_r A0 A1 ltac:(check_equal_triv) && check_equal_r B0 B1 ltac:(check_equal_triv); + check_equal _ _ _ _ := false + (* check_equal a b h := false; *) with check_equal_r (a b : PTm) (h0 : algo_dom_r a b) : bool by struct h0 := From 7b5e9f2562984c90f82dd011c977e38ed581e28c Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 28 Feb 2025 15:56:37 -0500 Subject: [PATCH 09/10] view needs more information --- theories/executable.v | 208 ++++++++++++++++++++++++++---------------- 1 file changed, 127 insertions(+), 81 deletions(-) diff --git a/theories/executable.v b/theories/executable.v index 955ef1d..e69a6dd 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -3,11 +3,11 @@ Require Import Autosubst2.core Autosubst2.unscoped Autosubst2.syntax. Derive NoConfusion for option sig nat PTag BTag PTm. Derive EqDec for BTag PTag PTm. Import Logic (inspect). +Require Import Cdcl.Itauto. Require Import ssreflect ssrbool. From Hammer Require Import Tactics. - Definition ishf (a : PTm) := match a with | PPair _ _ => true @@ -60,6 +60,104 @@ Module HRed. End HRed. +Definition isbind (a : PTm) := if a is PBind _ _ _ then true else false. + +Definition isuniv (a : PTm) := if a is PUniv _ then true else false. + +Definition ispair (a : PTm) := + match a with + | PPair _ _ => true + | _ => false + end. + +Definition isnat (a : PTm) := if a is PNat then true else false. + +Definition iszero (a : PTm) := if a is PZero then true else false. + +Definition issuc (a : PTm) := if a is PSuc _ then true else false. + +Definition isabs (a : PTm) := + match a with + | PAbs _ => true + | _ => false + end. + +Inductive eq_view : PTm -> PTm -> Type := +| V_AbsAbs a b : + eq_view (PAbs a) (PAbs b) +| V_AbsNeu a b : + ~~ isabs b -> + eq_view (PAbs a) b +| V_NeuAbs a b : + ~~ isabs a -> + eq_view a (PAbs b) +| V_VarVar i j : + eq_view (VarPTm i) (VarPTm j) +| V_PairPair a0 b0 a1 b1 : + eq_view (PPair a0 b0) (PPair a1 b1) +| V_PairNeu a0 b0 u : + ~~ ispair u -> + eq_view (PPair a0 b0) u +| V_NeuPair u a1 b1 : + ~~ ispair u -> + eq_view u (PPair a1 b1) +| V_ZeroZero : + eq_view PZero PZero +| V_SucSuc a b : + eq_view (PSuc a) (PSuc b) +| V_AppApp u0 b0 u1 b1 : + eq_view (PApp u0 b0) (PApp u1 b1) +| V_ProjProj p0 u0 p1 u1 : + eq_view (PProj p0 u0) (PProj p1 u1) +| V_IndInd P0 u0 b0 c0 P1 u1 b1 c1 : + eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) +| V_NatNat : + eq_view PNat PNat +| V_BindBind p0 A0 B0 p1 A1 B1 : + eq_view (PBind p0 A0 B0) (PBind p1 A1 B1) +| V_UnivUniv i j : + eq_view (PUniv i) (PUniv j) +| V_Others a b : + eq_view a b. + +Equations tm_to_eq_view (a b : PTm) : eq_view a b := + tm_to_eq_view (PAbs a) (PAbs b) := V_AbsAbs a b; + tm_to_eq_view (PAbs a) b := V_AbsNeu a b _; + tm_to_eq_view a (PAbs b) := V_NeuAbs a b _; + tm_to_eq_view (VarPTm i) (VarPTm j) := V_VarVar i j; + tm_to_eq_view (PPair a0 b0) (PPair a1 b1) := V_PairPair a0 b0 a1 b1; + tm_to_eq_view (PPair a0 b0) u := V_PairNeu a0 b0 u _; + tm_to_eq_view u (PPair a1 b1) := V_NeuPair u a1 b1 _; + tm_to_eq_view PZero PZero := V_ZeroZero; + tm_to_eq_view (PSuc a) (PSuc b) := V_SucSuc a b; + tm_to_eq_view (PApp a0 b0) (PApp a1 b1) := V_AppApp a0 b0 a1 b1; + tm_to_eq_view (PProj p0 b0) (PProj p1 b1) := V_ProjProj p0 b0 p1 b1; + tm_to_eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) := V_IndInd P0 u0 b0 c0 P1 u1 b1 c1; + tm_to_eq_view PNat PNat := V_NatNat; + tm_to_eq_view (PUniv i) (PUniv j) := V_UnivUniv i j; + tm_to_eq_view (PBind p0 A0 B0) (PBind p1 A1 B1) := V_BindBind p0 A0 B0 p1 A1 B1; + tm_to_eq_view a b := V_Others a b. + +Definition tm_nonconf (a b : PTm) : bool := + match a, b with + | PAbs _, _ => ishne b || isabs b + | _, PAbs _ => ishne a + | VarPTm _, VarPTm _ => true + | PPair _ _, _ => ishne b || ispair b + | _, PPair _ _ => ishne a + | PZero, PZero => true + | PSuc _, PSuc _ => true + | PApp _ _, PApp _ _ => ishne a && ishne b + | PProj _ _, PProj _ _ => ishne a && ishne b + | PInd _ _ _ _, PInd _ _ _ _ => ishne a && ishne b + | PNat, PNat => true + | PUniv _, PUniv _ => true + | PBind _ _ _, PBind _ _ _ => true + | _,_=> false + end. + +Definition tm_conf (a b : PTm) := ~~ tm_nonconf a b. + Inductive algo_dom : PTm -> PTm -> Prop := | A_AbsAbs a b : algo_dom_r a b -> @@ -146,6 +244,13 @@ Inductive algo_dom : PTm -> PTm -> Prop := algo_dom_r c0 c1 -> algo_dom (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) +| A_Conflicting a b : + ishne a \/ ishf a -> + ishne b \/ ishf b -> + (* yes they are equivalent, but need both sides to make the rule reduce better *) + ~ tm_nonconf a b -> + algo_dom a b + with algo_dom_r : PTm -> PTm -> Prop := | A_NfNf a b : algo_dom a b -> @@ -240,11 +345,10 @@ Ltac check_equal_triv := intros;subst; lazymatch goal with (* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *) - | [h : algo_dom _ _ |- _] => try inversion h; by subst + | [h : algo_dom _ _ |- _] => try (inversion h; subst;simpl in *; by first [done | exfalso; first [done|sfirstorder b:on]]) | _ => idtac end. - Ltac solve_check_equal := try solve [intros *; match goal with @@ -254,92 +358,24 @@ Ltac solve_check_equal := (* #[export,global] Obligation Tactic := idtac "fiewof". *) -Definition isbind (a : PTm) := if a is PBind _ _ _ then true else false. - -Definition isuniv (a : PTm) := if a is PUniv _ then true else false. - -Definition ispair (a : PTm) := - match a with - | PPair _ _ => true - | _ => false - end. - -Definition isnat (a : PTm) := if a is PNat then true else false. - -Definition iszero (a : PTm) := if a is PZero then true else false. - -Definition issuc (a : PTm) := if a is PSuc _ then true else false. - -Definition isabs (a : PTm) := - match a with - | PAbs _ => true - | _ => false - end. - -Inductive eq_view : PTm -> PTm -> Type := -| V_AbsAbs a b : - eq_view (PAbs a) (PAbs b) -| V_AbsNeu a b : - ~~ isabs b -> - eq_view (PAbs a) b -| V_NeuAbs a b : - ~~ isabs a -> - eq_view a (PAbs b) -| V_VarVar i j : - eq_view (VarPTm i) (VarPTm j) -| V_PairPair a0 b0 a1 b1 : - eq_view (PPair a0 b0) (PPair a1 b1) -| V_PairNeu a0 b0 u : - ~~ ispair u -> - eq_view (PPair a0 b0) u -| V_NeuPair u a1 b1 : - ~~ ispair u -> - eq_view u (PPair a1 b1) -| V_ZeroZero : - eq_view PZero PZero -| V_SucSuc a b : - eq_view (PSuc a) (PSuc b) -| V_AppApp u0 b0 u1 b1 : - eq_view (PApp u0 b0) (PApp u1 b1) -| V_ProjProj p0 u0 p1 u1 : - eq_view (PProj p0 u0) (PProj p1 u1) -| V_IndInd P0 u0 b0 c0 P1 u1 b1 c1 : - eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) -| V_NatNat : - eq_view PNat PNat -| V_BindBind p0 A0 B0 p1 A1 B1 : - eq_view (PBind p0 A0 B0) (PBind p1 A1 B1) -| V_UnivUniv i j : - eq_view (PUniv i) (PUniv j) -| V_Others a b : - eq_view a b. - -Equations tm_to_eq_view (a b : PTm) : eq_view a b := - tm_to_eq_view (PAbs a) (PAbs b) := V_AbsAbs a b; - tm_to_eq_view (PAbs a) b := V_AbsNeu a b _; - tm_to_eq_view a (PAbs b) := V_NeuAbs a b _; - tm_to_eq_view (VarPTm i) (VarPTm j) := V_VarVar i j; - tm_to_eq_view (PPair a0 b0) (PPair a1 b1) := V_PairPair a0 b0 a1 b1; - tm_to_eq_view (PPair a0 b0) u := V_PairNeu a0 b0 u _; - tm_to_eq_view u (PPair a1 b1) := V_NeuPair u a1 b1 _; - tm_to_eq_view PZero PZero := V_ZeroZero; - tm_to_eq_view (PSuc a) (PSuc b) := V_SucSuc a b; - tm_to_eq_view (PApp a0 b0) (PApp a1 b1) := V_AppApp a0 b0 a1 b1; - tm_to_eq_view (PProj p0 b0) (PProj p1 b1) := V_ProjProj p0 b0 p1 b1; - tm_to_eq_view (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) := V_IndInd P0 u0 b0 c0 P1 u1 b1 c1; - tm_to_eq_view PNat PNat := V_NatNat; - tm_to_eq_view (PUniv i) (PUniv j) := V_UnivUniv i j; - tm_to_eq_view (PBind p0 A0 B0) (PBind p1 A1 B1) := V_BindBind p0 A0 B0 p1 A1 B1; - tm_to_eq_view a b := V_Others a b. Set Transparent Obligations. +(* Lemma algo_dom_abs_inv a b : *) +(* algo_dom (PAbs a) b -> ishne b \/ isabs b. *) +(* Proof. *) +(* inversion 1; subst=>//=. itauto. *) +(* itauto. *) +(* simpl in H2. *) +(* simpl in H2. move /negP in H2. move/norP in H2. *) +(* clear H0. left. *) + Equations check_equal (a b : PTm) (h : algo_dom a b) : bool by struct h := check_equal a b h with tm_to_eq_view a b := check_equal _ _ h (V_VarVar i j) := nat_eqdec i j; check_equal _ _ h (V_AbsAbs a b) := check_equal_r a b ltac:(check_equal_triv); - check_equal _ _ h (V_AbsNeu a b _) := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv); + check_equal _ _ h (V_AbsNeu a b h') := check_equal_r a (PApp (ren_PTm shift b) (VarPTm var_zero)) ltac:(check_equal_triv); check_equal _ _ h (V_NeuAbs a b _) := check_equal_r (PApp (ren_PTm shift a) (VarPTm var_zero)) b ltac:(check_equal_triv); check_equal _ _ h (V_PairPair a0 b0 a1 b1) := check_equal_r a0 a1 ltac:(check_equal_triv) && check_equal_r b0 b1 ltac:(check_equal_triv); @@ -373,6 +409,15 @@ Equations check_equal (a b : PTm) (h : algo_dom a b) : | (exist _ None l) => check_equal a b _; | (exist _ (Some b') l) => check_equal_r a b' _. +Next Obligation. + inversion h; subst;simpl in *; try by first [done | exfalso; first [done|sfirstorder b:on]]. + exfalso. + move /negP /norP in H1. + destruct H0 => //=. sfirstorder b:on. + + + + Next Obligation. intros. destruct h. @@ -411,3 +456,4 @@ Defined. Next Obligation. qauto inv:algo_dom, algo_dom_r. Defined. +(* Do not step back from here or otherwise equations will cause an error *) From 3efca4160be6ae39cd7a4467ff64f88070a3188a Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 28 Feb 2025 16:39:10 -0500 Subject: [PATCH 10/10] Add noconf check --- theories/executable.v | 74 +++++++++++++------------------------------ 1 file changed, 22 insertions(+), 52 deletions(-) diff --git a/theories/executable.v b/theories/executable.v index e69a6dd..f7d6707 100644 --- a/theories/executable.v +++ b/theories/executable.v @@ -82,6 +82,26 @@ Definition isabs (a : PTm) := | _ => false end. +Definition tm_nonconf (a b : PTm) : bool := + match a, b with + | PAbs _, _ => ishne b || isabs b + | _, PAbs _ => ishne a + | VarPTm _, VarPTm _ => true + | PPair _ _, _ => ishne b || ispair b + | _, PPair _ _ => ishne a + | PZero, PZero => true + | PSuc _, PSuc _ => true + | PApp _ _, PApp _ _ => ishne a && ishne b + | PProj _ _, PProj _ _ => ishne a && ishne b + | PInd _ _ _ _, PInd _ _ _ _ => ishne a && ishne b + | PNat, PNat => true + | PUniv _, PUniv _ => true + | PBind _ _ _, PBind _ _ _ => true + | _,_=> false + end. + +Definition tm_conf (a b : PTm) := ~~ tm_nonconf a b. + Inductive eq_view : PTm -> PTm -> Type := | V_AbsAbs a b : eq_view (PAbs a) (PAbs b) @@ -138,26 +158,6 @@ Equations tm_to_eq_view (a b : PTm) : eq_view a b := tm_to_eq_view (PBind p0 A0 B0) (PBind p1 A1 B1) := V_BindBind p0 A0 B0 p1 A1 B1; tm_to_eq_view a b := V_Others a b. -Definition tm_nonconf (a b : PTm) : bool := - match a, b with - | PAbs _, _ => ishne b || isabs b - | _, PAbs _ => ishne a - | VarPTm _, VarPTm _ => true - | PPair _ _, _ => ishne b || ispair b - | _, PPair _ _ => ishne a - | PZero, PZero => true - | PSuc _, PSuc _ => true - | PApp _ _, PApp _ _ => ishne a && ishne b - | PProj _ _, PProj _ _ => ishne a && ishne b - | PInd _ _ _ _, PInd _ _ _ _ => ishne a && ishne b - | PNat, PNat => true - | PUniv _, PUniv _ => true - | PBind _ _ _, PBind _ _ _ => true - | _,_=> false - end. - -Definition tm_conf (a b : PTm) := ~~ tm_nonconf a b. - Inductive algo_dom : PTm -> PTm -> Prop := | A_AbsAbs a b : algo_dom_r a b -> @@ -244,13 +244,6 @@ Inductive algo_dom : PTm -> PTm -> Prop := algo_dom_r c0 c1 -> algo_dom (PInd P0 u0 b0 c0) (PInd P1 u1 b1 c1) -| A_Conflicting a b : - ishne a \/ ishf a -> - ishne b \/ ishf b -> - (* yes they are equivalent, but need both sides to make the rule reduce better *) - ~ tm_nonconf a b -> - algo_dom a b - with algo_dom_r : PTm -> PTm -> Prop := | A_NfNf a b : algo_dom a b -> @@ -345,7 +338,7 @@ Ltac check_equal_triv := intros;subst; lazymatch goal with (* | [h : algo_dom (VarPTm _) (PAbs _) |- _] => idtac *) - | [h : algo_dom _ _ |- _] => try (inversion h; subst;simpl in *; by first [done | exfalso; first [done|sfirstorder b:on]]) + | [h : algo_dom _ _ |- _] => try (inversion h; by subst) | _ => idtac end. @@ -356,20 +349,6 @@ Ltac solve_check_equal := | _ => idtac end]. -(* #[export,global] Obligation Tactic := idtac "fiewof". *) - - -Set Transparent Obligations. - -(* Lemma algo_dom_abs_inv a b : *) -(* algo_dom (PAbs a) b -> ishne b \/ isabs b. *) -(* Proof. *) -(* inversion 1; subst=>//=. itauto. *) -(* itauto. *) -(* simpl in H2. *) -(* simpl in H2. move /negP in H2. move/norP in H2. *) -(* clear H0. left. *) - Equations check_equal (a b : PTm) (h : algo_dom a b) : bool by struct h := check_equal a b h with tm_to_eq_view a b := @@ -406,18 +385,9 @@ Equations check_equal (a b : PTm) (h : algo_dom a b) : check_equal_r a b h with inspect (hred a) := check_equal_r a b h (exist _ (Some a') k) := check_equal_r a' b _; check_equal_r a b h (exist _ None k) with inspect (hred b) := - | (exist _ None l) => check_equal a b _; + | (exist _ None l) => tm_nonconf a b && check_equal a b _; | (exist _ (Some b') l) => check_equal_r a b' _. -Next Obligation. - inversion h; subst;simpl in *; try by first [done | exfalso; first [done|sfirstorder b:on]]. - exfalso. - move /negP /norP in H1. - destruct H0 => //=. sfirstorder b:on. - - - - Next Obligation. intros. destruct h.