import SessionCoTypes.Bisim.EQ2Extraction

/-! # SessionCoTypes.Bisim.EQ2ToBisim

Converts EQ2 to Bisim under well-formedness and proves EQ2 transitivity via Bisim detour.
-/

/-
The Problem. EQ2 transitivity is hard to prove directly because the intermediate
witness can have arbitrary constructor structure. We can detour through Bisim,
which doesn't require constructor matching, but need to convert EQ2 to Bisim.

Solution Structure. Proves `EQ2.to_bisim_of_well_formed` converting EQ2 to Bisim
for well-formed types. Then `bisim_refl` shows Bisim is reflexive via EQ2.
EQ2 transitivity follows: convert both EQ2 relations to Bisim, use Bisim.trans,
then convert back.
-/

set_option linter.dupNamespace false
set_option linter.unnecessarySimpa false

namespace SessionCoTypes.Bisim
open SessionTypes.LocalTypeR
open SessionTypes.GlobalType
open SessionCoTypes.Observable
open SessionCoTypes.EQ2
open SessionCoTypes.CoinductiveRel
/-! ## EQ2 to Bisim (Well-Formed Witness) -/

theorem EQ2.to_bisim_of_well_formed {a b : LocalTypeR} (hWFa : LocalTypeR.WellFormed a)
    (hWFb : LocalTypeR.WellFormed b) (h : EQ2 a b) : Bisim a b := by
  exact EQ2.to_bisim_raw h hWFa hWFb

theorem EQ2.to_bisim {a b : LocalTypeR} (h : EQ2 a b)
    (hWFa : LocalTypeR.WellFormed a) (hWFb : LocalTypeR.WellFormed b) : Bisim a b := by
  exact EQ2.to_bisim_raw h hWFa hWFb
/-- Bisim is reflexive (general version using EQ2).

    For any type a, Bisim a a holds because EQ2 a a holds (EQ2 is reflexive),
    and EQ2 implies Bisim.

    This version doesn't require closed or contractive hypotheses, making it
    suitable for use with arbitrary types (including those with free variables). -/
theorem bisim_refl (a : LocalTypeR) (hWF : LocalTypeR.WellFormed a) : Bisim a a :=
  EQ2.to_bisim (eq2_refl a) hWF hWF

namespace Bisim

/-- Observable types are reflexively bisimilar. -/
theorem refl_of_observable {a : LocalTypeR} (_hobs : Observable a) (hWF : LocalTypeR.WellFormed a) :
    Bisim a a :=
  bisim_refl a hWF

/-- Bisim is reflexive for closed, contractive types. -/
theorem refl (a : LocalTypeR)
    (hclosed : a.isClosed := by decide)
    (hcontr : a.isContractive = true := by decide) : Bisim a a :=
  bisim_refl a ⟨hclosed, hcontr⟩

end Bisim


/-! ## EQ2 Transitivity via Bisim

The Bisim detour provides an alternative proof of EQ2 transitivity that does not
require the TransRel_postfix lemma. This eliminates the need for one of the two
private detours in EQ2.lean. -/

/-- EQ2 transitivity via the Bisim detour.

    This theorem provides an alternative proof of EQ2_trans that does not require
    the TransRel_postfix lemma. The proof goes:
    1. Convert EQ2 proofs to Bisim using EQ2.to_bisim
    2. Apply Bisim.trans (fully proven)
    3. Convert back to EQ2 using Bisim.to_eq2

    This theorem can replace the Bisim-based EQ2_trans in EQ2.lean once we
    resolve the circular import issue. -/
theorem eq2_trans_via_bisim {a b c : LocalTypeR}
    (hab : EQ2 a b) (hbc : EQ2 b c)
    (hWFa : LocalTypeR.WellFormed a) (hWFb : LocalTypeR.WellFormed b)
    (hWFc : LocalTypeR.WellFormed c) : EQ2 a c := by
  have hBisim_ab := EQ2.to_bisim hab hWFa hWFb
  have hBisim_bc := EQ2.to_bisim hbc hWFb hWFc
  have hBisim_ac := Bisim.trans hBisim_ab hBisim_bc
  exact Bisim.to_eq2 hBisim_ac

/-- EQ2 transitivity via Bisim, for contractive types. -/
theorem eq2_trans_via_bisim_of_contractive {a b c : LocalTypeR}
    (hab : EQ2 a b) (hbc : EQ2 b c)
    (hWFa : LocalTypeR.WellFormed a) (hWFb : LocalTypeR.WellFormed b)
    (hWFc : LocalTypeR.WellFormed c) : EQ2 a c := by
  exact eq2_trans_via_bisim hab hbc hWFa hWFb hWFc

/-! ## Observable Correspondence (WF-gated toEQ2) -/

