Skip to content
GitLab
Commit a12d7ed4 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Strong induction now replaces normal induction. 

To be tested/checked.
parent c3d00f76
Hide whitespace changes
Inline Side-by-side
examples/dijkstra/why3session.xml
View file @ a12d7ed4
......@@ -3,19 +3,20 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.4.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../dijkstra.mlw" proved="true">
<theory name="DijkstraShortestPath" proved="true" sum="4d2b897a0ad84be2f910318d0c53a763">
<theory name="DijkstraShortestPath" proved="true" sum="501f8eee126b36613e1204b6238c589f">
<goal name="WP_parameter relax" expl="VC for relax" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="Length_nonneg" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="Length_nonneg.0" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="Length_nonneg.1" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
......@@ -23,32 +24,37 @@
</transf>
</goal>
<goal name="Path_inversion" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="9"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="Path_shortest_path" proved="true">
<transf name="assert" proved="true" arg1="(forall sn. forall d. 0 &lt;= d &lt; sn -&gt; forall v. path src v d -&gt; exists d&apos;:int. shortest_path src v d&apos; /\ d&apos; &lt;= d)">
<goal name="Path_shortest_path.0" proved="true">
<transf name="induction" proved="true" arg1="sn">
<goal name="Path_shortest_path.0.0" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Path_shortest_path.0.1" proved="true">
<proof prover="4"><result status="valid" time="0.05"/></proof>
<transf name="instantiate" proved="true" arg1="Hrec" arg2="sn">
<goal name="Path_shortest_path.0.1.0" proved="true">
<proof prover="1"><result status="valid" time="0.10"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="Path_shortest_path.1" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="Main_lemma" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="173"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="173"/></proof>
</goal>
<goal name="Completeness_lemma" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="Completeness_lemma.0" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="Completeness_lemma.1" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
......@@ -58,15 +64,15 @@
<goal name="inside_or_exit" proved="true">
<transf name="induction_pr" proved="true" >
<goal name="inside_or_exit.0" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
<goal name="inside_or_exit.1" proved="true">
<transf name="case" proved="true" arg1="(mem z s)">
<goal name="inside_or_exit.1.0" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inside_or_exit.1.1" proved="true">
<proof prover="4"><result status="valid" time="0.84"/></proof>
<proof prover="5"><result status="valid" time="0.84"/></proof>
</goal>
</transf>
</goal>
......@@ -75,73 +81,73 @@
<goal name="WP_parameter shortest_path_code" expl="VC for shortest_path_code" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter shortest_path_code.0" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="164"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="164"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.1" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="11"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.2" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="35"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.3" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.4" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="86"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="86"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.5" expl="loop invariant init" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="15"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.6" expl="loop invariant init" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.08" steps="321"/></proof>
<proof prover="2" timelimit="1"><result status="valid" time="0.08" steps="321"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.7" expl="loop invariant init" proved="true">
<proof prover="1" timelimit="60"><result status="valid" time="0.02" steps="110"/></proof>
<proof prover="2" timelimit="60"><result status="valid" time="0.02" steps="110"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.8" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.9" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
<proof prover="3"><result status="valid" time="0.18"/></proof>
<transf name="remove" proved="true" arg1="real,tuple0,unit,ref,zero,one,(&gt;),(-),( * ),(-),(==),singleton,union,inter,diff,choose,(!),Assoc,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm,Assoc1,Mul_distr_l,Mul_distr_r,Comm1,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Select_eq,Select_neq,extensionality,subset_refl,subset_trans,empty_def1,mem_empty,remove_def1,add_remove,remove_add,subset_remove,union_def1,inter_def1,diff_def1,subset_diff,choose_def,cardinal_nonneg,cardinal_empty,cardinal_add,cardinal_remove,subset_eq,cardinal1,G_succ_sound,Weight_nonneg,Length_nonneg,Path_inversion,Path_shortest_path,Main_lemma,Completeness_lemma,inside_or_exit">
<goal name="WP_parameter shortest_path_code.9.0" expl="assertion" proved="true">
<proof prover="2" timelimit="1"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3" timelimit="1"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter shortest_path_code.10" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="40"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="40"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11" expl="loop invariant preservation" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="WP_parameter shortest_path_code.11.0" expl="loop invariant preservation" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter shortest_path_code.11.0.0" expl="VC for shortest_path_code" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="64"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="64"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.1" expl="VC for shortest_path_code" proved="true">
<proof prover="0" timelimit="10" memlimit="4000"><result status="valid" time="1.40"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.2" expl="VC for shortest_path_code" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="25"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.3" expl="VC for shortest_path_code" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="8.42"/></proof>
<proof prover="4" timelimit="10" memlimit="4000"><result status="valid" time="8.42"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.4" expl="VC for shortest_path_code" proved="true">
<proof prover="1"><result status="valid" time="0.05" steps="191"/></proof>
<proof prover="2"><result status="valid" time="0.05" steps="191"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.5" expl="VC for shortest_path_code" proved="true">
<proof prover="1"><result status="valid" time="0.17" steps="495"/></proof>
<proof prover="2"><result status="valid" time="0.17" steps="495"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.6" expl="VC for shortest_path_code" proved="true">
<transf name="case" proved="true" arg1="(v = v1)">
<goal name="WP_parameter shortest_path_code.11.0.6.0" expl="VC for shortest_path_code" proved="true">
<proof prover="3"><result status="valid" time="0.70"/></proof>
<proof prover="4"><result status="valid" time="0.70"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.11.0.6.1" expl="VC for shortest_path_code" proved="true">
<proof prover="4"><result status="valid" time="0.12"/></proof>
<proof prover="5"><result status="valid" time="0.12"/></proof>
</goal>
</transf>
</goal>
......@@ -150,16 +156,16 @@
</transf>
</goal>
<goal name="WP_parameter shortest_path_code.12" expl="loop invariant preservation" proved="true">
<proof prover="4"><result status="valid" time="0.20"/></proof>
<proof prover="5"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.13" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="59"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="59"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.14" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="19"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.15" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.10" steps="291"/></proof>
<proof prover="2"><result status="valid" time="0.10" steps="291"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.16" expl="loop invariant preservation" proved="true">
<transf name="introduce_premises" proved="true" >
......@@ -168,28 +174,28 @@
<goal name="WP_parameter shortest_path_code.16.0.0" expl="loop invariant preservation" proved="true">
<transf name="cut" proved="true" arg1="(inv_succ src visited q d)">
<goal name="WP_parameter shortest_path_code.16.0.0.0" expl="loop invariant preservation" proved="true">
<proof prover="3"><result status="valid" time="0.39"/></proof>
<proof prover="4"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.16.0.0.1" proved="true">
<proof prover="4"><result status="valid" time="0.08"/></proof>
<proof prover="5"><result status="valid" time="0.08"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter shortest_path_code.16.0.1" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="WP_parameter shortest_path_code.17" expl="loop variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.04" steps="122"/></proof>
<proof prover="2"><result status="valid" time="0.04" steps="122"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.18" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="22"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
<goal name="WP_parameter shortest_path_code.19" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.18" steps="352"/></proof>
<proof prover="2"><result status="valid" time="0.18" steps="352"/></proof>
</goal>
</transf>
</goal>
......
src/transform/ind_itp.ml
View file @ a12d7ed4
......@@ -16,12 +16,53 @@ open Args_wrapper
(** This file contains the transformation with arguments 'induction on integer' *)
(* Documentation of induction:
From task [delta, x: int, delta'(x) |- G(x)], variable x and term bound, builds the tasks:
[delta, x: int, x <= bound, delta'(x) |- G(x)] and
[delta, x: int, x >= bound, (delta'(x) -> G(x)), delta'(x+1) |- G(x+1)]
x cannot occur in delta as it can only appear after its declaration (by
construction of the task). Also, G is not part of delta'.
In practice we are "chosing" delta'. The minimal set delta' such that this
transformation is correct is Min_d = {H | x *directly* appears in H} € delta'. (1)
Adding any declarations to delta' should be safe(2).
In practice, we define delta' iterately beginning with the goal (upward) and
adding any hypothesis that contains symbols defined in a set S.
Algorithm used:
S : symbol set = {x} union {symbol_appearing_in goal}
delta' : list decl = {}
For decl from goal to x_declaration do
if ((symbol_appearing_in decl) intersect S) != {} then
add decl to delta'
add (symbol_appearing_in decl) to S
else
()
done
(1) One may be convinced of this because it is possible to make a lemma of
the form "forall x: int. Min_d(x) -> G(x)" with appropriate abstract constant
symbol for every other constant (added in the context). One can then apply
an induction on this reduced example and apply this lemma on the initial case.
(This is an argument for the "reduction of context stuff" not a claim that
the induction is correct)
(2) If it does not talk about x, we will have to prove it (unchanged) to be
able to use it in the recursive part. So it should not change the provability.
*)
let is_good_type t ty =
try (Term.t_ty_check t (Some ty); true) with
| _ -> false
(* Reverts a declaration d to a goal g *)
let revert g d =
let revert g d : Term.term =
match d.d_node with
| Dtype _ -> raise (Arg_trans "revert: cannot revert type")
| Ddata _ -> raise (Arg_trans "revert: cannot revert type")
......@@ -49,61 +90,133 @@ let revert g d =
let revert_list (l: decl list) g =
List.fold_left revert g l
(* From task [delta, x: int, delta'(x) |- G(x)], variable x and term bound, builds the tasks:
[delta, x: int, x <= bound, delta'(x) |- G(x)] and
[delta, x: int, x >= bound, (delta'(x) -> G(x)), delta'(x+1) |- G(x+1)]
(* TODO To be checked *)
let add_ls_term s t =
let rec my_fold s t =
match t.t_node with
| Tapp (ls, []) ->
(* Interesting case *)
Sls.add ls s
| _ -> Term.t_fold my_fold s t
in
my_fold s t
let add_lsymbol s (ls_def: Decl.ls_defn) =
let _vsl, t = Decl.open_ls_defn ls_def in
add_ls_term s t
(* This collects the lsymbols appearing in a decl. It is useful to have
dependencies during induction. We want to generalize all decls that contain
some lsymbols (the one which appears in the goal or the symbol on which we do
the induction. *)
let collect_lsymbol s (d: decl) =
match d.d_node with
| Dtype _ | Ddata _ -> (* can be ignored. TODO to check. *)
s
| Dparam ls -> Sls.add ls s
| Dlogic logic_list ->
List.fold_left (fun s (ls, ls_def) ->
add_lsymbol (Sls.add ls s) ls_def) s logic_list
| Dind (_sign, ind_list) ->
List.fold_left (fun s (ls, pr_term_list) ->
let s = Sls.add ls s in
List.fold_left (fun s (_pr, t) -> add_ls_term s t) s pr_term_list) s ind_list
| Dprop (_k, _pr, t) ->
add_ls_term s t
(* s is a set of variables, g is a term. If d contains one of the elements of s
then all variables of d are added to s and the declaration is prepended to g.
*)
let revert_only_stuff (g, s) (d: decl) =
let d_set = collect_lsymbol Sls.empty d in
let interp = Sls.inter s d_set in
if Sls.equal interp Sls.empty then
(g, s)
else
(revert g d, Sls.union s d_set)
(* Build a term that generalizes all the declarations that were given in l and
that contains at least one of the variables in the set s. Actually, only
revert what is necessary to build a correct term. *)
let revert_only_stuff_list s (l: decl list) (g: decl) (t: term) =
(* The goal is a special case, we collect its variable independantly *)
let s = collect_lsymbol s g in
fst (List.fold_left revert_only_stuff (t, s) l)
let induction x bound env =
let th = Env.read_theory env ["int"] "Int" in
let le_int = Theory.ns_find_ls th.Theory.th_export ["infix <="] in
let plus_int = Theory.ns_find_ls th.Theory.th_export ["infix +"] in
let one_int =
Term.t_const (Number.ConstInt (Number.int_const_dec "1")) Ty.ty_int in
(* bound is optional and set to 0 if not given *)
(* Default bound is 0 if not given *)
let bound =
match bound with
| None -> Term.t_const (Number.ConstInt (Number.int_const_dec "0")) Ty.ty_int
| Some bound -> bound
in
(* Checking the type of the argument of the tactic *)
if (not (is_good_type x Ty.ty_int) || not (is_good_type bound Ty.ty_int)) then
raise (Arg_trans "induction")
else
let lsx = match x.t_node with
| Tvar lsx -> lsx.vs_name
| Tapp (lsx, []) -> lsx.ls_name
| _ -> raise (Arg_trans "induction") in
raise (Arg_trans "induction");
(* Loading of needed symbols from int theory *)
let th = Env.read_theory env ["int"] "Int" in
let le_int = Theory.ns_find_ls th.Theory.th_export ["infix <="] in
let plus_int = Theory.ns_find_ls th.Theory.th_export ["infix +"] in
let one_int =
Term.t_const (Number.ConstInt (Number.int_const_dec "1")) Ty.ty_int in
let le_bound = Trans.decl (fun d -> match d.d_node with
(* Symbol associated to term x *)
let lsx =
match x.t_node with
| Tapp (lsx, []) -> lsx
| _ -> raise (Arg_trans "induction")
in
(* Transformation used for the init case *)
let init_trans = Trans.decl (fun d -> match d.d_node with
| Dprop (Pgoal, _pr, _t) ->
let nt = Term.t_app_infer le_int [x; bound] in
let pr = create_prop_decl Paxiom (Decl.create_prsymbol (gen_ident "Init")) nt in
let pr =
create_prop_decl Paxiom (Decl.create_prsymbol (gen_ident "Init")) nt in
[pr; d]
| _ -> [d]) None in
let x_is_passed = ref false in
let delta_x = ref [] in
let ge_bound =
(* Transformation used for the recursive case *)
let rec_trans =
let x_is_passed = ref false in
let delta' = ref [] in
Trans.decl (fun d -> match d.d_node with
| Dparam ls when (Ident.id_equal lsx ls.ls_name) ->
| Dparam ls when (Term.ls_equal lsx ls) ->
(x_is_passed := true; [d])
| Dprop (Pgoal, _pr, t) ->
if not (!x_is_passed) then
raise (Arg_trans "induction")
else
let t_delta_x = revert_list !delta_x t in
let t_delta' =
revert_only_stuff_list (Sls.add lsx Sls.empty) !delta' d t in
let n = Term.create_vsymbol (Ident.id_fresh "n") Ty.ty_int in
(* t_delta' = forall n, n <= x -> t_delta'[x <- n] *)
let t_delta' =
t_forall_close [n] []
(t_implies (Term.t_app_infer le_int [t_var n; x]) (t_replace x (t_var n) t_delta'))
in
(* x_ge_bound = bound <= x *)
let x_ge_bound_t = t_app_infer le_int [bound; x] in
let x_ge_bound =
create_prop_decl Paxiom (Decl.create_prsymbol (gen_ident "Init")) x_ge_bound_t in
let rec_pr = create_prsymbol (gen_ident "Hrec") in
let new_pr = create_prsymbol (gen_ident "G") in
let new_goal = create_prop_decl Pgoal new_pr
(* new_goal: G[x <- x + 1] *)
let new_goal =
create_prop_decl Pgoal new_pr
(replace_in_term x (t_app_infer plus_int [x; one_int]) t) in
[x_ge_bound; create_prop_decl Paxiom rec_pr t_delta_x; new_goal]
let hrec = create_prop_decl Paxiom rec_pr t_delta' in
[x_ge_bound; hrec; new_goal]
| Dprop (p, pr, t) ->
if !x_is_passed then
begin
delta_x := d :: !delta_x;
delta' := d :: !delta';
(* d [x <- x + 1] *)
[create_prop_decl p pr (replace_in_term x (t_app_infer plus_int [x; one_int]) t)]
end
else
......@@ -111,23 +224,25 @@ let induction x bound env =
| Dind _ | Dlogic _ | Dtype _ | Ddata _ ->
if !x_is_passed then
raise (Arg_trans "induction Dlogic")
(* TODO we need to add Dlogic and Dind here. The problem is that we cannot
easily put them into the recursive hypothesis. So, for now, we do not
allow them. If x does not occur in the Dlogic/Dind, a workaround is to
use the "sort" tactic.
*)
else
[d]
| Dparam _ls ->
if !x_is_passed then
begin
delta_x := d :: !delta_x;
delta' := d :: !delta';
[d]
end
else
[d]
(* TODO | Dlogic l ->
if !x_is_passed then replace things inside and rebuild it else
[d]*)
) None in
Trans.par [le_bound; ge_bound]
Trans.par [init_trans; rec_trans]
let () = wrap_and_register
~desc:"induction <term1> [from] <term2> performs induction on int term1 from int term2. term2 is optional and default to 0."
~desc:"induction <term1> [from] <term2> performs a strong induction on int term1 from int term2. term2 is optional and default to 0."
"induction"
(Tterm (Topt ("from", Tterm Tenvtrans_l))) induction
Supports Markdown
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