Nicened packed_cfg_split

DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Cast.lean

@@ -8,7 +8,7 @@ variable [Φ: EffInstSet φ (Ty α) ε] [PartialOrder α] [SemilatticeSup ε] [O
 namespace Region
 
 def Eqv.acast {Γ : Ctx α ε} {L : LCtx α} {X Y : Ty α} (h : X = Y)
-  : Eqv φ ((X, ⊥)::Γ) (Y::L) := (Eqv.nil (targets := L)).cast rfl (by rw [h])
+  : Eqv φ ((X, ⊥)::Γ) (Y::L) := ret (Term.Eqv.nil.cast rfl (by rw [h]))
 
 @[simp]
 theorem Eqv.acast_rfl {Γ : Ctx α ε} {L : LCtx α} {X : Ty α}
@@ -17,7 +17,12 @@ theorem Eqv.acast_rfl {Γ : Ctx α ε} {L : LCtx α} {X : Ty α}
 @[simp]
 theorem Eqv.vwk1_acast {Γ : Ctx α ε} {L : LCtx α} {X Y : Ty α} {h : X = Y}
   : (Eqv.acast (φ := φ) (Γ := Γ) (L := L) h).vwk1 (inserted := inserted) = Eqv.acast h
-  := by cases h; simp
+  := rfl
+
+@[simp]
+theorem Eqv.lwk1_acast {Γ : Ctx α ε} {L : LCtx α} {X Y : Ty α} {h : X = Y}
+  : (Eqv.acast (φ := φ) (Γ := Γ) (L := L) h).lwk1 (inserted := inserted) = Eqv.acast h
+  := rfl
 
 theorem Eqv.acast_seq {Γ : Ctx α ε} {L : LCtx α} {X Y : Ty α} {h : X = Y}
   {r : Eqv φ ((Y, ⊥)::Γ) (Z::L)}

DeBruijnSSA/BinSyntax/Rewrite/Region/Compose/Completeness.lean

@@ -175,7 +175,7 @@ open Term.Eqv
 --   -- congr 1
 --   sorry
 
-theorem Eqv.unpacked_app_out_eq_left_exit {Γ : Ctx α ε} {R L : LCtx α}
+theorem Eqv.unpacked_app_out_eq_left_exit' {Γ : Ctx α ε} {R L : LCtx α}
   {r : Eqv φ ((A, ⊥)::Γ) [(R ++ L).pack]} : r.unpacked_app_out
   = (r ;; ret Term.Eqv.pack_app).lwk1 ;; left_exit
   := by
@@ -191,6 +191,11 @@ theorem Eqv.unpacked_app_out_eq_left_exit {Γ : Ctx α ε} {R L : LCtx α}
     Nat.zero_eq]
   rfl
 
