[wp] induction tactic

headers/header_spec.txt

@@ -1629,6 +1629,8 @@ src/plugins/wp/TacFilter.ml: CEA_WP
 src/plugins/wp/TacFilter.mli: CEA_WP
 src/plugins/wp/TacHavoc.ml: CEA_WP
 src/plugins/wp/TacHavoc.mli: CEA_WP
+src/plugins/wp/TacInduction.ml: CEA_WP
+src/plugins/wp/TacInduction.mli: CEA_WP
 src/plugins/wp/TacInstance.ml: CEA_WP
 src/plugins/wp/TacInstance.mli: CEA_WP
 src/plugins/wp/TacLemma.ml: CEA_WP

src/plugins/wp/Conditions.mli

@@ -142,7 +142,7 @@ val map_sequence : (pred -> pred) -> sequence -> sequence
 (** Rewrite all root predicates in sequence *)
 
 val map_sequent : (pred -> pred) -> sequent -> sequent
-(** Rewrite all root predocates in hypotheses and goal *)
+(** Rewrite all root predicates in hypotheses and goal *)
 
 val insert : ?at:int -> step -> sequent -> sequent
 (** Insert a step in the sequent immediately [at] the specified position.

src/plugins/wp/Makefile.in

@@ -85,7 +85,7 @@ PLUGIN_CMO:= \
 	CfgCompiler StmtSemantics \
 	VCS script proof wpo wpReport \
 	Footprint Tactical Strategy \
-	TacSplit TacChoice TacRange \
+	TacSplit TacChoice TacRange TacInduction \
 	TacArray TacCompound TacUnfold \
 	TacHavoc TacInstance TacLemma \
 	TacFilter TacCut WpTac TacNormalForm \

src/plugins/wp/TacInduction.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Lang
+
+type env = {
+  n : F.var ;
+  sigma : F.sigma ;
+  mutable hind : F.pred list ;
+}
+
+let rec strip env p =
+  match F.p_expr p with
+  | And ps -> F.p_all (strip env) ps
+  | _ ->
+      let p = F.p_subst env.sigma p in
+      if F.occursp env.n p then
+        ( env.hind <- p :: env.hind ; F.p_true )
+      else p
+
+let process value n0 ~inf ~sup seq =
+
+  (* Transfrom seq into: hyps => (forall n, goal) *)
+  let n = Lang.freshvar ~basename:"n" Qed.Logic.Int in
+  let i = Lang.freshvar ~basename:"i" Qed.Logic.Int in
+  let vn = F.e_var n in
+  let vi = F.e_var i in
+  let v0 = F.e_int n0 in
+  let sigma = Lang.sigma () in
+  F.Subst.add sigma value vn ;
+  let env = { n ; sigma ; hind = [] } in
+  let hyps = Conditions.map_sequence (strip env) (fst seq) in
+  let goal_n = F.p_hyps env.hind @@ F.p_subst sigma (snd seq) in
+  let goal_i = F.p_subst_var n vi goal_n in
+
+  (* Base: n = n0 *)
+  let goal_base = F.p_imply (F.p_equal vn v0) goal_n in
+
+  (* Hind: n0 <= i < n *)
+  let goal_sup =
+    if sup
+    then
+      let hsup = [ F.p_leq v0 vi ; F.p_lt vi vn ] in
+      let hind = F.p_forall [i] (F.p_hyps hsup goal_i) in
+      F.p_hyps [F.p_lt v0 vn; hind] goal_n
+    else F.p_leq value v0 in
+
+  (* Hind: n < i <= n0 *)
+  let goal_inf =
+    if inf
+    then
+      let hinf = [ F.p_lt vn vi ; F.p_leq vi v0 ] in
+      let hind = F.p_forall [i] (F.p_hyps hinf goal_i) in
+      F.p_hyps [F.p_lt vn v0; hind] goal_n
+    else F.p_leq v0 value in
+
+  (* All Cases *)
+  List.map (fun (name,goal) -> name , (hyps,goal)) [
+    "Base" , goal_base ;
+    "Induction (sup)" , goal_sup ;
+    "Induction (inf)" , goal_inf ;
+  ]
+
+(* -------------------------------------------------------------------------- *)
+(* --- Induction Tactical                                                 --- *)
+(* -------------------------------------------------------------------------- *)
+
+let vbase,pbase = Tactical.spinner ~id:"base"
+    ~title:"Base" ~descr:"Value of base case" ()
+let vsup,psup = Tactical.checkbox ~id:"hsup"
+    ~title:"Sup" ~descr:"Induction over base <= n" ~default:true ()
+let vinf,pinf = Tactical.checkbox ~id:"hinf"
+    ~title:"Inf" ~descr:"Induction over n <= base" ~default:true ()
+
+class induction =
+  object(self)
+    inherit Tactical.make
+        ~id:"Wp.induction"
+        ~title:"Induction"
+        ~descr:"Proof by integer induction"
+        ~params:[pbase;psup;pinf]
+
+    method select _feedback (s : Tactical.selection) =
+      let value = Tactical.selected s in
+      if F.is_int value then
+        let base = self#get_field vbase in
+        let inf = self#get_field vinf in
+        let sup = self#get_field vsup in
+        Applicable(process value base ~inf ~sup)
+      else Not_applicable
+
+  end
+
+let tactical = Tactical.export (new induction)
+
+(* -------------------------------------------------------------------------- *)

src/plugins/wp/TacInduction.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of WP plug-in of Frama-C.                           *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2020                                               *)
+(*    CEA (Commissariat a l'energie atomique et aux energies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Built-in Range Tactical (auto-registered) *)
+
+open Tactical
+
+val tactical : tactical
+
+(**************************************************************************)

src/plugins/wp/tests/wp_tip/induction.i

+/* run.config
+   DONTRUN:
+*/
+
+/* run.config_qualif
+   OPT: -wp-prover script,alt-ergo -wp-timeout 1
+   OPT: -wp-prover script,alt-ergo -wp-timeout 1
+   OPT: -wp-prover script,alt-ergo -wp-timeout 1
+*/
+
+// Script 0: induction on f(x) => success
+// Script 1: induction on x => unsuccess
+// Script 2: induction on y => unsuccess
+
+/*@
+  axiomatic Inductive {
+
+  logic integer f(integer x);
+  predicate P(integer x, integer y);
+
+  axiom Hbse: \forall integer y; P(0,y);
+  axiom Hsup: \forall integer i,y; 0 <= i ==> P(i,y) ==> P(i+1,y);
+  axiom Hinf: \forall integer i,y; i <= 0 ==> P(i,y) ==> P(i-1,y);
+
+  lemma ByInd: \forall integer x,y; P(f(x),y);
+
+  }
+*/

src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle

+# frama-c -wp -wp-timeout 1 [...]
+[kernel] Parsing tests/wp_tip/induction.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Script] Goal typed_lemma_ByInd : Valid
+[wp] Proved goals:    1 / 1
+  Qed:             0 
+  Script:          1
+------------------------------------------------------------
+ Axiomatics                WP     Alt-Ergo  Total   Success
+  Axiomatic Inductive       -        -        1       100%
+------------------------------------------------------------

src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json

+[ { "prover": "Alt-Ergo:2.2.0", "verdict": "unknown" },
+  { "prover": "script", "verdict": "valid" },
+  { "header": "Induction", "tactic": "Wp.induction",
+    "params": { "base": 0, "hsup": true, "hinf": true },
+    "select": { "select": "inside-goal", "occur": 0, "target": "(L_f x_0)",
+                "pattern": "L_f$x" },
+    "children": { "Base": [ { "prover": "Alt-Ergo:2.2.0", "verdict": "valid",
+                              "time": 0.0075, "steps": 6 } ],
+                  "Induction (sup)": [ { "prover": "Alt-Ergo:2.2.0",
+                                         "verdict": "valid", "time": 0.0113,
+                                         "steps": 21 } ],
+                  "Induction (inf)": [ { "prover": "Alt-Ergo:2.2.0",
+                                         "verdict": "valid", "time": 0.009,
+                                         "steps": 20 } ] } } ]

src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.res.oracle

+# frama-c -wp -wp-timeout 1 [...]
+[kernel] Parsing tests/wp_tip/induction.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Script] Goal typed_lemma_ByInd : Unsuccess
+[wp] Proved goals:    0 / 1
+------------------------------------------------------------
+ Axiomatics                WP     Alt-Ergo  Total   Success
+  Axiomatic Inductive       -        -        1       0.0%
+------------------------------------------------------------