/-- Build EQ2 from compatible observables (requires well-formedness). -/
theorem ObservableRel.to_eq2 {a b : LocalTypeR} {obs_a : Observable a} {obs_b : Observable b}
    (hrel : ObservableRel EQ2 obs_a obs_b)
    (hWFa : LocalTypeR.WellFormed a) (hWFb : LocalTypeR.WellFormed b) : EQ2 a b := by
  cases hrel with
  | is_end =>
      rename_i ha hb
      have ha_eq : EQ2 a .end := UnfoldsToEnd.to_eq2 ha
      have hb_eq : EQ2 b .end := UnfoldsToEnd.to_eq2 hb
      exact eq2_trans_via_end ha_eq (eq2_symm hb_eq)
  | is_var =>
      rename_i v ha hb
      have ha_eq : EQ2 a (.var v) := UnfoldsToVar.to_eq2 ha
      have hb_eq : EQ2 b (.var v) := UnfoldsToVar.to_eq2 hb
      exact eq2_trans_via_var ha_eq (eq2_symm hb_eq)
  | is_send hbr =>
      rename_i p bs cs ha hb
      have hWFbs := well_formed_branches_of_can_send ha hWFa
      have hWFcs := well_formed_branches_of_can_send hb hWFb
      have hWFsend_bs : LocalTypeR.WellFormed (.send p bs) :=
        LocalTypeR.well_formed_send hWFbs
      have hWFsend_cs : LocalTypeR.WellFormed (.send p cs) :=
        LocalTypeR.well_formed_send hWFcs
      have ha_eq : EQ2 a (.send p bs) := CanSend.to_eq2 ha
      have hb_eq : EQ2 b (.send p cs) := CanSend.to_eq2 hb
      have hsend_eq : EQ2 (.send p bs) (.send p cs) :=
        EQ2.construct (by exact ⟨rfl, hbr⟩)
      have h1 : EQ2 a (.send p cs) :=
        eq2_trans_via_bisim ha_eq hsend_eq hWFa hWFsend_bs hWFsend_cs
      exact eq2_trans_via_bisim h1 (eq2_symm hb_eq) hWFa hWFsend_cs hWFb
  | is_recv hbr =>
      rename_i p bs cs ha hb
      have hWFbs := well_formed_branches_of_can_recv ha hWFa
      have hWFcs := well_formed_branches_of_can_recv hb hWFb
      have hWFrecv_bs : LocalTypeR.WellFormed (.recv p bs) :=
        LocalTypeR.well_formed_recv hWFbs
      have hWFrecv_cs : LocalTypeR.WellFormed (.recv p cs) :=
        LocalTypeR.well_formed_recv hWFcs
      have ha_eq : EQ2 a (.recv p bs) := CanRecvD.to_eq2 (CanRecv.to_can_recv_d ha)
      have hb_eq : EQ2 b (.recv p cs) := CanRecvD.to_eq2 (CanRecv.to_can_recv_d hb)
      have hrecv_eq : EQ2 (.recv p bs) (.recv p cs) :=
        EQ2.construct (by exact ⟨rfl, hbr⟩)
      have h1 : EQ2 a (.recv p cs) :=
        eq2_trans_via_bisim ha_eq hrecv_eq hWFa hWFrecv_bs hWFrecv_cs
      exact eq2_trans_via_bisim h1 (eq2_symm hb_eq) hWFa hWFrecv_cs hWFb

/-! ## Observable Correspondence Equivalence -/

/-- EQ2 equivalence iff observables correspond (WF-gated). -/
theorem eq2_iff_observable_correspond {a b : LocalTypeR} (obs_a : Observable a)
    (hWFa : LocalTypeR.WellFormed a) (hWFb : LocalTypeR.WellFormed b) :
    EQ2 a b ↔ ∃ obs_b : Observable b, ObservableRel EQ2 obs_a obs_b := by
  constructor
  · intro h
    exact eq2_transfer_observable h obs_a hWFb
  · intro h
    obtain ⟨obs_b, hrel⟩ := h
    exact ObservableRel.to_eq2 hrel hWFa hWFb

/-! ## Round-trip Corollaries -/

/-- Round-trip: extract then inject recovers EQ2 (by proof irrelevance). -/
theorem extract_inject_roundtrip {a b : LocalTypeR} (h : EQ2 a b) (obs_a : Observable a)
    (hWFa : LocalTypeR.WellFormed a) (hWFb : LocalTypeR.WellFormed b) :
    ObservableRel.to_eq2 (eq2_transfer_observable h obs_a hWFb).2 hWFa hWFb = h :=
  Subsingleton.elim _ _

/-- Round-trip: inject then extract recovers the observable (by proof irrelevance). -/
theorem inject_extract_roundtrip {a b : LocalTypeR} {obs_a : Observable a} {obs_b : Observable b}
    (hrel : ObservableRel EQ2 obs_a obs_b)
    (hWFa : LocalTypeR.WellFormed a) (hWFb : LocalTypeR.WellFormed b) :
    eq2_transfer_observable (ObservableRel.to_eq2 hrel hWFa hWFb) obs_a hWFb = ⟨obs_b, hrel⟩ :=
  Subsingleton.elim _ _

end SessionCoTypes.Bisim