+theorem Eqv.unpacked_app_out_eq_left_exit {Γ : Ctx α ε} {R L : LCtx α}
+  {r : Eqv φ ((A, ⊥)::Γ) [(R ++ L).pack]} : r.unpacked_app_out
+  = r.lwk1 ;; ret Term.Eqv.pack_app ;; left_exit
+  := by rw [unpacked_app_out_eq_left_exit', lwk1_seq, lwk1_ret]
+
 theorem Eqv.packed_cfg_den {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G}
   : (cfg R β G).packed (L := []) (Δ := Δ)
   = (ret Term.Eqv.split ;; _ ⋊ (β.packed ;; ret Term.Eqv.pack_app) ;; distl_inv ;; sum pi_r nil)
@@ -264,4 +269,5 @@ theorem Eqv.packed_cfg_den {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R +
     simp [seq_assoc, ltimes_eq_ret, assoc_eq_ret, packed_out_ret_seq]
     apply congrArg
     apply congrArg
+    --simp only [unpacked_app_out_eq_left_exit]
     sorry

DeBruijnSSA/BinSyntax/Rewrite/Region/Structural.lean

@@ -97,6 +97,11 @@ theorem Eqv.vsubst_liftn₂_packed {Γ Δ Δ' : Ctx α ε} {R : LCtx α} {r : Eq
   : r.packed.vsubst (σ.liftn₂ (le_refl _) (le_refl V)) = r.packed (L := L) (Δ := _::Δ') := by
   simp [<-Term.Subst.Eqv.lift_lift]
 
+@[simp]
+theorem Eqv.lwk1_packed {Γ Δ : Ctx α ε} {R : LCtx α} {r : Eqv φ Γ R}
+  : r.packed.lwk1 (inserted := inserted) = r.packed (L := _::L)  (Δ := Δ) := by
+  rw [packed_def', lwk1_packed_out, <-packed_def']
+
 open Term.Eqv
 
 theorem Eqv.packed_br {Γ : Ctx α ε} {L : LCtx α}
@@ -157,21 +162,22 @@ theorem Eqv.packed_cfg_split {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R
       (ret Term.Eqv.split ;; _ ⋊ β.packed.unpacked_app_out)
       (ret Term.Eqv.split ⋉ _ ;; assoc
         ;; _ ⋊ (ret Term.Eqv.distl_pack
-          ;; pack_coprod (λi => acast R.get_dist
-            ;; (G (i.cast R.length_dist)).packed.unpacked_app_out))) := by
+          ;; (pack_coprod (λi => acast R.get_dist
+            ;; (G (i.cast R.length_dist)).packed)).unpacked_app_out)) := by
   rw [packed, packed_out_cfg_letc, packed_in_letc_split]
   congr 3
   · rw [packed_in_unpacked_app_out, <-packed]
-  · rw [packed_in_pack_coprod_arr]; congr; funext i; rw [packed_in_unpacked_app_out, <-packed]
+  · rw [packed_in_pack_coprod_arr, unpacked_app_out_pack_coprod]
+    congr; funext i; rw [packed_in_unpacked_app_out, <-packed, unpacked_app_out_seq, lwk1_acast]
 
 theorem Eqv.packed_cfg_split_vwk1 {Γ : Ctx α ε} {L R : LCtx α} {β : Eqv φ Γ (R ++ L)} {G}
   : (cfg R β G).packed (Δ := Δ)
   = letc (Γ.pack.prod R.pack)
       (ret Term.Eqv.split ;; _ ⋊ β.packed.unpacked_app_out)
       (ret Term.Eqv.split ⋉ _ ;; assoc
         ;; _ ⋊ (ret Term.Eqv.distl_pack
-          ;; pack_coprod (λi => acast R.get_dist
-            ;; (G (i.cast R.length_dist)).packed.unpacked_app_out))).vwk1 := by
+          ;; (pack_coprod (λi => acast R.get_dist
+            ;; (G (i.cast R.length_dist)).packed)).unpacked_app_out)).vwk1 := by
   rw [packed_cfg_split]
   simp only [List.get_eq_getElem, Fin.coe_cast, vwk1_seq, vwk1_ltimes, vwk1_br, wk1_split,
     vwk1_rtimes, wk1_distl_pack, vwk1_pack_coprod, vwk1_acast, vwk1_unpacked_app_out, vwk1_packed]

DeBruijnSSA/BinSyntax/Rewrite/Region/Structural/Sum.lean

@@ -1,6 +1,7 @@
 import DeBruijnSSA.BinSyntax.Rewrite.Region.LSubst
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Seq
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Sum
+import DeBruijnSSA.BinSyntax.Rewrite.Region.Compose.Cast
 import DeBruijnSSA.BinSyntax.Rewrite.Region.Structural.Letc
 import DeBruijnSSA.BinSyntax.Rewrite.Term.Structural.Sum
 import DeBruijnSSA.BinSyntax.Typing.Region.Structural
@@ -58,6 +59,11 @@ def Eqv.pack_coprod {Γ : Ctx α ε} {R L : LCtx α}
   | [] => loop
   | _::R => coprod (pack_coprod (λi => G i.succ)) (G (0 : Fin (R.length + 1)))
 
+theorem Eqv.pack_coprod_seq {Γ : Ctx α ε} {R L : LCtx α}
+  {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) (A::L)} {r : Eqv φ ((A, ⊥)::Γ) (B::L)}
+  : pack_coprod G ;; r = pack_coprod (λi => (G i) ;; r)
+  := by induction R <;> simp [pack_coprod, coprod_seq, *]
+
 theorem Eqv.pack_case_nil_vwk1 {Γ : Ctx α ε} {R L : LCtx α}
   (G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) L)
   : pack_case (e := e) Term.Eqv.nil (λi => (G i).vwk1) = pack_coprod G := by induction R with
