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)(ni : Nat_instance_cbv ks).
Export ks.
Module ks_monad := Kripke_structure_monad ks.
Export ks_monad.
Export ni.
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.
Export ni.
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 :=
proof_nf w annot A.
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.
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 NI <: Nat_instance_cbv U.
Module ks_monad := Kripke_structure_monad U.
Export ks_monad.
Module cbv_validity := sforces_cbv U.
Export cbv_validity.
Lemma Zero_interpretation : forall w annot, Kont sforces w annot Nat.
Lemma Succ_interpretation : forall w annot, Kont sforces w annot Nat -> Kont sforces w annot Nat.
Fixpoint reset_nf (Gamma:context)(r:proof_nf Gamma true Nat) {struct r} : proof_nf Gamma false Nat.
Lemma Reset_interpretation : forall w, Kont sforces w true Nat -> Kont sforces w false Nat.
Lemma 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.
End NI.
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 :=
proof_nf w annot A.
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.
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 NI <: Nat_instance_cbv U.
Module ks_monad := Kripke_structure_monad U.
Export ks_monad.
Module cbv_validity := sforces_cbv U.
Export cbv_validity.
Lemma Zero_interpretation : forall w annot, Kont sforces w annot Nat.
Lemma Succ_interpretation : forall w annot, Kont sforces w annot Nat -> Kont sforces w annot Nat.
Fixpoint reset_nf (Gamma:context)(r:proof_nf Gamma true Nat) {struct r} : proof_nf Gamma false Nat.
Lemma Reset_interpretation : forall w, Kont sforces w true Nat -> Kont sforces w false Nat.
Lemma 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.
End NI.
Module soundness_for_U := Soundness U NI.
Check soundness_for_U.soundness.
Definition NbE (annot:bool)(A:formula)(p:proof nil annot A) : proof_nf nil annot A.
set (compl := fst (completeness A nil annot)).
set (empty_cxt := nil).
assert (Hnil : sforces_cxt empty_cxt annot empty_cxt).
simpl.
constructor.
set (sndns := soundness_for_U.soundness p (w:=nil) (leb_refl _) Hnil).
exact (compl sndns).
End Completeness.
Extraction "nbe_cbv" Completeness.NbE.
Check soundness_for_U.soundness.
Definition NbE (annot:bool)(A:formula)(p:proof nil annot A) : proof_nf nil annot A.
set (compl := fst (completeness A nil annot)).
set (empty_cxt := nil).
assert (Hnil : sforces_cxt empty_cxt annot empty_cxt).
simpl.
constructor.
set (sndns := soundness_for_U.soundness p (w:=nil) (leb_refl _) Hnil).
exact (compl sndns).
End Completeness.
Extraction "nbe_cbv" Completeness.NbE.
This page has been generated by coqdoc