From ca73b5eac6e73f74da869d1e0d5c51e271993ab4 Mon Sep 17 00:00:00 2001 From: Yiyun Liu Date: Fri, 28 Feb 2025 14:42:40 -0500 Subject: [PATCH] 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.