WP does not simplify anymorer 'A -> False' into 'not A'

src/core/term.ml

@@ -1819,8 +1819,8 @@ let f_not_simp f = match f.f_node with
 let f_and_simp f1 f2 = match f1.f_node, f2.f_node with
   | Ftrue, _  -> f2
   | _, Ftrue  -> f1
-  | Ffalse, _ -> f1
-  | _, Ffalse -> f2
+  | Ffalse, _ -> f1 (* more efficient than f_false *)
+  | _, Ffalse -> f2 (* more efficient than f_false *)
   | _, _      -> if f_equal f1 f2 then f1 else f_and f1 f2
 
 let f_and_simp_l l = List.fold_left f_and_simp f_true l
@@ -1837,7 +1837,7 @@ let f_or_simp_l l = List.fold_left f_or_simp f_false l
 let f_implies_simp f1 f2 = match f1.f_node, f2.f_node with
   | Ftrue, _  -> f2
   | _, Ftrue  -> f2
-  | Ffalse, _ -> f_not_simp f1
+  | Ffalse, _ -> f_true
   | _, Ffalse -> f_not_simp f1
   | _, _      -> if f_equal f1 f2 then f_true else f_implies f1 f2
 

src/ide/gmain.ml

@@ -704,11 +704,31 @@ end
 (*  read previous data from db   *)
 (*********************************)
 
+(*
+type trans = 
+  | Trans_one of Task.task Trans.trans
+  | Trans_list of Task.task Trans.tlist
 
-let split_transformation = Trans.lookup_transform_l "split_goal" gconfig.env
-let intro_transformation = Trans.lookup_transform "introduce_premises"
-  gconfig.env
+let lookup_trans name =
+  try
+    let t = Trans.lookup_transform name gconfig.env in
+    Trans_one t
+  with Trans.UnknownTrans _ ->
+    let t = Trans.lookup_transform_l name gconfig.env in
+    Trans_list t
+
+let split_transformation = lookup_trans "split_goal"
+let unfold_transformation = lookup_trans "inline_goal"
+let intro_transformation = lookup_trans "introduce_premises"
 
+let apply_trans t task = 
+  match t with
+    | Trans_one t -> [Trans.apply t task]
+    | Trans_list t -> Trans.apply t task
+*)
+
+let split_transformation = Trans.lookup_transform_l "split_goal" gconfig.env
+let intro_transformation = Trans.lookup_transform "introduce_premises" gconfig.env
 
 let rec reimport_any_goal parent gname t db_goal goal_obsolete =
   let goal = Helpers.add_goal_row parent gname t db_goal in

src/programs/pgm_wp.ml

@@ -46,7 +46,9 @@ let wp_and ?(sym=false) f1 f2 =
 let wp_ands ?(sym=false) fl =
   List.fold_left (wp_and ~sym) f_true fl
 
-let wp_implies = f_implies_simp
+let wp_implies f1 f2 = match f2.f_node with
+  | Ffalse -> f_implies f1 f2
+  | _ -> f_implies_simp f1 f2
 
 let is_ref_ty env ty = match ty.ty_node with
   | Tyapp (ts, _) -> ts_equal ts env.ts_ref

tests/test-claude.why

@@ -28,6 +28,16 @@ theory TestInt
 
 end
 
+theory TestSplit
+
+  logic aa int
+
+  logic bb int
+
+  goal G : aa 0 /\ bb 1 -> false
+
+end
+
 theory TestDiv
 
    use import int.Int