fix bugs.

CNFCvterSolver.v

@@ -93,34 +93,36 @@ Proof.
 Qed.
 
 
-(** Check formula only has clause. *)
 Fixpoint is_clause (p : form) : bool :=
   match p with
+  | var _ => true
+  | boolv _ => true
   | land p1 p2 =>  false
   | lor p1 p2 =>  is_clause p1 && is_clause p2
   | mapsto _ _ => false
-  | _ => true                
+  | not (var _ ) => true (*only return true here*)
+  | not (boolv _) => false
+  | not (land _ _) => false
+  | not (lor _ _) => false
+  | not (mapsto _ _) => false
+  | not (not _) => false               
   end.
 
-(** Check formula is in cnf. *)
+
 Fixpoint is_cnf (p : form) : bool :=
   match p with
   | land p1 p2 =>  is_cnf p1 && is_cnf p2
   | lor p1 p2 =>  is_clause  p1 && is_clause p2
-  | mapsto _ _ => false
-  | _ => true                
+  | _ => is_clause p                
   end.
 
-(** Check formula is in cnf and nnf. *)
-Definition real_is_cnf (p : form) : bool :=
-  is_cnf p && is_nnf p.
 
 (** Conditions to use or_clause_cnf. *)
 Lemma cnf_eq_clause_cnf:forall (p1 p2:form), is_cnf (or_clause_cnf p1 p2) = is_clause p1 && is_cnf p2.
 Proof.
   intros.
-  induction p2;simpl;try reflexivity;try btauto.
-  - rewrite IHp2_1, IHp2_2. (* land *)
+  induction p2;try reflexivity; try (simpl;btauto).
+  - simpl. rewrite IHp2_1, IHp2_2. (* land *)
     btauto.
 Qed.
 
