Commit 7b0a228d authored by Allan Blanchard's avatar Allan Blanchard

[wp] Generializes int induction tactic to any base

parent d838ad2e
......@@ -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
......
[ { "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 } ] } } ]
[ { "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",
......
[ { "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",
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment