(*
   Higher-order syntax for Quantified Propositional Logic
   Venanzio Capretta and Amy Felty       
   March 2006

   see the article
   "Combining de Bruijn Indices and Higher-Order Abstract Syntax in Coq"
*)

Require Import Arith.
Require Import Bool.
Require Import Max.
Require Import deBruijn.

Inductive QPLcon:Set :=
  cNOT: QPLcon | cIMP: QPLcon | cAND: QPLcon
| cOR: QPLcon | cALL: QPLcon | cEX: QPLcon.

Definition oo: Set := expr QPLcon.

Fixpoint formula_check (e:oo): bool :=
match e with
  (VAR v) => true
| (BND b) => true
| (APP (CON cNOT) e) => formula_check e
| (APP (CON cALL) (ABS e)) => formula_check e
| (APP (CON cEX) (ABS e)) => formula_check e
| (APP (APP (CON cIMP) e1) e2) => andb (formula_check e1) (formula_check e2)
| (APP (APP (CON cAND) e1) e2) => andb (formula_check e1) (formula_check e2)
| (APP (APP (CON cOR) e1) e2) => andb (formula_check e1) (formula_check e2)
| _ => false
end.

Definition fcheck: oo -> Prop :=
  fun e => Is_true (formula_check e).

Lemma fcheck_ind:
  forall (P: oo -> Prop),
    (forall v, P (VAR _ v)) ->
    (forall i, P (BND _ i)) ->
    (forall e, P e -> P (APP (CON cNOT) e)) ->
    (forall e, P e -> P (APP (CON cALL) (ABS e))) ->
    (forall e, P e -> P (APP (CON cEX) (ABS e))) ->
    (forall e1 e2, P e1 -> P e2 -> P (APP (APP (CON cIMP) e1) e2)) ->
    (forall e1 e2, P e1 -> P e2 -> P (APP (APP (CON cAND) e1) e2)) ->
    (forall e1 e2, P e1 -> P e2 -> P (APP (APP (CON cOR) e1) e2)) ->
  forall e, fcheck e -> P e.
Proof.
intros P Hvar Hbnd Hnot Hall Hex Himp Hand Hor e'.
apply expr_star_ind with
  (con := QPLcon)
  (P := fun e => fcheck e -> P e).
intro e; case e.
intros q IH h; elim h.
intros v IH h; apply Hvar.
intros i IH h; apply Hbnd.
intros a; case a.
intros q; case q.
intros b IH h; apply Hnot.
 inversion_clear IH.
 apply H1; exact h.
intros b IH h; elim h.
intros b IH h; elim h.
intros b IH h; elim h.

(* ALL *)
intro b; case b.
intros q1 IH h; elim h.
intros v IH h; elim h.
intros i IH h; elim h.
intros b1 b2 IH h; elim h.
intros b1 IH h; apply Hall.
 inversion_clear IH.
 inversion_clear H2.
 apply H3; exact h.

(* EX *)
intro b; case b.
intros q1 IH h; elim h.
intros v IH h; elim h.
intros i IH h; elim h.
intros b1 b2 IH h; elim h.
intros b1 IH h; apply Hex.
 inversion_clear IH.
 inversion_clear H2.
 apply H3; exact h.

intros v b IH h; elim h.
intros i b IH h; elim h.
intro a1; case a1.
intro q; case q.
intros a2 b IH h; elim h.

(* IMP *)
intros a2 b IH h; inversion_clear IH.
 unfold fcheck in h; simpl in h.
 apply Himp. 
 inversion_clear H0.
 apply H5.
 unfold fcheck; eapply Is_true_conj_left; apply h.
 apply H1.
 unfold fcheck; eapply Is_true_conj_right; apply h.


(* AND *)
intros a2 b IH h; inversion_clear IH.
 unfold fcheck in h; simpl in h.
 apply Hand. 
 inversion_clear H0.
 apply H5.
 unfold fcheck; eapply Is_true_conj_left; apply h.
 apply H1.
 unfold fcheck; eapply Is_true_conj_right; apply h.

