import Choreography.Projection.Project.ImplHeadPreservation

/-! # Project ImplObservables

Observable preservation: CProjectTransRelComp cannot relate types with incompatible heads.
-/

/-
The Problem. State the projection/harmony lemma objective and the exact invariant boundary it preserves.
Solution Structure. Introduce local helper lemmas first, then discharge the main theorem by case analysis over the operational/projection relation.
-/

set_option linter.unnecessarySimpa false

namespace Choreography.Projection.Project

open SessionTypes.GlobalType
open SessionTypes.LocalTypeR
open Choreography.Projection.Project
open Choreography.Projection.Projectb
open SessionCoTypes.EQ2
open SessionCoTypes.EQ2Props
open SessionCoTypes.EQ2Paco
open Paco
open SessionTypes.Participation

/-! ## Observable Preservation Lemmas for CProjectTransRelComp

CProjectTransRelComp preserves observable structure: types with incompatible
head constructors cannot be related. This is because:
1. CProject preserves head constructor (modulo mu-unfolding)
2. trans preserves head constructor (modulo mu-unfolding)
3. EQ2 preserves observable behavior (equi-recursive equivalence)

The composition of these relations cannot relate `.end` to `.var`, etc.
These lemmas are semantically sound because CProject and trans compute
the same observable behavior (just with different representation).
-/

/-! ## End Source Cases -/

/-- End cannot be CProjectTransRelComp-related to var. -/
theorem c_project_trans_rel_comp_end_not_var
    {v : String} (h : CProjectTransRelComp .end (.var v))
    (hWFa : LocalTypeR.WellFormed .end) (hWFc : LocalTypeR.WellFormed (.var v)) : False := by
  rcases h with hbase | ⟨b, heq, hrel⟩ | ⟨b, hrel, heq⟩ | ⟨b, b', heq, hrel, heq'⟩
  · cases (c_project_trans_rel_source_end (b := .var v) hbase)

  · cases b with
    | «end» =>
        cases (c_project_trans_rel_source_end (b := .var v) hrel)
    | var _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | send _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | recv _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | mu t body =>
        rcases c_project_trans_rel_source_mu (v := t) (body := body) (b := .var v) hrel with ⟨body', hEq⟩
        cases hEq
  · have hb : b = .end := c_project_trans_rel_source_end hrel
    subst hb
    simpa [EQ2F] using (EQ2.destruct heq)
    · have hcomp := eq2_c_project_trans_rel_eq2_compose (a := .end) (c := .var v) heq hrel heq'
        hWFa hWFc
      simpa [EQ2F] using hcomp

/-! ## End Source Cases (Send/Recv Targets) -/

/-- End cannot be CProjectTransRelComp-related to send. -/
theorem c_project_trans_rel_comp_end_not_send
    {p : String} {bs : List BranchR}
    (h : CProjectTransRelComp .end (.send p bs))
    (hWFa : LocalTypeR.WellFormed .end) (hWFc : LocalTypeR.WellFormed (.send p bs)) : False := by
  rcases h with hbase | ⟨b, heq, hrel⟩ | ⟨b, hrel, heq⟩ | ⟨b, b', heq, hrel, heq'⟩
  · cases (c_project_trans_rel_source_end (b := .send p bs) hbase)
  · cases b with
    | «end» =>
        cases (c_project_trans_rel_source_end (b := .send p bs) hrel)
    | var _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | send _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | recv _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | mu t body =>
        rcases c_project_trans_rel_source_mu (v := t) (body := body) (b := .send p bs) hrel with ⟨body', hEq⟩
        cases hEq
  · have hb : b = .end := c_project_trans_rel_source_end hrel
    subst hb
    simpa [EQ2F] using (EQ2.destruct heq)
  · have hcomp := eq2_c_project_trans_rel_eq2_compose (a := .end) (c := .send p bs) heq hrel heq'
      hWFa hWFc
    simpa [EQ2F] using hcomp

/-- End cannot be CProjectTransRelComp-related to recv. -/
theorem c_project_trans_rel_comp_end_not_recv
    {p : String} {bs : List BranchR}
    (h : CProjectTransRelComp .end (.recv p bs))
    (hWFa : LocalTypeR.WellFormed .end) (hWFc : LocalTypeR.WellFormed (.recv p bs)) : False := by
  rcases h with hbase | ⟨b, heq, hrel⟩ | ⟨b, hrel, heq⟩ | ⟨b, b', heq, hrel, heq'⟩
  · cases (c_project_trans_rel_source_end (b := .recv p bs) hbase)
  · cases b with
    | «end» =>
        cases (c_project_trans_rel_source_end (b := .recv p bs) hrel)
    | var _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | send _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | recv _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | mu t body =>
        rcases c_project_trans_rel_source_mu (v := t) (body := body) (b := .recv p bs) hrel with ⟨body', hEq⟩
        cases hEq
  · have hb : b = .end := c_project_trans_rel_source_end hrel
    subst hb
    simpa [EQ2F] using (EQ2.destruct heq)
    · have hcomp := eq2_c_project_trans_rel_eq2_compose (a := .end) (c := .recv p bs) heq hrel heq'
        hWFa hWFc
      simpa [EQ2F] using hcomp

