Removed let1-pair axiom

DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean

@@ -969,19 +969,6 @@ theorem Eqv.let1_let1 {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   induction r using Quotient.inductionOn
   apply Eqv.sound; apply InS.let1_let1
 
-theorem Eqv.let1_pair {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
-  {r : Eqv φ (⟨Ty.prod A B, ⊥⟩::Γ) L}
-  (a : Term.Eqv φ Γ ⟨A, e⟩) (b : Term.Eqv φ Γ ⟨B, e⟩)
-    : Eqv.let1 (a.pair b) r = (
-      let1 a $
-      let1 (b.wk ⟨Nat.succ, (by simp)⟩) $
-      let1 ((var 1 (by simp)).pair (e := e') (var 0 (by simp))) $
-      r.vwk1.vwk1) := by
-  induction a using Quotient.inductionOn
-  induction b using Quotient.inductionOn
-  induction r using Quotient.inductionOn
-  apply Eqv.sound; apply InS.let1_pair
-
 theorem Eqv.let1_let2 {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   {r : Eqv φ (⟨C, ⊥⟩::Γ) L}
   (a : Term.Eqv φ Γ ⟨A.prod B, e⟩) (b : Term.Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨C, e⟩)
@@ -1106,6 +1093,17 @@ theorem Eqv.let2_eta {Γ : Ctx α ε} {L : LCtx α}
   rw [<-Term.Eqv.let2_eta (a := a), let1_let2, Term.Eqv.let2_eta]
   rfl
 
+theorem Eqv.let1_pair {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
+  {r : Eqv φ (⟨Ty.prod A B, ⊥⟩::Γ) L}
+  (a : Term.Eqv φ Γ ⟨A, e⟩) (b : Term.Eqv φ Γ ⟨B, e⟩)
+    : Eqv.let1 (a.pair b) r = (
+      let1 a $
+      let1 (b.wk ⟨Nat.succ, (by simp)⟩) $
+      let1 ((var 1 (by simp)).pair (e := e') (var 0 (by simp))) $
+      r.vwk1.vwk1) := by
+    rw [<-Term.Eqv.let2_eta (a := a.pair b), Term.Eqv.let2_pair, let1_let1, let1_let1]
+    rfl
+
 -- theorem Eqv.cfg_cfg_eq_cfg' {Γ : Ctx α ε} {L : LCtx α}
 --   (R S : LCtx α) (β : Eqv φ Γ (R ++ (S ++ L)))
 --   (G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (R ++ (S ++ L)))

DeBruijnSSA/BinSyntax/Rewrite/Region/Setoid.lean

@@ -205,16 +205,6 @@ theorem InS.let1_let1 {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
     ≈ (let1 a $ let1 b $ r.vwk1)
   := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
-theorem InS.let1_pair {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α} (e' := ⊥)
-  {r : InS φ (⟨Ty.prod A B, ⊥⟩::Γ) L}
-  (a : Term.InS φ Γ ⟨A, e⟩) (b : Term.InS φ Γ ⟨B, e⟩)
-    : r.let1 (a.pair b) ≈ (
-      let1 a $
-      let1 (b.wk ⟨Nat.succ, (by simp)⟩) $
-      let1 ((var 1 (by simp)).pair (e := e') (var 0 (by simp))) $
-      r.vwk1.vwk1)
-  := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
-
 theorem InS.let1_let2 {Γ : Ctx α ε} {L : LCtx α} {A B : Ty α}
   {r : InS φ (⟨C, ⊥⟩::Γ) L}
   (a : Term.InS φ Γ ⟨A.prod B, e⟩) (b : Term.InS φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨C, e⟩)

DeBruijnSSA/BinSyntax/Rewrite/Region/Step.lean

@@ -178,16 +178,6 @@ theorem TStep.let1_let1 {Γ : Ctx α ε} {L} {a b} {r : Region φ}
     (Region.Wf.let1 da (Region.Wf.let1 db dr.vwk1))
     (Rewrite.let1_let1 a b r)
 
-theorem TStep.let1_pair {Γ L a b} {r : Region φ}
-  (da : a.Wf Γ ⟨A, e⟩) (db : b.Wf Γ ⟨B, e⟩) (dr : r.Wf (⟨A.prod B, ⊥⟩::Γ) L)
-  : TStep Γ L (let1 (pair a b) r)
-    (let1 a $ let1 (b.wk Nat.succ) $ let1 (pair (var 1) (var 0)) $ r.vwk1.vwk1)
-  := TStep.rewrite
-    (dr.let1 (da.pair db))
-    (Region.Wf.let1 da (Region.Wf.let1 db.wk0
-      (Region.Wf.let1 (Term.Wf.pair (by simp) (Term.Wf.var Ctx.Var.shead)) dr.vwk1.vwk1)))
-    (Rewrite.let1_pair a b r)
-
 -- TODO: let1_let2, let1_inl, let1_inr, let1_case, let1_abort
 
 theorem TStep.wf {Γ L} {r r' : Region φ} (h : TStep Γ L r r') : r.Wf Γ L ∧ r'.Wf Γ L

DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean

@@ -1016,15 +1016,6 @@ theorem Eqv.let1_let1 {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ (
   induction c using Quotient.inductionOn
   apply Eqv.sound; apply InS.let1_let1
 
-theorem Eqv.let1_pair {Γ : Ctx α ε}
-  {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ (Γ) ⟨B, e⟩} {r : Eqv φ (⟨A.prod B, ⊥⟩::Γ) ⟨C, e⟩}
-  : let1 (pair a b) r
-  = (let1 a $ let1 b.wk0 $ let1 (pair (var 1 (by simp)) (var 0 (by simp))) $ r.wk1.wk1) := by
-  induction a using Quotient.inductionOn
-  induction b using Quotient.inductionOn
-  induction r using Quotient.inductionOn
-  apply Eqv.sound; apply InS.let1_pair
-
 theorem Eqv.let1_let2 {Γ : Ctx α ε} {a : Eqv φ Γ ⟨Ty.prod A B, e⟩}
   {b : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨C, e⟩} {r : Eqv φ (⟨C, ⊥⟩::Γ) ⟨D, e⟩}
   : let1 (let2 a b) r = (let2 a $ let1 b $ r.wk1.wk1) := by
@@ -1085,6 +1076,12 @@ theorem Eqv.let2_pair {Γ : Ctx α ε} {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ Γ
   induction r using Quotient.inductionOn
   apply Eqv.sound; apply InS.let2_pair
 
+theorem Eqv.let1_pair {Γ : Ctx α ε}
+  {a : Eqv φ Γ ⟨A, e⟩} {b : Eqv φ (Γ) ⟨B, e⟩} {r : Eqv φ (⟨A.prod B, ⊥⟩::Γ) ⟨C, e⟩}
+  : let1 (pair a b) r
+  = (let1 a $ let1 b.wk0 $ let1 (pair (var 1 (by simp)) (var 0 (by simp))) $ r.wk1.wk1) := by
+  rw [<-let2_eta (a := pair a b), let2_pair, let1_let1, let1_let1]
+
 theorem Eqv.let2_bind {Γ : Ctx α ε} {a : Eqv φ Γ ⟨Ty.prod A B, e⟩}
   {r : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨C, e⟩}
   : let2 a r = (let1 a $ let2 (var 0 (by simp)) $ r.wk2) := by

DeBruijnSSA/BinSyntax/Rewrite/Term/Setoid.lean

@@ -132,12 +132,6 @@ theorem InS.let1_let1 {Γ : Ctx α ε} {a : InS φ Γ ⟨A, e⟩} {b : InS φ (
   : let1 (let1 a b) c ≈ (let1 a $ let1 b $ c.wk1)
   := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
 
-theorem InS.let1_pair {Γ : Ctx α ε}
-  {a : InS φ Γ ⟨A, e⟩} {b : InS φ (Γ) ⟨B, e⟩} {r : InS φ (⟨A.prod B, ⊥⟩::Γ) ⟨C, e⟩}
-  : let1 (pair a b) r
-  ≈ (let1 a $ let1 b.wk0 $ let1 (pair (var 1 (by simp)) (var 0 (by simp))) $ r.wk1.wk1)
-  := Uniform.rel $ TStep.rewrite InS.coe_wf InS.coe_wf (by constructor)
-
 theorem InS.let1_let2 {Γ : Ctx α ε} {a : InS φ Γ ⟨Ty.prod A B, e⟩}
   {b : InS φ (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) ⟨C, e⟩} {r : InS φ (⟨C, ⊥⟩::Γ) ⟨D, e⟩}
   : let1 (let2 a b) r ≈ (let2 a $ let1 b $ r.wk1.wk1)

DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Equiv.lean

@@ -70,10 +70,6 @@ theorem eqv_let1_op {f e r} : @let1 φ (op f e) r ≈ (let1 e $ let1 (op f (var
 theorem eqv_let1_let1 {a b r} : @let1 φ (a.let1 b) r ≈ (let1 a $ let1 b $ r.vwk1)
   := Relation.EqvGen.rel _ _ $ Cong.rel $ Rewrite.let1_let1 a b r
 
-theorem eqv_let1_pair {a b r}
-  : @let1 φ (pair a b) r ≈ (let1 a $ let1 (b.wk Nat.succ) $ let1 (pair (var 1) (var 0)) $ r.vwk1.vwk1)
-  := Relation.EqvGen.rel _ _ $ Cong.rel $ Rewrite.let1_pair a b r
-
 theorem eqv_let1_let2 {a b r} : @let1 φ (a.let2 b) r ≈ (let2 a $ let1 b $ r.vwk1.vwk1)
   := Relation.EqvGen.rel _ _ $ Cong.rel $ Rewrite.let1_let2 a b r
 

DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Rewrite.lean

@@ -20,9 +20,6 @@ inductive RewriteD : Region φ → Region φ → Type _
     RewriteD (let1 (op f a) r) (let1 a $ let1 (op f (var 0)) $ r.vwk1)
   | let1_let1 (a b r) :
     RewriteD (let1 (Term.let1 a b) r) (let1 a $ let1 b $ r.vwk1)
-  | let1_pair (a b r) :
-    RewriteD (let1 (pair a b) r)
-    (let1 a $ let1 b.wk0 $ let1 (pair (var 1) (var 0)) $ r.vwk1.vwk1)
   | let1_let2 (a b r) :
     RewriteD (let1 (Term.let2 a b) r) (let2 a $ let1 b $ r.vwk1.vwk1)
   | let1_inl (e r) :
@@ -151,9 +148,6 @@ inductive Rewrite : Region φ → Region φ → Prop
     Rewrite (let1 (op f a) r) (let1 a $ let1 (op f (var 0)) $ r.vwk1)
   | let1_let1 (a b r) :
     Rewrite (let1 (Term.let1 a b) r) (let1 a $ let1 b $ r.vwk1)
-  | let1_pair (a b r) :
-    Rewrite (let1 (pair a b) r)
-    (let1 a $ let1 (b.wk Nat.succ) $ let1 (pair (var 1) (var 0)) $ r.vwk1.vwk1)
   | let1_let2 (a b r) :
     Rewrite (let1 (Term.let2 a b) r) (let2 a $ let1 b $ r.vwk1.vwk1)
   | let1_inl (e r) :
@@ -274,9 +268,6 @@ def RewriteD.vsubst {r r' : Region φ} (σ : Term.Subst φ) (p : RewriteD r r')
   | let1_let1 a b r =>
     convert (let1_let1 (a.subst σ) (b.subst σ.lift) (r.vsubst σ.lift)) using 1
     simp [Term.subst, Region.vsubst_lift₂_vwk1]
-  | let1_pair a b r =>
-    convert (let1_pair (a.subst σ) (b.subst σ) (r.vsubst σ.lift)) using 1
-    simp [Term.subst, Region.vsubst_lift₂_vwk1, Term.wk0_subst]
   | let1_let2 a b r =>
     convert (let1_let2 (a.subst σ) (b.subst (σ.liftn 2)) (r.vsubst σ.lift)) using 1
     simp [Term.subst, Region.vsubst_lift₂_vwk1, Term.Subst.liftn_two]
@@ -315,9 +306,6 @@ def RewriteD.lsubst {r r' : Region φ} (σ : Subst φ) (p : RewriteD r r')
   | let1_let1 a b r =>
     convert (let1_let1 a b (r.lsubst σ.vlift)) using 1
     simp [vwk1_lsubst_vlift]
-  | let1_pair a b r =>
-    convert (let1_pair a b (r.lsubst σ.vlift)) using 1
-    simp [vwk1_lsubst_vlift]
   | let1_let2 a b r =>
     convert (let1_let2 a b (r.lsubst σ.vlift)) using 1
     simp [vwk1_lsubst_vlift, Subst.vliftn_two]

DeBruijnSSA/BinSyntax/Syntax/Rewrite/Region/Step.lean

@@ -172,18 +172,6 @@ def StepD.let1_op_op {Γ : ℕ → ε} (f e) (r : Region φ)
     (let1 (op f e) r)
   := StepD.rw_op $ RewriteD.let1_op f e r
 
-@[match_pattern]
-def StepD.let1_pair {Γ : ℕ → ε} (a b) (r : Region φ)
-  : StepD Γ (let1 (pair a b) r)
-    (let1 a $ let1 (b.wk Nat.succ) $ let1 (pair (var 1) (var 0)) r.vwk1.vwk1)
-  := StepD.rw $ RewriteD.let1_pair a b r
-
-@[match_pattern]
-def StepD.let1_pair_op {Γ : ℕ → ε} (a b) (r : Region φ)
-  : StepD Γ (let1 a $ let1 (b.wk Nat.succ) $ let1 (pair (var 1) (var 0)) r.vwk1.vwk1)
-    (let1 (pair a b) r)
-  := StepD.rw_op $ RewriteD.let1_pair a b r
-
 @[match_pattern]
 def StepD.let1_inl {Γ : ℕ → ε} (e) (r : Region φ)
   : StepD Γ (let1 (inl e) r) (let1 e $ let1 (inl (var 0)) $ r.vwk (Nat.liftWk Nat.succ))

DeBruijnSSA/BinSyntax/Syntax/Rewrite/Term/Step.lean

@@ -21,9 +21,6 @@ inductive Rewrite : Term φ → Term φ → Prop
     Rewrite (let1 (op f e) r) (let1 e $ let1 (op f (var 0)) $ r.wk1)
   | let1_let1 (a b r) :
     Rewrite (let1 (let1 a b) r) (let1 a $ let1 b $ r.wk1)
-  | let1_pair (a b r) :
-    Rewrite (let1 (pair a b) r)
-    (let1 a $ let1 (b.wk Nat.succ) $ let1 (pair (var 1) (var 0)) $ r.wk1.wk1)
   | let1_let2 (a b r) :
     Rewrite (let1 (let2 a b) r) (let2 a $ let1 b $ r.wk1.wk1)
   | let1_inl (e r) :
@@ -66,10 +63,6 @@ theorem Rewrite.subst {e e' : Term φ} (h : e.Rewrite e') (σ) : (e.subst σ).Re
   | let1_let1 a b r =>
     simp only [Term.subst, <-wk1_subst_lift]
     exact let1_let1 (a.subst σ) (b.subst (σ.lift)) (r.subst (σ.lift))
-  | let1_pair a b r =>
-    simp only [Term.subst, Subst.lift_succ, wk, Nat.succ_eq_add_one, zero_add,
-      Subst.lift_zero, <-Term.wk1_subst_lift, Term.subst_lift]
-    exact let1_pair (a.subst σ) (b.subst σ) (r.subst (σ.lift))
   | let1_let2 a b r =>
     simp only [Term.subst, <-wk1_subst_lift, Subst.liftn_two]
     exact let1_let2 (a.subst σ) (b.subst σ.lift.lift) (r.subst σ.lift)