/-
Port of `Analysis/Sign.agda`.

Correspondence:
  Sign (+ / - / 0ˢ)         ↦ Sign.plus / Sign.minus / Sign.zero
  _≟ᵍ_, ≡-equiv, ≡-Decidable ↦ deriving DecidableEq
  SignLattice (AboveBelow)  ↦ SignLattice
  AB.Plain 0ˢ               ↦ the AboveBelow FiniteHeightLattice instance,
                              seeded by `Inhabited Sign := ⟨.zero⟩`
  plus, minus               ↦ plus, minus
  plus-Monoˡ/ʳ, minus-Monoˡ/ʳ (postulates in Agda!)
                            ↦ plus_mono_left/right, minus_mono_left/right —
                              now actually proved, via
                              AboveBelow.monotone₂_of_strict
  plus-Mono₂, minus-Mono₂   ↦ plus_mono₂, minus_mono₂
  ⟦_⟧ᵍ                      ↦ interpSign
  ⟦⟧ᵍ-respects-≈ᵍ           ↦ (trivial with `=`)
  ⟦⟧ᵍ-⊔ᵍ-∨, ⟦⟧ᵍ-⊓ᵍ-∧        ↦ interpSign_sup, interpSign_inf
  s₁≢s₂⇒¬s₁∧s₂              ↦ interpSign_mk_disjoint
  latticeInterpretationᵍ    ↦ signInterpretation
  WithProg.eval, eval-Monoʳ ↦ SignAnalysis.eval, eval_mono
  SignEval (instance)       ↦ SignAnalysis.exprEvaluator
  plus-valid, minus-valid   ↦ plus_valid, minus_valid
  eval-valid, SignEvalValid ↦ eval_valid
  output                    ↦ SignAnalysis.output
  analyze-correct           ↦ SignAnalysis.analyze_correct
-/
import Spa.Analysis.Forward
import Spa.Analysis.Utils
import Spa.Showable

namespace Spa

inductive Sign where
  | plus
  | minus
  | zero
  deriving DecidableEq

instance : Showable Sign :=
  ⟨fun
    | .plus => "+"
    | .minus => "-"
    | .zero => "0"⟩

/-- Agda: the module parameter `x = 0ˢ` of `AB.Plain` (it seeds the
`FiniteHeightLattice (AboveBelow Sign)` instance). -/
instance : Inhabited Sign := ⟨.zero⟩

abbrev SignLattice : Type := AboveBelow Sign

open AboveBelow in
/-- Agda: `plus`. -/
def plus : SignLattice → SignLattice → SignLattice
  | bot, _ => bot
  | _, bot => bot
  | top, _ => top
  | _, top => top
  | mk .plus, mk .plus => mk .plus
  | mk .plus, mk .minus => top
  | mk .plus, mk .zero => mk .plus
  | mk .minus, mk .plus => top
  | mk .minus, mk .minus => mk .minus
  | mk .minus, mk .zero => mk .minus
  | mk .zero, mk .plus => mk .plus
  | mk .zero, mk .minus => mk .minus
  | mk .zero, mk .zero => mk .zero

open AboveBelow in
/-- Agda: `minus`. -/
def minus : SignLattice → SignLattice → SignLattice
  | bot, _ => bot
  | _, bot => bot
  | top, _ => top
  | _, top => top
  | mk .plus, mk .plus => top
  | mk .plus, mk .minus => mk .plus
  | mk .plus, mk .zero => mk .plus
  | mk .minus, mk .plus => mk .minus
  | mk .minus, mk .minus => top
  | mk .minus, mk .zero => mk .minus
  | mk .zero, mk .plus => mk .minus
  | mk .zero, mk .minus => mk .plus
  | mk .zero, mk .zero => mk .zero

