import SessionTypes.LocalTypeR.Substitution

set_option linter.dupNamespace false
set_option linter.unusedSimpArgs false
set_option linter.unnecessarySimpa false
set_option linter.unnecessarySeqFocus false
set_option linter.unusedVariables false

/-
The Problem. Well-formedness (closed + contractive) must be preserved through unfold and
fullUnfold operations to maintain invariants during protocol verification. Branch well-formedness
propagates to/from enclosing send/recv types.

Solution Structure. `WellFormed.unfold` and `WellFormed.fullUnfold` prove preservation using
substitution lemmas from Substitution.lean. `branches_of_send/recv` extract branch well-formedness.
`WellFormed_send/recv` reconstruct type well-formedness from branches. `unguarded_unfolds_to_var`
(vacuous for closed types) shows the connection between guardedness and observable behavior.
-/

/-! # SessionTypes.LocalTypeR.WellFormedness

Well-formedness preservation (unfold, fullUnfold, branches) and unguarded variable theorem.
-/

namespace SessionTypes.LocalTypeR
open SessionTypes.GlobalType
/-! ## Well-formedness Preservation -/

/-- Unfold preserves well-formedness. -/
theorem LocalTypeR.WellFormed.unfold {t : LocalTypeR} (h : LocalTypeR.WellFormed t) :
    LocalTypeR.WellFormed t.unfold := by
  cases t with
  | «end» | var _ | send _ _ | recv _ _ =>
      simpa [LocalTypeR.unfold] using h
  | mu t body =>
      have hclosed : (body.substitute t (.mu t body)).isClosed :=
        LocalTypeR.is_closed_substitute_mu (t := t) (body := body) h.closed
      have hpair : body.isGuarded t = true ∧ body.isContractive = true := by
        simpa [LocalTypeR.isContractive, Bool.and_eq_true] using h.contractive
      have hbody_contr : body.isContractive = true := hpair.2
      have hcontr : (body.substitute t (.mu t body)).isContractive = true :=
        LocalTypeR.is_contractive_substitute body t (.mu t body) hbody_contr h.contractive h.closed
      exact ⟨hclosed, hcontr⟩

