import Semantics.EnvStep
import Choreography.Projection.Project
import SessionTypes.Participation
import SessionCoTypes.EQ2
import SessionCoTypes.EQ2Props
import SessionCoTypes.EQ2Paco
import Choreography.Projection.ProjSubst
import Semantics.Determinism
import Choreography.Harmony.MuUnfoldLemmas
import Choreography.Harmony.SubstEndUnguarded

/-
The Problem. Relate global protocol steps to environment steps in the operational
semantics, showing that projection commutes with execution. The key difficulty is
that projection distinguishes participants from non-participants, so step alignment
must preserve non-participant projections while respecting communication structure
for participants.

Solution Structure. Prove step harmony for direct communication steps, then show
non-participant projections are stable across unrelated steps. Combine these into
a Claims bundle that exposes the main harmony properties for downstream safety
proofs.
-/

/-! # Choreography.Harmony

Harmony between global steps and environment steps.

## Expose

The following definitions form the semantic interface for proofs:

- `Claims`: bundle of harmony properties
- `step_harmony`: global step induces matching env step
- `proj_trans_other_step`: non-participant projection unchanged after step

## Technical Debt Summary (legacy gaps removed; assumption-free in this file)

**MAJOR PROGRESS**: `trans_branches_coherent` ELIMINATED!
Coherence is now proven from first principles using participation structure, following Coq's proof strategy.

**Mu-unfolding (from MuUnfoldLemmas.lean):**
- `eq2_mu_crossed_unfold_left`: **PROVEN** via proj_subst + eq2_mu_self_unfold
- `eq2_mu_crossed_unfold_right`: **PROVEN** via proj_subst + eq2_mu_to_unfold
- `eq2_mu_unguarded_to_end`: **PROVEN** (vacuously true - hypotheses contradict when s ≠ t)
- `eq2_end_to_mu_unguarded`: **PROVEN** (vacuously true for closed types)

**Closedness theorems (PROVEN in GlobalType.lean):**
- `GlobalType.is_closed_substitute_mu`: **PROVEN** - mu-unfolding preserves closedness
- `GlobalType.is_closed_comm_branches`: **PROVEN** - closed comm has closed branches

**Proven coinductive theorems:**
- `subst_end_unguarded_eq2_end`: **PROVEN** in SubstEndUnguarded.lean via UnfoldsToEnd induction
- `trans_subst_comm`: **PROVEN** using paco coinduction (requires closedness)
- `eq2_trans_wf`: **PROVEN** via Bisim (EQ2Props.lean); used with explicit well-formedness witnesses

**Remaining Assumptions:** None (sender/receiver lemmas proven via head-action predicate)

**COHERENCE PROOF COMPLETE (modulo helper lemmas):**
- `trans_branches_coherent_eq2`: **PROVEN** using participation structure
  - Case 1 (non-participant): Uses `eq_end` - all branches project to .end
  - Case 2 (participant): Uses `part_of_all2` - uniform participation ✓
- `trans_produces_c_project`: Bridges trans to CProject (uses coherence)
- `branches_project_coherent`: Extracts EQ2 equivalence from AllBranchesProj

**Inherited from MuUnfoldLemmas.lean (via ProjSubst.lean):**
4. `proj_subst`: Projection-substitution commutation (Coq indProj.v:173)

**Key changes from Coq alignment:**
- `trans` now checks `(trans body role).isGuarded t` instead of `lcontractive body`
- This matches Coq's `eguarded` check on the projected type, not the global type
- Non-contractive projections are replaced with `.end` by construction
- The old `step_noncontr_impossible` assumption was removed (it was false for nested mu)
- All theorems require closedness of global types (standard for protocol verification)
-/

/-! ## Notes

## Projection Coherence

These lemmas establish that projection is coherent with stepping:
after a global step, the projected environment correctly reflects
the new local types for each role.

**Branch coherence follows from CProject's AllBranchesProj requirement:**

Lean's CProject definition ALREADY has Coq's coherence built-in via AllBranchesProj
(Projectb.lean:204-206). The coherence requirement is structurally present; we just need
to connect it to the trans function via c_project_implies_eq2_trans.

**Proof via wellFormedness** (outline):
Given a well-formed comm node with branches and non-participant role:
1. AllBranchesProj in CProject ensures all branches project to the same candidate
2. c_project_implies_eq2_trans connects CProject to trans
3. Transitivity gives us branch-to-branch EQ2 equivalence