/-- Agda: `plus-Mono₂` (its components were postulates in Agda; `plus` is a
strict operation on the flat lattice, so monotonicity holds regardless of the
sign table). -/
theorem plus_mono₂ : Monotone₂ plus :=
  AboveBelow.monotone₂_of_strict plus
    (fun y => by cases y <;> rfl)
    (fun x => by rcases x with _ | _ | s <;> first | rfl | (cases s <;> rfl))
    (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
    (fun x hx => by
      rcases x with _ | _ | s <;>
        first | exact absurd rfl hx | rfl | (cases s <;> rfl))

/-- Agda: `plus-Monoˡ` — a postulate there, a theorem here. -/
theorem plus_mono_left (s₂ : SignLattice) : Monotone (plus · s₂) := plus_mono₂.1 s₂

/-- Agda: `plus-Monoʳ` — a postulate there, a theorem here. -/
theorem plus_mono_right (s₁ : SignLattice) : Monotone (plus s₁) := plus_mono₂.2 s₁

/-- Agda: `minus-Mono₂` (likewise from strictness of `minus`). -/
theorem minus_mono₂ : Monotone₂ minus :=
  AboveBelow.monotone₂_of_strict minus
    (fun y => by cases y <;> rfl)
    (fun x => by rcases x with _ | _ | s <;> first | rfl | (cases s <;> rfl))
    (fun y hy => by cases y <;> first | exact absurd rfl hy | rfl)
    (fun x hx => by
      rcases x with _ | _ | s <;>
        first | exact absurd rfl hx | rfl | (cases s <;> rfl))

/-- Agda: `minus-Monoˡ` — a postulate there, a theorem here. -/
theorem minus_mono_left (s₂ : SignLattice) : Monotone (minus · s₂) := minus_mono₂.1 s₂

/-- Agda: `minus-Monoʳ` — a postulate there, a theorem here. -/
theorem minus_mono_right (s₁ : SignLattice) : Monotone (minus s₁) := minus_mono₂.2 s₁

/-- Agda: `⟦_⟧ᵍ`. -/
def interpSign : SignLattice → Value → Prop
  | .bot, _ => False
  | .top, _ => True
  | .mk .plus, v => ∃ n : ℕ, v = .int (n + 1)
  | .mk .zero, v => v = .int 0
  | .mk .minus, v => ∃ n : ℕ, v = .int (-(n + 1))

/-- Agda: `s₁≢s₂⇒¬s₁∧s₂`. -/
theorem interpSign_mk_disjoint {s₁ s₂ : Sign} (hne : s₁ ≠ s₂) {v : Value} :
    ¬(interpSign (.mk s₁) v ∧ interpSign (.mk s₂) v) := by
  rintro ⟨h₁, h₂⟩
  rcases s₁ <;> rcases s₂ <;> try exact hne rfl
  all_goals simp only [interpSign] at h₁ h₂
  · obtain ⟨n₁, rfl⟩ := h₁
    obtain ⟨n₂, hv⟩ := h₂
    injection hv with hz
    omega
  · obtain ⟨n₁, rfl⟩ := h₁
    injection h₂ with hz
    omega
  · obtain ⟨n₁, rfl⟩ := h₁
    obtain ⟨n₂, hv⟩ := h₂
    injection hv with hz
    omega
  · obtain ⟨n₁, rfl⟩ := h₁
    injection h₂ with hz
    omega
  · subst h₁
    obtain ⟨n₂, hv⟩ := h₂
    injection hv with hz
    omega
  · subst h₁
    obtain ⟨n₂, hv⟩ := h₂
    injection hv with hz
    omega

/-- Agda: `⟦⟧ᵍ-⊔ᵍ-∨` (via the factored flat-lattice lemma). -/
theorem interpSign_sup {s₁ s₂ : SignLattice} (v : Value)
    (h : interpSign s₁ v ∨ interpSign s₂ v) : interpSign (s₁ ⊔ s₂) v :=
  AboveBelow.interp_sup_of (fun _ h => h) (fun _ => trivial) v h

/-- Agda: `⟦⟧ᵍ-⊓ᵍ-∧` (via the factored flat-lattice lemma). -/
theorem interpSign_inf {s₁ s₂ : SignLattice} (v : Value)
    (h : interpSign s₁ v ∧ interpSign s₂ v) : interpSign (s₁ ⊓ s₂) v :=
  AboveBelow.interp_inf_of (fun hne _ => interpSign_mk_disjoint hne) v h

/-- Agda: `latticeInterpretationᵍ` (an instance there too). -/
instance signInterpretation : LatticeInterpretation SignLattice where
  interp := interpSign
  interp_sup := fun {l₁ l₂} v h => interpSign_sup (s₁ := l₁) (s₂ := l₂) v h
  interp_inf := fun {l₁ l₂} v h => interpSign_inf (s₁ := l₁) (s₂ := l₂) v h

namespace SignAnalysis

/-! Agda: `module WithProg (prog : Program)`. -/

variable (prog : Program)

/-- Agda: `WithProg.eval`. -/
def eval : Expr → VariableValues SignLattice prog → SignLattice
  | .add e₁ e₂, vs => plus (eval e₁ vs) (eval e₂ vs)
  | .sub e₁ e₂, vs => minus (eval e₁ vs) (eval e₂ vs)
  | .var k, vs =>
    if h : FiniteMap.MemKey k vs then (FiniteMap.locate h).1 else .top
  | .num 0, _ => .mk .zero
  | .num (_ + 1), _ => .mk .plus

/-- Agda: `WithProg.eval-Monoʳ`. -/
theorem eval_mono (e : Expr) : Monotone (eval prog e) := by
  induction e with
  | add e₁ e₂ ih₁ ih₂ =>
    intro vs₁ vs₂ h
    exact eval_combine₂ plus_mono₂ (ih₁ h) (ih₂ h)
  | sub e₁ e₂ ih₁ ih₂ =>
    intro vs₁ vs₂ h
    exact eval_combine₂ minus_mono₂ (ih₁ h) (ih₂ h)
  | var k =>
    intro vs₁ vs₂ h
    simp only [eval]
    by_cases hk : k ∈ prog.vars
    · rw [dif_pos (FiniteMap.memKey_iff.mpr hk),
          dif_pos (FiniteMap.memKey_iff.mpr hk)]
      exact FiniteMap.le_of_mem_mem prog.vars_nodup h
        (FiniteMap.locate _).2 (FiniteMap.locate _).2
    · rw [dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm)),
          dif_neg (fun hm => hk (FiniteMap.memKey_iff.mp hm))]
  | num n =>
    intro vs₁ vs₂ _
    cases n <;> exact le_refl _