(* OR *)
intros a2 b IH h; inversion_clear IH.
 unfold fcheck in h; simpl in h.
 apply Hor. 
 inversion_clear H0.
 apply H5.
 unfold fcheck; eapply Is_true_conj_left; apply h.
 apply H1.
 unfold fcheck; eapply Is_true_conj_right; apply h.

intros a2 b IH h; elim h.
intros a2 b IH h; elim h.
intros v a2 b IH h; elim h.
intros i a2 b IH h; elim h.
intros a2 a3 a4 b IH h; elim h.
intros a2 a3 b IH h; elim h.
intros a2 b IH h; elim h.
intros a IH h; elim h.
Qed.

Record formula: Set := mk_formula {
  f_expr: oo;
  f_check: fcheck f_expr
}.

Lemma bshift_aux_check:
  forall e, fcheck e -> forall i, fcheck (bshift_aux e i).
Proof.
intros e' h';
apply fcheck_ind with (P := fun e => forall i, fcheck (bshift_aux e i)).
(* Var *)
intros v i; red; simpl. exact I.
(* Bind *)
intros j i; red; simpl.
case (le_lt_dec i j); intro; exact I.
(* Not *)
intros e IH i; red; simpl; apply IH.
(* All *)
intros e IH i; red; simpl; apply IH.
(* Ex *)
intros e IH i; red; simpl; apply IH.
(* Imp *)
intros e1 e2 IH1 IH2 i; red; simpl.
apply Is_true_conj; [apply IH1 | apply IH2].
(* And *)
intros e1 e2 IH1 IH2 i; red; simpl.
apply Is_true_conj; [apply IH1 | apply IH2].
(* Or *)
intros e1 e2 IH1 IH2 i; red; simpl.
apply Is_true_conj; [apply IH1 | apply IH2].

exact h'.
Qed.

Lemma bshift_check: forall e, fcheck e -> fcheck (bshift e).
Proof.
intros e h; unfold bshift; apply bshift_aux_check; exact h.
Qed.

Lemma bsubst_check:
  forall e1 j e2, fcheck e1 -> fcheck e2 ->
                  fcheck (bsubst e1 j e2).
Proof.
intros e1 j e2 h1; generalize e2; generalize j; clear e2; clear j.
apply fcheck_ind with
  (P := fun e1 => forall j e2, fcheck e2 -> fcheck (bsubst e1 j e2)).
(* VAR *)
intros v j e2 h2; exact I.
(* BND *)
intros i j e2 h2; simpl.
case (bnd_dec i j).
intros _; exact h2.
intros _; exact I.
(* NOT *)
intros e IH j e2 h2; simpl.
unfold fcheck; simpl.
change (fcheck (bsubst e j e2)).
apply IH.
exact h2.
(* ALL *)
intros e IH j e2 h2.
change (fcheck (bsubst e (S j) (bshift e2))).
apply IH.
apply bshift_check; exact h2.
(* EX *)
intros e IH j e2 h2.
change (fcheck (bsubst e (S j) (bshift e2))).
apply IH.
apply bshift_check; exact h2.
(* IMP *)
intros a b IHa IHb j e2 h2.
unfold fcheck; simpl.
apply Is_true_conj.
apply IHa; exact h2.
apply IHb; exact h2.
(* AND *)
intros a b IHa IHb j e2 h2.
unfold fcheck; simpl.
apply Is_true_conj.
apply IHa; exact h2.
apply IHb; exact h2.
(* OR *)
intros a b IHa IHb j e2 h2.
unfold fcheck; simpl.
apply Is_true_conj.
apply IHa; exact h2.
apply IHb; exact h2.

exact h1.
Qed.

Lemma ebind_check:
  forall e, fcheck e -> forall w j, fcheck (ebind w j e).
Proof.
intros e' h'.
apply fcheck_ind with
  (P := fun e => forall w j, fcheck (ebind w j e)).
