Arrow induction

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

@@ -56,6 +56,7 @@ theorem Eqv.vwk2_left_exit {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
 def Eqv.fixpoint {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α} (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L))
   : Eqv φ (⟨A, ⊥⟩::Γ) (B::L) := cfg [A] nil (Fin.elim1 (f.vwk1.lwk1 ;; left_exit))
 
+@[simp]
 theorem Eqv.fixpoint_quot {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (f : InS φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L))
   : fixpoint ⟦f⟧ = ⟦f.fixpoint⟧ := by
@@ -66,6 +67,21 @@ theorem Eqv.fixpoint_quot {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   intro i
   cases i using Fin.elim1; rfl
 
+theorem Eqv.vwk_lift_fixpoint {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
+  {r : Eqv φ (⟨A, ⊥⟩::Δ) ((B.coprod A)::L)}
+  {ρ : Ctx.InS Γ Δ}
+  : r.fixpoint.vwk ρ.slift = (r.vwk ρ.slift).fixpoint := by
+  induction r using Quotient.inductionOn
+  simp [InS.vwk_lift_fixpoint]
+
+theorem Eqv.vsubst_lift_fixpoint {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
+  {r : Eqv φ (⟨A, ⊥⟩::Δ) ((B.coprod A)::L)}
+  {σ : Term.Subst.Eqv φ Γ Δ}
+  : r.fixpoint.vsubst (σ.lift (le_refl _)) = (r.vsubst (σ.lift (le_refl _))).fixpoint := by
+  induction r using Quotient.inductionOn
+  induction σ using Quotient.inductionOn
+  simp [InS.vsubst_lift_fixpoint]
+
 theorem Eqv.fixpoint_iter_cfg {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (f : Eqv φ (⟨A, ⊥⟩::Γ) ((B.coprod A)::L))
   : fixpoint f = cfg [A] (f.lwk1 ;; left_exit) (Fin.elim1 (f.vwk1.lwk1 ;; left_exit)) := by
@@ -94,7 +110,11 @@ theorem Eqv.seq_cont {A B C : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   (f : Eqv φ (⟨A, ⊥⟩::Γ) (B::L)) (g : Eqv φ (⟨B, ⊥⟩::Γ) (C::D::L))
   (h : Eqv φ (⟨C, ⊥⟩::Γ) (C::D::L))
   : cfg [C] (f.lwk1 ;; g) (Fin.elim1 h.vwk1) = f ;; cfg [C] g (Fin.elim1 h.vwk1)
-  := sorry
+  := by sorry
+  -- let Γ' := (A, ⊥)::Γ;
+  -- let L' := B::L;
+  -- induction f using Eqv.induction with
+  -- | _ => sorry
 
 theorem Eqv.ret_var_zero_eq_nil_vwk1 {A : Ty α} {Γ : Ctx α ε} {L : LCtx α}
   : ret (var 0 (by simp)) = (nil (φ := φ) (ty := A) (rest := Γ) (targets := L)).vwk1 (inserted := X)

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

@@ -230,8 +230,8 @@ theorem Eqv.vsubst_lift_seq {A B C : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
   induction right using Quotient.inductionOn;
   induction σ using Quotient.inductionOn;
   apply Eqv.eq_of_reg_eq
-  simp only [Set.mem_setOf_eq, InS.coe_vsubst, Term.Subst.coe_lift, InS.coe_lsubst, InS.coe_alpha0,
-    InS.coe_vwk, Ctx.InS.coe_wk1, vsubst_lift_lsubst_alpha,
+  simp only [Set.mem_setOf_eq, InS.coe_vsubst, Term.Subst.InS.coe_lift, InS.coe_lsubst,
+    InS.coe_alpha0, InS.coe_vwk, Ctx.InS.coe_wk1, vsubst_lift_lsubst_alpha,
     <-Region.vsubst_fromWk, Region.vsubst_vsubst]
   congr
   apply congrArg

DeBruijnSSA/BinSyntax/Rewrite/Region/Eqv.lean

@@ -21,7 +21,8 @@ namespace Region
 def Eqv (φ) [EffInstSet φ (Ty α) ε] (Γ : Ctx α ε) (L : LCtx α) := Quotient (InS.Setoid φ Γ L)
 
 def Eqv.cast {Γ : Ctx α ε} {L : LCtx α} (hΓ : Γ = Γ') (hL : L = L') (r : Eqv φ Γ L)
-  : Eqv φ Γ' L' := hΓ ▸ hL ▸ r
+  : Eqv φ Γ' L' := Quotient.liftOn r (λr => ⟦r.cast hΓ hL⟧)
+    (λ_ _ h => Quotient.sound (by cases hΓ; cases hL; exact h))
 
 def InS.q (a : InS φ Γ L) : Eqv φ Γ L := Quotient.mk _ a
 
@@ -172,6 +173,40 @@ def Eqv.induction
       rw [cfg_quot] at res
       exact res
 
+
+
+theorem Eqv.arrow_induction
+  {motive : (X : Ty α) → (Γ : Ctx α ε) → (Y : Ty α) → (L : LCtx α)
+    → Eqv φ ((X, ⊥)::Γ) (Y::L) → Prop}
+  (br : ∀{X Γ Y L A} (ℓ)
+    (a : Term.Eqv φ ((X, ⊥)::Γ) ⟨A, ⊥⟩) (hℓ : LCtx.Trg (Y::L) ℓ A), motive X Γ Y L (Eqv.br ℓ a hℓ))
+  (let1 : ∀{X Γ Y L A e} (a : Term.Eqv φ ((X, ⊥)::Γ) ⟨A, e⟩) (t : Eqv φ (⟨A, ⊥⟩::⟨X, ⊥⟩::Γ) (Y::L)),
+    motive _ _ _ _ t → motive _ Γ _ L (Eqv.let1 a t))
+  (let2 : ∀{X Γ Y L A B e}
+    (a : Term.Eqv φ ((X, ⊥)::Γ) ⟨Ty.prod A B, e⟩) (t : Eqv φ (⟨B, ⊥⟩::⟨A, ⊥⟩::⟨X, ⊥⟩::Γ) (Y::L)),
+    motive _ _ _ _ t → motive _ Γ _ L (Eqv.let2 a t))
+  (case : ∀{X Γ Y L A B e} (a : Term.Eqv φ ((X, ⊥)::Γ) ⟨Ty.coprod A B, e⟩)
+    (s : Eqv φ (⟨A, ⊥⟩::⟨X, ⊥⟩::Γ) (Y::L)) (t : Eqv φ (⟨B, ⊥⟩::⟨X, ⊥⟩::Γ) (Y::L)),
+    motive _ _ _ _ s → motive _ _ _ _ t → motive _ Γ _ L (Eqv.case a s t))
+  (cfg : ∀{X Γ Y L} (R)
+    (dβ : Eqv φ ((X, ⊥)::Γ) (R ++ (Y :: L)))
+    (dG : ∀i : Fin R.length, Eqv φ (⟨R.get i, ⊥⟩::⟨X, ⊥⟩::Γ) (R ++ (Y :: L))),
+    motive X Γ _ _ (dβ.cast rfl output_reshuffle_helper)
+    → (∀i, motive _ _ _ _ ((dG i).cast rfl output_reshuffle_helper))
+    → motive _ Γ _ L (Eqv.cfg R dβ dG))
+  {X Γ Y L} (r : Eqv φ ((X, ⊥)::Γ) (Y::L)) : motive _ _ _ _ r := by
+  induction r using Quotient.inductionOn with
+  | h r =>
+    induction r using InS.arrow_induction with
+    | br ℓ a hℓ => exact br ℓ ⟦a⟧ hℓ
+    | let1 a r Ir => exact let1 ⟦a⟧ ⟦r⟧ Ir
+    | let2 a r Ir => exact let2 ⟦a⟧ ⟦r⟧ Ir
+    | case a r s Ir Is => exact case ⟦a⟧ ⟦r⟧ ⟦s⟧ Ir Is
+    | cfg R β G Iβ IG =>
+      have h := cfg R ⟦β⟧ (λi => ⟦G i⟧) Iβ IG
+      rw [cfg_quot] at h
+      exact h
+
 def Eqv.vwk
   {Γ Δ : Ctx α ε} {L : LCtx α} (ρ : Γ.InS Δ) (r : Eqv φ Δ L)
   : Eqv φ Γ L := Quotient.liftOn r

DeBruijnSSA/BinSyntax/Rewrite/Term/Compose/Product.lean

@@ -506,8 +506,8 @@ theorem Eqv.braid_rtimes {A B B' : Ty α} {Γ : Ctx α ε}
   apply congrArg
   ext
   simp only [Set.mem_setOf_eq, InS.coe_wk0, Term.wk0, InS.coe_wk1, Term.wk1, ← subst_fromWk, ←
-    Subst.fromWk_lift, Term.subst_subst, InS.coe_subst, InS.coe_subst0, InS.coe_var, Subst.coe_lift,
-    ← Subst.lift_comp]
+    Subst.fromWk_lift, Term.subst_subst, InS.coe_subst, InS.coe_subst0, InS.coe_var,
+    Subst.InS.coe_lift, ←Subst.lift_comp]
   congr
   funext k
   cases k <;> rfl
@@ -585,7 +585,8 @@ theorem Eqv.Pure.left_central {A A' B B' : Ty α} {Γ : Ctx α ε}
   induction l using Quotient.inductionOn
   apply eq_of_term_eq
   simp only [Set.mem_setOf_eq, InS.coe_wk, Ctx.InS.coe_wk0, Ctx.InS.coe_wk1, ← subst_fromWk,
-    Term.subst_subst, InS.coe_subst, Subst.coe_lift, InS.coe_subst0, InS.coe_var, Ctx.InS.coe_wk2]
+    Term.subst_subst, InS.coe_subst, Subst.InS.coe_lift, InS.coe_subst0, InS.coe_var,
+    Ctx.InS.coe_wk2]
   congr
   funext k
   cases k <;> rfl

DeBruijnSSA/BinSyntax/Rewrite/Term/Eqv.lean

@@ -1221,7 +1221,7 @@ theorem Eqv.let1_wk_eff_let1 {Γ : Ctx α ε}
   induction c using Quotient.inductionOn
   induction a using Quotient.inductionOn
   apply Eqv.eq_of_term_eq
-  simp only [Set.mem_setOf_eq, InS.coe_subst, Subst.coe_lift, InS.coe_subst0, InS.coe_wk0,
+  simp only [Set.mem_setOf_eq, InS.coe_subst, Subst.InS.coe_lift, InS.coe_subst0, InS.coe_wk0,
     InS.coe_wk, Ctx.InS.coe_swap01, ← subst_fromWk, Term.subst_subst]
   congr
   funext k

DeBruijnSSA/BinSyntax/Typing/Region/Basic.lean

@@ -227,6 +227,75 @@ theorem InS.induction
     simp only [Fin.cast_eq_self] at *
     exact cfg R ⟨_, dβ⟩ (λi => ⟨_, dG i⟩) Iβ IG
 
+def output_first (R : LCtx α) (Y : Ty α) (L : LCtx α) : Ty α
+  := (R ++ (Y::L))[0]
+
+def output_rest (R : LCtx α) (Y : Ty α) (L : LCtx α) : LCtx α
+  := (R ++ (Y::L)).drop 1
+
+theorem output_reshuffle_helper {R : LCtx α} {Y : Ty α} {L : LCtx α}
+  : (R ++ (Y::L)) = (output_first R Y L)::(output_rest R Y L)
+  := by cases R <;> rfl
+
+theorem InS.arrow_induction
+  {motive : (X : Ty α) → (Γ : Ctx α ε) → (Y : Ty α) → (L : LCtx α)
+    → InS φ ((X, ⊥)::Γ) (Y::L) → Prop}
+  (br : ∀{X Γ Y L A} (ℓ)
+    (a : Term.InS φ ((X, ⊥)::Γ) ⟨A, ⊥⟩) (hℓ : LCtx.Trg (Y::L) ℓ A), motive X Γ Y L (InS.br ℓ a hℓ))
+  (let1 : ∀{X Γ Y L A e} (a : Term.InS φ ((X, ⊥)::Γ) ⟨A, e⟩) (t : InS φ (⟨A, ⊥⟩::⟨X, ⊥⟩::Γ) (Y::L)),
+    motive _ _ _ _ t → motive _ Γ _ L (InS.let1 a t))
+  (let2 : ∀{X Γ Y L A B e}
+    (a : Term.InS φ ((X, ⊥)::Γ) ⟨Ty.prod A B, e⟩) (t : InS φ (⟨B, ⊥⟩::⟨A, ⊥⟩::⟨X, ⊥⟩::Γ) (Y::L)),
+    motive _ _ _ _ t → motive _ Γ _ L (InS.let2 a t))
+  (case : ∀{X Γ Y L A B e} (a : Term.InS φ ((X, ⊥)::Γ) ⟨Ty.coprod A B, e⟩)
+    (s : InS φ (⟨A, ⊥⟩::⟨X, ⊥⟩::Γ) (Y::L)) (t : InS φ (⟨B, ⊥⟩::⟨X, ⊥⟩::Γ) (Y::L)),
+    motive _ _ _ _ s → motive _ _ _ _ t → motive _ Γ _ L (InS.case a s t))
+  (cfg : ∀{X Γ Y L} (R)
+    (dβ : InS φ ((X, ⊥)::Γ) (R ++ (Y :: L)))
+    (dG : ∀i : Fin R.length, InS φ (⟨R.get i, ⊥⟩::⟨X, ⊥⟩::Γ) (R ++ (Y :: L))),
+    motive X Γ _ _ (dβ.cast rfl output_reshuffle_helper)
+    → (∀i, motive _ _ _ _ ((dG i).cast rfl output_reshuffle_helper))
+    → motive _ Γ _ L (InS.cfg R dβ dG))
+  {X Γ Y L} : (h : InS φ ((X, ⊥)::Γ) (Y::L)) → motive _ _ _ _ h
+  | ⟨r, hr⟩ => by
+    let Γr := (X, ⊥)::Γ
+    generalize hΓ' : Γr = Γ'
+    have hΓ' : (X, ⊥)::Γ = Γ' := hΓ'
+    let Lr := Y::L
+    generalize hL' : Lr = L'
+    have hL' : Y::L = L' := hL'
+    rw [hΓ', hL'] at hr
+    induction hr generalizing X Γ Y L with
+    | br hℓ ha =>
+      cases hΓ'
+      cases hL'
+      exact br _ ⟨_, ha⟩ hℓ
+    | let1 ha hr Ir =>
+      cases hΓ'
+      cases hL'
+      exact let1 ⟨_, ha⟩ ⟨_, hr⟩ (Ir hr rfl rfl rfl rfl)
+    | let2 ha hr Ir =>
+      cases hΓ'
+      cases hL'
+      exact let2 ⟨_, ha⟩ ⟨_, hr⟩ (Ir hr rfl rfl rfl rfl)
+    | case ha hl hr Il Ir =>
+      cases hΓ'
+      cases hL'
+      exact case ⟨_, ha⟩ ⟨_, hl⟩ ⟨_, hr⟩ (Il hl rfl rfl rfl rfl) (Ir hr rfl rfl rfl rfl)
+    | cfg n R hR dβ dG Iβ IG =>
+      cases hΓ'
+      cases hL'
+      cases hR
+      simp only [Fin.cast_eq_self] at *
+      apply cfg R ⟨_, dβ⟩ (λi => ⟨_, dG i⟩)
+      exact Iβ (output_reshuffle_helper ▸ dβ) rfl rfl
+        output_reshuffle_helper.symm
+        output_reshuffle_helper.symm
+      intro i
+      apply IG i (output_reshuffle_helper ▸ dG i) rfl rfl
+        output_reshuffle_helper.symm
+        output_reshuffle_helper.symm
+
 def InD (φ) [EffInstSet φ (Ty α) ε] (Γ : Ctx α ε) (L : LCtx α) : Type _
   := Σr : Region φ, r.WfD Γ L
 

DeBruijnSSA/BinSyntax/Typing/Region/Compose.lean

@@ -202,9 +202,16 @@ theorem InS.coe_fixpoint {A B : Ty α} {Γ : Ctx α ε} {L : LCtx α}
     heq_eq_eq, true_and]
   ext i; cases i using Fin.elim1; rfl
 
-theorem InS.vwk_fixpoint {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
+theorem InS.vwk_lift_fixpoint {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
   {r : InS φ (⟨A, ⊥⟩::Δ) ((B.coprod A)::L)}
   {ρ : Ctx.InS Γ Δ}
   : r.fixpoint.vwk ρ.slift = (r.vwk ρ.slift).fixpoint := by
   ext
-  sorry
+  simp only [coe_fixpoint, coe_vwk, Ctx.InS.coe_slift, Region.vwk_lift_fixpoint]
+
+theorem InS.vsubst_lift_fixpoint {A B : Ty α} {Γ Δ : Ctx α ε} {L : LCtx α}
+  {r : InS φ (⟨A, ⊥⟩::Δ) ((B.coprod A)::L)}
+  {σ : Term.Subst.InS φ Γ Δ}
+  : r.fixpoint.vsubst (σ.lift (le_refl _)) = (r.vsubst (σ.lift (le_refl _))).fixpoint := by
+  ext
+  simp only [coe_fixpoint, coe_vsubst, Term.Subst.InS.coe_lift, Region.vsubst_lift_fixpoint]

DeBruijnSSA/BinSyntax/Typing/Term/Subst.lean

@@ -47,7 +47,7 @@ def Subst.InS.lift (h : V ≤ V') (σ : InS φ Γ Δ) : InS φ (V::Γ) (V'::Δ)
   := ⟨Subst.lift σ, σ.prop.lift h⟩
 
 @[simp]
-theorem Subst.coe_lift {h : V ≤ V'} {σ : InS φ Γ Δ}
+theorem Subst.InS.coe_lift {h : V ≤ V'} {σ : InS φ Γ Δ}
   : (σ.lift h : Subst φ) = Subst.lift σ
   := rfl
 
@@ -57,6 +57,14 @@ def Subst.WfD.slift {head} (hσ : σ.WfD Γ Δ) : σ.lift.WfD (head::Γ) (head::
 theorem Subst.Wf.slift {head} (hσ : σ.Wf Γ Δ) : σ.lift.Wf (head::Γ) (head::Δ)
   := hσ.lift (le_refl head)
 
+def Subst.InS.slift {head} (σ : Subst.InS φ Γ Δ) : Subst.InS φ (head::Γ) (head::Δ)
+  := σ.lift (le_refl _)
+
+@[simp]
+theorem Subst.coe_slift {head} {σ : Subst.InS φ Γ Δ}
+  : (σ.slift (head := head) : Subst φ) = (σ : Subst φ).lift
+  := rfl
+
 def Subst.WfD.lift₂ (h₁ : V₁ ≤ V₁') (h₂ : V₂ ≤ V₂') (hσ : σ.WfD Γ Δ)
   : σ.lift.lift.WfD (V₁::V₂::Γ) (V₁'::V₂'::Δ)
   := (hσ.lift h₂).lift h₁