From 7b0a228d4412134b5afd1371ee097632ef03953a Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 4 Nov 2020 09:27:52 +0100
Subject: [PATCH] [wp] Generializes int induction tactic to any base
---
src/plugins/wp/TacInduction.ml | 24 ++++++++++++++-----
.../script/lemma_ByInd.json | 12 +++++-----
.../script/lemma_ByInd.json | 4 +++-
.../script/lemma_ByInd.json | 4 +++-
4 files changed, 30 insertions(+), 14 deletions(-)
diff --git a/src/plugins/wp/TacInduction.ml b/src/plugins/wp/TacInduction.ml
index 7a5a4185418..1a57d547d79 100644
--- a/src/plugins/wp/TacInduction.ml
+++ b/src/plugins/wp/TacInduction.ml
@@ -44,7 +44,7 @@ let process value n0 ~inf ~sup seq =
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 v0 = n0 in
let sigma = Lang.sigma () in
F.Subst.add sigma value vn ;
let env = { n ; sigma ; hind = [] } in
@@ -84,7 +84,7 @@ let process value n0 ~inf ~sup seq =
(* --- Induction Tactical --- *)
(* -------------------------------------------------------------------------- *)
-let vbase,pbase = Tactical.spinner ~id:"base"
+let vbase,pbase = Tactical.composer ~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 ()
@@ -99,13 +99,25 @@ class induction =
~descr:"Proof by integer induction"
~params:[pbase;psup;pinf]
+ method private get_base () =
+ match self#get_field vbase with
+ | Tactical.Compose(Code(t, _, _))
+ | Inside(_, t) when Lang.F.typeof t = Lang.t_int ->
+ Some t
+ | Compose(Cint i) ->
+ Some (Lang.F.e_bigint i)
+ | _ ->
+ None
+
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)
+ match self#get_base () with
+ | Some base ->
+ let inf = self#get_field vinf in
+ let sup = self#get_field vsup in
+ Applicable(process value base ~inf ~sup)
+ | None -> Not_configured
else Not_applicable
end
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json
index c70ff7e2d9c..ac3d5e1db48 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json
@@ -1,14 +1,14 @@
-[ { "prover": "Alt-Ergo:2.2.0", "verdict": "unknown" },
- { "prover": "script", "verdict": "valid" },
+[ { "prover": "script", "verdict": "valid" },
{ "header": "Induction", "tactic": "Wp.induction",
- "params": { "base": 0, "hsup": true, "hinf": true },
+ "params": { "base": { "select": "kint", "val": "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 } ],
+ "time": 0.0044, "steps": 6 } ],
"Induction (sup)": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0113,
+ "verdict": "valid", "time": 0.0035,
"steps": 21 } ],
"Induction (inf)": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.009,
+ "verdict": "valid", "time": 0.0067,
"steps": 20 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.session/script/lemma_ByInd.json
index 5a250b7fa27..acf6a2d7d5e 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.session/script/lemma_ByInd.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.session/script/lemma_ByInd.json
@@ -1,6 +1,8 @@
[ { "prover": "Alt-Ergo:2.2.0", "verdict": "unknown" },
+ { "prover": "script", "verdict": "unknown" },
{ "header": "Induction", "tactic": "Wp.induction",
- "params": { "base": 0, "hsup": true, "hinf": true },
+ "params": { "base": { "select": "kint", "val": "0" }, "hsup": true,
+ "hinf": true },
"select": { "select": "inside-goal", "occur": 0, "target": "x_0",
"pattern": "$x" },
"children": { "Base": [ { "prover": "Alt-Ergo:2.2.0",
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.session/script/lemma_ByInd.json
index c3224ca1dac..3defdcb3dcb 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.session/script/lemma_ByInd.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.session/script/lemma_ByInd.json
@@ -1,6 +1,8 @@
[ { "prover": "Alt-Ergo:2.2.0", "verdict": "unknown" },
+ { "prover": "script", "verdict": "unknown" },
{ "header": "Induction", "tactic": "Wp.induction",
- "params": { "base": 0, "hsup": true, "hinf": true },
+ "params": { "base": { "select": "kint", "val": "0" }, "hsup": true,
+ "hinf": true },
"select": { "select": "inside-goal", "occur": 0, "target": "y_0",
"pattern": "$y" },
"children": { "Base": [ { "prover": "Alt-Ergo:2.2.0",
--
GitLab