Library PropiLmodel

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

Heyting Algebras as semantics for Intuitionistic Logic

Record HeytingAlgebra : Type :=
  mkHeytingAlgebra {
    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.

Soundness of Heyting algebra

Section HASound.

  Variable HA : HeytingAlgebra.

  Variable interp : var H HA.

  Fixpoint evalH (s : form) : H HA :=
    match s with
      | Var xinterp x
      | Falbot HA
      | Imp s timp (evalH s) (evalH t)
      | And s tmeet (evalH s) (evalH t)
      | Or s tjoin (evalH s) (evalH t)

  Fixpoint evalH' (A : list form) : H HA :=
    match A with
      | niltop HA
      | s::Ameet (evalH' A) (evalH s)

  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.

Completeness of Heyting algebra

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.

  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::Altr A (Imp t s)

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).

Completeness of Heyting Algebras
Theorem HA_iff_nd A s:
  ( (HA: HeytingAlgebra) (V: var H HA), hent V A s)
   nd A s.

Kripke Semantics

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 xinterp x
    | Falfun _False
    | And s1 s2fun wevalK s1 w evalK s2 w
    | Or s1 s2fun wevalK s1 w evalK s2 w
    | Imp s1 s2fun w v, WR w v evalK s1 v evalK s2 v

  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.

From Kripke to Heyting

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 blet (p,_) := a in let (q,_) := b in u, p u q u.

  Let bot: H.

  Let meet: H H H.

  Let join: H H H.

  Let UC (w: W KM) : W KM Prop := fun vWR w v.

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

  Definition K2H: HeytingAlgebra.

  Definition K2Hinterp: var H.

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

End Kripke2Heyting.