(* VAR *)
intros v w j; simpl.
case (var_dec v w).
intros _; exact I.
intros _; exact I.
(* BND *)
intros i w j; simpl.
case (bnd_dec i j).
intros _; exact I.
intros _; exact I.
(* NOT *)
unfold fcheck; intros e IH w j; simpl.
apply IH.
(* ALL *)
unfold fcheck; intros e IH w j; simpl.
apply IH.
(* EX *)
unfold fcheck; intros e IH w j; simpl.
apply IH.
(* IMP *)
unfold fcheck; intros e1 e2 IH1 IH2 w j; simpl.
apply Is_true_conj; [apply IH1 | apply IH2].
(* AND *)
unfold fcheck; intros e1 e2 IH1 IH2 w j; simpl.
apply Is_true_conj; [apply IH1 | apply IH2].
(* OR *)
unfold fcheck; intros e1 e2 IH1 IH2 w j; simpl.
apply Is_true_conj; [apply IH1 | apply IH2].

exact h'.
Qed.

Lemma formula_check_unicity:
  forall (e:oo)(c1 c2: fcheck e), c1=c2.
Proof.
intro e; unfold fcheck.
case (formula_check e); simpl.
intros [] []; trivial.
intro c1; case c1.
Qed.

Lemma mk_formula_unicity:
  forall (e1 e2:oo), e1=e2 ->
    forall (c1:fcheck e1)(c2:fcheck e2),
      mk_formula e1 c1 = mk_formula e2 c2.
Proof.
intros e1 e2 Heq; rewrite Heq.
intros c1 c2; rewrite (formula_check_unicity e2 c1 c2).
trivial.
Qed.

Lemma formula_unicity:
  forall a1 a2, (f_expr a1)=(f_expr a2) -> a1=a2.
Proof.
intros [e1 c1] [e2 c2] Heq; simpl in Heq.
apply mk_formula_unicity.
exact Heq.
Qed.

Definition Var (v:var): formula := mk_formula (VAR _ v) I.

Definition Bind (i:bnd): formula := mk_formula (BND _ i) I.

Definition Not (a:formula): formula :=
  mk_formula (APP (CON cNOT) (f_expr a)) (f_check a).

Definition fImp (a1 a2:formula): formula :=
  mk_formula (APP (APP (CON cIMP) (f_expr a1)) (f_expr a2))
             (Is_true_conj (f_check a1) (f_check a2)).
Notation "A 'Imp' B" := (fImp A B) (at level 23, right associativity).

Definition fAnd (a1 a2:formula): formula :=
  mk_formula (APP (APP (CON cAND) (f_expr a1)) (f_expr a2))
             (Is_true_conj (f_check a1) (f_check a2)).
Notation "A 'And' B" := (fAnd A B) (at level 21, left associativity).

Definition fOr (a1 a2:formula): formula :=
  mk_formula (APP (APP (CON cOR) (f_expr a1)) (f_expr a2))
             (Is_true_conj (f_check a1) (f_check a2)).
Notation "A 'Or' B" := (fOr A B) (at level 22, left associativity).

Section Quantifiers.

Variable f: formula -> formula.

Definition nvar := newvar (f_expr (f (Bind 0))).
Definition fvar := f (Var nvar).
Definition fbind := ebind nvar 0 (f_expr fvar).

Lemma fbind_check: fcheck fbind.
Proof.
unfold fbind.
apply ebind_check.
exact (f_check (f (Var nvar))).
Qed.

(* The "function body": f applied to (Bind 0). *)
Definition fbody: formula :=
  mk_formula fbind fbind_check.

Definition fAll: formula :=
  mk_formula (APP (CON cALL) (ABS fbind)) fbind_check.

Definition fEx: formula :=
  mk_formula (APP (CON cEX) (ABS fbind)) fbind_check.

End Quantifiers.

Notation "'forAll' V , A" := (fAll (fun V => A)) (at level 20).
Notation "'thereEx' V , A" := (fEx (fun V => A)) (at level 20).

Lemma fbind_extensional:
  forall f1 f2: formula->formula,
    (forall x, f1 x = f2 x) -> fbind f1 = fbind f2.
Proof.
intros f1 f2 H.
unfold fbind; simpl.
unfold fvar; simpl.
unfold nvar; simpl.
rewrite H.
rewrite H.
trivial.
Qed.

