
import Mathlib
import SessionCoTypes.Coinductive.LocalTypeC
import SessionCoTypes.Coinductive.Bridge
import SessionCoTypes.Coinductive.Observable
import SessionTypes.LocalTypeR

/- ## Structured Block 1 -/
set_option linter.dupNamespace false

/-! # toCoind Injectivity

Proof that toCoind embedding is injective for round-trip correctness. -/

/-
The Problem. The toCoind embedding from inductive to coinductive types should
be injective: distinct inductive types map to distinct coinductive types.
This is essential for round-trip correctness.

Solution Structure. Proves to_coind_injective by case analysis over constructors,
to_coind_branches_injective for branch list injectivity (mutually recursive),
and indexing lemmas for toCoindBranches (length, get).
-/

namespace SessionCoTypes.Coinductive

open SessionTypes.GlobalType
open SessionTypes.LocalTypeR

-- toCoind Injectivity

mutual
  theorem to_coind_injective : ∀ {t u : LocalTypeR}, toCoind t = toCoind u → t = u
    | .end, .end, _ => rfl
    | .end, .var _, h => by cases (congrArg head h)
    | .end, .mu _ _, h => by cases (congrArg head h)
    | .end, .send _ _, h => by cases (congrArg head h)
    | .end, .recv _ _, h => by cases (congrArg head h)
    | .var _, .end, h => by cases (congrArg head h)
    | .var x, .var y, h => by
        have hhead := congrArg head h
        have hx : x = y := by simpa [head_mk_var] using hhead
        subst hx; rfl
    | .var _, .mu _ _, h => by cases (congrArg head h)
    | .var _, .send _ _, h => by cases (congrArg head h)
    | .var _, .recv _ _, h => by cases (congrArg head h)
    | .mu _ _, .end, h => by cases (congrArg head h)
    | .mu _ _, .var _, h => by cases (congrArg head h)
    | .mu x body, .mu y body', h => by
        have hdest := congrArg PFunctor.M.dest h
        simp [toCoind, mkMu] at hdest
        have hxhy := (Sigma.mk.inj_iff.mp hdest)
        have hx : x = y := by cases hxhy.1; rfl
        subst hx
        have hfun : (fun _ : Unit => toCoind body) = (fun _ : Unit => toCoind body') := by
          exact eq_of_heq hxhy.2
        have hchild : toCoind body = toCoind body' := by
          simpa using congrArg (fun f => f ()) hfun
        exact congrArg (LocalTypeR.mu x) (to_coind_injective hchild)
    | .mu _ _, .send _ _, h => by cases (congrArg head h)
    | .mu _ _, .recv _ _, h => by cases (congrArg head h)
    -- toCoind Injectivity: Send/Recv Constructor Cases
    | .send _ _, .end, h => by cases (congrArg head h)
    | .send _ _, .var _, h => by cases (congrArg head h)
    | .send _ _, .mu _ _, h => by cases (congrArg head h)
    | .send p bs, .send q cs, h => by
        have hhead := congrArg head h
        have hhead' : p = q ∧ (toCoindBranches bs).map Prod.fst =
            (toCoindBranches cs).map Prod.fst := by
          simpa [toCoind, head_mk_send] using hhead
        have hpq : p = q := hhead'.1
        subst hpq
        have hbranches : toCoindBranches bs = toCoindBranches cs := by
          have h' := congrArg branchesOf h
          simpa [toCoind, branches_of_mk_send] using h'
        have hbs : bs = cs := to_coind_branches_injective hbranches
        subst hbs; rfl
    | .send _ _, .recv _ _, h => by cases (congrArg head h)
/- ## Structured Block 2 -/
    | .recv _ _, .end, h => by cases (congrArg head h)
    | .recv _ _, .var _, h => by cases (congrArg head h)
    | .recv _ _, .mu _ _, h => by cases (congrArg head h)
    | .recv _ _, .send _ _, h => by cases (congrArg head h)
    | .recv p bs, .recv q cs, h => by
        have hhead := congrArg head h
        have hhead' : p = q ∧ (toCoindBranches bs).map Prod.fst =
            (toCoindBranches cs).map Prod.fst := by
          simpa [toCoind, head_mk_recv] using hhead
        have hpq : p = q := hhead'.1
        subst hpq
        have hbranches : toCoindBranches bs = toCoindBranches cs := by
          have h' := congrArg branchesOf h
          simpa [toCoind, branches_of_mk_recv] using h'
        have hbs : bs = cs := to_coind_branches_injective hbranches
        subst hbs; rfl

  -- toCoindBranches Injectivity

  theorem to_coind_branches_injective :
      ∀ {bs cs : List BranchR}, toCoindBranches bs = toCoindBranches cs → bs = cs
    | [], [], _ => rfl
    | [], _ :: _, h => by simp [toCoindBranches] at h
    | _ :: _, [], h => by simp [toCoindBranches] at h
    | (lb, vt, t) :: bs, (lc, wt, u) :: cs, h => by
        have hcons :
            (lb, toCoind t) = (lc, toCoind u) ∧
              toCoindBranches bs = toCoindBranches cs := by
          simpa [toCoindBranches] using h
        rcases hcons with ⟨hhead, htail⟩
        have hlabel : lb = lc := congrArg Prod.fst hhead
        have ht : t = u := to_coind_injective (congrArg Prod.snd hhead)
        have hvt : vt = wt := by simpa [toCoindBranches] using h
        subst hlabel; subst ht; subst hvt
        have hrest : bs = cs := to_coind_branches_injective htail
        subst hrest; rfl
end

-- toCoindBranches Indexing

lemma to_coind_branches_length (bs : List BranchR) :
    (toCoindBranches bs).length = bs.length := by
  induction bs with
  | nil => rfl
  | cons _ _ ih => simp [toCoindBranches, ih]

lemma to_coind_branches_get {bs : List BranchR} (i : Fin bs.length) :
    (toCoindBranches bs).get (castFin (to_coind_branches_length bs).symm i) =
      ((bs.get i).1, toCoind (bs.get i).2.2) := by
  induction bs with
  | nil => exact (Fin.elim0 i)
  | cons b bs ih =>
      cases i using Fin.cases with
      | zero =>
          cases b with
          | mk label rest => cases rest with | mk vt cont => simp [toCoindBranches, castFin, to_coind_branches_length]
      | succ i => simpa [castFin, to_coind_branches_length] using ih i

/- ## Structured Block 3 -/
lemma to_coind_branches_get_snd {bs : List BranchR} (i : Fin bs.length) :
    ((toCoindBranches bs).get (castFin (to_coind_branches_length bs).symm i)).2 =
      toCoind (bs.get i).2.2 := by
  simpa using congrArg Prod.snd (to_coind_branches_get (bs := bs) i)

lemma labels_get_eq {bs : List BranchR} (i : Fin (bs.map Prod.fst).length) :
    (bs.map Prod.fst).get i = (bs.get (castFin (by simp) i)).1 := by
  induction bs with
  | nil => exact (Fin.elim0 i)
  | cons b bs ih =>
      cases i using Fin.cases with
      | zero => cases b with | mk label rest => cases rest with | mk vt cont => simp [castFin]
      | succ i => simp [castFin]

end SessionCoTypes.Coinductive