@@ -135,7 +137,7 @@ Qed.
 
 
 (*got stucked here if use equivalent:
-is_conj_normal (or_cnf_cnf p1 p2) =true <-> is_cnf p1 =true && is_cnf p2=true
+is_conj_normal (or_cnf_cnf p1 p2) =true <-> is_cnf p1 =true /\ is_cnf p2=true
  *)
 
 (** true/false doesn't effect is_cnf. *)
@@ -185,74 +187,6 @@ Proof.
     assumption.
 Qed.
 
-(** or_clause_cnf keeps is_nnf. *)
-Lemma clause_cnf_keep_nnf:forall (p1 p2:form), is_nnf (or_clause_cnf p1 p2) = is_nnf p1 && is_nnf p2.
-Proof.
-  intros.
-  induction p2;simpl;
-    try reflexivity;
-    try btauto.
-  - rewrite IHp2_1, IHp2_2. (* land *)
-    btauto.
-Qed.
-
-(** or_cnf_cnf keeps is_nnf. *)
-Lemma cnf_cnf_keep_nnf:forall (p1 p2:form), is_nnf (or_cnf_cnf p1 p2) = is_nnf p1 && is_nnf p2.
-Proof.
-  intros.
-  induction p1;simpl;
-    try(rewrite clause_cnf_keep_nnf;reflexivity).
-  - rewrite IHp1_1, IHp1_2. (*land*)
-    btauto.
-Qed.
-
-(** true/false doesn't effect is_nnf. *)
-Lemma is_nnf_neg_cnf : forall (p:form), is_nnf (nnf_cnf_converter (nnf_converter false p))= is_nnf (nnf_cnf_converter (nnf_converter true p)).
-  Proof.
-    intros.
-    induction p;simpl;
-      try (try(destruct b); (*var and boolv *)
-           reflexivity);
-      try (rewrite cnf_cnf_keep_nnf; (*land lor mapsto*)
-           rewrite IHp1, IHp2;
-           reflexivity).
-    - symmetry in IHp. (*not*)
-      assumption.
-Qed.
-
-(** Conversion is correct for nnf. *)
-Lemma cnf_converter_nnf_correctness: forall (p:form), is_nnf (cnf_converter  p) = true.
-Proof.
-  intros.
-  induction p;
-    try (reflexivity);
-    unfold cnf_converter;
-    simpl;
-    try(try (rewrite cnf_cnf_keep_nnf); (* land lor*)
-        unfold cnf_converter in IHp1, IHp2;
-        rewrite IHp1, IHp2;
-        reflexivity).
-  - rewrite cnf_cnf_keep_nnf. (*mapsto case, handle the not with is_nnf_neg_cnf*)
-    unfold cnf_converter in IHp1.
-    rewrite is_nnf_neg_cnf in IHp1.
-    rewrite IHp1.
-    assumption.
-  - (*not case, handle the not with is_nnf_neg_cnf*)
-    unfold cnf_converter in IHp.
-    rewrite is_nnf_neg_cnf in IHp.
-    assumption.
-Qed.
-
-(** Conversion is really correct.*)
-Lemma cnf_converter_correctness_real: forall (p:form), real_is_cnf (cnf_converter  p) = true.
-Proof.
-  intros.
-  unfold real_is_cnf.
-  rewrite cnf_converter_cnf_correctness.
-  now rewrite cnf_converter_nnf_correctness.
-Qed.
-
-
 (** Integration *)
 Definition solver (p : form) : bool:=
   match find_valuation (cnf_converter p) with

Formula.v

@@ -13,10 +13,8 @@ Definition eqb_string (x y : string) : bool :=
 
 (** Define the equality on id. *)
 Definition eqb_id  (i1 i2:id): bool :=
-  match i1 with
-  | Id x => match i2 with
-            | Id y => eqb_string x y (*use equality on string*)
-            end
+  match i1, i2 with
+  |Id x, Id y => eqb_string x y (*use equality on string*)
   end.
 
 (** Equality on Ids is decidable. *)

NNFCvtrSolver.v

@@ -27,13 +27,6 @@ Definition f :=  (mapsto (land (var x) (var y)) (var y)).
 
 Eval compute in (nnf_converter false f).
 
-(** Helper lemma. *)
-Lemma negb_swap : forall (a b : bool), negb a = b -> a = negb b.
-Proof.
-  intros.
-  rewrite <-H.
-  apply negb_involutive_reverse.
-Qed.
 
 (** Boolean argument works well.*)
 Lemma converter_neg:forall (V : valuation) (p:form),  negb (interp V (nnf_converter false p)) = interp V (nnf_converter true p).
@@ -49,13 +42,11 @@ Proof.
     rewrite <-IHp1, <-IHp2.
     btauto.
   - simpl. (* mapsto *)
-    apply negb_swap in IHp2.
-    rewrite <-IHp1, IHp2.
+    rewrite <-IHp1, <-IHp2.
     btauto.
   - simpl. (* not *)
-    symmetry.
-    apply negb_swap.
-    assumption.
+    rewrite <-IHp.
+    btauto.
 Qed.     
 
 (** Interpretations are same. *)
@@ -87,7 +78,7 @@ Fixpoint is_nnf  (p : form) : bool :=
   | boolv _ => true
   | land p1 p2 =>  is_nnf p1 && is_nnf p2
   | lor p1 p2 =>  is_nnf p1 && is_nnf p2
-  | mapsto p1 p2 =>  is_nnf p1 && is_nnf p2  
+  | mapsto p1 p2 =>  false  
   | not (var _ ) => true (*only return true here*)
   | not (boolv _) => false
   | not (land _ _) => false

OptSolver.v

@@ -2,83 +2,66 @@ Require Import Formula FindVal.
 Require Import Btauto.
 
 
+Definition andf (p1 p2 : form): form :=
+  match p1,p2 with
+  | (var x), (boolv true) => (var x)
+  | (var x), (boolv false) => (boolv false)
+  | (boolv true), (var x) => (var x)
+  | (boolv false), (var x) => (boolv false) 
+  | _, _ => land p1 p2
+  end.
+
+Definition orf (p1 p2 : form): form :=
+  match p1,p2 with
+  | (var x), (boolv true) => (boolv true)
+  | (var x), (boolv false) => (var x) 
+  | (boolv true), (var x) => (boolv true)
+  | (boolv false), (var x) => (var x) 
+  | _, _ => lor p1 p2
+  end.
+
+
 Fixpoint formula_optimizer (p : form): form :=
   match p with
   | var _ => p
-  | boolv _  => p
-  | land (var x) (boolv true) => (var x)
-  | land (var x) (boolv false) => (boolv false)
-  | land (boolv true) (var x) => (var x) 
-  | land (boolv false) (var x) => (boolv false)                                
-  | land p1 p2 => land (formula_optimizer p1) (formula_optimizer p2)
-  | lor (var x) (boolv true) => (boolv true)
-  | lor (var x) (boolv false) => (var x) 
-  | lor (boolv true) (var x) => (boolv true)
-  | lor (boolv false) (var x) => (var x) 
-  | lor p1 p2 => lor (formula_optimizer p1) (formula_optimizer p2)
+  | boolv _  => p           
+  | land p1 p2 => andf (formula_optimizer p1) (formula_optimizer p2)
+  | lor p1 p2 => orf (formula_optimizer p1) (formula_optimizer p2)
   | mapsto p1 p2 => mapsto (formula_optimizer p1) (formula_optimizer p2)
   | not p => not (formula_optimizer p)
   end.
 
 
+Lemma interp_opt_land :forall (V : valuation) (p1 p2 : form), interp V (andf p1 p2) = interp V p1 && interp V p2.
+Proof.
+  intros.
+  destruct p1 eqn:P1 , p2 eqn:P2;try reflexivity;try (destruct b;simpl;btauto).
+Qed.
 
-Lemma interp_opt_land : forall (V : valuation) (p1 p2 : form),interp V (formula_optimizer (land p1 p2)) = interp V (formula_optimizer p1) && interp V (formula_optimizer p2).
-  Proof.
-    intros.
-    destruct p1 eqn:P1 , p2 eqn:P2;
-      unfold formula_optimizer;
-      try reflexivity; (*trivial cases, form is not changed*)
-      try (destruct b; (*boolv case*)
-       unfold interp);
-      try (btauto). (*land and lor cases*)
-    Qed.
-(**      
-      try (symmetry;apply andb_true_l);
-      try (symmetry;apply andb_false_r);
-      try (symmetry;apply andb_false_l).
-*)
-
+
 
-
-
-Lemma interp_opt_lor : forall (V : valuation) (p1 p2 : form),interp V (formula_optimizer (lor p1 p2)) = interp V (formula_optimizer p1) || interp V (formula_optimizer p2).
+Lemma interp_opt_lor :forall (V : valuation) (p1 p2 : form), interp V (orf p1 p2) = interp V p1 || interp V p2.
 Proof.
-    intros.
-    destruct p1 eqn:P1 , p2 eqn:P2;
-      unfold formula_optimizer;
-      try reflexivity; (*trivial cases, form is not changed*)
-      try (destruct b; (*boolv case*)
-           unfold interp);
-      try (btauto). (*land and lor cases*)
-  Qed.
-(**     
-        try (symmetry;apply orb_true_r);
-        try (symmetry;apply orb_true_l);
-        try (symmetry;apply orb_false_l).
-        try (symmetry;apply orb_false_r).
-*)
+  intros.
+  destruct p1 eqn:P1 , p2 eqn:P2;try reflexivity;try (destruct b;simpl;btauto).
+Qed.
+
 
 
 Lemma optimizer_correctness:forall (V : valuation) (p : form), (interp V p) =  (interp V (formula_optimizer p)).
 Proof.
   intros.
-  induction p;try reflexivity. 
+  induction p;try reflexivity;simpl. 
   - rewrite interp_opt_land. (*land *)
     rewrite <-IHp1, <-IHp2.
     reflexivity.
   - rewrite interp_opt_lor. (*lor*)
     rewrite <-IHp1, <-IHp2.
     reflexivity.
-  - unfold formula_optimizer. (*mapsto, just rewrite*)
-    unfold interp.
-    unfold formula_optimizer in IHp1, IHp2.
-    unfold interp in IHp1, IHp2.
+  - simpl. (*mapsto, just rewrite*)
     rewrite IHp1, IHp2.
     reflexivity.
-  - unfold formula_optimizer. (*not, just rewrite*)
-    unfold interp.
-    unfold formula_optimizer in IHp.
-    unfold interp in IHp.
+  - simpl.
     rewrite IHp.
     reflexivity.
 Qed.       

predicate_nnf.v

@@ -0,0 +1,67 @@
+Require Import Formula FindVal OptSolver.
+Require Import Btauto.
+
+
+
+Fixpoint nnf_converter (hn :Datatypes.bool) (p :form) : form :=
+  match hn, p with
+  | false, var _ =>  p
+  | true, var _ => (not  p)
+  | false, boolv _ => p
+  | true, boolv true => boolv false
+  | true, boolv false => boolv true   
+  | false, land p1 p2 => land (nnf_converter false p1) (nnf_converter false p2)
+  | true, land p1 p2 =>  lor (nnf_converter true  p1) (nnf_converter true  p2)
+  | false, lor p1 p2 => lor (nnf_converter false p1) (nnf_converter false p2)
+  | true, lor p1 p2 =>  land (nnf_converter true  p1) (nnf_converter true  p2)
+  | false, mapsto p1 p2 => lor (nnf_converter true p1) (nnf_converter false p2)
+  | true, mapsto p1 p2 => land  (nnf_converter false p1)  (nnf_converter true p2)   
+  | false, not p1  => (nnf_converter true p1)
+  | true, not p1  => (nnf_converter false p1)
+  end.
+
+
+
+(** Check formula is in NNF form. *)
+Inductive is_nnf : form -> Prop :=
+| var : forall i, is_nnf (var i)
+| boolv : forall b, is_nnf (boolv b)
+| land: forall p1 p2, is_nnf p1 -> is_nnf p2 -> is_nnf (land p1 p2)
+| lor: forall p1 p2, is_nnf p1 -> is_nnf p2 -> is_nnf (lor p1 p2)
+| not: forall i, is_nnf (not (var i))
+.
+
+(** true/false doesn't matter! *)
+(* can't do split at beginning*)
+Lemma is_nnf_neg : forall (p:form), is_nnf (nnf_converter true p) <-> is_nnf (nnf_converter false p).
+  Proof.
+    intros.
+    induction  p;simpl;
+    constructor;intros;
+      try (inversion H; (*land lor mapsto*)
+        apply IHp1 in H2;
+        apply IHp2 in H3;
+        constructor;
+        assumption);
+      try constructor; (*var*)
+      try (apply IHp in H; (*not*)
+        assumption).
+    - destruct b;constructor. (*bool*)
+  Qed.
+
+
+(** Conversion is correct. *)
+Lemma nnf_converter_correctness_2: forall (p:form), is_nnf (nnf_converter false  p).
+Proof.
+  intro.
+  induction p;simpl.
+  - constructor.
+  - constructor.
+  - constructor;assumption.
+  - constructor;assumption.
+  - apply is_nnf_neg in IHp1.
+    constructor;assumption.
+  - apply is_nnf_neg.
+    assumption.
+Qed.
+