(* The inverse operation: given a quantified expression, build the function. *)
Section Quantified_Expression.

Variables (e:oo)(h:fcheck e).
Variable x:formula.

Let xe := f_expr x.
Let xh := f_check x.
Let esx := bsubst e 0 xe.

Lemma esx_check: fcheck esx.
Proof.
unfold esx.
apply bsubst_check; [exact h | exact xh].
Qed.

Definition ffun := mk_formula esx esx_check.

End Quantified_Expression.

Definition fapp (a:formula): formula -> formula :=
  ffun (f_expr a) (f_check a).

Lemma fbody_fapp: forall a, fbody (fapp a) = a.
Proof.
intros [e h]; apply formula_unicity; unfold fbody; unfold fapp; simpl.
unfold ffun; unfold fbind; simpl.
unfold nvar; simpl.
rewrite bsubst_bnd.
rewrite ebind_bsubst_eq.
trivial.
Qed.

(* "Canonical form" of a function on formulas. *)
Definition funf: (formula -> formula) -> (formula -> formula) :=
fun f => fapp (fbody f).

Section Formula_Recursion_Principle.

(* Theorem 4 of article. *)

(* Recursion principle on formulas. *)
(* Non-dependent recursion. *)

Variables
  (B: Set)
  (Hvar: var -> B)
  (Hbind: bnd -> B)
  (Hnot: formula -> B -> B)
  (Himp: formula -> formula -> B -> B -> B)
  (Hand: formula -> formula -> B -> B -> B)
  (Hor: formula -> formula -> B -> B -> B)
  (Hall: (formula -> formula) -> B -> B)
  (Hex: (formula -> formula) -> B -> B).
(*
In the case of Hall and Hex we have a single recursive argument
of type B, instead of a function of type formula->B.
This is because we are not really doing higher order recursion.
The single argument is the result of the recursive call
on the "body" of the function.
*)

Fixpoint oo_form_rec (e:oo): fcheck e -> B :=
match e return fcheck e -> B with
| (VAR v) => fun h => Hvar v
| (BND i) => fun h => Hbind i
| (APP (CON cNOT) e1) =>
    fun h => Hnot (mk_formula e1 h) (oo_form_rec e1 h)
| (APP (APP (CON cIMP) e1) e2) => 
    fun h => Himp (mk_formula e1 (Is_true_conj_left  h))
                  (mk_formula e2 (Is_true_conj_right h))
                  (oo_form_rec e1 (Is_true_conj_left h))
                  (oo_form_rec e2 (Is_true_conj_right h))
| (APP (APP (CON cAND) e1) e2) => 
    fun h => Hand (mk_formula e1 (Is_true_conj_left  h))
                  (mk_formula e2 (Is_true_conj_right h))
                  (oo_form_rec e1 (Is_true_conj_left h))
                  (oo_form_rec e2 (Is_true_conj_right h))
| (APP (APP (CON cOR) e1) e2) => 
    fun h => Hor  (mk_formula e1 (Is_true_conj_left  h))
                  (mk_formula e2 (Is_true_conj_right h))
                  (oo_form_rec e1 (Is_true_conj_left h))
                  (oo_form_rec e2 (Is_true_conj_right h))
