Further castlore

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

@@ -14,6 +14,21 @@ def Eqv.acast {Γ : Ctx α ε} {L : LCtx α} {X Y : Ty α} (h : X = Y)
 theorem Eqv.acast_rfl {Γ : Ctx α ε} {L : LCtx α} {X : Ty α}
   : Eqv.acast (φ := φ) (Γ := Γ) (L := L) (X := X) rfl = Eqv.nil := rfl
 
+@[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
+
+theorem Eqv.acast_seq {Γ : Ctx α ε} {L : LCtx α} {X Y : Ty α} {h : X = Y}
+  {r : Eqv φ ((Y, ⊥)::Γ) (Z::L)}
+  : Eqv.acast (φ := φ) (Γ := Γ) (L := L) h ;; r = r.cast (by rw [h]) rfl
+  := by cases h; simp
+
+theorem Eqv.seq_acast {Γ : Ctx α ε} {L : LCtx α} {Y Z : Ty α} {h : Y = Z}
+  {r : Eqv φ ((X, ⊥)::Γ) (Y::L)}
+  : r ;; Eqv.acast (φ := φ) (Γ := Γ) (L := L) h = r.cast rfl (by rw [h])
+  := by cases h; simp
+
 theorem Eqv.acast_acast {Γ : Ctx α ε} {L : LCtx α} {X Y Z : Ty α} {h : X = Y} {h' : Y = Z}
   : (Eqv.acast (φ := φ) (Γ := Γ) (L := L) h) ;; acast h' = Eqv.acast (by rw [h, h'])
   := by cases h; cases h'; simp

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