**Alternative: Direct proof** (without wellFormedness):
We can prove this inductively on the branch list structure by showing that
consecutive branches project coherently, which composes to full coherence.
This approach uses only the structure of trans without requiring CProject proofs.

## Substitution Commutation

The core coinductive property: projection (via trans) commutes with global mu-substitution.

For any GlobalType g, recursion variable t, and mu-body G (where G = mu t g for some g):
  `EQ2 (projTrans (g.substitute t G) role) ((projTrans g role).substitute t (projTrans G role))`

This is the "projection commutes with substitution" lemma (Coq: `full_eunf_subst`).
The property requires coinductive reasoning because branch continuations recurse indefinitely.

## ProjSubstRel Postfixpoint Proof Notes

ProjSubstRel is a post-fixpoint of EQ2F (with EQ2 as accumulator).

This encapsulates the coinductive reasoning for projection-substitution commutation.
The proof proceeds by case analysis on the GlobalType witness:
- `.end`: both sides are `.end` ✓
- `.var v`: split on v = t; both sides match ✓
- `.mu s inner`:
  - s = t (shadowed): both sides identical ✓
  - s ≠ t:
    - Both guarded: mu-mu case via eq2_mu_crossed_unfold_left/right ✓
    - Mismatched guardedness: via eq2_mu_unguarded_to_end/eq2_end_to_mu_unguarded ✓
    - Both unguarded: both .end ✓
- `.comm sender receiver branches`:
  - role = sender: both .send, branches via trans_branches_proj_subst_rel ✓
  - role = receiver: both .recv, branches via trans_branches_proj_subst_rel ✓
  - non-participant:
    - empty branches: both .end ✓
    - non-empty: recursive call on continuation subterm ✓

## trans_subst_comm intent

Projection commutes with substitution.

For any GlobalType g, recursion variable t, mu-type G, and role:
  `EQ2 (projTrans (g.substitute t G) role) ((projTrans g role).substitute t (projTrans G role))`

This is semantically sound: the LHS and RHS represent the same infinite communication tree
when fully unfolded.

**Coq reference:** `full_eunf_subst` in `coLocal.v`

## EQ2 transitivity + subst_end_unguarded_eq2_end

EQ2 transitivity now uses `eq2_trans_wf` from EQ2Props (Bisim detour).
This replaces the prior `EQ2_trans` path and requires explicit
well-formedness witnesses for intermediate types.

Substituting `.end` for an unguarded variable produces something EQ2 to `.end`.

When `lt.isGuarded v = false`, the type `lt` has the structure:
- Either `lt = .var v` (directly), or
- `lt = .mu s body` where `s ≠ v` and `body.isGuarded v = false`

This is because `.send`/`.recv` always return `true` for `isGuarded`.

After substituting `.end` for `v`:
- `.var v` becomes `.end` (EQ2 .end .end)
- `.mu s body` becomes `.mu s (body.substitute v .end)`, which unfolds to `.end`
  because the inner structure eventually reaches `.var v` → `.end`

**PROVEN** in SubstEndUnguarded.lean via UnfoldsToEnd induction.
-/

namespace Choreography.Harmony

open SessionTypes.GlobalType
open SessionTypes.LocalTypeR
open Choreography.Projection.Projectb
open Choreography.Projection.Project
  (eq_end part_of2_or_end c_project_implies_eq2_trans Projectable ProjectableClosedWellFormed)
open SessionTypes.Participation (part_of2 part_of_all2 part_of_all2_comm_inv not_part_of2_comm)
open SessionCoTypes.EQ2
open SessionCoTypes.EQ2Props
open SessionCoTypes.Quotient
open Semantics.EnvStep

-- Alias to avoid ambiguity with Trans typeclass


abbrev projTrans := Choreography.Projection.Project.trans
open Choreography.Projection.Project (trans_comm_sender trans_comm_receiver trans_comm_other
  transBranches lcontractive trans_well_formed_of_well_formed)

/-! ## Claims Bundle -/

/-- Claims bundle for harmony lemmas. -/


