Normalise.v
Require Export Arith.
Require Export Logique.
Mutual Inductive
expr: Set :=
T: expr
| F: expr
| Var: nat ->expr
| Not: expr ->expr
| And: expr -> expr ->expr
| Or: expr -> expr ->expr
| Impl: expr -> expr ->expr
| Eq: expr -> expr ->expr .
Fixpoint
eval[f:nat ->bool; x:expr]: bool :=
Cases x of
T => true
| F => false
| (Var n) => (f n)
| (Not x) => (negb (eval f x))
| (And x1 x2) => (andb (eval f x1) (eval f x2))
| (Or x1 x2) => (orb (eval f x1) (eval f x2))
| (Impl x1 x2) => (implb (eval f x1) (eval f x2))
| (Eq x1 x2) => (eqb (eval f x1) (eval f x2))
end.
Mutual Inductive
node1: Set :=
And1: node1
| Or1: node1
| Impl1: node1
| Eq1: node1 .
Mutual Inductive
expr1: Set :=
T1: expr1
| F1: expr1
| V1: nat ->expr1
| N1: expr1 ->expr1
| Node1: node1 -> expr1 -> expr1 ->expr1 .
Fixpoint
conv[e:expr]: expr1 :=
Cases e of
T => T1
| F => F1
| (Var n) => (V1 n)
| (Not p) => (N1 (conv p))
| (And p q) => (Node1 And1 (conv p) (conv q))
| (Or p q) => (Node1 Or1 (conv p) (conv q))
| (Impl p q) => (Node1 Impl1 (conv p) (conv q))
| (Eq p q) => (Node1 Eq1 (conv p) (conv q))
end.
Fixpoint
eval1[f:nat ->bool; e:expr1]: bool :=
Cases e of
T1 => true
| F1 => false
| (V1 n) => (f n)
| (N1 p) => (negb (eval1 f p))
| (Node1 n1 p q) => Cases n1 of
And1 => (andb (eval1 f p) (eval1 f q))
| Or1 => (orb (eval1 f p) (eval1 f q))
| Impl1 => (implb (eval1 f p) (eval1 f q))
| Eq1 => (eqb (eval1 f p) (eval1 f q))
end
end.
Theorem
th_conv: (e:expr) (f:nat ->bool)(eval f e)=(eval1 f (conv e)).
Induction e; Intros; Simpl; Auto; Rewrite H; Auto; Rewrite H0; Auto.
Qed.
Mutual Inductive
node2: Set :=
And2: node2
| Eq2: node2 .
Definition
f_assoc :=
[n:node2]
Cases n of
And2 => andb
| Eq2 => eqb
end.
Mutual Inductive
expr2: Set :=
T2: expr2
| F2: expr2
| V2: nat ->expr2
| N2: expr2 ->expr2
| Node2: node2 -> expr2 -> expr2 ->expr2 .
Fixpoint
eval2[f:nat ->bool; x:expr2]: bool :=
Cases x of
T2 => true
| F2 => false
| (V2 n) => (f n)
| (N2 x) => (negb (eval2 f x))
| (Node2 n x1 x2) => Cases n of
And2 => (andb (eval2 f x1) (eval2 f x2))
| Eq2 => (eqb (eval2 f x1) (eval2 f x2))
end
end.
Mutual Inductive
in_expr2: nat -> expr2 ->Prop :=
in_V2: (n:nat)(in_expr2 n (V2 n))
| in_N2: (n:nat) (e:expr2) (in_expr2 n e) ->(in_expr2 n (N2 e))
| in_Node2_1:
(i:nat) (n:node2) (e1, e2:expr2) (in_expr2 i e1) ->
(in_expr2 i (Node2 n e1 e2))
| in_Node2_2:
(i:nat) (n:node2) (e1, e2:expr2) (in_expr2 i e2) ->
(in_expr2 i (Node2 n e1 e2)) .
Hint in_V2 in_N2 in_Node2_1 in_Node2_2.
Theorem
support2:
(f, g:nat ->bool) (e:expr2) ((n:nat) (in_expr2 n e) ->(f n)=(g n)) ->
(eval2 f e)=(eval2 g e).
Intros f g e.
Elim e; Intros; Simpl; Auto; Rewrite H; Auto; Rewrite H0; Auto.
Qed.
Hint support2.
Definition
norm_not :=
[p:expr2]
Cases p of
T2 => F2
| T2 => F2
| (N2 p1) => p1
| p1 => (N2 p1)
end.
Lemma
th_norm_not:
(p:expr2) (f:nat ->bool)(eval2 f (norm_not p))=(negb (eval2 f p)).
Intros; Case p; Simpl; Auto; Intros; Rewrite negb_elim; Auto.
Qed.
Hint th_norm_not.
Definition
norm_and :=
[p, q:expr2]
Cases p q of
T2 q1 => q1
| p1 T2 => p1
| F2 _ => F2
| _ F2 => F2
| p1 q1 => (Node2 And2 p1 q1)
end.
Lemma
th_norm_and:
(p, q:expr2) (f:nat ->bool)
(eval2 f (norm_and p q))=(andb (eval2 f p) (eval2 f q)).
Intros; Case p; Case q; Intros; Simpl; Auto;
Rewrite andb_b_true Orelse Rewrite andb_b_false; Auto.
Qed.
Hint th_norm_and.
Definition
norm_or :=
[p, q:expr2]
Cases p q of
T2 _ => T2
| _ T2 => T2
| F2 q1 => q1
| p1 F2 => p1
| (N2 p1) (N2 q1) => (N2 (Node2 And2 p1 q1))
| (N2 p1) q1 => (N2 (Node2 And2 p1 (N2 q1)))
| p1 (N2 q1) => (N2 (Node2 And2 (N2 p1) q1))
| p1 q1 => (N2 (Node2 And2 (N2 p1) (N2 q1)))
end.
Lemma
th_norm_or:
(p, q:expr2) (f:nat ->bool)
(eval2 f (norm_or p q))=(orb (eval2 f p) (eval2 f q)).
Intros; Case p; Case q; Intros; Simpl; Auto; Rewrite de_morgan2;
Rewrite negb_elim; Auto.
Qed.
Hint th_norm_or.
Definition
norm_impl :=
[p, q:expr2]
Cases p q of
T2 q1 => q1
| _ T2 => T2
| F2 _ => T2
| p1 F2 => (N2 p1)
| (N2 p1) (N2 q1) => (N2 (Node2 And2 (N2 p1) q1))
| (N2 p1) q1 => (N2 (Node2 And2 (N2 p1) (N2 q1)))
| p1 (N2 q1) => (N2 (Node2 And2 p1 q1))
| p1 q1 => (N2 (Node2 And2 p1 (N2 q1)))
end.
Lemma
th_norm_impl:
(p, q:expr2) (f:nat ->bool)
(eval2 f (norm_impl p q))=(implb (eval2 f p) (eval2 f q)).
Intros; Case p; Case q; Intros; Simpl; Auto; Rewrite implb_elim;
Rewrite negb_elim; Auto.
Qed.
Hint th_norm_impl.
Definition
norm_eq :=
[p, q:expr2]
Cases p q of
T2 q1 => q1
| p1 T2 => p1
| F2 q1 => (N2 q1)
| p1 F2 => (N2 p1)
| p1 q1 => (Node2 Eq2 p1 q1)
end.
Lemma
th_norm_eq:
(p, q:expr2) (f:nat ->bool)
(eval2 f (norm_eq p q))=(eqb (eval2 f p) (eval2 f q)).
Intros; Case p; Case q; Unfold norm_eq; Auto.
Qed.
Hint th_norm_eq.
Fixpoint
norm[e:expr1]: expr2 :=
Cases e of
T1 => T2
| F1 => F2
| (V1 n) => (V2 n)
| (N1 p) => (norm_not (norm p))
| (Node1 n1 p q) => Cases n1 of
And1 => (norm_and (norm p) (norm q))
| Or1 => (norm_or (norm p) (norm q))
| Impl1 => (norm_impl (norm p) (norm q))
| Eq1 => (norm_eq (norm p) (norm q))
end
end.
Theorem
th_norm: (f:nat ->bool) (e:expr1)(eval1 f e)=(eval2 f (norm e)).
Induction e; Clear e; Simpl; Auto.
Intros p H; Rewrite th_norm_not; Rewrite H; Auto.
Intros n p Hp q Hq; Case n.
Rewrite th_norm_and; Rewrite Hp; Rewrite Hq; Auto.
Rewrite th_norm_or; Rewrite Hp; Rewrite Hq; Auto.
Rewrite th_norm_impl; Rewrite Hp; Rewrite Hq; Auto.
Rewrite th_norm_eq; Rewrite Hp; Rewrite Hq; Auto.
Qed.
Definition
tauto := [e:expr] (f:nat ->bool)(eval f e)=true.
Definition
tauto2 := [e:expr2] (f:nat ->bool)(eval2 f e)=true.
Theorem
tauto_tauto2: (e:expr)(iff (tauto e) (tauto2 (norm (conv e)))).
Split.
Unfold tauto; Unfold tauto2.
Intros.
Rewrite <- th_norm.
Rewrite <- th_conv.
Auto.
Unfold tauto; Unfold tauto2.
Intros.
Rewrite th_conv.
Rewrite th_norm.
Auto.
Qed.
14/09/98, 09:21