/-! ## Var Source Cases -/

/-- Var cannot be CProjectTransRelComp-related to end. -/
theorem c_project_trans_rel_comp_var_not_end
    {v : String} (h : CProjectTransRelComp (.var v) .end)
    (hWFa : LocalTypeR.WellFormed (.var v)) (hWFc : LocalTypeR.WellFormed .end) : False := by
  rcases h with hbase | ⟨b, heq, hrel⟩ | ⟨b, hrel, heq⟩ | ⟨b, b', heq, hrel, heq'⟩
  · cases (c_project_trans_rel_source_var (v := v) (b := .end) hbase)
  · cases b with
    | «end» =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | var v' =>
        cases (c_project_trans_rel_source_var (v := v') (b := .end) hrel)
    | send _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | recv _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | mu t body =>
        rcases c_project_trans_rel_source_mu (v := t) (body := body) (b := .end) hrel with ⟨body', hEq⟩
        cases hEq
  · have hb : b = .var v := c_project_trans_rel_source_var (v := v) hrel
    subst hb
    simpa [EQ2F] using (EQ2.destruct heq)
    · have hcomp := eq2_c_project_trans_rel_eq2_compose (a := .var v) (c := .end) heq hrel heq'
        hWFa hWFc
      simpa [EQ2F] using hcomp

/-! ## Var Source Cases (Send/Recv Targets) -/

/-- Var cannot be CProjectTransRelComp-related to send. -/
theorem c_project_trans_rel_comp_var_not_send
    {v : String} {p : String} {bs : List BranchR}
    (h : CProjectTransRelComp (.var v) (.send p bs))
    (hWFa : LocalTypeR.WellFormed (.var v)) (hWFc : LocalTypeR.WellFormed (.send p bs)) : False := by
  rcases h with hbase | ⟨b, heq, hrel⟩ | ⟨b, hrel, heq⟩ | ⟨b, b', heq, hrel, heq'⟩
  · cases (c_project_trans_rel_source_var (v := v) (b := .send p bs) hbase)
  · cases b with
    | «end» =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | var v' =>
        cases (c_project_trans_rel_source_var (v := v') (b := .send p bs) hrel)
    | send _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | recv _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | mu t body =>
        rcases c_project_trans_rel_source_mu (v := t) (body := body) (b := .send p bs) hrel with ⟨body', hEq⟩
        cases hEq
  · have hb : b = .var v := c_project_trans_rel_source_var (v := v) hrel
    subst hb
    simpa [EQ2F] using (EQ2.destruct heq)
  · have hcomp := eq2_c_project_trans_rel_eq2_compose (a := .var v) (c := .send p bs) heq hrel heq'
      hWFa hWFc
    simpa [EQ2F] using hcomp

/-- Var cannot be CProjectTransRelComp-related to recv. -/
theorem c_project_trans_rel_comp_var_not_recv
    {v : String} {p : String} {bs : List BranchR}
    (h : CProjectTransRelComp (.var v) (.recv p bs))
    (hWFa : LocalTypeR.WellFormed (.var v)) (hWFc : LocalTypeR.WellFormed (.recv p bs)) : False := by
  rcases h with hbase | ⟨b, heq, hrel⟩ | ⟨b, hrel, heq⟩ | ⟨b, b', heq, hrel, heq'⟩
  · cases (c_project_trans_rel_source_var (v := v) (b := .recv p bs) hbase)
  · cases b with
    | «end» =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | var v' =>
        cases (c_project_trans_rel_source_var (v := v') (b := .recv p bs) hrel)
    | send _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | recv _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | mu t body =>
        rcases c_project_trans_rel_source_mu (v := t) (body := body) (b := .recv p bs) hrel with ⟨body', hEq⟩
        cases hEq
  · have hb : b = .var v := c_project_trans_rel_source_var (v := v) hrel
    subst hb
    simpa [EQ2F] using (EQ2.destruct heq)
    · have hcomp := eq2_c_project_trans_rel_eq2_compose (a := .var v) (c := .recv p bs) heq hrel heq'
        hWFa hWFc
      simpa [EQ2F] using hcomp

/-! ## Send Source Cases -/

/-- Send cannot be CProjectTransRelComp-related to end. -/
theorem c_project_trans_rel_comp_send_not_end
    {p : String} {bs : List BranchR}
    (h : CProjectTransRelComp (.send p bs) .end)
    (hWFa : LocalTypeR.WellFormed (.send p bs)) (hWFc : LocalTypeR.WellFormed .end) : False := by
  rcases h with hbase | ⟨b, heq, hrel⟩ | ⟨b, hrel, heq⟩ | ⟨b, b', heq, hrel, heq'⟩
  · cases (c_project_trans_rel_source_send (p := p) (bs := bs) (b := .end) hbase) with
    | intro cs hEq => cases hEq
  · cases b with
    | «end» =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | var _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | send p' bs' =>
        cases (c_project_trans_rel_source_send (p := p') (bs := bs') (b := .end) hrel) with
        | intro cs hEq => cases hEq
    | recv _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | mu t body =>
        rcases c_project_trans_rel_source_mu (v := t) (body := body) (b := .end) hrel with ⟨body', hEq⟩
        cases hEq
  · rcases c_project_trans_rel_source_send (p := p) (bs := bs) hrel with ⟨cs, hEq⟩
    cases hEq
    simpa [EQ2F] using (EQ2.destruct heq)
    · have hcomp := eq2_c_project_trans_rel_eq2_compose (a := .send p bs) (c := .end) heq hrel heq'
        hWFa hWFc
      simpa [EQ2F] using hcomp

/-! ## Send Source Cases (Var/Recv Targets) -/

/-- Send cannot be CProjectTransRelComp-related to var. -/
theorem c_project_trans_rel_comp_send_not_var
    {p : String} {bs : List BranchR} {v : String}
    (h : CProjectTransRelComp (.send p bs) (.var v))
    (hWFa : LocalTypeR.WellFormed (.send p bs)) (hWFc : LocalTypeR.WellFormed (.var v)) : False := by
  rcases h with hbase | ⟨b, heq, hrel⟩ | ⟨b, hrel, heq⟩ | ⟨b, b', heq, hrel, heq'⟩
  · cases (c_project_trans_rel_source_send (p := p) (bs := bs) (b := .var v) hbase) with
    | intro cs hEq => cases hEq
  · cases b with
    | «end» =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | var _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | send p' bs' =>
        cases (c_project_trans_rel_source_send (p := p') (bs := bs') (b := .var v) hrel) with
        | intro cs hEq => cases hEq
    | recv _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | mu t body =>
        rcases c_project_trans_rel_source_mu (v := t) (body := body) (b := .var v) hrel with ⟨body', hEq⟩
        cases hEq
  · rcases c_project_trans_rel_source_send (p := p) (bs := bs) hrel with ⟨cs, hEq⟩
    cases hEq
    simpa [EQ2F] using (EQ2.destruct heq)
    · have hcomp := eq2_c_project_trans_rel_eq2_compose (a := .send p bs) (c := .var v) heq hrel heq'
        hWFa hWFc
      simpa [EQ2F] using hcomp

/-! ## Send Source Cases (Recv Target) -/

/-- Send cannot be CProjectTransRelComp-related to recv. -/
theorem c_project_trans_rel_comp_send_not_recv
    {p1 : String} {bs1 : List BranchR}
    {p2 : String} {bs2 : List BranchR}
    (h : CProjectTransRelComp (.send p1 bs1) (.recv p2 bs2))
    (hWFa : LocalTypeR.WellFormed (.send p1 bs1)) (hWFc : LocalTypeR.WellFormed (.recv p2 bs2)) :
    False := by
  rcases h with hbase | ⟨b, heq, hrel⟩ | ⟨b, hrel, heq⟩ | ⟨b, b', heq, hrel, heq'⟩
  · cases (c_project_trans_rel_source_send (p := p1) (bs := bs1) (b := .recv p2 bs2) hbase) with
    | intro cs hEq => cases hEq
  · cases b with
    | «end» =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | var _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | send p' bs' =>
        cases (c_project_trans_rel_source_send (p := p') (bs := bs') (b := .recv p2 bs2) hrel) with
        | intro cs hEq => cases hEq
    | recv _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | mu t body =>
        rcases c_project_trans_rel_source_mu (v := t) (body := body) (b := .recv p2 bs2) hrel with ⟨body', hEq⟩
        cases hEq
  · rcases c_project_trans_rel_source_send (p := p1) (bs := bs1) hrel with ⟨cs, hEq⟩
    cases hEq
    simpa [EQ2F] using (EQ2.destruct heq)
    · have hcomp := eq2_c_project_trans_rel_eq2_compose (a := .send p1 bs1) (c := .recv p2 bs2) heq hrel heq'
        hWFa hWFc
      simpa [EQ2F] using hcomp

/-! ## Recv Source Cases -/

/-- Recv cannot be CProjectTransRelComp-related to end. -/
theorem c_project_trans_rel_comp_recv_not_end
    {p : String} {bs : List BranchR}
    (h : CProjectTransRelComp (.recv p bs) .end)
    (hWFa : LocalTypeR.WellFormed (.recv p bs)) (hWFc : LocalTypeR.WellFormed .end) : False := by
  rcases h with hbase | ⟨b, heq, hrel⟩ | ⟨b, hrel, heq⟩ | ⟨b, b', heq, hrel, heq'⟩
  · cases (c_project_trans_rel_source_recv (p := p) (bs := bs) (b := .end) hbase) with
    | intro cs hEq => cases hEq
  · cases b with
    | «end» =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | var _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | send _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | recv p' bs' =>
        cases (c_project_trans_rel_source_recv (p := p') (bs := bs') (b := .end) hrel) with
        | intro cs hEq => cases hEq
    | mu t body =>
        rcases c_project_trans_rel_source_mu (v := t) (body := body) (b := .end) hrel with ⟨body', hEq⟩
        cases hEq
  · rcases c_project_trans_rel_source_recv (p := p) (bs := bs) hrel with ⟨cs, hEq⟩
    cases hEq
    simpa [EQ2F] using (EQ2.destruct heq)
    · have hcomp := eq2_c_project_trans_rel_eq2_compose (a := .recv p bs) (c := .end) heq hrel heq'
        hWFa hWFc
      simpa [EQ2F] using hcomp

/-! ## Recv Source Cases (Var/Send Targets) -/

/-- Recv cannot be CProjectTransRelComp-related to var. -/
theorem c_project_trans_rel_comp_recv_not_var
    {p : String} {bs : List BranchR} {v : String}
    (h : CProjectTransRelComp (.recv p bs) (.var v))
    (hWFa : LocalTypeR.WellFormed (.recv p bs)) (hWFc : LocalTypeR.WellFormed (.var v)) : False := by
  rcases h with hbase | ⟨b, heq, hrel⟩ | ⟨b, hrel, heq⟩ | ⟨b, b', heq, hrel, heq'⟩
  · cases (c_project_trans_rel_source_recv (p := p) (bs := bs) (b := .var v) hbase) with
    | intro cs hEq => cases hEq
  · cases b with
    | «end» =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | var _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | send _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | recv p' bs' =>
        cases (c_project_trans_rel_source_recv (p := p') (bs := bs') (b := .var v) hrel) with
        | intro cs hEq => cases hEq
    | mu t body =>
        rcases c_project_trans_rel_source_mu (v := t) (body := body) (b := .var v) hrel with ⟨body', hEq⟩
        cases hEq
  · rcases c_project_trans_rel_source_recv (p := p) (bs := bs) hrel with ⟨cs, hEq⟩
    cases hEq
    simpa [EQ2F] using (EQ2.destruct heq)
    · have hcomp := eq2_c_project_trans_rel_eq2_compose (a := .recv p bs) (c := .var v) heq hrel heq'
        hWFa hWFc
      simpa [EQ2F] using hcomp

/-! ## Recv Source Cases (Send Target) -/

/-- Recv cannot be CProjectTransRelComp-related to send. -/
theorem c_project_trans_rel_comp_recv_not_send
    {p1 : String} {bs1 : List BranchR}
    {p2 : String} {bs2 : List BranchR}
    (h : CProjectTransRelComp (.recv p1 bs1) (.send p2 bs2))
    (hWFa : LocalTypeR.WellFormed (.recv p1 bs1)) (hWFc : LocalTypeR.WellFormed (.send p2 bs2)) :
    False := by
  rcases h with hbase | ⟨b, heq, hrel⟩ | ⟨b, hrel, heq⟩ | ⟨b, b', heq, hrel, heq'⟩
  · cases (c_project_trans_rel_source_recv (p := p1) (bs := bs1) (b := .send p2 bs2) hbase) with
    | intro cs hEq => cases hEq
  · cases b with
    | «end» =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | var _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | send _ _ =>
        simpa [EQ2F] using (EQ2.destruct heq)
    | recv p' bs' =>
        cases (c_project_trans_rel_source_recv (p := p') (bs := bs') (b := .send p2 bs2) hrel) with
        | intro cs hEq => cases hEq
    | mu t body =>
        rcases c_project_trans_rel_source_mu (v := t) (body := body) (b := .send p2 bs2) hrel with ⟨body', hEq⟩
        cases hEq
  · rcases c_project_trans_rel_source_recv (p := p1) (bs := bs1) hrel with ⟨cs, hEq⟩;
      cases hEq; simpa [EQ2F] using (EQ2.destruct heq)
  · simpa [EQ2F] using
      (eq2_c_project_trans_rel_eq2_compose (a := .recv p1 bs1) (c := .send p2 bs2) heq hrel heq'
        hWFa hWFc)


end Choreography.Projection.Project
