Library model_validity_generic
Require Import model_structure.
Module forcing_generic_properties (ks : Kripke_structure)(sforces_implementation : sforces_instance ks).
Export ks.
Module ks_monad := Kripke_structure_monad ks.
Export ks_monad.
Export sforces_implementation.
Notation " w ||- A ; annot " := (Kont sforces w annot A) (at level 70).
monadic unit and bind (no monad laws à la functional programming
are checked, since this is not necessary for our purposes, that
are just to use them to structure proofs)
Definition ret {w annot A} : sforces w annot A -> Kont sforces w annot A.
Definition bind {w annot A B} :
(forall w', w <= w' -> sforces w' annot A -> Kont sforces w' annot B) ->
Kont sforces w annot A -> Kont sforces w annot B.
Definition bind {w annot A B} :
(forall w', w <= w' -> sforces w' annot A -> Kont sforces w' annot B) ->
Kont sforces w annot A -> Kont sforces w annot B.
The sforce and Kont defined on *lists* of formulas
Fixpoint sforces_cxt (w:K)(annot:bool)(Gamma:context) : Type :=
match Gamma with
| nil => unit
| cons aA Gamma' =>
prod (sforces w annot aA) (sforces_cxt w annot Gamma')
end.
Notation " w ||++ Gamma ; annot " := (sforces_cxt w annot Gamma) (at level 70).
Lemma sforces_cxt_mon : forall Gamma w annot, w ||++ Gamma ; annot ->
forall w', w <= w' -> w' ||++ Gamma ; annot.
Lemma sforces_cxt_mon2 : forall Gamma w annot, w ||++ Gamma ; annot ->
forall annot', leb annot annot' -> w ||++ Gamma ; annot'.
Fixpoint Kont_cxt (w:K)(annot:bool)(Gamma:context) : Type :=
match Gamma with
| nil => unit
| cons aA Gamma' =>
prod (Kont sforces w annot aA) (Kont_cxt w annot Gamma')
end.
Notation " w ||-- Gamma ; annot " := (Kont_cxt w annot Gamma) (at level 70).
Lemma Kont_cxt_mon : forall Gamma w annot, w ||-- Gamma ; annot ->
forall w', w <= w' -> w' ||-- Gamma ; annot.
Lemma Kont_sforces_cxt_mon2 : forall Gamma w annot, w ||-- Gamma ; annot ->
forall annot', leb annot annot' -> w ||-- Gamma ; annot'.
End forcing_generic_properties.
This page has been generated by coqdoc