/-- Agda: the `SignEval` instance. -/
instance exprEvaluator : ExprEvaluator SignLattice prog :=
  ⟨eval prog, eval_mono prog⟩

/-- Agda: `WithProg.result`/`output` — the analysis result, printed. -/
def output : String :=
  show' (result SignLattice prog)

/-- Agda: `plus-valid`. -/
theorem plus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
    (h₁ : interpSign g₁ (.int z₁)) (h₂ : interpSign g₂ (.int z₂)) :
    interpSign (plus g₁ g₂) (.int (z₁ + z₂)) := by
  rcases g₁ with _ | _ | s₁
  · exact h₁.elim
  · rcases g₂ with _ | _ | s₂
    · exact h₂.elim
    · exact trivial
    · exact trivial
  · rcases g₂ with _ | _ | s₂
    · exact h₂.elim
    · rcases s₁ <;> exact trivial
    · rcases s₁ <;> rcases s₂ <;>
        simp only [plus, interpSign, Value.int.injEq] at h₁ h₂ ⊢ <;>
        try trivial
      · obtain ⟨n₁, rfl⟩ := h₁
        obtain ⟨n₂, rfl⟩ := h₂
        exact ⟨n₁ + n₂ + 1, by omega⟩
      · obtain ⟨n₁, rfl⟩ := h₁
        subst h₂
        exact ⟨n₁, by omega⟩
      · obtain ⟨n₁, rfl⟩ := h₁
        obtain ⟨n₂, rfl⟩ := h₂
        exact ⟨n₁ + n₂ + 1, by omega⟩
      · obtain ⟨n₁, rfl⟩ := h₁
        subst h₂
        exact ⟨n₁, by omega⟩
      · subst h₁
        obtain ⟨n₂, rfl⟩ := h₂
        exact ⟨n₂, by omega⟩
      · subst h₁
        obtain ⟨n₂, rfl⟩ := h₂
        exact ⟨n₂, by omega⟩
      · subst h₁
        subst h₂
        omega