src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.session/script/lemma_ByInd.json

+[ { "prover": "Alt-Ergo:2.2.0", "verdict": "unknown" },
+  { "header": "Induction", "tactic": "Wp.induction",
+    "params": { "base": 0, "hsup": true, "hinf": true },
+    "select": { "select": "inside-goal", "occur": 0, "target": "x_0",
+                "pattern": "$x" },
+    "children": { "Base": [ { "prover": "Alt-Ergo:2.2.0",
+                              "verdict": "unknown" } ],
+                  "Induction (sup)": [ { "prover": "Alt-Ergo:2.2.0",
+                                         "verdict": "unknown" } ],
+                  "Induction (inf)": [ { "prover": "Alt-Ergo:2.2.0",
+                                         "verdict": "timeout", "time": 1. } ] } } ]

src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.res.oracle

+# frama-c -wp -wp-timeout 1 [...]
+[kernel] Parsing tests/wp_tip/induction.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Script] Goal typed_lemma_ByInd : Unsuccess
+[wp] Proved goals:    0 / 1
+------------------------------------------------------------
+ Axiomatics                WP     Alt-Ergo  Total   Success
+  Axiomatic Inductive       -        -        1       0.0%
+------------------------------------------------------------

src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.session/script/lemma_ByInd.json

+[ { "prover": "Alt-Ergo:2.2.0", "verdict": "unknown" },
+  { "header": "Induction", "tactic": "Wp.induction",
+    "params": { "base": 0, "hsup": true, "hinf": true },
+    "select": { "select": "inside-goal", "occur": 0, "target": "y_0",
+                "pattern": "$y" },
+    "children": { "Base": [ { "prover": "Alt-Ergo:2.2.0",
+                              "verdict": "unknown" } ],
+                  "Induction (sup)": [ { "prover": "Alt-Ergo:2.2.0",
+                                         "verdict": "unknown" } ],
+                  "Induction (inf)": [ { "prover": "Alt-Ergo:2.2.0",
+                                         "verdict": "timeout", "time": 1. } ] } } ]

