normalize.v

(* Definition of the normalization that removes disjunction and implication     by conjunction and equality (from Expr to rExpr) *)

Require Export BoolAux.
Require Export rZ.

(* Here is the full set of boolean operator  (True is (V zero) !!!)*)

Mutual Inductive boolOp: Set :=
     And: boolOp
    | Or: boolOp
    | Impl: boolOp
    | Eq: boolOp .

Mutual Inductive Expr: Set :=
     V: rNat ->Expr
    | N: Expr ->Expr
    | Node: boolOp -> Expr -> Expr ->Expr .

(*The semantics of the boolean operator *)

Definition boolOpFun :=
   [n:boolOp]
      Cases n of
          And => andb
         | Or => orb
         | Impl => implb
         | Eq => eqb
      end.
(* A valuation function *)

Fixpoint Eval[f:rNat ->bool; e:Expr]: bool :=
   Cases e of
       (V n) => (f n)
      | (N p) => (negb (Eval f p))
      | (Node n p q) => ((boolOpFun n) (Eval f p) (Eval f q))
   end.
(* The reduced set *)

Mutual Inductive rBoolOp: Set :=
     rAnd: rBoolOp
    | rEq: rBoolOp .

Definition rBoolOpFun :=
   [n:rBoolOp]
      Cases n of
          rAnd => andb
         | rEq => eqb
      end.

Mutual Inductive rExpr: Set :=
     rV: rNat ->rExpr
    | rN: rExpr ->rExpr
    | rNode: rBoolOp -> rExpr -> rExpr ->rExpr .
(* the valuation function *)

Fixpoint rEval[f:rNat ->bool; x:rExpr]: bool :=
   Cases x of
       (rV n) => (f n)
      | (rN x) => (negb (rEval f x))
      | (rNode n x1 x2) => ((rBoolOpFun n) (rEval f x1) (rEval f x2))
   end.
(*Compute the maximum variable in an expression *)

Fixpoint maxVar[e:rExpr]: rNat :=
   Cases e of
       (rV n) => n
      | (rN p) => (maxVar p)
      | (rNode n p q) => (rmax (maxVar p) (maxVar q))
   end.

Mutual Inductive inRExpr[n:rNat]: rExpr ->Prop :=
     inRV: (inRExpr n (rV n))
    | inRN: (e:rExpr) (inRExpr n e) ->(inRExpr n (rN e))
    | inRNodeLeft:
        (i:rBoolOp) (e1, e2:rExpr) (inRExpr n e1) ->(inRExpr n (rNode i e1 e2))
    | inRNodeRight:
        (i:rBoolOp) (e1, e2:rExpr) (inRExpr n e2) ->(inRExpr n (rNode i e1 e2)) .
Hints Resolve inRV inRN inRNodeLeft inRNodeRight.

Theorem support:
  (f, g:rNat ->bool) (e:rExpr) ((n:rNat) (inRExpr n e) ->(f n)=(g n)) ->
  (rEval f e)=(rEval g e).
Intros f g e.
Elim e; Intros; Simpl; Auto; Rewrite H; Auto; Rewrite H0; Auto.
Qed.
Hints Resolve support.

Definition normNot :=
   [p:rExpr]
      Cases p of
          (rN p1) => p1
         | p1 => (rN p1)
      end.

Lemma normNotEval:
  (p:rExpr) (f:rNat ->bool)(rEval f (normNot p))=(negb (rEval f p)).
Intros; Case p; Simpl; Auto; Intros; Rewrite negb_elim; Auto.
Qed.

Definition normOr :=
   [p, q:rExpr]
      Cases p q of
          (rN p1) (rN q1) => (rN (rNode rAnd p1 q1))
         | (rN p1) q1 => (rN (rNode rAnd p1 (rN q1)))
         | p1 (rN q1) => (rN (rNode rAnd (rN p1) q1))
         | p1 q1 => (rN (rNode rAnd (rN p1) (rN q1)))
      end.

Lemma normOrEval:
  (p, q:rExpr) (f:rNat ->bool)
  (rEval f (normOr p q))=(orb (rEval f p) (rEval f q)).
Intros; Case p; Case q; Intros; Simpl; Auto with bool; Try Rewrite de_morgan2;
Try Rewrite negb_elim; Auto.
Qed.

Definition normImpl :=
   [p, q:rExpr]
      Cases p q of
          (rN p1) (rN q1) => (rN (rNode rAnd (rN p1) q1))
         | (rN p1) q1 => (rN (rNode rAnd (rN p1) (rN q1)))
         | p1 (rN q1) => (rN (rNode rAnd p1 q1))
         | p1 q1 => (rN (rNode rAnd p1 (rN q1)))
      end.

Lemma normImplEval:
  (p, q:rExpr) (f:rNat ->bool)
  (rEval f (normImpl p q))=(implb (rEval f p) (rEval f q)).
Intros; Case p; Case q; Intros; Simpl; Auto; Rewrite implb_elim;
Rewrite negb_elim; Auto.
Qed.

Fixpoint norm[e:Expr]: rExpr :=
   Cases e of
       (V n) => (rV n)
      | (N p) => (normNot (norm p))
      | (Node n1 p q) => Cases n1 of
                             And => (rNode rAnd (norm p) (norm q))
                            | Or => (normOr (norm p) (norm q))
                            | Impl => (normImpl (norm p) (norm q))
                            | Eq => (rNode rEq (norm p) (norm q))
                         end
   end.

Theorem normEval: (f:rNat ->bool) (e:Expr)(Eval f e)=(rEval f (norm e)).
Induction e; Clear e; Simpl; Auto.
Intros p H; Rewrite normNotEval; Rewrite H; Auto.
Intros b p Hp q Hq; Case b; Rewrite Hp; Rewrite Hq; Auto;
Rewrite normOrEval Orelse Rewrite normImplEval; Auto.
Qed.

(* Remember that we code True as (V zero) *)

Definition Tautology :=
   [e:Expr] (f:rNat ->bool) (f zero)=true ->(Eval f e)=true.

Definition rTautology :=
   [e:rExpr] (f:rNat ->bool) (f zero)=true ->(rEval f e)=true.
(* We didn't change the notion of tautology *)

Theorem TautoRTauto: (e:Expr)(iff (Tautology e) (rTautology (norm e))).
Intros e; Unfold Tautology; Unfold rTautology; Split.
Intros H' f; Rewrite <- normEval; Auto.
Intros H' f; Rewrite normEval; Auto.
Qed.

29/06/100, 12:53