@@ -26,18 +26,36 @@ theorem Eqv.lwk1_coprod {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : (l.coprod r).lwk1 (inserted := inserted) = (l.lwk1).coprod (r.lwk1)
   := by simp only [lwk1, <-LCtx.InS.slift_wk0, lwk_coprod]
 
-theorem Eqv.vwk_slift_coprod {A B C : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
+theorem Eqv.vwk_slift_coprod {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
   {ρ : Γ.InS Δ}
-  {l : Eqv φ (⟨A, ⊥⟩::Δ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Δ) (C::L)}
+  {l : Eqv φ (⟨A, ⊥⟩::Δ) L} {r : Eqv φ (⟨B, ⊥⟩::Δ) L}
   : (l.coprod r).vwk ρ.slift = (l.vwk ρ.slift).coprod (r.vwk ρ.slift) := by
   simp only [coprod, vwk_case, vwk1, vwk_vwk]
   congr 2 <;> ext k <;> cases k <;> rfl
 
-theorem Eqv.vwk1_coprod {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
-  {l : Eqv φ (⟨A, ⊥⟩::Γ) (C::L)} {r : Eqv φ (⟨B, ⊥⟩::Γ) (C::L)}
+theorem Eqv.vwk1_coprod {A B: Ty α} {Γ : Ctx α ε} {L : LCtx α}
+  {l : Eqv φ (⟨A, ⊥⟩::Γ) L} {r : Eqv φ (⟨B, ⊥⟩::Γ) L}
   : (l.coprod r).vwk1 (inserted := inserted) = l.vwk1.coprod r.vwk1 := by
   simp only [vwk1, <-Ctx.InS.lift_wk0, vwk_slift_coprod]
 
+theorem Eqv.vsubst_lift_coprod {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
+  {σ : Term.Subst.Eqv φ Γ Δ}
+  {l : Eqv φ (⟨A, ⊥⟩::Δ) L} {r : Eqv φ (⟨B, ⊥⟩::Δ) L}
+  : (l.coprod r).vsubst (σ.lift (le_refl _))
+  = (l.vsubst (σ.lift (le_refl _))).coprod (r.vsubst (σ.lift (le_refl _))) := by
+  simp only [coprod, vsubst_case, vwk1, <-vsubst_fromWk, vsubst_vsubst, subst_lift_var_zero]
+  congr 2 <;> {
+    ext k; induction σ using Quotient.inductionOn;
+    apply eq_of_term_eq
+    cases k using Fin.cases with
+    | zero => rfl
+    | succ k => simp only [List.get_eq_getElem, List.length_cons, Fin.val_succ,
+      List.getElem_cons_succ, Set.mem_setOf_eq, Term.Subst.InS.get_comp, Fin.getElem_fin,
+      Nat.succ_eq_add_one, Term.InS.coe_subst, Term.subst, Ctx.InS.coe_wk1, Nat.liftWk_succ,
+      Term.Subst.InS.coe_lift, Term.Subst.lift_succ, Term.wk_wk, Ctx.InS.coe_toSubst,
+      Term.Subst.InS.coe_get, Term.subst_fromWk, Nat.liftWk_succ_comp_succ]; rfl
+  }
+
 theorem Eqv.lsubst_vlift_coprod {A B : Ty α} {Γ : Ctx α ε} {L K : LCtx α}
   {σ : Subst.Eqv φ Γ L K} {l : Eqv φ (⟨A, ⊥⟩::Γ) L} {r : Eqv φ (⟨B, ⊥⟩::Γ) L}
   : (l.coprod r).lsubst σ.vlift = (l.lsubst σ.vlift).coprod (r.lsubst σ.vlift)

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

@@ -24,4 +24,7 @@ theorem Eqv.packed_in_pack_coprod_arr {Γ : Ctx α ε} {R L : LCtx α}
   : (pack_coprod G).packed_in (Δ := Δ)
   = ret (distl_pack (X := Γ.pack))
     ;; pack_coprod (λi => acast R.get_dist ;; (G (i.cast R.length_dist)).packed_in)
-  := by rw [packed_in_pack_coprod, ret_seq]; congr; sorry
+  := by
+    rw [packed_in_pack_coprod, ret_seq]; congr;
+    rw [vwk1_pack_coprod]; congr; funext i
+    rw [vwk1_seq, vwk1_packed_in, vwk1_acast, acast_seq]

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

@@ -86,6 +86,22 @@ theorem Eqv.pack_coprod_zero {Γ : Ctx α ε} {L : LCtx α}
   (G : (i : Fin 0) → Eqv φ (⟨[].get i, ⊥⟩::Γ) (A::L)) : (pack_coprod (R := []) G) = zero := by
   rw [pack_coprod_empty]; apply Eqv.zero_eq
 
+theorem Eqv.vwk_lift_pack_coprod {Γ Δ : Ctx α ε} {R L : LCtx α}
+  {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Δ) L} {ρ : Γ.InS Δ}
+  : (pack_coprod G).vwk ρ.slift = pack_coprod (λi => (G i).vwk ρ.slift) := by
+  induction R <;> simp [pack_coprod, vwk_slift_coprod, *]
+
+theorem Eqv.vwk1_pack_coprod {Γ : Ctx α ε} {R L : LCtx α}
+  {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Γ) L}
+  : (pack_coprod G).vwk1 (inserted := inserted) = pack_coprod (λi => (G i).vwk1) := by
+  rw [vwk1, <-Ctx.InS.lift_wk0, vwk_lift_pack_coprod]; rfl
+
+theorem Eqv.vsubst_lift_pack_coprod {Γ Δ : Ctx α ε} {R L : LCtx α}
+  {G : (i : Fin R.length) → Eqv φ (⟨R.get i, ⊥⟩::Δ) L} {σ : Term.Subst.Eqv φ Γ Δ}
+  : (pack_coprod G).vsubst (σ.lift (le_refl _))
+  = pack_coprod (λi => (G i).vsubst (σ.lift (le_refl _))) := by
+  induction R <;> simp [pack_coprod, vsubst_lift_coprod, *]
+
 @[simp]
 theorem Eqv.vwk_lift_unpack {Γ Δ : Ctx α ε} {R : LCtx α} (ρ : Γ.InS Δ)
   : Eqv.vwk (ρ.lift (le_refl _)) (Eqv.unpack (φ := φ) (R := R)) = unpack := by