Library HeytingAndKripke
Require Export PropL.
Record HeytingAlgebra : Type :=
mkHeytingAlgebra {
H:Type;
R: H -> H -> Prop;
bot: H;
top: H;
meet: H -> H -> H;
join: H -> H -> H;
imp: H -> H -> H;
Rref : forall w, R w w;
Rtra : forall u v w, R u v -> R v w -> R u w;
bot1 : forall u, R bot u;
top1 : forall u, R u top;
meet1 : forall u v, R (meet u v) u;
meet2 : forall u v, R (meet u v) v;
meet3 : forall u v w, R w u -> R w v -> R w (meet u v);
join1 : forall u v, R u (join u v);
join2 : forall u v, R v (join u v);
join3 : forall u v w, R u w -> R v w -> R (join u v) w;
imp1 : forall u v, R (meet (imp u v) u) v;
imp2 : forall u v w, R (meet w u) v -> R w (imp u v)
}.
Section HeytingAlgebra.
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)
end.
Fixpoint evalH' (A : list form) : H HA :=
match A with
| nil => top HA
| s::A => meet (evalH' A) (evalH s)
end.
Lemma nd_soundH A s : nd A s -> R (evalH' A) (evalH s).
End HeytingAlgebra.
Section HeytingHa5.
Inductive Ha5 : Type := Ha5bot | Ha5ab | Ha5a | Ha5b | Ha5top.
Definition Ha5R (a b : Ha5) : Prop :=
match a,b with
| Ha5bot,_ => True
| _,Ha5bot => False
| _,Ha5top => True
| Ha5top,_ => False
| Ha5a, Ha5a => True
| Ha5a, Ha5b => False
| Ha5a, Ha5ab => False
| Ha5b, Ha5a => False
| Ha5b, Ha5b => True
| Ha5b, Ha5ab => False
| Ha5ab, Ha5a => True
| Ha5ab, Ha5b => True
| Ha5ab, Ha5ab => True
end.
Definition Ha5meet (a b : Ha5) : Ha5 :=
match a,b with
| Ha5bot,_ => Ha5bot
| _,Ha5bot => Ha5bot
| Ha5top,b => b
| a,Ha5top => a
| Ha5a, Ha5a => Ha5a
| Ha5a, Ha5b => Ha5ab
| Ha5a, Ha5ab => Ha5ab
| Ha5b, Ha5a => Ha5ab
| Ha5b, Ha5b => Ha5b
| Ha5b, Ha5ab => Ha5ab
| Ha5ab, Ha5a => Ha5ab
| Ha5ab, Ha5b => Ha5ab
| Ha5ab, Ha5ab => Ha5ab
end.
Definition Ha5join (a b : Ha5) : Ha5 :=
match a,b with
| Ha5top,_ => Ha5top
| _,Ha5top => Ha5top
| Ha5bot,b => b
| a,Ha5bot => a
| Ha5a, Ha5a => Ha5a
| Ha5a, Ha5b => Ha5top
| Ha5a, Ha5ab => Ha5a
| Ha5b, Ha5a => Ha5top
| Ha5b, Ha5b => Ha5b
| Ha5b, Ha5ab => Ha5b
| Ha5ab, Ha5a => Ha5a
| Ha5ab, Ha5b => Ha5b
| Ha5ab, Ha5ab => Ha5ab
end.
Definition Ha5imp (a b : Ha5) : Ha5 :=
match a,b with
| Ha5bot, _ => Ha5top
| _, Ha5top => Ha5top
| Ha5a, Ha5bot => Ha5bot
| Ha5a, Ha5a => Ha5top
| Ha5a, Ha5b => Ha5b
| Ha5a, Ha5ab => Ha5b
| Ha5b, Ha5bot => Ha5bot
| Ha5b, Ha5a => Ha5a
| Ha5b, Ha5b => Ha5top
| Ha5b, Ha5ab => Ha5a
| Ha5ab, Ha5bot => Ha5bot
| Ha5ab, Ha5a => Ha5top
| Ha5ab, Ha5b => Ha5top
| Ha5ab, Ha5ab => Ha5top
| Ha5top, Ha5bot => Ha5bot
| Ha5top, Ha5a => Ha5a
| Ha5top, Ha5b => Ha5b
| Ha5top, Ha5ab => Ha5ab
end.
Lemma Ha5Rref a : Ha5R a a.
Lemma Ha5Rtra a b c : Ha5R a b -> Ha5R b c -> Ha5R a c.
Definition Ha5HA : HeytingAlgebra.
Defined.
Definition Ha5interp (x : var) : Ha5 :=
match x with
| O => Ha5a
| S _ => Ha5b
end.
Let Ha5eval := @evalH Ha5HA Ha5interp.
Lemma undef_a_And_b u : Ha5eval u <> Ha5ab.
End HeytingHa5.
Section HeytingHb5.
Inductive Hb5 : Type := Hb5bot | Hb5a | Hb5b | Hb5ab | Hb5top.
Definition Hb5R (a b : Hb5) : Prop :=
match a,b with
| Hb5bot,_ => True
| _,Hb5bot => False
| _,Hb5top => True
| Hb5top,_ => False
| Hb5a, Hb5a => True
| Hb5a, Hb5b => False
| Hb5a, Hb5ab => True
| Hb5b, Hb5a => False
| Hb5b, Hb5b => True
| Hb5b, Hb5ab => True
| Hb5ab, Hb5a => False
| Hb5ab, Hb5b => False
| Hb5ab, Hb5ab => True
end.
Definition Hb5meet (a b : Hb5) : Hb5 :=
match a,b with
| Hb5bot,_ => Hb5bot
| _,Hb5bot => Hb5bot
| Hb5top,b => b
| a,Hb5top => a
| Hb5a, Hb5a => Hb5a
| Hb5a, Hb5b => Hb5bot
| Hb5a, Hb5ab => Hb5a
| Hb5b, Hb5a => Hb5bot
| Hb5b, Hb5b => Hb5b
| Hb5b, Hb5ab => Hb5b
| Hb5ab, Hb5a => Hb5a
| Hb5ab, Hb5b => Hb5b
| Hb5ab, Hb5ab => Hb5ab
end.
Definition Hb5imp (a b : Hb5) : Hb5 :=
match a,b with
| Hb5bot, _ => Hb5top
| _, Hb5top => Hb5top
| Hb5a, Hb5bot => Hb5b
| Hb5a, Hb5a => Hb5top
| Hb5a, Hb5b => Hb5b
| Hb5a, Hb5ab => Hb5top
| Hb5b, Hb5bot => Hb5a
| Hb5b, Hb5a => Hb5a
| Hb5b, Hb5b => Hb5top
| Hb5b, Hb5ab => Hb5top
| Hb5ab, Hb5bot => Hb5bot
| Hb5ab, Hb5a => Hb5a
| Hb5ab, Hb5b => Hb5b
| Hb5ab, Hb5ab => Hb5top
| Hb5top, Hb5bot => Hb5bot
| Hb5top, Hb5a => Hb5a
| Hb5top, Hb5b => Hb5b
| Hb5top, Hb5ab => Hb5ab
end.
Definition Hb5join (a b : Hb5) : Hb5 :=
match a,b with
| Hb5bot,b => b
| a,Hb5bot => a
| Hb5top,_ => Hb5top
| _,Hb5top => Hb5top
| _, Hb5ab => Hb5ab
| Hb5ab, _ => Hb5ab
| Hb5a, Hb5a => Hb5a
| Hb5a, Hb5b => Hb5ab
| Hb5b, Hb5a => Hb5ab
| Hb5b, Hb5b => Hb5b
end.
Lemma Hb5Rref a : Hb5R a a.
Lemma Hb5Rtra a b c : Hb5R a b -> Hb5R b c -> Hb5R a c.
Definition Hb5HA : HeytingAlgebra.
Defined.
Definition Hb5interp (x : var) : Hb5 :=
match x with
| O => Hb5a
| S _ => Hb5b
end.
Let Hb5eval := @evalH Hb5HA Hb5interp.
Lemma undef_a_Or_b u : Hb5eval u <> Hb5ab.
End HeytingHb5.
Record KripkeModel : Type :=
mkKripkeModel {
state : Type;
step : state -> state -> Prop;
pred := state -> Prop;
label : nat -> pred;
label_mon : forall a b n, step a b -> label n a -> label n b;
step_refl : forall a, step a a;
step_trans : forall a b c, step a b -> step b c -> step a c
}.
Section KripkeModel.
Variable M:KripkeModel.
Fixpoint evalK (s:form) : pred M :=
match s with
| Var n => label n
| Fal => fun _ => False
| Imp s1 s2 => fun w => forall w', step w w' -> evalK s1 w' -> evalK s2 w'
end.
Lemma monotone (s:form) : forall w w', @step M w w' -> evalK s w -> evalK s w'.
Definition evalK' (A:context) : pred M := fun w => forall s, s el A -> evalK s w.
Lemma monotone_ctx (A:context) : forall w w', @step M w w' -> evalK' A w -> evalK' A w'.
Lemma nd_soundK (A:context) (s:form) (D:nd A s) : forall w, evalK' A w -> evalK s w.
End KripkeModel.
Section KripkeModelToHeytingAlgebra.
Variable M : KripkeModel.
Let Cl : (state M -> Prop) -> Prop := fun p => forall u v : state M, step u v -> p u -> p v.
Let H:Type := {p:state M -> Prop | Cl p}.
Let R: H -> H -> Prop := fun a b => let (p,_) := a in let (q,_) := b in forall u, p u -> q u.
Let bot: H.
Defined.
Let top: H.
Defined.
Let meet: H -> H -> H.
Defined.
Let imp: H -> H -> H.
Defined.
Let join: H -> H -> H.
Defined.
Definition HeytingAlgebraOfKripkeModel : HeytingAlgebra.
Defined.
Definition HeytingInterpOfKripkeModel : var -> H.
Defined.
Theorem evalK_evalH_agree s :
let (X,_) := @evalH HeytingAlgebraOfKripkeModel HeytingInterpOfKripkeModel s in
forall w : state M, evalK s w <-> X w.
End KripkeModelToHeytingAlgebra.
Section HeytingAlgebraToKripkeModel.
Variable A : HeytingAlgebra.
Definition ProperFilter (F:H A -> Prop) : Prop :=
~ (F (bot A))
/\
F (top A)
/\
(forall a b, F a -> F b -> F (meet a b))
/\
(forall a b, F a -> R a b -> F b).
Variable interp : var -> H A.
Definition KripkeModelOfHeytingAlgebra : KripkeModel.
Defined.
Hypothesis xm : forall X:Prop, X \/ ~ X.
Lemma evalH_evalK_agree s :
forall F: H A -> Prop, forall FF: ProperFilter F,
@evalK KripkeModelOfHeytingAlgebra s (exist ProperFilter F FF) <->
F (@evalH A interp s).
End HeytingAlgebraToKripkeModel.
Record HeytingAlgebra : Type :=
mkHeytingAlgebra {
H:Type;
R: H -> H -> Prop;
bot: H;
top: H;
meet: H -> H -> H;
join: H -> H -> H;
imp: H -> H -> H;
Rref : forall w, R w w;
Rtra : forall u v w, R u v -> R v w -> R u w;
bot1 : forall u, R bot u;
top1 : forall u, R u top;
meet1 : forall u v, R (meet u v) u;
meet2 : forall u v, R (meet u v) v;
meet3 : forall u v w, R w u -> R w v -> R w (meet u v);
join1 : forall u v, R u (join u v);
join2 : forall u v, R v (join u v);
join3 : forall u v w, R u w -> R v w -> R (join u v) w;
imp1 : forall u v, R (meet (imp u v) u) v;
imp2 : forall u v w, R (meet w u) v -> R w (imp u v)
}.
Section HeytingAlgebra.
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)
end.
Fixpoint evalH' (A : list form) : H HA :=
match A with
| nil => top HA
| s::A => meet (evalH' A) (evalH s)
end.
Lemma nd_soundH A s : nd A s -> R (evalH' A) (evalH s).
End HeytingAlgebra.
Section HeytingHa5.
Inductive Ha5 : Type := Ha5bot | Ha5ab | Ha5a | Ha5b | Ha5top.
Definition Ha5R (a b : Ha5) : Prop :=
match a,b with
| Ha5bot,_ => True
| _,Ha5bot => False
| _,Ha5top => True
| Ha5top,_ => False
| Ha5a, Ha5a => True
| Ha5a, Ha5b => False
| Ha5a, Ha5ab => False
| Ha5b, Ha5a => False
| Ha5b, Ha5b => True
| Ha5b, Ha5ab => False
| Ha5ab, Ha5a => True
| Ha5ab, Ha5b => True
| Ha5ab, Ha5ab => True
end.
Definition Ha5meet (a b : Ha5) : Ha5 :=
match a,b with
| Ha5bot,_ => Ha5bot
| _,Ha5bot => Ha5bot
| Ha5top,b => b
| a,Ha5top => a
| Ha5a, Ha5a => Ha5a
| Ha5a, Ha5b => Ha5ab
| Ha5a, Ha5ab => Ha5ab
| Ha5b, Ha5a => Ha5ab
| Ha5b, Ha5b => Ha5b
| Ha5b, Ha5ab => Ha5ab
| Ha5ab, Ha5a => Ha5ab
| Ha5ab, Ha5b => Ha5ab
| Ha5ab, Ha5ab => Ha5ab
end.
Definition Ha5join (a b : Ha5) : Ha5 :=
match a,b with
| Ha5top,_ => Ha5top
| _,Ha5top => Ha5top
| Ha5bot,b => b
| a,Ha5bot => a
| Ha5a, Ha5a => Ha5a
| Ha5a, Ha5b => Ha5top
| Ha5a, Ha5ab => Ha5a
| Ha5b, Ha5a => Ha5top
| Ha5b, Ha5b => Ha5b
| Ha5b, Ha5ab => Ha5b
| Ha5ab, Ha5a => Ha5a
| Ha5ab, Ha5b => Ha5b
| Ha5ab, Ha5ab => Ha5ab
end.
Definition Ha5imp (a b : Ha5) : Ha5 :=
match a,b with
| Ha5bot, _ => Ha5top
| _, Ha5top => Ha5top
| Ha5a, Ha5bot => Ha5bot
| Ha5a, Ha5a => Ha5top
| Ha5a, Ha5b => Ha5b
| Ha5a, Ha5ab => Ha5b
| Ha5b, Ha5bot => Ha5bot
| Ha5b, Ha5a => Ha5a
| Ha5b, Ha5b => Ha5top
| Ha5b, Ha5ab => Ha5a
| Ha5ab, Ha5bot => Ha5bot
| Ha5ab, Ha5a => Ha5top
| Ha5ab, Ha5b => Ha5top
| Ha5ab, Ha5ab => Ha5top
| Ha5top, Ha5bot => Ha5bot
| Ha5top, Ha5a => Ha5a
| Ha5top, Ha5b => Ha5b
| Ha5top, Ha5ab => Ha5ab
end.
Lemma Ha5Rref a : Ha5R a a.
Lemma Ha5Rtra a b c : Ha5R a b -> Ha5R b c -> Ha5R a c.
Definition Ha5HA : HeytingAlgebra.
Defined.
Definition Ha5interp (x : var) : Ha5 :=
match x with
| O => Ha5a
| S _ => Ha5b
end.
Let Ha5eval := @evalH Ha5HA Ha5interp.
Lemma undef_a_And_b u : Ha5eval u <> Ha5ab.
End HeytingHa5.
Section HeytingHb5.
Inductive Hb5 : Type := Hb5bot | Hb5a | Hb5b | Hb5ab | Hb5top.
Definition Hb5R (a b : Hb5) : Prop :=
match a,b with
| Hb5bot,_ => True
| _,Hb5bot => False
| _,Hb5top => True
| Hb5top,_ => False
| Hb5a, Hb5a => True
| Hb5a, Hb5b => False
| Hb5a, Hb5ab => True
| Hb5b, Hb5a => False
| Hb5b, Hb5b => True
| Hb5b, Hb5ab => True
| Hb5ab, Hb5a => False
| Hb5ab, Hb5b => False
| Hb5ab, Hb5ab => True
end.
Definition Hb5meet (a b : Hb5) : Hb5 :=
match a,b with
| Hb5bot,_ => Hb5bot
| _,Hb5bot => Hb5bot
| Hb5top,b => b
| a,Hb5top => a
| Hb5a, Hb5a => Hb5a
| Hb5a, Hb5b => Hb5bot
| Hb5a, Hb5ab => Hb5a
| Hb5b, Hb5a => Hb5bot
| Hb5b, Hb5b => Hb5b
| Hb5b, Hb5ab => Hb5b
| Hb5ab, Hb5a => Hb5a
| Hb5ab, Hb5b => Hb5b
| Hb5ab, Hb5ab => Hb5ab
end.
Definition Hb5imp (a b : Hb5) : Hb5 :=
match a,b with
| Hb5bot, _ => Hb5top
| _, Hb5top => Hb5top
| Hb5a, Hb5bot => Hb5b
| Hb5a, Hb5a => Hb5top
| Hb5a, Hb5b => Hb5b
| Hb5a, Hb5ab => Hb5top
| Hb5b, Hb5bot => Hb5a
| Hb5b, Hb5a => Hb5a
| Hb5b, Hb5b => Hb5top
| Hb5b, Hb5ab => Hb5top
| Hb5ab, Hb5bot => Hb5bot
| Hb5ab, Hb5a => Hb5a
| Hb5ab, Hb5b => Hb5b
| Hb5ab, Hb5ab => Hb5top
| Hb5top, Hb5bot => Hb5bot
| Hb5top, Hb5a => Hb5a
| Hb5top, Hb5b => Hb5b
| Hb5top, Hb5ab => Hb5ab
end.
Definition Hb5join (a b : Hb5) : Hb5 :=
match a,b with
| Hb5bot,b => b
| a,Hb5bot => a
| Hb5top,_ => Hb5top
| _,Hb5top => Hb5top
| _, Hb5ab => Hb5ab
| Hb5ab, _ => Hb5ab
| Hb5a, Hb5a => Hb5a
| Hb5a, Hb5b => Hb5ab
| Hb5b, Hb5a => Hb5ab
| Hb5b, Hb5b => Hb5b
end.
Lemma Hb5Rref a : Hb5R a a.
Lemma Hb5Rtra a b c : Hb5R a b -> Hb5R b c -> Hb5R a c.
Definition Hb5HA : HeytingAlgebra.
Defined.
Definition Hb5interp (x : var) : Hb5 :=
match x with
| O => Hb5a
| S _ => Hb5b
end.
Let Hb5eval := @evalH Hb5HA Hb5interp.
Lemma undef_a_Or_b u : Hb5eval u <> Hb5ab.
End HeytingHb5.
Record KripkeModel : Type :=
mkKripkeModel {
state : Type;
step : state -> state -> Prop;
pred := state -> Prop;
label : nat -> pred;
label_mon : forall a b n, step a b -> label n a -> label n b;
step_refl : forall a, step a a;
step_trans : forall a b c, step a b -> step b c -> step a c
}.
Section KripkeModel.
Variable M:KripkeModel.
Fixpoint evalK (s:form) : pred M :=
match s with
| Var n => label n
| Fal => fun _ => False
| Imp s1 s2 => fun w => forall w', step w w' -> evalK s1 w' -> evalK s2 w'
end.
Lemma monotone (s:form) : forall w w', @step M w w' -> evalK s w -> evalK s w'.
Definition evalK' (A:context) : pred M := fun w => forall s, s el A -> evalK s w.
Lemma monotone_ctx (A:context) : forall w w', @step M w w' -> evalK' A w -> evalK' A w'.
Lemma nd_soundK (A:context) (s:form) (D:nd A s) : forall w, evalK' A w -> evalK s w.
End KripkeModel.
Section KripkeModelToHeytingAlgebra.
Variable M : KripkeModel.
Let Cl : (state M -> Prop) -> Prop := fun p => forall u v : state M, step u v -> p u -> p v.
Let H:Type := {p:state M -> Prop | Cl p}.
Let R: H -> H -> Prop := fun a b => let (p,_) := a in let (q,_) := b in forall u, p u -> q u.
Let bot: H.
Defined.
Let top: H.
Defined.
Let meet: H -> H -> H.
Defined.
Let imp: H -> H -> H.
Defined.
Let join: H -> H -> H.
Defined.
Definition HeytingAlgebraOfKripkeModel : HeytingAlgebra.
Defined.
Definition HeytingInterpOfKripkeModel : var -> H.
Defined.
Theorem evalK_evalH_agree s :
let (X,_) := @evalH HeytingAlgebraOfKripkeModel HeytingInterpOfKripkeModel s in
forall w : state M, evalK s w <-> X w.
End KripkeModelToHeytingAlgebra.
Section HeytingAlgebraToKripkeModel.
Variable A : HeytingAlgebra.
Definition ProperFilter (F:H A -> Prop) : Prop :=
~ (F (bot A))
/\
F (top A)
/\
(forall a b, F a -> F b -> F (meet a b))
/\
(forall a b, F a -> R a b -> F b).
Variable interp : var -> H A.
Definition KripkeModelOfHeytingAlgebra : KripkeModel.
Defined.
Hypothesis xm : forall X:Prop, X \/ ~ X.
Lemma evalH_evalK_agree s :
forall F: H A -> Prop, forall FF: ProperFilter F,
@evalK KripkeModelOfHeytingAlgebra s (exist ProperFilter F FF) <->
F (@evalH A interp s).
End HeytingAlgebraToKripkeModel.