Removed let1_inl, let1_inr

DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean

@@ -1,5 +1,6 @@
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Setoid
 import DeBruijnSSA.BinSyntax.Rewrite.Term.Eqv
+import DeBruijnSSA.BinSyntax.Rewrite.Term.Case
 
 import Discretion.Utils.Quotient
 
@@ -980,24 +981,6 @@ theorem Eqv.let1_let2 {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   induction b using Quotient.inductionOn
   apply Eqv.sound; apply InS.let1_let2
 
-theorem Eqv.let1_inl {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
-  {r : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) L}
-  (a : Term.Eqv φ Γ ⟨A, e⟩)
-    : Eqv.let1 a.inl r
-    = (r.vwk1.let1 ((var 0 (by simp)).inl (e := e'))).let1 a := by
-  induction a using Quotient.inductionOn
-  induction r using Quotient.inductionOn
-  apply Eqv.sound; apply InS.let1_inl
-
-theorem Eqv.let1_inr {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
-  {r : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) L}
-  (b : Term.Eqv φ Γ ⟨B, e⟩)
-    : Eqv.let1 b.inr r
-    = (r.vwk1.let1 ((var 0 (by simp)).inr (e := e'))).let1 b := by
-  induction b using Quotient.inductionOn
-  induction r using Quotient.inductionOn
-  apply Eqv.sound; apply InS.let1_inr
-
 theorem Eqv.let1_case {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   {s : Eqv φ (⟨C, ⊥⟩::Γ) L}
   (a : Term.Eqv φ Γ ⟨Ty.coprod A B, e⟩)
@@ -1010,15 +993,6 @@ theorem Eqv.let1_case {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   induction s using Quotient.inductionOn
   apply Eqv.sound; apply InS.let1_case
 
-theorem Eqv.let1_abort {Γ : Ctx α ε} {L : LCtx α} {A : Ty α} (e' := ⊥)
-  {r : Eqv φ (⟨A, ⊥⟩::Γ) L}
-  (a : Term.Eqv φ Γ ⟨Ty.empty, e⟩)
-    : Eqv.let1 (a.abort _) r
-    = (r.vwk1.let1 ((var 0 (by simp)).abort (e := e') _)).let1 a := by
-  induction a using Quotient.inductionOn
-  induction r using Quotient.inductionOn
-  apply Eqv.sound; apply InS.let1_abort
-
 theorem Eqv.let2_bind {Γ : Ctx α ε} {L : LCtx α}
   {e : Term.Eqv φ Γ ⟨A.prod B, e⟩} {r : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) L}
   : let2 e r
@@ -1233,6 +1207,31 @@ theorem Eqv.case_inr {Γ : Ctx α ε} {L : LCtx α}
   induction s using Quotient.inductionOn
   case _ e r s => exact Eqv.sound (InS.case_inr e r s)
 
+theorem Eqv.let1_inl {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
+  {r : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) L}
+  (a : Term.Eqv φ Γ ⟨A, e⟩)
+    : Eqv.let1 a.inl r
+    = (r.vwk1.let1 ((var 0 (by simp)).inl (e := e'))).let1 a := by
+  rw [<-Term.Eqv.case_eta (a := inl a), let1_case, case_inl]
+  rfl
+
+theorem Eqv.let1_inr {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
+  {r : Eqv φ (⟨A.coprod B, ⊥⟩::Γ) L}
+  (b : Term.Eqv φ Γ ⟨B, e⟩)
+    : Eqv.let1 b.inr r
+    = (r.vwk1.let1 ((var 0 (by simp)).inr (e := e'))).let1 b := by
+  rw [<-Term.Eqv.case_eta (a := inr b), let1_case, case_inr]
+  rfl
+
+theorem Eqv.let1_abort {Γ : Ctx α ε} {L : LCtx α} {A : Ty α} (e' := ⊥)
+  {r : Eqv φ (⟨A, ⊥⟩::Γ) L}
+  (a : Term.Eqv φ Γ ⟨Ty.empty, e⟩)
+    : Eqv.let1 (a.abort _) r
+    = (r.vwk1.let1 ((var 0 (by simp)).abort (e := e') _)).let1 a := by
+  induction a using Quotient.inductionOn
+  induction r using Quotient.inductionOn
+  apply Eqv.sound; apply InS.let1_abort
+
 -- TODO: Eqv.dead_cfg_left
 
 theorem Eqv.let1_beta {Γ : Ctx α ε} {L : LCtx α}

DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean

@@ -212,20 +212,6 @@ theorem InS.let1_let2 {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
     ≈ (let2 a $ let1 b $ r.vwk1.vwk1)
   := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
-theorem InS.let1_inl {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
-  {r : InS φ (⟨A.coprod B, ⊥⟩::Γ) L}
-  (a : Term.InS φ Γ ⟨A, e⟩)
-    : r.let1 a.inl
-    ≈ (r.vwk1.let1 ((var 0 (by simp)).inl (e := e'))).let1 a
-  := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
-
-theorem InS.let1_inr {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
-  {r : InS φ (⟨A.coprod B, ⊥⟩::Γ) L}
-  (b : Term.InS φ Γ ⟨B, e⟩)
-    : r.let1 b.inr
-    ≈ (r.vwk1.let1 ((var 0 (by simp)).inr (e := e'))).let1 b
-  := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
-
 theorem InS.let1_case {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   {s : InS φ (⟨C, ⊥⟩::Γ) L}
   (a : Term.InS φ Γ ⟨Ty.coprod A B, e⟩)

DeBruijnSSA/BinSyntax/Rewrite/Region/Step.lean

@@ -1,5 +1,6 @@
 import DeBruijnSSA.BinSyntax.Typing.Region
-import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Region.Step
+import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Region.Rewrite
+import DeBruijnSSA.BinSyntax.Syntax.Rewrite.Region.Reduce
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Cong
 import DeBruijnSSA.BinSyntax.Rewrite.Term.Setoid
 

DeBruijnSSA/BinSyntax/Rewrite/Term/Case.lean

@@ -215,6 +215,46 @@ theorem Eqv.case_let1_wk0_pure {Γ : Ctx α ε}
 
 -- TODO: derive these...
 
+theorem Eqv.let1_inl {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {r : Eqv φ (⟨Ty.coprod A B, ⊥⟩::Γ) ⟨C, e⟩}
+  : let1 (inl a) r = (let1 a $ let1 (inl (var 0 (by simp))) $ r.wk1) := by
+  rw [<-case_eta (a := inl a), let1_case, case_inl]
+
+theorem Eqv.let1_inr {Γ : Ctx α ε} {a : Eqv φ Γ ⟨B, e⟩} {r : Eqv φ (⟨Ty.coprod A B, ⊥⟩::Γ) ⟨C, e⟩}
+  : let1 (inr a) r = (let1 a $ let1 (inr (var 0 (by simp))) $ r.wk1) := by
+  rw [<-case_eta (a := inr a), let1_case, case_inr]
+
+theorem Eqv.inl_bind {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩}
+  : a.inl (B := B) = let1 a (inl (var 0 (by simp))) := calc
+  _ = let1 a.inl (var 0 Ctx.Var.bhead) := by rw [let1_eta]
+  _ = let1 a (let1 (inl (var 0 Ctx.Var.bhead)) (var 0 Ctx.Var.bhead)) := by rw [let1_inl, wk1_var0]
+  _ = let1 a (let1 (wk_eff bot_le (inl (var 0 Ctx.Var.shead))) (var 0 Ctx.Var.bhead)) := by rfl
+  _ = _ := by rw [let1_beta]; rfl
+
+theorem Eqv.inr_bind {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩}
+  : a.inr (A := B) = let1 a (inr (var 0 (by simp))) := calc
+  _ = let1 a.inr (var 0 Ctx.Var.bhead) := by rw [let1_eta]
+  _ = let1 a (let1 (inr (var 0 Ctx.Var.bhead)) (var 0 Ctx.Var.bhead)) := by rw [let1_inr, wk1_var0]
+  _ = let1 a (let1 (wk_eff bot_le (inr (var 0 Ctx.Var.shead))) (var 0 Ctx.Var.bhead)) := by rfl
+  _ = _ := by rw [let1_beta]; rfl
+
+theorem Eqv.inl_let1 {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ ((A, ⊥)::Γ) ⟨B, e⟩}
+  : (let1 a b).inl = let1 a (b.inl (B := C)) := by
+  rw [inl_bind, let1_let1, wk1_inl, wk1_var0, <-inl_bind]
+
+theorem Eqv.inr_let1 {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ ((A, ⊥)::Γ) ⟨B, e⟩}
+  : (let1 a b).inr = let1 a (b.inr (A := C)) := by
+  rw [inr_bind, let1_let1, wk1_inr, wk1_var0, <-inr_bind]
+
+theorem Eqv.inl_let2 {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A.prod B, e⟩} {b : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) ⟨C, e⟩}
+  : (let2 a b).inl = let2 a (b.inl (B := D)) := by
+  rw [inl_bind, let1_let2, wk1_inl, wk1_inl, wk1_var0, wk1_var0, <-inl_bind]
+
+theorem Eqv.inr_let2 {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A.prod B, e⟩} {b : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) ⟨C, e⟩}
+  : (let2 a b).inr = let2 a (b.inr (A := D)) := by
+  rw [inr_bind, let1_let2, wk1_inr, wk1_inr, wk1_var0, wk1_var0, <-inr_bind]
+
 theorem Eqv.case_inl_inl {Γ : Ctx α ε}
   {a : Eqv φ Γ ⟨A.coprod B, e⟩}
   {r : Eqv φ (⟨A, ⊥⟩::Γ) ⟨C, e⟩}

DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean

@@ -1029,18 +1029,6 @@ theorem Eqv.let1_let2_inv {Γ : Ctx α ε} {a : Eqv φ Γ ⟨Ty.prod A B, e⟩}
   (h : r' = r.wk1.wk1)
   :  (let2 a $ let1 b $ r') = let1 (let2 a b) r := by cases h; rw [let1_let2]
 
-theorem Eqv.let1_inl {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {r : Eqv φ (⟨Ty.coprod A B, ⊥⟩::Γ) ⟨C, e⟩}
-  : let1 (inl a) r = (let1 a $ let1 (inl (var 0 (by simp))) $ r.wk1) := by
-  induction a using Quotient.inductionOn
-  induction r using Quotient.inductionOn
-  apply Eqv.sound; apply InS.let1_inl
-
-theorem Eqv.let1_inr {Γ : Ctx α ε} {a : Eqv φ Γ ⟨B, e⟩} {r : Eqv φ (⟨Ty.coprod A B, ⊥⟩::Γ) ⟨C, e⟩}
-  : let1 (inr a) r = (let1 a $ let1 (inr (var 0 (by simp))) $ r.wk1) := by
-  induction a using Quotient.inductionOn
-  induction r using Quotient.inductionOn
-  apply Eqv.sound; apply InS.let1_inr
-
 theorem Eqv.let1_case {Γ : Ctx α ε} {a : Eqv φ Γ ⟨Ty.coprod A B, e⟩}
   {l : Eqv φ (⟨A, ⊥⟩::Γ) ⟨C, e⟩} {r : Eqv φ (⟨B, ⊥⟩::Γ) ⟨C, e⟩}
   {s : Eqv φ (⟨C, ⊥⟩::Γ) ⟨D, e⟩}
@@ -1600,38 +1588,6 @@ theorem Eqv.Pure.let2_let1_of_left {Γ : Ctx α ε}
   : let2 b (let1 a' c') = let1 a (let2 b.wk0 c) := by
     rw [ha.let1_let2_of_right, ha', hc']
 
-theorem Eqv.inl_bind {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩}
-  : a.inl (B := B) = let1 a (inl (var 0 (by simp))) := calc
-  _ = let1 a.inl (var 0 Ctx.Var.bhead) := by rw [let1_eta]
-  _ = let1 a (let1 (inl (var 0 Ctx.Var.bhead)) (var 0 Ctx.Var.bhead)) := by rw [let1_inl, wk1_var0]
-  _ = let1 a (let1 (wk_eff bot_le (inl (var 0 Ctx.Var.shead))) (var 0 Ctx.Var.bhead)) := by rfl
-  _ = _ := by rw [let1_beta]; rfl
-
-theorem Eqv.inr_bind {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩}
-  : a.inr (A := B) = let1 a (inr (var 0 (by simp))) := calc
-  _ = let1 a.inr (var 0 Ctx.Var.bhead) := by rw [let1_eta]
-  _ = let1 a (let1 (inr (var 0 Ctx.Var.bhead)) (var 0 Ctx.Var.bhead)) := by rw [let1_inr, wk1_var0]
-  _ = let1 a (let1 (wk_eff bot_le (inr (var 0 Ctx.Var.shead))) (var 0 Ctx.Var.bhead)) := by rfl
-  _ = _ := by rw [let1_beta]; rfl
-
-theorem Eqv.inl_let1 {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ ((A, ⊥)::Γ) ⟨B, e⟩}
-  : (let1 a b).inl = let1 a (b.inl (B := C)) := by
-  rw [inl_bind, let1_let1, wk1_inl, wk1_var0, <-inl_bind]
-
-theorem Eqv.inr_let1 {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ ((A, ⊥)::Γ) ⟨B, e⟩}
-  : (let1 a b).inr = let1 a (b.inr (A := C)) := by
-  rw [inr_bind, let1_let1, wk1_inr, wk1_var0, <-inr_bind]
-
-theorem Eqv.inl_let2 {Γ : Ctx α ε}
-  {a : Eqv φ Γ ⟨A.prod B, e⟩} {b : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) ⟨C, e⟩}
-  : (let2 a b).inl = let2 a (b.inl (B := D)) := by
-  rw [inl_bind, let1_let2, wk1_inl, wk1_inl, wk1_var0, wk1_var0, <-inl_bind]
-
-theorem Eqv.inr_let2 {Γ : Ctx α ε}
-  {a : Eqv φ Γ ⟨A.prod B, e⟩} {b : Eqv φ ((B, ⊥)::(A, ⊥)::Γ) ⟨C, e⟩}
-  : (let2 a b).inr = let2 a (b.inr (A := D)) := by
-  rw [inr_bind, let1_let2, wk1_inr, wk1_inr, wk1_var0, wk1_var0, <-inr_bind]
-
 end Basic
 
 end Term

DeBruijnSSA/BinSyntax/Rewrite/Term/Setoid.lean

@@ -137,14 +137,6 @@ theorem InS.let1_let2 {Γ : Ctx α ε} {a : InS φ Γ ⟨Ty.prod A B, e⟩}
   : let1 (let2 a b) r ≈ (let2 a $ let1 b $ r.wk1.wk1)
   := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
-theorem InS.let1_inl {Γ : Ctx α ε} {a : InS φ Γ ⟨A, e⟩} {r : InS φ (⟨Ty.coprod A B, ⊥⟩::Γ) ⟨C, e⟩}
-  : let1 (inl a) r ≈ (let1 a $ let1 (inl (var 0 (by simp))) $ r.wk1)
-  := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
-
-theorem InS.let1_inr {Γ : Ctx α ε} {a : InS φ Γ ⟨B, e⟩} {r : InS φ (⟨Ty.coprod A B, ⊥⟩::Γ) ⟨C, e⟩}
-  : let1 (inr a) r ≈ (let1 a $ let1 (inr (var 0 (by simp))) $ r.wk1)
-  := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
-
 theorem InS.let1_case {Γ : Ctx α ε} {a : InS φ Γ ⟨Ty.coprod A B, e⟩}
   {l : InS φ (⟨A, ⊥⟩::Γ) ⟨C, e⟩} {r : InS φ (⟨B, ⊥⟩::Γ) ⟨C, e⟩}
   {s : InS φ (⟨C, ⊥⟩::Γ) ⟨D, e⟩}

DeBruijnSSA/BinSyntax/Syntax/Compose/Term.lean

@@ -1,5 +1,4 @@
 import DeBruijnSSA.BinSyntax.Syntax.Subst
-import DeBruijnSSA.BinSyntax.Syntax.Rewrite
 import DeBruijnSSA.InstSet
 
 namespace BinSyntax