Skip to content

Commit

Permalink
Term sorry eradication
Browse files Browse the repository at this point in the history
  • Loading branch information
@imbrem
imbrem committed Sep 6, 2024
1 parent 396e5de commit 64b20f4
Show file tree
Hide file tree
Showing 3 changed files with 67 additions and 45 deletions.
17 changes: 13 additions & 4 deletions DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Seq.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,14 +81,23 @@ theorem Eqv.pure_seq {A B C : Ty α} {Γ : Ctx α ε}
theorem Eqv.wk_lift_seq {A B C : Ty α} {Δ : Ctx α ε} {ρ : Ctx.InS Γ Δ}
(a : Eqv φ ((A, ⊥)::Δ) (B, e)) (b : Eqv φ ((B, ⊥)::Δ) (C, e))
: (a ;;' b).wk (ρ.lift (le_refl _)) = (a.wk (ρ.lift (le_refl _))) ;;' (b.wk (ρ.lift (le_refl _)))
-- TODO: obviously true, need InS lemma
:= by rw [seq, seq, wk_let1]; sorry
:= by rw [seq, seq, wk_let1]; simp only [wk1, wk_wk]; congr 2; ext k; cases k <;> rfl

theorem Eqv.subst_lift_seq {A B C : Ty α} {Δ : Ctx α ε} {σ : Subst.Eqv φ Γ Δ}
(a : Eqv φ ((A, ⊥)::Δ) (B, e)) (b : Eqv φ ((B, ⊥)::Δ) (C, e))
: (a ;;' b).subst (σ.lift (le_refl _))
= (a.subst (σ.lift (le_refl _))) ;;' (b.subst (σ.lift (le_refl _)))
:= sorry
= (a.subst (σ.lift (le_refl _))) ;;' (b.subst (σ.lift (le_refl _))) := by
rw [seq, seq, subst_let1]
congr
induction σ using Quotient.inductionOn
induction b using Quotient.inductionOn
apply Eqv.eq_of_term_eq
simp only [Set.mem_setOf_eq, InS.coe_subst, Subst.InS.coe_lift, InS.coe_wk, Ctx.InS.coe_wk1, ←
Term.subst_fromWk, Term.subst_subst]
congr
funext k; cases k <;> simp only [Subst.comp, Term.subst, Nat.liftWk_succ, Nat.succ_eq_add_one,
Subst.lift_succ, Term.wk_wk, Term.subst_fromWk, Nat.liftWk_succ_comp_succ] <;> rfl

theorem Eqv.wk0_seq {A B C : Ty α} {Γ : Ctx α ε}
(a : Eqv φ ((A, ⊥)::Γ) (B, e)) (b : Eqv φ ((B, ⊥)::Γ) (C, e))
: (a ;;' b).wk0 (head := ⟨head, ⊥⟩) = a.wk0 ;;' b.wk1 := by rw [seq, wk0_let1]; rfl
Expand Down
36 changes: 20 additions & 16 deletions DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Sum.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,19 +22,17 @@ theorem Eqv.swap_sum_swap_sum {A B : Ty α} {Γ : Ctx α ε}
simp [swap_sum, case_inl, case_inr, case_eta, case_case, let1_beta_var0]

theorem Eqv.let1_swap_sum {A B : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X, e⟩}
{r : Eqv φ (⟨X, ⊥⟩::Γ) ⟨A.coprod B, e⟩}
: let1 a (swap_sum r) = swap_sum (let1 a r) := sorry
{a : Eqv φ Γ ⟨X, e⟩} {r : Eqv φ (⟨X, ⊥⟩::Γ) ⟨A.coprod B, e⟩}
: let1 a (swap_sum r) = swap_sum (let1 a r) := by simp only [swap_sum, case_let1]; rfl

theorem Eqv.swap_sum_let1 {A B : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨A, e⟩}
{r : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B.coprod A, e⟩}
{a : Eqv φ Γ ⟨A, e⟩} {r : Eqv φ (⟨A, ⊥⟩::Γ) ⟨B.coprod A, e⟩}
: swap_sum (let1 a r) = let1 a (swap_sum r) := let1_swap_sum.symm

theorem Eqv.let2_swap_sum {A B : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X.prod Y, e⟩}
{r : Eqv φ (⟨Y, ⊥⟩::⟨X, ⊥⟩::Γ) ⟨A.coprod B, e⟩}
: let2 a (swap_sum r) = swap_sum (let2 a r) := sorry
: let2 a (swap_sum r) = swap_sum (let2 a r) := by simp only [swap_sum, case_let2]; rfl

theorem Eqv.swap_sum_let2 {A B : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X.prod Y, e⟩}
Expand All @@ -45,7 +43,8 @@ theorem Eqv.case_swap_sum {A B : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X.coprod Y, e⟩}
{r : Eqv φ (⟨X, ⊥⟩::Γ) ⟨A.coprod B, e⟩}
{s : Eqv φ (⟨Y, ⊥⟩::Γ) ⟨A.coprod B, e⟩}
: case a (swap_sum r) (swap_sum s) = swap_sum (case a r s) := sorry
: case a (swap_sum r) (swap_sum s) = swap_sum (case a r s)
:= by simp only [swap_sum, case_case]; rfl

theorem Eqv.swap_sum_case {A B : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X.coprod Y, e⟩}
Expand All @@ -55,7 +54,7 @@ theorem Eqv.swap_sum_case {A B : Ty α} {Γ : Ctx α ε}

theorem Eqv.wk_swap_sum {A B : Ty α} {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ}
{r : Eqv φ Δ ⟨A.coprod B, e⟩}
: wk ρ (swap_sum r) = swap_sum (wk ρ r) := sorry
: wk ρ (swap_sum r) = swap_sum (wk ρ r) := by simp [swap_sum]

theorem Eqv.swap_sum_wk {A B : Ty α} {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ}
{r : Eqv φ Δ ⟨A.coprod B, e⟩}
Expand Down Expand Up @@ -139,7 +138,7 @@ theorem Eqv.reassoc_inv_reassoc_sum {A B C : Ty α} {Γ : Ctx α ε}
theorem Eqv.let1_reassoc_sum {A B C : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X, e⟩}
{r : Eqv φ (⟨X, ⊥⟩::Γ) ⟨(A.coprod B).coprod C, e⟩}
: let1 a (reassoc_sum r) = reassoc_sum (let1 a r) := sorry
: let1 a (reassoc_sum r) = reassoc_sum (let1 a r) := by simp only [reassoc_sum, case_let1]; rfl

theorem Eqv.reassoc_sum_let1 {A B C : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X, e⟩}
Expand All @@ -149,7 +148,7 @@ theorem Eqv.reassoc_sum_let1 {A B C : Ty α} {Γ : Ctx α ε}
theorem Eqv.let2_reassoc_sum {A B C : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X.prod Y, e⟩}
{r : Eqv φ (⟨Y, ⊥⟩::⟨X, ⊥⟩::Γ) ⟨(A.coprod B).coprod C, e⟩}
: let2 a (reassoc_sum r) = reassoc_sum (let2 a r) := sorry
: let2 a (reassoc_sum r) = reassoc_sum (let2 a r) := by simp only [reassoc_sum, case_let2]; rfl

theorem Eqv.reassoc_sum_let2 {A B C : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X.prod Y, e⟩}
Expand All @@ -160,7 +159,8 @@ theorem Eqv.case_reassoc_sum {A B C : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X.coprod Y, e⟩}
{r : Eqv φ (⟨X, ⊥⟩::Γ) ⟨(A.coprod B).coprod C, e⟩}
{s : Eqv φ (⟨Y, ⊥⟩::Γ) ⟨(A.coprod B).coprod C, e⟩}
: case a (reassoc_sum r) (reassoc_sum s) = reassoc_sum (case a r s) := sorry
: case a (reassoc_sum r) (reassoc_sum s) = reassoc_sum (case a r s)
:= by simp only [reassoc_sum, case_case]; rfl

theorem Eqv.reassoc_sum_case {A B C : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X.coprod Y, e⟩}
Expand All @@ -170,7 +170,7 @@ theorem Eqv.reassoc_sum_case {A B C : Ty α} {Γ : Ctx α ε}

theorem Eqv.wk_reassoc_sum {A B C : Ty α} {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ}
{r : Eqv φ Δ ⟨(A.coprod B).coprod C, e⟩}
: wk ρ (reassoc_sum r) = reassoc_sum (wk ρ r) := sorry
: wk ρ (reassoc_sum r) = reassoc_sum (wk ρ r) := by simp [reassoc_sum]

theorem Eqv.reassoc_sum_wk {A B C : Ty α} {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ}
{r : Eqv φ Δ ⟨(A.coprod B).coprod C, e⟩}
Expand Down Expand Up @@ -210,7 +210,8 @@ theorem Eqv.reassoc_sum_seq {X Y A B C : Ty α} {Γ : Ctx α ε}
theorem Eqv.let1_reassoc_inv_sum {A B C : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X, e⟩}
{r : Eqv φ (⟨X, ⊥⟩::Γ) ⟨A.coprod (B.coprod C), e⟩}
: let1 a (reassoc_inv_sum r) = reassoc_inv_sum (let1 a r) := sorry
: let1 a (reassoc_inv_sum r) = reassoc_inv_sum (let1 a r)
:= by simp only [reassoc_inv_sum, case_let1]; rfl

theorem Eqv.reassoc_inv_sum_let1 {A B C : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X, e⟩}
Expand All @@ -220,7 +221,8 @@ theorem Eqv.reassoc_inv_sum_let1 {A B C : Ty α} {Γ : Ctx α ε}
theorem Eqv.let2_reassoc_inv_sum {A B C : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X.prod Y, e⟩}
{r : Eqv φ (⟨Y, ⊥⟩::⟨X, ⊥⟩::Γ) ⟨A.coprod (B.coprod C), e⟩}
: let2 a (reassoc_inv_sum r) = reassoc_inv_sum (let2 a r) := sorry
: let2 a (reassoc_inv_sum r) = reassoc_inv_sum (let2 a r)
:= by simp only [reassoc_inv_sum, case_let2]; rfl

theorem Eqv.reassoc_inv_sum_let2 {A B C : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X.prod Y, e⟩}
Expand All @@ -231,7 +233,8 @@ theorem Eqv.case_reassoc_inv_sum {A B C : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X.coprod Y, e⟩}
{r : Eqv φ (⟨X, ⊥⟩::Γ) ⟨A.coprod (B.coprod C), e⟩}
{s : Eqv φ (⟨Y, ⊥⟩::Γ) ⟨A.coprod (B.coprod C), e⟩}
: case a (reassoc_inv_sum r) (reassoc_inv_sum s) = reassoc_inv_sum (case a r s) := sorry
: case a (reassoc_inv_sum r) (reassoc_inv_sum s) = reassoc_inv_sum (case a r s)
:= by simp only [reassoc_inv_sum, case_case]; rfl

theorem Eqv.reassoc_inv_sum_case {A B C : Ty α} {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨X.coprod Y, e⟩}
Expand All @@ -242,7 +245,8 @@ theorem Eqv.reassoc_inv_sum_case {A B C : Ty α} {Γ : Ctx α ε}

theorem Eqv.wk_reassoc_inv_sum {A B C : Ty α} {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ}
{r : Eqv φ Δ ⟨A.coprod (B.coprod C), e⟩}
: wk ρ (reassoc_inv_sum r) = reassoc_inv_sum (wk ρ r) := sorry
: wk ρ (reassoc_inv_sum r) = reassoc_inv_sum (wk ρ r)
:= by simp [reassoc_inv_sum]

theorem Eqv.reassoc_inv_sum_wk {A B C : Ty α} {Γ Δ : Ctx α ε} {ρ : Γ.InS Δ}
{r : Eqv φ Δ ⟨A.coprod (B.coprod C), e⟩}
Expand Down
59 changes: 34 additions & 25 deletions DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1590,38 +1590,47 @@ theorem Eqv.Pure.pair_pi_l_pi_r' {Γ : Ctx α ε}
: pair (let2 a (var 1 (by simp))) (let2 a (var 0 (by simp))) = a
:= by rw [<-ha.let2_dist_pair, let2_eta]

theorem Eqv.let2_var0_dist_let1 {Γ : Ctx α ε}
{b : Eqv φ ((B, ⊥)::(A, ⊥)::(A.prod B, ⊥)::Γ) ⟨C, e⟩}
{c : Eqv φ ((C, ⊥)::(B, ⊥)::(A, ⊥)::(A.prod B, ⊥)::Γ) ⟨D, e⟩}
: let2 (var 0 (by simp)) (let1 b c)
= let1 (let2 (var 0 (by simp)) b) (let2 (var 1 (by simp)) c.swap02) := by
conv => lhs; rw [<-Pure.pair_pi_l_pi_r' (a := (var 0 (by simp))) ⟨var 0 Ctx.Var.shead, rfl⟩]
rw [let2_pair]
sorry
theorem Eqv.pair_pi_l_pi_r'_pure {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨A.prod B, ⊥⟩}
: (pair
(let2 a (var 1 Ctx.Var.shead.step))
(let2 a (var 0 Ctx.Var.shead)))
= a := by rw [Pure.pair_pi_l_pi_r']; simp

theorem Eqv.pair_pi_l_pi_r'_wk_eff {Γ : Ctx α ε} {e}
{a : Eqv φ Γ ⟨A.prod B, ⊥⟩}
: (pair
(let2 a (var 1 Ctx.Var.shead.step))
(let2 a (var 0 Ctx.Var.shead))).wk_eff (by simp)
= a.wk_eff (hi := e) (by simp) := by rw [pair_pi_l_pi_r'_pure]

theorem Eqv.Pure.let2_dist_let1 {Γ : Ctx α ε}
{a : Eqv φ Γ ⟨A.prod B, e⟩} {b : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) ⟨C, e⟩}
{c : Eqv φ ((C, ⊥)::(B, ⊥)::(A, ⊥)::Γ) ⟨D, e⟩} (ha : a.Pure)
: let2 a (let1 b c) = let1 (let2 a b) (let2 a.wk0 c.swap02) := by
rw [let2_bind (a := a)]
simp only [wk2, wk_let1, let2_var0_dist_let1]
cases ha with
| intro a ha =>
{c : Eqv φ ((C, ⊥)::(B, ⊥)::(A, ⊥)::Γ) ⟨D, e⟩}
: a.Pure → let2 a (let1 b c) = let1 (let2 a b) (let2 a.wk0 c.swap02)
| ⟨a, ha⟩ => by
cases ha
simp only [let1_beta, subst_let1, subst_let2, var0_subst0, List.length_cons, Fin.zero_eta,
List.get_eq_getElem, Fin.val_zero, List.getElem_cons_zero, wk_res_eff, subst_lift_var_succ,
Nat.reduceAdd, wk0_wk_eff]
rw [<-pair_pi_l_pi_r'_wk_eff]
simp only [wk_eff_pair, wk0_pair, let2_pair, wk0_wk_eff, let1_beta]
simp only [wk0_let2, wk2_var0, List.length_cons, Fin.zero_eta, List.get_eq_getElem,
Fin.val_zero, List.getElem_cons_zero, subst_let1, wk2_var1, Fin.mk_one, Fin.val_one,
List.getElem_cons_succ]
congr 1
induction a using Quotient.inductionOn
induction b using Quotient.inductionOn
induction c using Quotient.inductionOn
apply Eqv.eq_of_term_eq
simp only [Set.mem_setOf_eq, InS.coe_let1, InS.coe_let2, InS.coe_subst, Subst.InS.coe_liftn₂,
InS.coe_subst0, InS.coe_wk, Ctx.InS.coe_wk2, Subst.InS.coe_lift, Ctx.InS.coe_swap02,
Ctx.InS.coe_lift, Term.wk_wk, let2.injEq, let1.injEq, true_and]
simp only [← Term.subst_fromWk, Term.subst_subst]
constructor
· apply Term.subst_id'; funext k; cases k using Nat.cases2 <;> rfl
· congr; funext k; cases k using Nat.cases3 <;> rfl
simp only [Set.mem_setOf_eq, InS.coe_subst, Subst.InS.coe_lift, InS.coe_subst0, InS.coe_let2,
InS.coe_var, InS.coe_wk, Ctx.InS.coe_wk0, Ctx.InS.coe_swap02, Term.wk_wk]
simp only [<-Term.subst_fromWk, Term.subst_subst]
congr
funext k
cases k using Nat.cases3 with
| one =>
simp only [Subst.comp, Term.subst, ← Term.subst_fromWk, Term.subst_subst, Subst.liftn,
Nat.liftnWk, zero_lt_two, ↓reduceIte, let2.injEq, and_true]
rfl
| two => simp [Subst.comp, Term.subst_fromWk, Nat.liftnWk]
| _ => rfl

theorem Eqv.Pure.let2_wk0_wk0 {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A.prod B, e⟩} {b : Eqv φ Γ ⟨C, e⟩}
(ha : a.Pure) : let2 a b.wk0.wk0 = b := by
Expand Down

0 comments on commit 64b20f4

Please sign in to comment.