/-- Agda: `minus-valid`. -/
theorem minus_valid {g₁ g₂ : SignLattice} {z₁ z₂ : ℤ}
    (h₁ : interpSign g₁ (.int z₁)) (h₂ : interpSign g₂ (.int z₂)) :
    interpSign (minus g₁ g₂) (.int (z₁ - z₂)) := by
  rcases g₁ with _ | _ | s₁
  · exact h₁.elim
  · rcases g₂ with _ | _ | s₂
    · exact h₂.elim
    · exact trivial
    · exact trivial
  · rcases g₂ with _ | _ | s₂
    · exact h₂.elim
    · rcases s₁ <;> exact trivial
    · rcases s₁ <;> rcases s₂ <;>
        simp only [minus, interpSign, Value.int.injEq] at h₁ h₂ ⊢ <;>
        try trivial
      · obtain ⟨n₁, rfl⟩ := h₁
        obtain ⟨n₂, rfl⟩ := h₂
        exact ⟨n₁ + n₂ + 1, by omega⟩
      · obtain ⟨n₁, rfl⟩ := h₁
        subst h₂
        exact ⟨n₁, by omega⟩
      · obtain ⟨n₁, rfl⟩ := h₁
        obtain ⟨n₂, rfl⟩ := h₂
        exact ⟨n₁ + n₂ + 1, by omega⟩
      · obtain ⟨n₁, rfl⟩ := h₁
        subst h₂
        exact ⟨n₁, by omega⟩
      · subst h₁
        obtain ⟨n₂, rfl⟩ := h₂
        exact ⟨n₂, by omega⟩
      · subst h₁
        obtain ⟨n₂, rfl⟩ := h₂
        exact ⟨n₂, by omega⟩
      · subst h₁
        subst h₂
        omega

/-- Agda: `eval-valid` / the `SignEvalValid` instance. -/
instance eval_valid : ValidExprEvaluator SignLattice prog := by
  constructor
  intro vs ρ e v hev
  induction hev with
  | num n =>
    intro _
    show interpSign (eval prog (.num n) vs) (.int n)
    cases n with
    | zero => rfl
    | succ n' => exact ⟨n', congrArg Value.int (by push_cast; ring)⟩
  | var x v hxv =>
    intro hvs
    show interpSign (eval prog (.var x) vs) v
    simp only [eval]
    by_cases hk : FiniteMap.MemKey x vs
    · rw [dif_pos hk]
      exact hvs _ _ (FiniteMap.locate hk).2 _ hxv
    · rw [dif_neg hk]
      exact trivial
  | add e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ =>
    intro hvs
    have h₁ : interpSign (eval prog e₁ vs) (.int z₁) := ih₁ hvs
    have h₂ : interpSign (eval prog e₂ vs) (.int z₂) := ih₂ hvs
    show interpSign (eval prog (.add e₁ e₂) vs) (.int (z₁ + z₂))
    exact plus_valid h₁ h₂
  | sub e₁ e₂ z₁ z₂ _ _ ih₁ ih₂ =>
    intro hvs
    have h₁ : interpSign (eval prog e₁ vs) (.int z₁) := ih₁ hvs
    have h₂ : interpSign (eval prog e₂ vs) (.int z₂) := ih₂ hvs
    show interpSign (eval prog (.sub e₁ e₂) vs) (.int (z₁ - z₂))
    exact minus_valid h₁ h₂

/-- Agda: `WithProg.analyze-correct`. -/
theorem analyze_correct {ρ : Env} (hrun : EvalStmt [] prog.rootStmt ρ) :
    interpV (variablesAt prog.finalState (result SignLattice prog)) ρ :=
  Spa.analyze_correct SignLattice prog hrun

end SignAnalysis

end Spa