Library nbe_cbv_atomic
Require Import syntax.
Require Import model_structure.
Require Import model_validity_generic.
Require Import model_validity_cbv.
Module Soundness (ks : Kripke_structure).
Export ks.
Module ks_monad := Kripke_structure_monad ks.
Export ks_monad.
Module cbv_validity := sforces_cbv ks.
Export cbv_validity.
Module generic_properties := forcing_generic_properties ks cbv_validity.
Export generic_properties.
Theorem soundness :
forall Gamma annot A, proof Gamma annot A ->
forall w, forall annot', leb annot annot' ->
w ||++ Gamma ; annot' -> w ||- A ; annot'.
End Soundness.
Export ks.
Module ks_monad := Kripke_structure_monad ks.
Export ks_monad.
Module cbv_validity := sforces_cbv ks.
Export cbv_validity.
Module generic_properties := forcing_generic_properties ks cbv_validity.
Export generic_properties.
Theorem soundness :
forall Gamma annot A, proof Gamma annot A ->
forall w, forall annot', leb annot annot' ->
w ||++ Gamma ; annot' -> w ||- A ; annot'.
End Soundness.
The "Universal" Kripke model U build from syntax
Module U <: Kripke_structure.
Definition K := context.
Definition wle := prefix.
Notation "w <= w'" := (wle w w').
Definition wle_refl := prefix_refl.
Definition wle_trans := prefix_trans.
Definition X (w:context)(annot:bool)(A:formula) : Set :=
match A with
| Bot => proof_ne w annot Bot
| Atom a => proof_ne w annot (Atom a)
| Sum A1 A2 => proof_nf w annot (Sum A1 A2)
| Func A1 A2 => proof_nf w annot (Func A1 A2)
end.
Lemma X_mon : forall w annot A, X w annot A ->
forall w', w <= w' -> X w' annot A.
Lemma X_mon2 : forall w annot A, X w annot A ->
forall annot', leb annot annot' -> X w annot' A.
Lemma X_reset : forall w annot, X w true Bot -> X w annot Bot.
End U.
Export U.
Module ks_monad := Kripke_structure_monad U.
Export ks_monad.
Module cbv_validity := sforces_cbv U.
Export cbv_validity.
Module generic_properties := forcing_generic_properties U cbv_validity.
Export generic_properties.
Theorem completeness : forall A w annot,
(Kont sforces w annot A -> proof_nf w annot A) *
(proof_ne w annot A -> Kont sforces w annot A).
Definition K := context.
Definition wle := prefix.
Notation "w <= w'" := (wle w w').
Definition wle_refl := prefix_refl.
Definition wle_trans := prefix_trans.
Definition X (w:context)(annot:bool)(A:formula) : Set :=
match A with
| Bot => proof_ne w annot Bot
| Atom a => proof_ne w annot (Atom a)
| Sum A1 A2 => proof_nf w annot (Sum A1 A2)
| Func A1 A2 => proof_nf w annot (Func A1 A2)
end.
Lemma X_mon : forall w annot A, X w annot A ->
forall w', w <= w' -> X w' annot A.
Lemma X_mon2 : forall w annot A, X w annot A ->
forall annot', leb annot annot' -> X w annot' A.
Lemma X_reset : forall w annot, X w true Bot -> X w annot Bot.
End U.
Export U.
Module ks_monad := Kripke_structure_monad U.
Export ks_monad.
Module cbv_validity := sforces_cbv U.
Export cbv_validity.
Module generic_properties := forcing_generic_properties U cbv_validity.
Export generic_properties.
Theorem completeness : forall A w annot,
(Kont sforces w annot A -> proof_nf w annot A) *
(proof_ne w annot A -> Kont sforces w annot A).
Module soundness_for_U := Soundness U.
Lemma Hnil : forall annot, sforces_cxt nil annot nil.
Definition NbE (annot:bool)(A:formula)(p:proof nil annot A) : proof_nf nil annot A.
set (compl := fst (completeness A nil annot)).
set (sndns := soundness_for_U.soundness p (w:=nil) (leb_refl _) (Hnil annot)).
exact (compl sndns).
End Completeness.
Extraction "nbe_cbv" Completeness.NbE.
Lemma Hnil : forall annot, sforces_cxt nil annot nil.
Definition NbE (annot:bool)(A:formula)(p:proof nil annot A) : proof_nf nil annot A.
set (compl := fst (completeness A nil annot)).
set (sndns := soundness_for_U.soundness p (w:=nil) (leb_refl _) (Hnil annot)).
exact (compl sndns).
End Completeness.
Extraction "nbe_cbv" Completeness.NbE.
This page has been generated by coqdoc