@@ -577,6 +583,13 @@ theorem Eqv.vwk1_packed_out {Γ : Ctx α ε} {R : LCtx α} {r : Eqv φ (V::Γ) R
   rw [packed_out, packed_out, <-Subst.Eqv.vlift_pack, Subst.Eqv.vwk1_lsubst_vlift,
       Subst.Eqv.vlift_pack, Subst.Eqv.vlift_pack, <-packed_out]
 
+theorem Eqv.vsubst_unpacked_app_out  {Γ Δ : Ctx α ε} {R L : LCtx α}
+  {σ : Term.Subst.Eqv φ Γ Δ} {r : Eqv φ Δ [(R ++ L).pack]}
+  : r.unpacked_app_out.vsubst σ = (r.vsubst σ).unpacked_app_out := by
+  rw [unpacked_app_out, vsubst_lsubst, Subst.Eqv.vsubst_unpack_app_out]
+  rfl
+
+@[simp]
 theorem Eqv.lwk1_packed_out {Γ : Ctx α ε} {R : LCtx α} {r : Eqv φ (V::Γ) R}
   : (r.packed_out (L := L)).lwk1 (inserted := inserted) = r.packed_out := by
   rw [packed_out, packed_out, <-Subst.Eqv.vlift_pack, lwk1, <-lsubst_toSubstE, lsubst_lsubst,
@@ -598,6 +611,11 @@ theorem Eqv.unpacked_app_out_case {Γ : Ctx α ε} {R L : LCtx α}
   : (case a l r).unpacked_app_out = case a l.unpacked_app_out r.unpacked_app_out
   := by simp [unpacked_app_out]
 
+theorem Eqv.unpacked_app_out_coprod {Γ : Ctx α ε} {R L : LCtx α}
+  {l : Eqv φ ((A, ⊥)::Γ) [(R ++ L).pack]} {r : Eqv φ ((B, ⊥)::Γ) [(R ++ L).pack]}
+  : (coprod l r).unpacked_app_out = coprod l.unpacked_app_out r.unpacked_app_out
+  := by simp [coprod, unpacked_app_out_case, vwk1_unpacked_app_out]
+
 theorem Eqv.extend_unpack_unpacked_app_out
   {Γ : Ctx α ε} {R L : LCtx α} {r : Eqv φ Γ [(R ++ L).pack]}
   : r.unpacked_app_out.lsubst Subst.Eqv.unpack.extend = r.unpacked_right_out := by
@@ -691,20 +709,36 @@ theorem Eqv.packed_out_unpacked_app_out  {Γ : Ctx α ε} {R L : LCtx α}
   rw [packed_out_unpacked_app_out_inner]
   simp [Term.Eqv.sum, ret_of_coprod, sum, ret_of_seq, inj_l_eq_ret, inj_r_eq_ret, seq_assoc]
 
-theorem Eqv.packed_out_unpacked_app_out_ret_seq  {Γ : Ctx α ε} {R L : LCtx α}
+theorem Eqv.packed_out_unpacked_app_out_ret_seq {Γ : Ctx α ε} {R L : LCtx α}
   {r : Eqv φ ((X, ⊥)::Γ) [(R ++ L).pack]} {c : Term.Eqv φ ((R.pack, ⊥)::Γ) (C, ⊥)}
   : (r.unpacked_app_out ;; ret c).packed_out
   = r ;; ret Term.Eqv.pack_app ;; sum inj_r (ret c) := by
   rw [packed_out_binary_ret_seq, packed_out_unpacked_app_out, seq_assoc, sum_seq_sum]
   simp
 
-theorem Eqv.packed_out_unpacked_app_out_ret_seq_inner  {Γ : Ctx α ε} {R L : LCtx α}
+theorem Eqv.packed_out_unpacked_app_out_ret_seq_inner {Γ : Ctx α ε} {R L : LCtx α}
   {r : Eqv φ ((X, ⊥)::Γ) [(R ++ L).pack]} {c : Term.Eqv φ ((R.pack, ⊥)::Γ) (C, ⊥)}
   : (r.unpacked_app_out ;; ret c).packed_out
   = r ;; (ret (Term.Eqv.pack_app ;;' Term.Eqv.sum Term.Eqv.inj_r c)) := by
   rw [packed_out_unpacked_app_out_ret_seq, ret_of_seq]
   simp [Term.Eqv.sum, ret_of_coprod, sum, ret_of_seq, inj_l_eq_ret, inj_r_eq_ret, seq_assoc]
 
-end Region
-
-end BinSyntax
+theorem Eqv.unpacked_app_out_pack_coprod {Γ : Ctx α ε} {R L K : LCtx α}
+  {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) [(L ++ K).pack]}
+  : (pack_coprod G).unpacked_app_out = pack_coprod (λi => (G i).unpacked_app_out)
+  := by induction R with
+  | nil => simp [pack_coprod, unpacked_app_out]
+  | cons B R I => simp [pack_coprod, unpacked_app_out_coprod, I]
+
+theorem Eqv.unpacked_app_out_seq {Γ : Ctx α ε} {R L : LCtx α}
+  {r : Eqv φ ((A, ⊥)::Γ) [B]} {s : Eqv φ ((B, ⊥)::Γ) [(R ++ L).pack]}
+  : (r ;; s).unpacked_app_out = r.lwk1 ;; s.unpacked_app_out := by
+  rw [seq, unpacked_app_out, lsubst_lsubst, seq, lwk1, <-lsubst_toSubstE, lsubst_lsubst]
+  congr 1; ext k; cases k using Fin.elim1
+  simp only [Fin.isValue, List.get_eq_getElem, List.length_singleton, Fin.val_zero,
+    List.getElem_cons_zero, Subst.Eqv.get_comp, Subst.Eqv.vlift_unpack_app_out, get_alpha0,
+    List.length_nil, Fin.val_succ, List.getElem_cons_succ, Fin.cases_zero, Subst.Eqv.get_toSubstE,
+    Set.mem_setOf_eq, Fin.coe_fin_one, LCtx.InS.coe_wk1, Nat.liftWk_zero, lsubst_br,
+    List.length_cons, Nat.reduceAdd, Fin.zero_eta, Subst.Eqv.get_vlift, zero_add, vwk_id_eq,
+    vsubst0_var0_vwk1]
+  rw [vwk1_unpacked_app_out]; rfl