Library model_validity_cbv
Require Import model_structure.
Module sforces_cbv (ks : Kripke_structure).
Export ks.
Module ks_monad := (Kripke_structure_monad ks).
Export ks_monad.
sforces is the strong forcing relation for call-by-value models
Fixpoint sforces (w:K)(annot:bool)(A:formula) {struct A} : Type :=
match A with
| Func A1 A2 =>
forall w', w <= w' ->
forall annot', leb annot annot' ->
sforces w' annot' A1 -> Kont sforces w' annot' A2
| Sum A1 A2 => sum (sforces w annot A1) (sforces w annot A2)
| Nat => X w annot Nat
end.
match A with
| Func A1 A2 =>
forall w', w <= w' ->
forall annot', leb annot annot' ->
sforces w' annot' A1 -> Kont sforces w' annot' A2
| Sum A1 A2 => sum (sforces w annot A1) (sforces w annot A2)
| Nat => X w annot Nat
end.
Monotonicity properties of sforces
Lemma sforces_mon : forall A w annot, sforces w annot A ->
forall w', w <= w' -> sforces w' annot A.
Lemma sforces_mon2 : forall A w, sforces w false A -> sforces w true A.
The "run" of the continuations monad
A module type specifying an interpretation of the ground type Nat
Module Type Nat_instance_cbv (ks : Kripke_structure).
Export ks.
Module ks_monad := Kripke_structure_monad ks.
Export ks_monad.
Module cbv_validity := sforces_cbv ks.
Export cbv_validity.
Parameter Zero_interpretation : forall w annot, Kont sforces w annot Nat.
Parameter Succ_interpretation : forall w annot, Kont sforces w annot Nat -> Kont sforces w annot Nat.
Parameter Rec_interpretation : forall A w annot, Kont sforces w annot Nat -> Kont sforces w annot A -> Kont sforces w annot (Func Nat (Func A A)) -> Kont sforces w annot A.
Parameter Reset_interpretation : forall w, Kont sforces w true Nat -> Kont sforces w false Nat.
End Nat_instance_cbv.
Export ks.
Module ks_monad := Kripke_structure_monad ks.
Export ks_monad.
Module cbv_validity := sforces_cbv ks.
Export cbv_validity.
Parameter Zero_interpretation : forall w annot, Kont sforces w annot Nat.
Parameter Succ_interpretation : forall w annot, Kont sforces w annot Nat -> Kont sforces w annot Nat.
Parameter Rec_interpretation : forall A w annot, Kont sforces w annot Nat -> Kont sforces w annot A -> Kont sforces w annot (Func Nat (Func A A)) -> Kont sforces w annot A.
Parameter Reset_interpretation : forall w, Kont sforces w true Nat -> Kont sforces w false Nat.
End Nat_instance_cbv.
This page has been generated by coqdoc