structure Claims where
  /-- Global step induces environment step. -/
  harmony : ∀ g g' act, step g act g' → EnvStep (projEnv g) act (projEnv g')
  /-- Domain containment through steps (post ⊆ pre). -/
  dom_subset : ∀ env env' act, EnvStep env act env' →
    ∀ p, p ∈ env'.map Prod.fst → p ∈ env.map Prod.fst

/-! ## Step Harmony

The harmony property states that global steps are faithfully reflected in
the projected environment. This is the key lemma connecting global semantics
to local session type semantics. -/

/-- Global step induces environment step through projection. -/


theorem step_harmony (g g' : GlobalType) (act : GlobalActionR)
    (hstep : step g act g') :
    EnvStep (projEnv g) act (projEnv g') :=
  -- Directly lift the global step to an environment step.
  step_to_envstep g g' act hstep

/-! ## Projection Coherence -/

/-! ## Key Theorem: trans Produces Valid Projections

The trans function produces valid CProject proofs for well-formed types.
This is the bridge between computational projection (trans) and relational projection (CProject). -/

/-- Helper: wellFormed implies allCommsNonEmpty. -/
private theorem all_comms_non_empty_of_wf (g : GlobalType) (hwf : g.wellFormed = true) :
    g.allCommsNonEmpty = true := by
  -- Unpack the wellFormed conjunction to reach allCommsNonEmpty.
  simp only [GlobalType.wellFormed, Bool.and_eq_true] at hwf
  rcases hwf with ⟨⟨⟨_havb, hne⟩, _hnsc⟩, _hprod⟩
  exact hne

/-- Helper: CProject + wellFormed gives the exact trans candidate. -/
private theorem trans_eq_of_c_project_wf (g : GlobalType) (role : String) (lt : LocalTypeR)
    (hproj : CProject g role lt) (hwf : g.wellFormed = true) :
    projTrans g role = lt := by
  -- Use trans_eq_of_c_project after extracting allCommsNonEmpty.
  have hne := all_comms_non_empty_of_wf g hwf
  simpa [projTrans] using (trans_eq_of_c_project g role lt hproj hne)

/-- Helper: non-participant comms yield AllBranchesProj from CProject. -/
private theorem all_branches_proj_of_comm_nonpart
    (sender receiver : String) (branches : List (Label × GlobalType)) (role : String) (lt : LocalTypeR)
    (hns : role ≠ sender) (hnr : role ≠ receiver)
    (hproj : CProject (GlobalType.comm sender receiver branches) role lt) :
    AllBranchesProj CProject branches role lt := by
  -- Destructure the comm case in CProjectF and drop sender/receiver branches.
  have hF := c_project_destruct hproj
  simpa [CProjectF, hns, hnr] using hF

/-- Branch coherence from participation structure.

For well-formed communications where role is not a participant, all branch continuations
project to EQ2-equivalent local types. This is proven using the participation infrastructure:
- If role doesn't participate at all: all branches project to .end (via eq_end)
- If role participates through branches: all branches have part_of_all2 (uniform participation)

This theorem eliminates the trans_branches_coherent assumption by proving coherence from
first principles, following Coq's proof strategy. -/

/-! ## Participant Case -/

private theorem trans_branches_coherent_eq2_participant
    (sender receiver : String) (branches : List (Label × GlobalType)) (role : String)
    (hnp : role ≠ sender ∧ role ≠ receiver)
    (hne : branches ≠ [])
    (hwf : (GlobalType.comm sender receiver branches).wellFormed = true)
    (lt : LocalTypeR) (hproj_comm : CProject (.comm sender receiver branches) role lt) :
    ∀ b ∈ branches, EQ2 (projTrans b.2 role) (projTrans branches.head!.2 role) := by
  -- Use AllBranchesProj to identify a common candidate across branches.
  cases hbranches : branches with
  | nil => cases (hne hbranches)
  | cons hd tl =>
      intro b hmem
      have hwf' : (GlobalType.comm sender receiver (hd :: tl)).wellFormed = true := by
        simpa [hbranches] using hwf
      have hproj_comm' : CProject (GlobalType.comm sender receiver (hd :: tl)) role lt := by
        simpa [hbranches] using hproj_comm
      have hall : AllBranchesProj CProject (hd :: tl) role lt :=
        all_branches_proj_of_comm_nonpart sender receiver (hd :: tl) role lt hnp.1 hnp.2 hproj_comm'
      have hproj_hd : CProject hd.2 role lt := hall hd (List.Mem.head tl)
      have hproj_b : CProject b.2 role lt := hall b hmem
      have hwf_hd : hd.2.wellFormed = true :=
        GlobalType.well_formed_comm_branches sender receiver (hd :: tl) hwf' hd (List.Mem.head tl)
      have hwf_b : b.2.wellFormed = true :=
        GlobalType.well_formed_comm_branches sender receiver (hd :: tl) hwf' b hmem
      have htrans_hd : projTrans hd.2 role = lt := trans_eq_of_c_project_wf hd.2 role lt hproj_hd hwf_hd
      have htrans_b : projTrans b.2 role = lt := trans_eq_of_c_project_wf b.2 role lt hproj_b hwf_b
      have hEq : projTrans b.2 role = projTrans hd.2 role := by simp [htrans_b, htrans_hd]
      simpa [hbranches, List.head!, hEq] using (eq2_refl (projTrans hd.2 role))

/-! ## Non-Participant Case -/

private theorem trans_branches_coherent_eq2_nonpart
    (sender receiver : String) (branches : List (Label × GlobalType)) (role : String)
    (hne : branches ≠ [])
    (hwf : (GlobalType.comm sender receiver branches).wellFormed = true)
    (hnot : ¬ part_of2 role (.comm sender receiver branches)) :
    ∀ b ∈ branches, EQ2 (projTrans b.2 role) (projTrans branches.head!.2 role) := by
  -- Non-participants project each branch to .end.
  intro b hmem
  rcases not_part_of2_comm hnot with ⟨_, hnotbranch⟩
  cases hbranches : branches with
  | nil => cases (hne hbranches)
  | cons hd tl =>
      have hmem_hd : hd ∈ branches := by simp [hbranches]
      have hnopart_hd : ¬ part_of2 role hd.2 := hnotbranch hd hmem_hd
      have hnopart_b : ¬ part_of2 role b.2 := hnotbranch b hmem
      have hwf_hd : hd.2.wellFormed = true :=
        GlobalType.well_formed_comm_branches sender receiver branches hwf hd hmem_hd
      have hwf_b : b.2.wellFormed = true :=
        GlobalType.well_formed_comm_branches sender receiver branches hwf b hmem
      have hhd_end : EQ2 (projTrans hd.2 role) .end := eq2_symm (eq_end role hd.2 hnopart_hd hwf_hd)
      have hb_end : EQ2 (projTrans b.2 role) .end := eq2_symm (eq_end role b.2 hnopart_b hwf_b)
      simpa [hbranches, List.head!] using (eq2_trans_via_end hb_end (eq2_symm hhd_end))

/-- All branch projections are EQ2-coherent with the head branch for non-participants. -/


theorem trans_branches_coherent_eq2
    (sender receiver : String) (branches : List (Label × GlobalType)) (role : String)
    (hnp : role ≠ sender ∧ role ≠ receiver)
    (hne : branches ≠ [])
    (hwf : (GlobalType.comm sender receiver branches).wellFormed = true)
    (hproj_comm : ∃ lt, CProject (.comm sender receiver branches) role lt) :
    ∀ b ∈ branches, EQ2 (projTrans b.2 role) (projTrans branches.head!.2 role) := by
  -- Split on whether the role participates in the comm.
  intro b hmem
  by_cases hpart : part_of2 role (.comm sender receiver branches)
  · rcases hproj_comm with ⟨lt, hproj⟩
    exact trans_branches_coherent_eq2_participant sender receiver branches role hnp hne hwf lt hproj b hmem
  · exact trans_branches_coherent_eq2_nonpart sender receiver branches role hne hwf hpart b hmem

/-! ## BranchesProjRel Infrastructure -/

/-- Helper: transBranches produces branches satisfying BranchesProjRel with the witness relation. -/
private theorem trans_branches_satisfies_branches_proj_rel
    (gbs : List (Label × GlobalType)) (role : String)
    (hwf : ∀ gb ∈ gbs, gb.2.allCommsNonEmpty = true) :
    BranchesProjRel (fun g role cand => cand = projTrans g role ∧ g.allCommsNonEmpty = true)
      gbs role (transBranches gbs role) := by
  induction gbs with
  | nil =>
      simp only [transBranches, BranchesProjRel]
      exact List.Forall₂.nil
  | cons hd tl ih =>
      -- BranchesProjRel (hd :: tl) role (transBranches (hd :: tl) role)
      unfold transBranches BranchesProjRel
      -- Goal: List.Forall₂ (fun gb lb => gb.1 = lb.1 ∧ R gb.2 role lb.2) (hd :: tl) ((hd.1, trans hd.2 role) :: transBranches tl role)
      refine List.Forall₂.cons ?head ?tail
      case head =>
        -- Show: hd.1 = hd.1 ∧ R hd.2 role (trans hd.2 role)
        constructor
        · rfl
        · constructor
          · rfl
          · exact hwf hd (List.Mem.head tl)
      case tail =>
        -- Show: BranchesProjRel for tl
        exact ih (fun gb hmem => hwf gb (List.Mem.tail hd hmem))

/-! ## Branch Witness Extraction -/

/-- Helper: extract per-branch CProject witnesses from BranchesProjRel. -/
private theorem branches_proj_rel_to_c_project
    (gbs : List (Label × GlobalType)) (role : String) (lbs : List BranchR)
    (h : BranchesProjRel CProject gbs role lbs) :
    ∀ p ∈ gbs, ∃ lt, CProject p.2 role lt := by
  induction h with
  | nil =>
      intro p hp
      cases hp
  | cons hpair _hrest ih =>
      intro p hp
      cases hp with
      | head =>
          rcases hpair with ⟨_hlabel, hproj⟩
          exact ⟨_, hproj⟩
      | tail _ hmem =>
          exact ih _ hmem

/-- trans produces a valid projection that satisfies CProject.

This theorem establishes that when CProject already holds (and g is wellFormed),
the computational trans function produces the same candidate, hence also satisfies CProject.

**Proof strategy:**
It uses `trans_eq_of_c_project` to rewrite the candidate to `trans g role`. -/


theorem trans_produces_c_project (g : GlobalType) (role : String) (lt : LocalTypeR)
    (hproj : CProject g role lt) (hwf : g.wellFormed = true) :
    CProject g role (projTrans g role) := by
  -- Reduce to the original candidate via trans_eq_of_c_project.
  have htrans_eq : projTrans g role = lt := trans_eq_of_c_project_wf g role lt hproj hwf
  simpa [htrans_eq] using hproj

/-- Helper: derive equality of branch projections via a common CProject candidate. -/
private theorem branches_project_coherent_eq (sender receiver : String)
    (first_label : Label) (first_cont : GlobalType) (rest : List (Label × GlobalType))
    (label : Label) (cont : GlobalType) (role : String)
    (hmem : (label, cont) ∈ ((first_label, first_cont) :: rest))
    (hns : role ≠ sender) (hnr : role ≠ receiver)
    (hallwf_branches : ∀ b ∈ ((first_label, first_cont) :: rest), b.2.wellFormed = true)
    (hproj_comm :
      ∃ lt, CProject (GlobalType.comm sender receiver ((first_label, first_cont) :: rest)) role lt) :
    projTrans cont role = projTrans first_cont role := by
  -- Use CProject to get a common candidate and rewrite both branches to it.
  rcases hproj_comm with ⟨lt, hproj_comm⟩
  have hall : AllBranchesProj CProject ((first_label, first_cont) :: rest) role lt :=
    all_branches_proj_of_comm_nonpart sender receiver ((first_label, first_cont) :: rest)
      role lt hns hnr hproj_comm
  have hproj_first : CProject first_cont role lt :=
    hall (first_label, first_cont) (List.Mem.head rest)
  have hproj_cont : CProject cont role lt := hall (label, cont) hmem
  have hwf_first : first_cont.wellFormed = true :=
    hallwf_branches (first_label, first_cont) (List.Mem.head rest)
  have hwf_cont : cont.wellFormed = true := hallwf_branches (label, cont) hmem
  have htrans_first : projTrans first_cont role = lt :=
    trans_eq_of_c_project_wf first_cont role lt hproj_first hwf_first
  have htrans_cont : projTrans cont role = lt :=
    trans_eq_of_c_project_wf cont role lt hproj_cont hwf_cont
  simp [htrans_cont, htrans_first]

/-! ## Branch Coherence Theorem -/

/-- Branch coherence for non-participants: all branches project to EQ2-equivalent types. -/


theorem branches_project_coherent (sender receiver : String)
    (first_label : Label) (first_cont : GlobalType)
    (rest : List (Label × GlobalType)) (label : Label) (cont : GlobalType) (role : String)
    (hmem : (label, cont) ∈ ((first_label, first_cont) :: rest))
    (hns : role ≠ sender) (hnr : role ≠ receiver)
    (_hclosed_branches : ∀ b ∈ ((first_label, first_cont) :: rest), b.2.isClosed = true)
    (hallwf_branches : ∀ b ∈ ((first_label, first_cont) :: rest), b.2.wellFormed = true)
    (hproj_comm :
      ∃ lt, CProject (GlobalType.comm sender receiver ((first_label, first_cont) :: rest)) role lt) :
    EQ2 (projTrans cont role) (projTrans first_cont role) := by
  -- Reduce to equality of projections, then use EQ2 reflexivity.
  have hEq :=
    branches_project_coherent_eq sender receiver first_label first_cont rest label cont role
      hmem hns hnr hallwf_branches hproj_comm
  simpa [hEq] using (eq2_refl (projTrans cont role))

end Choreography.Harmony
