Normalize.v

Require Export Arith.
Require Export Logique.
Require Export rZ.

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

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

Definition boolOpFun :=
   [n:boolOp]
      Cases n of
          And => andb
         | Or => orb
         | Impl => implb
         | Eq => eqb
      end.

Fixpoint Eval[f:rNat ->bool; e:Expr]: bool :=
   Cases e of
       T => true
      | F => false
      | (V n) => (f n)
      | (N p) => (negb (Eval f p))
      | (Node n p q) => ((boolOpFun n) (Eval f p) (Eval f q))
   end.

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

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

Mutual Inductive rExpr: Set :=
     rT: rExpr
    | rF: rExpr
    | rV: rNat ->rExpr
    | rN: rExpr ->rExpr
    | rNode: rBoolOp -> rExpr -> rExpr ->rExpr .

Fixpoint rEval[f:rNat ->bool; x:rExpr]: bool :=
   Cases x of
       rT => true
      | rF => false
      | (rV n) => (f n)
      | (rN x) => (negb (rEval f x))
      | (rNode n x1 x2) => ((rBoolOpFun n) (rEval f x1) (rEval f x2))
   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
          rT => rF
         | rF => rT
         | (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 normAnd :=
   [p, q:rExpr]
      Cases p q of
          rT q1 => q1
         | p1 rT => p1
         | rF _ => rF
         | _ rF => rF
         | p1 q1 => (rNode rAnd p1 q1)
      end.

Lemma normAndEval:
  (p, q:rExpr) (f:rNat ->bool)
  (rEval f (normAnd p q))=(andb (rEval f p) (rEval f q)).
Intros; Case p; Case q; Intros; Simpl; Auto;
Rewrite andb_b_true Orelse Rewrite andb_b_false; Auto.
Qed.

Definition normOr :=
   [p, q:rExpr]
      Cases p q of
          rT _ => rT
         | _ rT => rT
         | rF q1 => q1
         | p1 rF => p1
         | (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
          rT q1 => q1
         | _ rT => rT
         | rF _ => rT
         | p1 rF => (rN p1)
         | (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.

Definition normEq :=
   [p, q:rExpr]
      Cases p q of
          rT q1 => q1
         | p1 rT => p1
         | rF q1 => (rN q1)
         | p1 rF => (rN p1)
         | p1 q1 => (rNode rEq p1 q1)
      end.

Lemma normEqEval:
  (p, q:rExpr) (f:rNat ->bool)
  (rEval f (normEq p q))=(eqb (rEval f p) (rEval f q)).
Intros; Case p; Case q; Unfold normEq; Auto.
Qed.

Fixpoint norm[e:Expr]: rExpr :=
   Cases e of
       T => rT
      | F => rF
      | (V n) => (rV n)
      | (N p) => (normNot (norm p))
      | (Node n1 p q) => Cases n1 of
                             And => (normAnd (norm p) (norm q))
                            | Or => (normOr (norm p) (norm q))
                            | Impl => (normImpl (norm p) (norm q))
                            | Eq => (normEq (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 n p Hp q Hq; Case n.
Rewrite normAndEval; Rewrite Hp; Rewrite Hq; Auto.
Rewrite normOrEval; Rewrite Hp; Rewrite Hq; Auto.
Rewrite normImplEval; Rewrite Hp; Rewrite Hq; Auto.
Rewrite normEqEval; Rewrite Hp; Rewrite Hq; Auto.
Qed.

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

Definition rTautology := [e:rExpr] (f:rNat ->bool)(rEval f e)=true.

Theorem Tauto_rTauto: (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.

26/01/99, 11:04