Require Import syntax.
Require Import model_structure.
Require Import model_validity_generic.
Require Import model_validity_cbn.

Module Soundness (ks : Kripke_structure).
  Export ks.
  Module ks_monad := Kripke_structure_monad ks.
  Export ks_monad.
  Module cbn_validity := sforces_cbn ks.
  Export cbn_validity.
  Module generic_properties := forcing_generic_properties ks cbn_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.

Module Completeness.

  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 cbn_validity := sforces_cbn U.
  Export cbn_validity.
  Module generic_properties := forcing_generic_properties U cbn_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.

  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_cbn" Completeness.NbE.