import Choreography.Projection.Projectb
import SessionCoTypes.EQ2
import SessionCoTypes.EQ2Props

/-
The Problem. Projection from global to local types is not unique: different
local types may project from the same global type. However, these projections
should be equivalent up to EQ2.

We must prove: if CProject g role e1 and CProject g role e2, then EQ2 e1 e2.
This establishes determinism modulo observational equivalence.

Solution Structure. Use trans_eq_of_c_project to relate both e1 and e2
to trans g role, then conclude by equality and EQ2 reflexivity.
-/

/-! # Choreography.Projection.ProjectProps

Determinism properties for CProject (up to EQ2).
-/

namespace Choreography.Projection.Projectb

open SessionTypes.GlobalType
open SessionTypes.LocalTypeR
open SessionCoTypes.EQ2
open SessionCoTypes.EQ2Props

/-! ## Claims -/

/-- Projection is deterministic up to EQ2 for well-formed globals. -/
def ProjectDeterministic (g : GlobalType) (role : String) (e1 e2 : LocalTypeR) : Prop :=
  CProject g role e1 → CProject g role e2 → g.wellFormed = true → EQ2 e1 e2

/-- Branch-wise projection is deterministic up to EQ2 (assuming well-formed branches). -/
def BranchesProjDeterministic (gbs : List (Label × GlobalType)) (role : String)
    (lbs1 lbs2 : List BranchR) : Prop :=
  BranchesProjRel CProject gbs role lbs1 →
  BranchesProjRel CProject gbs role lbs2 →
  (∀ gb ∈ gbs, gb.2.wellFormed = true) →
  BranchesRel EQ2 lbs1 lbs2

/-- Claims bundle for projection determinism. -/
structure Claims where
  /-- Projection is deterministic up to EQ2. -/
  project_deterministic :
    ∀ g role e1 e2, ProjectDeterministic g role e1 e2
  /-- Branch-wise projection is deterministic up to EQ2. -/
  branches_proj_deterministic :
    ∀ gbs role lbs1 lbs2, BranchesProjDeterministic gbs role lbs1 lbs2

/-! ## Determinism Theorems -/

/-- Projection is deterministic up to EQ2 (assuming well-formed global types).

Uses c_project_implies_eq2_trans twice and composes via eq2_trans_wf. -/
theorem project_deterministic {g : GlobalType} {role : String} {e1 e2 : LocalTypeR}
    (hp1 : CProject g role e1) (hp2 : CProject g role e2)
    (hwf : g.wellFormed = true) : EQ2 e1 e2 := by
  -- Reduce both projections to trans and conclude by equality.
  have hne : g.allCommsNonEmpty = true := by
    have hwf' := hwf
    simp [GlobalType.wellFormed, Bool.and_eq_true] at hwf'
    exact hwf'.1.1.2
  have htrans_eq : trans g role = e1 :=
    trans_eq_of_c_project g role e1 hp1 hne
  have htrans_eq2 : trans g role = e2 :=
    trans_eq_of_c_project g role e2 hp2 hne
  have hEq : e1 = e2 := by
    exact htrans_eq.symm.trans htrans_eq2
  subst hEq
  exact eq2_refl _

/-! ## Branch Determinism Helper -/

/-- Helper: cons case for branches_proj_deterministic. -/
private theorem branches_proj_deterministic_cons
    (lb1 : BranchR) (lbs1' : List BranchR)
    (lb2 : BranchR) (lbs2' : List BranchR)
    (gb : Label × GlobalType) (gbs' : List (Label × GlobalType))
    {role : String}
    (hpair1 : gb.1 = lb1.1 ∧ lb1.2.1 = none ∧ CProject gb.2 role lb1.2.2)
    (htail1 : BranchesProjRel CProject gbs' role lbs1')
    (hpair2 : gb.1 = lb2.1 ∧ lb2.2.1 = none ∧ CProject gb.2 role lb2.2.2)
    (htail2 : BranchesProjRel CProject gbs' role lbs2')
    (hwf : ∀ gb' ∈ (gb :: gbs'), gb'.2.wellFormed = true)
    (branches_det : ∀ {lbs1 lbs2}, BranchesProjRel CProject gbs' role lbs1 →
      BranchesProjRel CProject gbs' role lbs2 →
      (∀ gb'' ∈ gbs', gb''.2.wellFormed = true) → BranchesRel EQ2 lbs1 lbs2) :
    BranchesRel EQ2 (lb1 :: lbs1') (lb2 :: lbs2') := by
  cases gb with
  | mk l gcont =>
      cases lb1 with
      | mk l1 t1 =>
          cases lb2 with
          | mk l2 t2 =>
              rcases hpair1 with ⟨hlabel1, _hnone1, hcont1⟩
              rcases hpair2 with ⟨hlabel2, _hnone2, hcont2⟩
              have hwf_head : gcont.wellFormed = true := hwf (l, gcont) (by simp)
              have hcont_eq : EQ2 t1.2 t2.2 := project_deterministic hcont1 hcont2 hwf_head
              have hlabel_eq : l1 = l2 := hlabel1.symm.trans hlabel2; cases hlabel_eq
              have hwf_tail : ∀ gb' ∈ gbs', gb'.2.wellFormed = true := by
                intro gb' hmem; exact hwf gb' (by simp [hmem])
              have htail_eq := branches_det htail1 htail2 hwf_tail
              exact List.Forall₂.cons ⟨rfl, hcont_eq⟩ htail_eq

/-! ## Branch Determinism Theorem -/

/-- Determinism for branch-wise projection up to EQ2 (assuming well-formed branches). -/
theorem branches_proj_deterministic {gbs : List (Label × GlobalType)} {role : String}
    {lbs1 lbs2 : List BranchR}
    (h1 : BranchesProjRel CProject gbs role lbs1)
    (h2 : BranchesProjRel CProject gbs role lbs2)
    (hwf : ∀ gb ∈ gbs, gb.2.wellFormed = true) :
    BranchesRel EQ2 lbs1 lbs2 := by
  -- Induct over the branch list and use the head lemma.
  cases gbs with
  | nil =>
      cases h1
      cases h2
      exact List.Forall₂.nil
  | cons gb gbs' =>
      cases lbs1 with
      | nil => cases h1
      | cons lb1 lbs1' =>
          cases lbs2 with
          | nil => cases h2
          | cons lb2 lbs2' =>
              cases h1 with
              | cons hpair1 htail1 =>
                  cases h2 with
                  | cons hpair2 htail2 =>
                      exact branches_proj_deterministic_cons lb1 lbs1' lb2 lbs2' gb gbs'
                        hpair1 htail1 hpair2 htail2 hwf
                        (fun h1 h2 hwf' => branches_proj_deterministic h1 h2 hwf')

/-! ## Claims Bundle -/

/-- Assemble the determinism claims. -/
def claims : Claims := by
  -- Package the two determinism theorems.
  refine ⟨?_, ?_⟩
  · intro g role e1 e2
    exact project_deterministic
  · intro gbs role lbs1 lbs2
    exact branches_proj_deterministic

end Choreography.Projection.Projectb
