Require Export PropiL.
Require Export Coq.Relations.Relation_Definitions.

Record HeytingAlgebra : Type :=
  mkHeytingAlgebra {
    H:Type;
    R: H → H → Prop;
    bot: H;
    meet: H → H → H;
    join: H → H → H;
    imp: H → H → H;
    Rref : reflexive _ R;
    Rtra : transitive _ R;
    bot1 : ∀ u, R bot u;
    meet1 : ∀ u v w, R w u ∧ R w v ↔ R w (meet u v);
    join1 : ∀ u v w, R u w ∧ R v w ↔ R (join u v) w;
    imp1 : ∀ u v w, R (meet w u) v ↔ R w (imp u v)
}.

Section HAProperty.

  Variable HA: HeytingAlgebra.
  Implicit Type u v w: H HA.

  Definition eqH u v := R u v ∧ R v u.

  Lemma meet2 u v: R (meet u v) u.

  Lemma meet3 u v: R (meet u v) v.

  Lemma meet_com u v: eqH (meet u v) (meet v u).

  Definition top := imp (bot HA) (bot HA).

  Lemma top1 u: R u top.

  Lemma join2 u v: R u (join u v).

  Lemma join3 u v: R v (join u v).

  Lemma join_com u v: eqH (join u v) (join v u).

  Lemma imp2 u v: R (meet (imp u v) u) v.

End HAProperty.

Section HASound.

  Variable HA : HeytingAlgebra.

  Variable interp : var → H HA.

  Fixpoint evalH (s : form) : H HA :=
    match s with
      | Var x ⇒ interp x
      | Fal ⇒ bot HA
      | Imp s t ⇒ imp (evalH s) (evalH t)
      | And s t ⇒ meet (evalH s) (evalH t)
      | Or s t ⇒ join (evalH s) (evalH t)
    end.

  Fixpoint evalH' (A : list form) : H HA :=
    match A with
      | nil ⇒ top HA
      | s::A ⇒ meet (evalH' A) (evalH s)
    end.

  Definition hent A s := R (evalH' A) (evalH s).

  Lemma nd_soundHA A s : nd A s → hent A s.

  Lemma HAequiv s t : nd [] (Equi s t) → eqH (evalH s) (evalH t).

End HASound.

Section FormHeytingAlgebra.

  Let H := form.

  Let R s t := nd [] (Imp s t).

  Let bot := Fal.

  Let meet s t := And s t.

  Let join s t := Or s t.

  Let imp s t := Imp s t.

  Definition FormHA: HeytingAlgebra.
  Defined.

  Definition Vf (x: var) := (Var x).

  Lemma evalHf s: (@evalH FormHA Vf s) = s.

End FormHeytingAlgebra.

Lemma HA_nd s:
  (∀ (HA: HeytingAlgebra) (V: var → H HA), R (top HA) (evalH V s))
  → nd [] s.

Fixpoint ltr (A: context) (s: form): form :=
  match A with
  | [] ⇒ s
  | t::A ⇒ ltr A (Imp t s)
  end.

Lemma ltr_CharImp E A s:
  CharImp E → E A s ↔ E [] (ltr A s).

Lemma hent_imp (HA: HeytingAlgebra) V: CharImp (@hent HA V).

Theorem HA_iff_nd A s:
  (∀ (HA: HeytingAlgebra) (V: var → H HA), hent V A s)
  ↔ nd A s.

Record KripkeModel : Type :=
  mkKripkeModel {
    W: Type;
    WR: W → W → Prop;
    WRref : reflexive _ WR;
    WRtra : transitive _ WR;
    pred := W → Prop;
    interp: var → pred;
    persist: ∀ x a b, interp x a → WR a b → interp x b
}.

Section KripkeSemantics.
  Variable KM: KripkeModel.

  Fixpoint evalK s: pred KM :=
    match s with
    | Var x ⇒ interp x
    | Fal ⇒ fun _ ⇒ False
    | And s1 s2 ⇒ fun w ⇒ evalK s1 w ∧ evalK s2 w
    | Or s1 s2 ⇒ fun w ⇒ evalK s1 w ∨ evalK s2 w
    | Imp s1 s2 ⇒ fun w ⇒ ∀ v, WR w v → evalK s1 v → evalK s2 v
    end.

  Lemma evalK_mono u v s: evalK s u → WR u v → evalK s v.

  Definition evalKA A w := ∀ s, s el A → evalK s w.

  Lemma nd_soundKM A s: nd A s → ∀ w, evalKA A w → evalK s w.

End KripkeSemantics.

Section Kripke2Heyting.

  Variable KM : KripkeModel.

  Let UCS: pred KM → Prop
    := fun p ⇒ ∀ u v: W KM, WR u v → p u → p v.

  Let H: Type := {p: pred KM | UCS p}.

  Let R: H → H → Prop
    := fun a b ⇒ let (p,_) := a in let (q,_) := b in ∀ u, p u → q u.

  Let bot: H.
  Defined.

  Let meet: H → H → H.
  Defined.

  Let join: H → H → H.
  Defined.

  Let UC (w: W KM) : W KM → Prop := fun v ⇒ WR w v.

  (* imp s t := {w | (UCS of w) inter s is subset of t } *)
  Let imp: H → H → H.
  Defined.

  Definition K2H: HeytingAlgebra.
  Defined.

  Definition K2Hinterp: var → H.
  Defined.

  (* evalK s = evalH s *)
  Theorem evalK_evalH_agree s:
    let (p, _) := @evalH K2H K2Hinterp s in
    ∀ w, evalK s w ↔ p w.

End Kripke2Heyting.