# Library PropiLmodel

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

Heyting Algebras as semantics for Intuitionistic Logic

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.

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

Fixpoint evalH' (A : list form) : H HA :=
match A with
| niltop HA
| s::Ameet (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.

# 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.
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::Altr 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).

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

# 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.
Defined.

Let meet: H H H.
Defined.

Let join: H H H.
Defined.

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