src/plugins/wp/tests/wp_tip/oracle_qualif/induction.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_tip/induction.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 1 goal scheduled
+[wp] [Script] Goal typed_lemma_Simple : Unsuccess
+[wp] Proved goals:    0 / 1
+------------------------------------------------------------
+ Axiomatics                WP     Alt-Ergo  Total   Success
+  Axiomatic Inductive       -        -        1       0.0%
+------------------------------------------------------------

src/plugins/wp/tests/wp_tip/oracle_qualif/induction_prove.0.session/script/lemma_ByInd.json

+[ { "prover": "script", "verdict": "valid", "time": 0.0549, "steps": 117 },
+  { "header": "Induction", "tactic": "Wp.induction",
+    "params": { "base": 0, "hsup": true, "hinf": true },
+    "select": { "select": "inside-goal", "occur": 0, "target": "(L_f x_0)",
+                "pattern": "L_f$x" },
+    "children": { "Base": [ { "prover": "Alt-Ergo:2.2.0", "verdict": "valid",
+                              "time": 0.0083, "steps": 6 } ],
+                  "Induction (sup)": [ { "prover": "Alt-Ergo:2.2.0",
+                                         "verdict": "valid", "time": 0.0549,
+                                         "steps": 117 } ],
+                  "Induction (inf)": [ { "prover": "Alt-Ergo:2.2.0",
+                                         "verdict": "valid", "time": 0.0274,
+                                         "steps": 86 } ] } } ]