destruct: adhoc unsoundness correction

examples/bts/231_destruct.mlw

@@ -25,6 +25,31 @@ module T2
   goal G : (forall x. p1 x \/ p2 x \/ p3 x) -> 1 = 1
 end
 
+module Unsoundness
+
+  predicate a
+  predicate b
+  predicate c
+  (* Here if we do things badly we could use a on the right to prove the new 
+     hypothesis a on the left (and vice versa with b) 
+     This should not be provable.
+  *)
+  axiom H: (a -> (c /\ b)) /\ (b -> a)
+  goal t1: c
+
+end
+
+module Incompleteness
+
+  predicate a
+  predicate b
+  predicate c
+
+  axiom H: (a -> (c /\ b)) /\ (b -> a) /\ a
+  goal t1: c
+
+end
+
 module Imbrication
   predicate p1
   predicate p2

examples/bts/231_destruct/why3session.xml

@@ -2,6 +2,7 @@
 <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
 "http://why3.lri.fr/why3session.dtd">
 <why3session shape_version="5">
+<prover id="0" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
 <file name="../231_destruct.mlw">
 <theory name="T">
  <goal name="G">
@@ -49,6 +50,25 @@
  </transf>
  </goal>
 </theory>
+<theory name="Unsoundness">
+ <goal name="t1">
+ </goal>
+</theory>
+<theory name="Incompleteness">
+ <goal name="t1">
+ <transf name="destruct_rec" arg1="H">
+  <goal name="t1.0" expl="destruct premise">
+  <proof prover="0"><result status="unknown" time="0.00"/></proof>
+  </goal>
+  <goal name="t1.1" expl="destruct premise">
+  <proof prover="0"><result status="unknown" time="0.00"/></proof>
+  </goal>
+  <goal name="t1.2" proved="true">
+  <proof prover="0"><result status="valid" time="0.00"/></proof>
+  </goal>
+ </transf>
+ </goal>
+</theory>
 <theory name="Imbrication">
  <goal name="G">
  <transf name="destruct" arg1="H">
@@ -121,5 +141,29 @@
  </transf>
  </goal>
 </theory>
+<theory name="Tsurfail">
+ <goal name="t">
+ <transf name="destruct_rec" arg1="H">
+  <goal name="t.0" expl="destruct premise">
+  </goal>
+  <goal name="t.1" expl="destruct premise">
+  </goal>
+  <goal name="t.2">
+  </goal>
+ </transf>
+ </goal>
+</theory>
+<theory name="Tfail">
+ <goal name="G">
+ <transf name="destruct_rec" arg1="H">
+  <goal name="G.0" expl="destruct premise">
+  </goal>
+  <goal name="G.1" expl="destruct premise">
+  </goal>
+  <goal name="G.2">
+  </goal>
+ </transf>
+ </goal>
+</theory>
 </file>
 </why3session>

src/transform/destruct.ml

@@ -149,6 +149,11 @@ let destruct_term ~recursive (t: term) =
     l.ls_constr <> 0
   in
 
+  (* Check if a new goal is created in the branch *)
+  let contains_goal l =
+    List.exists (fun x -> match x with | Goal_term _ -> true | _ -> false) l
+  in
+
   (* Main function *)
   let rec destruct_term (t: term) =
     let destruct_term_exception t =
@@ -163,12 +168,23 @@ let destruct_term ~recursive (t: term) =
         let l1 = destruct_term_exception t1 in
         let l2 = destruct_term_exception t2 in
         (* For each parallel branch of l1 we have to append *all* parallel
-           branch of l2. *)
+           branch of l2 which are not new goals. In case of new goals, we are
+           not allowed to use the left/right conclusions to prove the goal.
+           Example:
+           H: (A -> (B /\ C) /\ (C -> A)
+           Goal g: C
+        *)
         (* TODO efficiency: this is not expected to work on very large terms
            with tons of Tand/Tor. *)
         List.fold_left (fun par_acc seq_list1 ->
-            List.fold_left (fun par_acc seq_list2 ->
-                par_acc @ ([seq_list1 @ seq_list2])) par_acc l2
+            if contains_goal seq_list1 then
+              par_acc @ [seq_list1]
+            else
+              List.fold_left (fun par_acc seq_list2 ->
+                  if contains_goal seq_list2 then
+                    par_acc @ [seq_list2]
+                  else
+                    par_acc @ [seq_list1 @ seq_list2]) par_acc l2
           ) [] l1
     | Tbinop (Tor, t1, t2) ->
         let l1 = destruct_term_exception t1 in