| (APP (CON cALL) (ABS e')) =>
    fun h => Hall (ffun e' h)
                  (oo_form_rec e' h)
| (APP (CON cEX) (ABS e')) =>
    fun h => Hex  (ffun e' h)
                  (oo_form_rec e' h)
| _ => fun h => Hvar 0 (* this never happens *)
end.

(* Recursive function. *)
Definition form_rec (a:formula): B:=
  oo_form_rec (f_expr a) (f_check a).

(* Proof of the recursive equations. *)

Lemma form_rec_Var:
  forall v, form_rec (Var v) = Hvar v.
Proof.
auto.
Qed.

Lemma form_rec_Bind:
  forall b, form_rec (Bind b) = Hbind b.
Proof.
auto.
Qed.

Lemma form_rec_Not:
  forall a, form_rec (Not a) = Hnot a (form_rec a).
Proof.
intros [e h]; auto.
Qed.

Lemma form_rec_Imp:
  forall a1 a2, form_rec (a1 Imp a2) = Himp a1 a2 (form_rec a1) (form_rec a2).
Proof.
intros [e1 h1] [e2 h2].
set (h:= (f_check (mk_formula e1 h1 Imp mk_formula e2 h2))).
change (Himp (mk_formula e1 (Is_true_conj_left  h))
                          (mk_formula e2 (Is_true_conj_right h))
                          (form_rec (mk_formula e1 (Is_true_conj_left h)))
                          (form_rec (mk_formula e2 (Is_true_conj_right h)))
               = Himp (mk_formula e1 h1)
                            (mk_formula e2 h2)
                            (form_rec (mk_formula e1 h1))
                            (form_rec (mk_formula e2 h2))).
rewrite formula_unicity with
  (a1 := mk_formula e1 (Is_true_conj_left  h))
  (a2 := mk_formula e1 h1).

rewrite formula_unicity with
  (a1 := mk_formula e2 (Is_true_conj_right  h))
  (a2 := mk_formula e2 h2).

auto.
auto.
auto.
Qed.

Lemma form_rec_And:
  forall a1 a2, form_rec (a1 And a2) = Hand a1 a2 (form_rec a1) (form_rec a2).
Proof.
intros [e1 h1] [e2 h2].
set (h:= (f_check (mk_formula e1 h1 Imp mk_formula e2 h2))).
change (Hand (mk_formula e1 (Is_true_conj_left  h))
                            (mk_formula e2 (Is_true_conj_right h))
                            (form_rec (mk_formula e1 (Is_true_conj_left h)))
                            (form_rec (mk_formula e2 (Is_true_conj_right h)))
             = Hand (mk_formula e1 h1)
                    (mk_formula e2 h2)
                    (form_rec (mk_formula e1 h1))
                    (form_rec (mk_formula e2 h2))).
rewrite formula_unicity with
  (a1 := mk_formula e1 (Is_true_conj_left  h))
  (a2 := mk_formula e1 h1).

rewrite formula_unicity with
  (a1 := mk_formula e2 (Is_true_conj_right  h))
  (a2 := mk_formula e2 h2).

auto.
auto.
auto.
Qed.

Lemma form_rec_Or:
  forall a1 a2, form_rec (a1 Or a2) = Hor a1 a2 (form_rec a1) (form_rec a2).
Proof.
intros [e1 h1] [e2 h2].
set (h:= (f_check (mk_formula e1 h1 Imp mk_formula e2 h2))).
change (Hor (mk_formula e1 (Is_true_conj_left  h))
                           (mk_formula e2 (Is_true_conj_right h))
                           (form_rec (mk_formula e1 (Is_true_conj_left h)))
                           (form_rec (mk_formula e2 (Is_true_conj_right h)))
            = Hor (mk_formula e1 h1)
                  (mk_formula e2 h2)
                  (form_rec (mk_formula e1 h1))
                  (form_rec (mk_formula e2 h2))).
rewrite formula_unicity with
  (a1 := mk_formula e1 (Is_true_conj_left  h))
  (a2 := mk_formula e1 h1).

rewrite formula_unicity with
  (a1 := mk_formula e2 (Is_true_conj_right  h))
  (a2 := mk_formula e2 h2).

auto.
auto.
auto.
Qed.

Lemma form_rec_All:
  forall f: formula -> formula,
    form_rec (forAll x, f x) = 
    Hall (funf (fun x => f x)) (form_rec (fbody (fun x => f x))).
Proof.
auto.
Qed.

Lemma form_rec_Ex:
  forall f: formula -> formula,
    form_rec (thereEx x, f x) = 
    Hex (funf (fun x => f x)) (form_rec (fbody (fun x => f x))).
Proof.
auto.
Qed.

End Formula_Recursion_Principle.

Section Formula_Induction_Principle.

(* Theorem 5 of article. *)
(* Induction principle on formulas. *)

Variables
  (P: formula -> Prop)
  (Hvar: forall (v:var), P (Var v))
  (Hbind: forall (i:bnd), P (Bind i))
  (Hnot: forall (a:formula), P a -> P (Not a))
  (Himp: forall (a1 a2:formula), P a1 -> P a2 -> P (a1 Imp a2))
  (Hand: forall (a1 a2:formula), P a1 -> P a2 -> P (a1 And a2))
  (Hor: forall (a1 a2:formula), P a1 -> P a2 -> P (a1 Or a2))
  (Hall: forall (f:formula -> formula), P (fbody (fun x => f x)) ->
                                        P (forAll x, f x))
  (Hex: forall (f:formula -> formula), P (fbody (fun x => f x)) ->
                                       P (thereEx x, f x)).


Theorem form_ind: forall a, P a.
Proof.
intros [e' h']; generalize h';
apply fcheck_ind with (P := fun e => forall h:fcheck e, P (mk_formula e h)).
(* Var *)
intros v h; rewrite formula_unicity with (a2 := Var v);
  [apply Hvar | trivial].
(* Bind *)
intros i h; rewrite formula_unicity with (a2 := Bind i);
  [apply Hbind | trivial].
(* Not *)
intros e IH h; rewrite formula_unicity with (a2 := Not (mk_formula e h)).
apply Hnot; apply IH.
trivial.
(* All *)
intros e IH h; rewrite formula_unicity with (a2 := forAll x, ffun e h x).
apply Hall.
rewrite formula_unicity with (a2 := mk_formula e h).
apply IH.
simpl.
unfold fbind; unfold nvar; unfold ffun; simpl.
unfold nvar; unfold ffun; simpl.
rewrite bsubst_bnd.
exact (ebind_bsubst_eq e 0).
simpl.
unfold fbind; unfold nvar; unfold ffun; simpl.
unfold nvar; unfold ffun; simpl.
rewrite bsubst_bnd.
rewrite ebind_bsubst_eq.
trivial.
(* Ex *)
intros e IH h; rewrite formula_unicity with (a2 := thereEx x, ffun e h x).
apply Hex.
rewrite formula_unicity with (a2 := mk_formula e h).
apply IH.
simpl.
unfold fbind; unfold nvar; unfold ffun; simpl.
unfold nvar; unfold ffun; simpl.
rewrite bsubst_bnd.
exact (ebind_bsubst_eq e 0).
simpl.
unfold fbind; unfold nvar; unfold ffun; simpl.
unfold nvar; unfold ffun; simpl.
rewrite bsubst_bnd.
rewrite ebind_bsubst_eq.
trivial.
(* Imp *)
intros e1 e2 IH1 IH2 h.
unfold fcheck in h; simpl in h.
rewrite formula_unicity with
  (a2 := (mk_formula e1 (Is_true_conj_left h)) Imp
         (mk_formula e2 (Is_true_conj_right h)) ).
apply Himp.
apply IH1.
apply IH2.
trivial.
(* And *)
intros e1 e2 IH1 IH2 h.
unfold fcheck in h; simpl in h.
rewrite formula_unicity with
  (a2 := (mk_formula e1 (Is_true_conj_left h)) And
         (mk_formula e2 (Is_true_conj_right h)) ).
apply Hand.
apply IH1.
apply IH2.
trivial.
(* Or *)
intros e1 e2 IH1 IH2 h.
unfold fcheck in h; simpl in h.
rewrite formula_unicity with
  (a2 := (mk_formula e1 (Is_true_conj_left h)) Or
         (mk_formula e2 (Is_true_conj_right h)) ).
apply Hor.
apply IH1.
apply IH2.
trivial.

exact h'.
Qed.

End Formula_Induction_Principle.

(* Definition of negation normal form *)

Inductive isNnf: formula -> Prop :=
  isNnf_Var: forall i, isNnf (Var i)
| isNnf_Bind: forall i, isNnf (Bind i)
| isNnf_nVar: forall i, isNnf (Not (Var i))
| isNnf_nBind: forall i, isNnf (Not (Bind i))
| isNnf_And: forall a1 a2, isNnf a1 -> isNnf a2 -> isNnf (a1 And a2)
| isNnf_Or: forall a1 a2, isNnf a1 -> isNnf a2 -> isNnf (a1 Or a2)
| isNnf_All: forall f:formula -> formula, isNnf (fbody f)
               -> isNnf (forAll x, f x)
| isNnf_Ex: forall f: formula -> formula, isNnf (fbody f)
               -> isNnf (thereEx x, f x).

(* nnf_aux a = (nnf a, nnf (fNot a). *)
Definition nnf_aux: formula -> formula*formula :=
form_rec (formula*formula)%type
(* matching the argument with: *)
(* (Var i)   *) (fun i => (Var i, Not (Var i)))
(* (Bind i)  *) (fun i => (Bind i, Not (Bind i)))
(* (Not a)   *) (fun a na => (snd na, fst na))
(* (a Imp b) *) (fun a b na nb => ((snd na) Or  (fst nb),
                                   (fst na) And (snd nb)))
(* (a And b) *) (fun a b na nb => ((fst na) And (fst nb),
                                   (snd na) Or  (snd nb)))
(* (a Or b)  *)  (fun a b na nb => ((fst na) Or (fst nb),
                                    (snd na) And (snd nb)))
(* (forAll x, f x)  *)  (fun f nb => (forAll x,  fapp (fst nb) x,
                                      thereEx x, fapp (snd nb) x))
(* (thereEx x, f x) *)  (fun f nb => (thereEx x, fapp (fst nb) x,
                                      forAll x,  fapp (snd nb) x)).

Definition nnf: formula -> formula :=
  fun a => fst (nnf_aux a).

Lemma nnf_aux_correct:
  forall a:formula, isNnf (fst (nnf_aux a)) /\ isNnf (snd (nnf_aux a)).
Proof.
apply form_ind with
  (P := fun a => isNnf (fst (nnf_aux a)) /\ isNnf (snd (nnf_aux a))).
(* Var *)
intro v; simpl; split.
apply isNnf_Var.
apply isNnf_nVar.
(* Bind *)
intro i; simpl; split.
apply isNnf_Bind.
apply isNnf_nBind.
(* Not *)
intros a [IH1 IH2].
unfold nnf_aux; rewrite form_rec_Not; fold nnf_aux; simpl; split.
exact IH2.
exact IH1.
(* Imp *)
intros a1 a2 [IH11 IH12] [IH21 IH22].
unfold nnf_aux; rewrite form_rec_Imp; fold nnf_aux; simpl; split.
apply isNnf_Or.
exact IH12.
exact IH21.
apply isNnf_And.
exact IH11.
exact IH22.
(* And *)
intros a1 a2 [IH11 IH12] [IH21 IH22].
unfold nnf_aux; rewrite form_rec_And; fold nnf_aux; simpl; split.
apply isNnf_And.
exact IH11.
exact IH21.
apply isNnf_Or.
exact IH12.
exact IH22.
(* Or *)
intros a1 a2 [IH11 IH12] [IH21 IH22].
unfold nnf_aux; rewrite form_rec_Or; fold nnf_aux; simpl; split.
apply isNnf_Or.
exact IH11.
exact IH21.
apply isNnf_And.
exact IH12.
exact IH22.
(* All *)
intros f [IH1 IH2].
unfold nnf_aux; rewrite form_rec_All; fold nnf_aux; simpl; split.
apply isNnf_All; simpl.
rewrite fbody_fapp.
exact IH1.
apply isNnf_Ex; simpl.
rewrite fbody_fapp.
exact IH2.
(* Ex *)
intros f [IH1 IH2].
unfold nnf_aux; rewrite form_rec_Ex; fold nnf_aux; simpl; split.
apply isNnf_Ex; simpl.
rewrite fbody_fapp.
exact IH1.
apply isNnf_All; simpl.
rewrite fbody_fapp.
exact IH2.
Qed.

Theorem nnf_correct: forall a, isNnf (nnf a).
Proof.
intro a; case (nnf_aux_correct a).
intros H1 H2; exact H1.
Qed.