Library nbe_cbv_atomic

Call-by-VALUE TDPE for shift and reset and higher type recursion over natural numbers (System T)


Require Import syntax.
Require Import model_structure.
Require Import model_validity_generic.
Require Import model_validity_cbv.


Evaluator of typed terms in Kripke models (aka Soundness)

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.

The reifyer from Kripke models to terms in normal form (aka Completeness for the Universal model)

Module Completeness.

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.

Now we can define NbE as composition of soundness and completeness

  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.

This page has been generated by coqdoc