Require Export BoolAux.
Require Export rZ.

Inductive boolOp : Set :=
  | ANd : boolOp
  | Or : boolOp
  | Impl : boolOp
  | Eq : boolOp.

Inductive Expr : Set :=
  | V : rNat → Expr
  | N : Expr → Expr
  | Node : boolOp → Expr → Expr → Expr.


Definition boolOpFun (n : boolOp) :=
  match n with
  | ANd ⇒ andb
  | Or ⇒ orb
  | Impl ⇒ implb
  | normalize.Eq ⇒ eqb
  end.

Fixpoint Eval (f : rNat → bool) (e : Expr) {struct e} : bool :=
  match e with
  | V n ⇒ f n
  | normalize.N p ⇒ negb (Eval f p)
  | Node n p q ⇒ boolOpFun n (Eval f p) (Eval f q)
  end.

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

Definition rBoolOpFun (n : rBoolOp) :=
  match n with
  | rAnd ⇒ andb
  | rEq ⇒ eqb
  end.

Inductive rExpr : Set :=
  | rV : rNat → rExpr
  | rN : rExpr → rExpr
  | rNode : rBoolOp → rExpr → rExpr → rExpr.

Fixpoint rEval (f : rNat → bool) (x : rExpr) {struct x} : bool :=
  match x with
  | rV n ⇒ f n
  | rN x ⇒ negb (rEval f x)
  | rNode n x1 x2 ⇒ rBoolOpFun n (rEval f x1) (rEval f x2)
  end.

Fixpoint maxVar (e : rExpr) : rNat :=
  match e with
  | rV n ⇒ n
  | rN p ⇒ maxVar p
  | rNode n p q ⇒ rmax (maxVar p) (maxVar q)
  end.

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).
Hint 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 in |- *; auto; rewrite H; auto; rewrite H0; auto.
Qed.
Hint Resolve support.


Definition normNot (p : rExpr) :=
  match p with
  | 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 in |- *; auto; intros; rewrite negb_elim; auto.
Qed.

Definition normOr (p q : rExpr) :=
  match p, q with
  | 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) = rEval f p || rEval f q.
intros; case p; case q; intros; simpl in |- *; auto with bool;
 try rewrite de_morgan2; try rewrite negb_elim; auto.
Qed.

Definition normImpl (p q : rExpr) :=
  match p, q with
  | 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 in |- *; auto; rewrite implb_elim;
 rewrite negb_elim; auto.
Qed.

Fixpoint norm (e : Expr) : rExpr :=
  match e with
  | V n ⇒ rV n
  | normalize.N p ⇒ normNot (norm p)
  | Node n1 p q ⇒
      match n1 with
      | ANd ⇒ rNode rAnd (norm p) (norm q)
      | Or ⇒ normOr (norm p) (norm q)
      | Impl ⇒ normImpl (norm p) (norm q)
      | normalize.Eq ⇒ rNode rEq (norm p) (norm q)
      end
  end.

Theorem normEval :
 ∀ (f : rNat → bool) (e : Expr), Eval f e = rEval f (norm e).
simple induction e; clear e; simpl in |- *; auto.
intros p H; rewrite normNotEval; rewrite H; auto.
intros b p Hp q Hq; case b; rewrite Hp; rewrite Hq; auto;
 rewrite normOrEval || rewrite normImplEval; auto.
Qed.


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.

Theorem TautoRTauto : ∀ e : Expr, Tautology e ↔ rTautology (norm e).
intros e; unfold Tautology in |- *; unfold rTautology in |- *; split.
intros H' f; rewrite <- normEval; auto.
intros H' f; rewrite normEval; auto.
Qed.