/-- Iterated unfold preserves well-formedness. -/
private theorem LocalTypeR.WellFormed.unfold_iter {t : LocalTypeR} (h : LocalTypeR.WellFormed t) :
    ∀ n, LocalTypeR.WellFormed ((LocalTypeR.unfold)^[n] t) := by
  intro n
  induction n with
  | zero =>
      simpa using h
  | succ n ih =>
      simpa [Function.iterate_succ_apply'] using (LocalTypeR.WellFormed.unfold (t := (LocalTypeR.unfold)^[n] t) ih)

/-- fullUnfold preserves well-formedness. -/
theorem LocalTypeR.WellFormed.full_unfold {t : LocalTypeR} (h : LocalTypeR.WellFormed t) :
    LocalTypeR.WellFormed t.fullUnfold := by
  simpa [LocalTypeR.fullUnfold] using (LocalTypeR.WellFormed.unfold_iter (t := t) h t.muHeight)

/-! ## Branch Well-Formedness Extraction Helpers -/

private theorem LocalTypeR.branches_well_formed_of_closed_contractive
    (bs : List BranchR)
    (hclosed : freeVarsOfBranches bs = [])
    (hcontr : isContractiveBranches bs = true) :
    ∀ lb ∈ bs, LocalTypeR.WellFormed lb.2.2 := by
  induction bs with
  | nil =>
      intro lb hmem
      cases hmem
  | cons head tail ih =>
      cases head with
      | mk label rest =>
          cases rest with
          | mk _vt cont =>
              have happend : cont.freeVars ++ freeVarsOfBranches tail = [] := by
                simpa [freeVarsOfBranches] using hclosed
              have hcont_nil : cont.freeVars = [] := (List.append_eq_nil_iff.mp happend).1
              have htail_nil : freeVarsOfBranches tail = [] := (List.append_eq_nil_iff.mp happend).2
              have hcont_closed : cont.isClosed := by
                simp [LocalTypeR.isClosed, List.is_empty_eq_true, hcont_nil]
              have hpair : cont.isContractive = true ∧ isContractiveBranches tail = true := by
                simpa [isContractiveBranches, Bool.and_eq_true] using hcontr
              have hcont_wf : LocalTypeR.WellFormed cont := ⟨hcont_closed, hpair.1⟩
              have htail_wf : ∀ lb ∈ tail, LocalTypeR.WellFormed lb.2.2 :=
                ih htail_nil hpair.2
              intro lb hmem
              have hmem' : lb = (label, _vt, cont) ∨ lb ∈ tail := by
                simpa [List.mem_cons] using hmem
              cases hmem' with
              | inl h_eq =>
                  subst h_eq
                  exact hcont_wf
              | inr hmem_tail =>
                  exact htail_wf lb hmem_tail

/-! ## Branch Well-Formedness from Send/Recv -/

/-- Well-formed send branches are well-formed. -/
theorem LocalTypeR.WellFormed.branches_of_send {p : String} {bs : List BranchR}
    (h : LocalTypeR.WellFormed (.send p bs)) :
    ∀ lb ∈ bs, LocalTypeR.WellFormed lb.2.2 := by
  have hclosed : freeVarsOfBranches bs = [] := by
    have hclosed' : (freeVarsOfBranches bs).isEmpty = true := by
      simpa [LocalTypeR.isClosed, LocalTypeR.freeVars] using h.closed
    exact (List.is_empty_eq_true _).1 hclosed'
  have hcontr : isContractiveBranches bs = true := by
    simpa [LocalTypeR.isContractive] using h.contractive
  exact LocalTypeR.branches_well_formed_of_closed_contractive bs hclosed hcontr

/-- Well-formed recv branches are well-formed. -/
theorem LocalTypeR.WellFormed.branches_of_recv {p : String} {bs : List BranchR}
    (h : LocalTypeR.WellFormed (.recv p bs)) :
    ∀ lb ∈ bs, LocalTypeR.WellFormed lb.2.2 := by
  have hclosed : freeVarsOfBranches bs = [] := by
    have hclosed' : (freeVarsOfBranches bs).isEmpty = true := by
      simpa [LocalTypeR.isClosed, LocalTypeR.freeVars] using h.closed
    exact (List.is_empty_eq_true _).1 hclosed'
  have hcontr : isContractiveBranches bs = true := by
    simpa [LocalTypeR.isContractive] using h.contractive
  exact LocalTypeR.branches_well_formed_of_closed_contractive bs hclosed hcontr

/-! ## Branch Aggregation Helpers -/

/-- If all branches are well-formed, then `freeVarsOfBranches` is empty. -/
private theorem free_vars_of_branches_of_well_formed (bs : List BranchR)
    (hWFbs : ∀ lb ∈ bs, LocalTypeR.WellFormed lb.2.2) :
    freeVarsOfBranches bs = [] := by
  induction bs with
  | nil => simp [freeVarsOfBranches]
  | cons head tail ih =>
      cases head with
      | mk label rest =>
          cases rest with
          | mk _vt cont =>
              have hcont_wf := hWFbs (label, _vt, cont) (List.Mem.head _)
              have htail_wf : ∀ lb ∈ tail, LocalTypeR.WellFormed lb.2.2 :=
                fun lb hm => hWFbs lb (List.Mem.tail _ hm)
              have hcont_closed : cont.freeVars = [] := by
                have h := hcont_wf.closed
                simp [LocalTypeR.isClosed, List.is_empty_eq_true] at h
                exact h
              have htail_nil := ih htail_wf
              simp [freeVarsOfBranches, hcont_closed, htail_nil]

/-- If all branches are well-formed, then `isContractiveBranches` is true. -/
private theorem is_contractive_branches_of_well_formed (bs : List BranchR)
    (hWFbs : ∀ lb ∈ bs, LocalTypeR.WellFormed lb.2.2) :
    isContractiveBranches bs = true := by
  induction bs with
  | nil => simp [isContractiveBranches]
  | cons head tail ih =>
      cases head with
      | mk label rest =>
          cases rest with
          | mk _vt cont =>
              have hcont_wf := hWFbs (label, _vt, cont) (List.Mem.head _)
              have htail_wf : ∀ lb ∈ tail, LocalTypeR.WellFormed lb.2.2 :=
                fun lb hm => hWFbs lb (List.Mem.tail _ hm)
              simp [isContractiveBranches, hcont_wf.contractive, ih htail_wf]

/-! ## Reconstructing Well-Formed Send/Recv -/

/-- Well-formed send: if all branches are well-formed, then the send type is well-formed. -/
theorem LocalTypeR.well_formed_send {p : String} {bs : List BranchR}
    (hWFbs : ∀ lb ∈ bs, LocalTypeR.WellFormed lb.2.2) :
    LocalTypeR.WellFormed (.send p bs) := by
  constructor
  · -- isClosed
    simp [LocalTypeR.isClosed, LocalTypeR.freeVars, List.is_empty_eq_true]
    exact free_vars_of_branches_of_well_formed bs hWFbs
  · -- isContractive
    simp [LocalTypeR.isContractive]
    exact is_contractive_branches_of_well_formed bs hWFbs

/-- Well-formed recv: if all branches are well-formed, then the recv type is well-formed. -/
theorem LocalTypeR.well_formed_recv {p : String} {bs : List BranchR}
    (hWFbs : ∀ lb ∈ bs, LocalTypeR.WellFormed lb.2.2) :
    LocalTypeR.WellFormed (.recv p bs) := by
  constructor
  · -- isClosed
    simp [LocalTypeR.isClosed, LocalTypeR.freeVars, List.is_empty_eq_true]
    exact free_vars_of_branches_of_well_formed bs hWFbs
  · -- isContractive
    simp [LocalTypeR.isContractive]
    exact is_contractive_branches_of_well_formed bs hWFbs

/-! ## Unguarded Variable Theorem (Coq's `eguarded_test`)

This is the key bridge between guardedness and observable behavior.
If a variable is free in a type but NOT guarded, then the type fully
unfolds to that variable.

The intuition is:
- An unguarded free variable sits at the "head" position
- Unfolding only substitutes under mu, so the variable stays at head
- After enough unfolding, we reach just the variable -/

/-! ## Vacuous Unguarded-Variable Lemmas (Closed Case) -/

/-- Helper for double substitution case in unfold_iter_subst_unguarded.

    NOTE: This theorem is NOT NEEDED for the contractive case!

    For closed + contractive types, fullUnfold can never reach .var because:
    1. Closed means no free variables → no unbound vars
    2. Contractive means all bound variables are guarded → no bound vars at head after unfolding

    This complex double substitution theorem only matters for NON-contractive types
    with unguarded variables, which are not our target use case.

    The theorem statement is now restricted to closed bodies, where it is vacuous,
    and kept only for API completeness. -/
theorem LocalTypeR.unfold_iter_double_subst (body : LocalTypeR)
    (t : String) (repl : LocalTypeR) (s : String) (v : String)
    (hvt : v ≠ t) (hvs : v ≠ s)
    (hclosed : body.isClosed)
    (h_free : body.isFreeIn v = true) (h_not_guarded : body.isGuarded v = false) :
    (LocalTypeR.unfold)^[body.muHeight] ((body.substitute t repl).substitute s (.mu s (body.substitute t repl))) = .var v := by
  -- For closed bodies this is vacuous: no free variables exist.
  have hmem : v ∈ body.freeVars := is_free_in_mem_free_vars body v h_free
  have hnil : body.freeVars = [] := by
    have : body.freeVars.isEmpty = true := by
      simpa [LocalTypeR.isClosed] using hclosed
    exact (List.is_empty_eq_true _).1 this
  have : False := by
    simpa [hnil] using hmem
  exact this.elim

/-- Auxiliary lemma for unguarded_unfolds_to_var.

    If v is free and unguarded in e, and v ≠ t, then iterating unfold e.muHeight
    times on (e.substitute t repl) gives .var v.

    This is the generalization of Coq's `eguarded_test` that handles arbitrary substitutions.
    The key insight is that the iteration count is determined by the ORIGINAL type e,
    not by the substituted type. Since v ≠ t, substituting t doesn't affect occurrences of v,
    and after e.muHeight iterations, we reach .var v.

    This lemma is now restricted to closed types, where it is vacuous. -/
theorem LocalTypeR.unfold_iter_subst_unguarded (e : LocalTypeR) (t : String) (repl : LocalTypeR)
    (v : String) (hvt : v ≠ t)
    (hclosed : e.isClosed)
    (h_free : e.isFreeIn v = true) (h_not_guarded : e.isGuarded v = false) :
    (LocalTypeR.unfold)^[e.muHeight] (e.substitute t repl) = .var v := by
  -- For closed types this is vacuous: no free variables exist.
  have hmem : v ∈ e.freeVars := is_free_in_mem_free_vars e v h_free
  have hnil : e.freeVars = [] := by
    have : e.freeVars.isEmpty = true := by
      simpa [LocalTypeR.isClosed] using hclosed
    exact (List.is_empty_eq_true _).1 this
  have : False := by
    simpa [hnil] using hmem
  exact this.elim

/-- If a variable is not guarded in a type (appears at head position after unfolding),
    then fully unfolding produces that variable.

    This corresponds to Coq's `eguarded_test`:
    ```coq
    Lemma eguarded_test : forall e sigma i, ~~ eguarded i e ->
      iter (emu_height e) eunf e [e sigma] = sigma i.
    ```

    This lemma is now restricted to closed types, where it is vacuous. -/
theorem LocalTypeR.unguarded_unfolds_to_var (lt : LocalTypeR) (v : String)
    (hclosed : lt.isClosed)
    (h_free : lt.isFreeIn v = true) (h_not_guarded : lt.isGuarded v = false) :
    lt.fullUnfold = .var v := by
  -- For closed types this is vacuous: no free variables exist.
  have hmem : v ∈ lt.freeVars := is_free_in_mem_free_vars lt v h_free
  have hnil : lt.freeVars = [] := by
    have : lt.freeVars.isEmpty = true := by
      simpa [LocalTypeR.isClosed] using hclosed
    exact (List.is_empty_eq_true _).1 this
  have : False := by
    simpa [hnil] using hmem
  exact this.elim

/-! ## Guarded Corollary for fullUnfold -/

/-- The converse: if a free variable IS guarded, fullUnfold reaches a non-variable form.

    This is the key property for proving observable_of_closed: closed types
    (with all bound variables guarded) unfold to send/recv/end. -/
theorem LocalTypeR.guarded_full_unfold_not_var (lt : LocalTypeR) (v : String)
    (h_guarded : lt.isGuarded v = true) (hclosed : lt.isClosed) :
    ∀ w, lt.fullUnfold ≠ .var w ∨ lt.isFreeIn v = false := by
  intro w
  right
  by_cases h_free : lt.isFreeIn v = true
  · have hmem : v ∈ lt.freeVars := is_free_in_mem_free_vars lt v h_free
    have hnil : lt.freeVars = [] := by
      have : lt.freeVars.isEmpty = true := by
        simpa [LocalTypeR.isClosed] using hclosed
      exact (List.is_empty_eq_true _).1 this
    have : False := by
      simpa [hnil] using hmem
    exact this.elim
  · simp [Bool.not_eq_true] at h_free
    exact h_free

end SessionTypes.LocalTypeR
