(* File: Normal_Form.v  (last edited on 27/10/2000) (c) Klaus Weich  *)

Require Export Forms.


(*******   Normal forms    ***********************************************)

Inductive normal_form : Set :=
  | NFalsum : normal_form
  | NAtom : Int -> normal_form
  | NDisj : Int -> Int -> normal_form
  | AImp : Int -> normal_form -> normal_form
  | NImp_NF : nimp -> normal_form
with nimp : Set :=
    NImp : Int -> Int -> normal_form -> nimp.




Fixpoint nf2form (x : normal_form) : form :=
  match x with
  | NFalsum => Falsum
  | NAtom i => Atom i
  | NDisj i j => OrF (Atom i) (Atom j)
  | AImp i b => Imp (Atom i) (nf2form b)
  | NImp_NF x => nimp2form x
  end
 
 with nimp2form (x : nimp) : form :=
  match x with
  | NImp i j b => Imp (Imp (Atom i) (Atom j)) (nf2form b)
  end.

Definition nf_list := list normal_form.
Definition nf_nil := nil (A:=normal_form).


Fixpoint nvimp (l : list Int) : normal_form -> normal_form :=
  match l with
  | nil => fun a : normal_form => a
  | i :: l => fun a : normal_form => nvimp l (AImp i a)
  end.


Lemma vimp2nform :
 forall (l : list Int) (a : normal_form),
 {b : normal_form | nf2form b = vimp l (nf2form a)}.
(* Goal: forall (l : list Int) (a : normal_form), @eq form (vimp l (nf2form a)) (nf2form (nvimp l a)) *)
intros l; elim l; clear l.
(* Goal: forall a : normal_form, @sig normal_form (fun b : normal_form => @eq normal_form b (nvimp (@nil Int) a)) *)
(* Goal: forall (a : Int) (l : list Int) (_ : forall a0 : normal_form, @sig normal_form (fun b : normal_form => @eq normal_form b (nvimp l a0))) (a0 : normal_form), @sig normal_form (fun b : normal_form => @eq normal_form b (nvimp (@cons Int a l) a0)) *)
intros a; exists a; trivial.
(* Goal: forall (a : Int) (l : list Int) (_ : forall a0 : normal_form, @eq form (vimp l (nf2form a0)) (nf2form (nvimp l a0))) (a0 : normal_form), @eq form (vimp (@cons Int a l) (nf2form a0)) (nf2form (nvimp (@cons Int a l) a0)) *)
intros i l ih a.
(* Goal: @sig normal_form (fun b : normal_form => @eq normal_form b (nvimp (@cons Int i l) a)) *)
elim (ih (AImp i a)); clear ih.
(* Goal: forall (x : normal_form) (_ : @eq normal_form x (nvimp l (AImp i a))), @sig normal_form (fun b : normal_form => @eq normal_form b (nvimp (@cons Int i l) a)) *)
intros b nf_b.
(* Goal: @sig normal_form (fun b : normal_form => @eq normal_form b (nvimp (@cons Int i l) a)) *)
exists b; assumption.
Qed.


Lemma vimp2nvimp :
 forall (l : list Int) (a : normal_form), {b : normal_form | b = nvimp l a}.
(* Goal: forall (l : list Int) (a : normal_form), @eq form (vimp l (nf2form a)) (nf2form (nvimp l a)) *)
intros l; elim l; clear l.
(* Goal: forall a : normal_form, @sig normal_form (fun b : normal_form => @eq normal_form b (nvimp (@nil Int) a)) *)
(* Goal: forall (a : Int) (l : list Int) (_ : forall a0 : normal_form, @sig normal_form (fun b : normal_form => @eq normal_form b (nvimp l a0))) (a0 : normal_form), @sig normal_form (fun b : normal_form => @eq normal_form b (nvimp (@cons Int a l) a0)) *)
intros a; exists a; trivial.
(* Goal: forall (a : Int) (l : list Int) (_ : forall a0 : normal_form, @eq form (vimp l (nf2form a0)) (nf2form (nvimp l a0))) (a0 : normal_form), @eq form (vimp (@cons Int a l) (nf2form a0)) (nf2form (nvimp (@cons Int a l) a0)) *)
intros i l ih a.
(* Goal: @sig normal_form (fun b : normal_form => @eq normal_form b (nvimp (@cons Int i l) a)) *)
elim (ih (AImp i a)); clear ih.
(* Goal: forall (x : normal_form) (_ : @eq normal_form x (nvimp l (AImp i a))), @sig normal_form (fun b : normal_form => @eq normal_form b (nvimp (@cons Int i l) a)) *)
intros b nf_b.
(* Goal: @sig normal_form (fun b : normal_form => @eq normal_form b (nvimp (@cons Int i l) a)) *)
exists b; assumption.
Qed.


Lemma vimp_eq_nvimp :
 forall (l : list Int) (a : normal_form),
 vimp l (nf2form a) = nf2form (nvimp l a).
(* Goal: forall (l : list Int) (a : normal_form), @eq form (vimp l (nf2form a)) (nf2form (nvimp l a)) *)
intros l; elim l; clear l.
(* Goal: forall a : normal_form, @eq form (vimp (@nil Int) (nf2form a)) (nf2form (nvimp (@nil Int) a)) *)
(* Goal: forall (a : Int) (l : list Int) (_ : forall a0 : normal_form, @eq form (vimp l (nf2form a0)) (nf2form (nvimp l a0))) (a0 : normal_form), @eq form (vimp (@cons Int a l) (nf2form a0)) (nf2form (nvimp (@cons Int a l) a0)) *)
intros a; trivial.
(* Goal: forall (a : Int) (l : list Int) (_ : forall a0 : normal_form, @eq form (vimp l (nf2form a0)) (nf2form (nvimp l a0))) (a0 : normal_form), @eq form (vimp (@cons Int a l) (nf2form a0)) (nf2form (nvimp (@cons Int a l) a0)) *)
intros i l ih a.
(* Goal: @eq form (vimp (@cons Int i l) (nf2form a)) (nf2form (nvimp (@cons Int i l) a)) *)
apply (ih (AImp i a)).
Qed.
