Commit 1e2952f1 authored by Allan Blanchard's avatar Allan Blanchard

Merge branch 'master' into feature/wp/repeat-tactic

parents a3a1dc0c 7d242b80
...@@ -1629,6 +1629,8 @@ src/plugins/wp/TacFilter.ml: CEA_WP ...@@ -1629,6 +1629,8 @@ src/plugins/wp/TacFilter.ml: CEA_WP
src/plugins/wp/TacFilter.mli: CEA_WP src/plugins/wp/TacFilter.mli: CEA_WP
src/plugins/wp/TacHavoc.ml: CEA_WP src/plugins/wp/TacHavoc.ml: CEA_WP
src/plugins/wp/TacHavoc.mli: 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.ml: CEA_WP
src/plugins/wp/TacInstance.mli: CEA_WP src/plugins/wp/TacInstance.mli: CEA_WP
src/plugins/wp/TacLemma.ml: CEA_WP src/plugins/wp/TacLemma.ml: CEA_WP
......
...@@ -24,6 +24,9 @@ ...@@ -24,6 +24,9 @@
Plugin WP <next-release> Plugin WP <next-release>
######################### #########################
- WP [2020-11-05] New tactic: Induction
- WP [2020-11-04] Removed option -wp-bits (now always enabled)
######################### #########################
Plugin WP 22.0 (Titanium) Plugin WP 22.0 (Titanium)
######################### #########################
......
...@@ -800,41 +800,40 @@ type l_builtin = { ...@@ -800,41 +800,40 @@ type l_builtin = {
let () = let () =
Context.register Context.register
begin fun () -> begin fun () ->
if Wp_parameters.Bits.get () then begin
begin let mk_builtin n f ?eq ?leq smp = n, { f ; eq; leq; smp } in
let mk_builtin n f ?eq ?leq smp = n, { f ; eq; leq; smp } in
(* From [smp_mk_bit_stdlib], the built-in [f_bit_stdlib] is such that there is
(* From [smp_mk_bit_stdlib], the built-in [f_bit_stdlib] is such that there is no creation of [e_fun f_bit_stdlib args] *)
no creation of [e_fun f_bit_stdlib args] *) let bi_lbit_stdlib = mk_builtin "f_bit_stdlib" f_bit_stdlib smp_mk_bit_stdlib in
let bi_lbit_stdlib = mk_builtin "f_bit_stdlib" f_bit_stdlib smp_mk_bit_stdlib in let bi_lbit = mk_builtin "f_bit" f_bit_positive smp_bitk_positive in
let bi_lbit = mk_builtin "f_bit" f_bit_positive smp_bitk_positive in let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot
let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot (smp1 Integer.lognot) in
(smp1 Integer.lognot) in let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor
let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor (smp2 f_lxor Integer.logxor) in
(smp2 f_lxor Integer.logxor) in let bi_lor = mk_builtin "f_lor" f_lor ~eq:smp_eq_with_lor
let bi_lor = mk_builtin "f_lor" f_lor ~eq:smp_eq_with_lor (smp2 f_lor Integer.logor) in
(smp2 f_lor Integer.logor) in let bi_land = mk_builtin "f_land" f_land ~eq:smp_eq_with_land ~leq:smp_leq_with_land
let bi_land = mk_builtin "f_land" f_land ~eq:smp_eq_with_land ~leq:smp_leq_with_land smp_land in
smp_land in let bi_lsl = mk_builtin "f_lsl" f_lsl ~eq:smp_eq_with_lsl ~leq:smp_leq_with_lsl
let bi_lsl = mk_builtin "f_lsl" f_lsl ~eq:smp_eq_with_lsl ~leq:smp_leq_with_lsl (smp_shift Integer.shift_left) in
(smp_shift Integer.shift_left) in let bi_lsr = mk_builtin "f_lsr" f_lsr ~eq:smp_eq_with_lsr ~leq:smp_leq_with_lsr
let bi_lsr = mk_builtin "f_lsr" f_lsr ~eq:smp_eq_with_lsr ~leq:smp_leq_with_lsr (smp_shift Integer.shift_right) in
(smp_shift Integer.shift_right) in
List.iter
List.iter begin fun (_name, { f; eq; leq; smp }) ->
begin fun (_name, { f; eq; leq; smp }) -> F.set_builtin f smp ;
F.set_builtin f smp ; (match eq with
(match eq with | None -> ()
| None -> () | Some eq -> F.set_builtin_eq f eq);
| Some eq -> F.set_builtin_eq f eq); (match leq with
(match leq with | None -> ()
| None -> () | Some leq -> F.set_builtin_leq f leq)
| Some leq -> F.set_builtin_leq f leq) end
end [bi_lbit_stdlib ; bi_lbit; bi_lnot; bi_lxor; bi_lor; bi_land; bi_lsl; bi_lsr];
[bi_lbit_stdlib ; bi_lbit; bi_lnot; bi_lxor; bi_lor; bi_land; bi_lsl; bi_lsr];
Lang.For_export.set_builtin_eq f_land export_eq_with_land Lang.For_export.set_builtin_eq f_land export_eq_with_land
end end
end end
(* ACSL Semantics *) (* ACSL Semantics *)
......
...@@ -142,7 +142,7 @@ val map_sequence : (pred -> pred) -> sequence -> sequence ...@@ -142,7 +142,7 @@ val map_sequence : (pred -> pred) -> sequence -> sequence
(** Rewrite all root predicates in sequence *) (** Rewrite all root predicates in sequence *)
val map_sequent : (pred -> pred) -> sequent -> sequent 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 val insert : ?at:int -> step -> sequent -> sequent
(** Insert a step in the sequent immediately [at] the specified position. (** Insert a step in the sequent immediately [at] the specified position.
......
...@@ -198,6 +198,7 @@ class mkcomposer ...@@ -198,6 +198,7 @@ class mkcomposer
Wutil.on filter (fun f -> wvalid <- f) ; Wutil.on filter (fun f -> wvalid <- f) ;
Wutil.on range (fun r -> ranged <- r) ; Wutil.on range (fun r -> ranged <- r) ;
ignore vmin ; ignore vmax ; ignore vmin ; ignore vmax ;
self#updated
end end
end end
......
...@@ -85,7 +85,7 @@ PLUGIN_CMO:= \ ...@@ -85,7 +85,7 @@ PLUGIN_CMO:= \
CfgCompiler StmtSemantics \ CfgCompiler StmtSemantics \
VCS script proof wpo wpReport \ VCS script proof wpo wpReport \
Footprint Tactical Strategy \ Footprint Tactical Strategy \
TacSplit TacChoice TacRange \ TacSplit TacChoice TacRange TacInduction \
TacArray TacCompound TacUnfold \ TacArray TacCompound TacUnfold \
TacHavoc TacInstance TacLemma \ TacHavoc TacInstance TacLemma \
TacFilter TacCut WpTac TacNormalForm \ TacFilter TacCut WpTac TacNormalForm \
......
(**************************************************************************)
(* *)
(* 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 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 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 n0) goal_n in
(* Hind: n0 <= i < n *)
let goal_sup =
let hsup = [ F.p_leq n0 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 n0 vn; hind] goal_n in
(* Hind: n < i <= n0 *)
let goal_inf =
let hinf = [ F.p_lt vn vi ; F.p_leq vi n0 ] in
let hind = F.p_forall [i] (F.p_hyps hinf goal_i) in
F.p_hyps [F.p_lt vn n0; hind] goal_n 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.composer ~id:"base"
~title:"Base" ~descr:"Value of base case" ()
class induction =
object(self)
inherit Tactical.make
~id:"Wp.induction"
~title:"Induction"
~descr:"Proof by integer induction"
~params:[pbase]
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) =
begin match self#get_field vbase with
| Empty ->
self#set_field vbase (Tactical.int 0) ;
feedback#update_field vbase
| _ -> ()
end ;
let value = Tactical.selected s in
if F.is_int value then
match self#get_base () with
| Some base -> Applicable(process value base)
| None -> Not_configured
else Not_applicable
end
let tactical = Tactical.export (new induction)
(* -------------------------------------------------------------------------- *)
(**************************************************************************)
(* *)
(* 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
(**************************************************************************)
...@@ -90,7 +90,7 @@ struct ...@@ -90,7 +90,7 @@ struct
(* Authorized written region from an assigns specification *) (* Authorized written region from an assigns specification *)
type effect = { type effect = {
e_pid : P.t ; (* Assign Property *) e_pid : P.t ; (* Assign Property *)
e_kind : a_kind ; (* Requires post effects (in case of loop-assigns) *) e_post : bool ; (* Requires post effects (loop-assigns or post-assigns) *)
e_label : c_label ; (* scope for collection *) e_label : c_label ; (* scope for collection *)
e_valid : L.sigma ; (* sigma where locations are filtered for validity *) e_valid : L.sigma ; (* sigma where locations are filtered for validity *)
e_region : L.region ; (* expected from spec *) e_region : L.region ; (* expected from spec *)
...@@ -444,21 +444,23 @@ struct ...@@ -444,21 +444,23 @@ struct
ainfo.a_assigns ainfo.a_assigns
in match authorized_region with in match authorized_region with
| None -> None | None -> None
| Some region -> Some { | Some region ->
e_pid = pid ; let post = match ainfo.a_kind with
e_kind = ainfo.a_kind ; | LoopAssigns -> true
e_label = from ; | StmtAssigns -> NormAtLabels.has_postassigns ainfo.a_assigns
e_valid = sigma ; in Some {
e_region = region ; e_pid = pid ;
e_warn = Warning.Set.empty ; e_post = post ;
} e_label = from ;
e_valid = sigma ;
e_region = region ;
e_warn = Warning.Set.empty ;
}
let cc_posteffect e vcs = let cc_posteffect e vcs =
match e.e_kind with if not e.e_post then vcs else
| StmtAssigns -> vcs let vc = { empty_vc with vars = L.vars e.e_region } in
| LoopAssigns -> Gmap.add (Gposteffect e.e_pid) (Splitter.singleton vc) vcs
let vc = { empty_vc with vars = L.vars e.e_region } in
Gmap.add (Gposteffect e.e_pid) (Splitter.singleton vc) vcs
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
(* --- WP RULES : adding axioms, hypotheses and goals --- *) (* --- WP RULES : adding axioms, hypotheses and goals --- *)
...@@ -549,14 +551,13 @@ struct ...@@ -549,14 +551,13 @@ struct
vars = xs } vars = xs }
in in
let group = let group =
match e.e_kind with if not e.e_post then
| StmtAssigns -> Splitter.singleton (setup empty_vc)
Splitter.singleton (setup empty_vc) else
| LoopAssigns -> try Splitter.map setup (Gmap.find (Gposteffect e.e_pid) vcs)
try Splitter.map setup (Gmap.find (Gposteffect e.e_pid) vcs) with Not_found ->
with Not_found -> Wp_parameters.fatal "Missing post-effect for %a"
Wp_parameters.fatal "Missing post-effect for %a" WpPropId.pretty e.e_pid
WpPropId.pretty e.e_pid
in in
let target = match sloc with let target = match sloc with
| None -> Gprop e.e_pid | None -> Gprop e.e_pid
......
...@@ -74,6 +74,11 @@ let of_logic = function ...@@ -74,6 +74,11 @@ let of_logic = function
| BuiltinLabel LoopEntry -> loopentry | BuiltinLabel LoopEntry -> loopentry
| StmtLabel s -> stmt !s | StmtLabel s -> stmt !s
let is_post = function
| BuiltinLabel Post -> true
| FormalLabel a -> a = post
| _ -> false
let name = function FormalLabel a -> a | _ -> "" let name = function FormalLabel a -> a | _ -> ""
let lookup labels a = let lookup labels a =
......
...@@ -65,6 +65,9 @@ val of_logic : Cil_types.logic_label -> c_label ...@@ -65,6 +65,9 @@ val of_logic : Cil_types.logic_label -> c_label
labels. Ambiguous labels are: Old, LoopEntry and LoopCurrent, since labels. Ambiguous labels are: Old, LoopEntry and LoopCurrent, since
they points to different program points dependending on the context. *) they points to different program points dependending on the context. *)
val is_post : Cil_types.logic_label -> bool
(** Checks whether the logic-label is [Post] or [to_logic post] *)
val pretty : Format.formatter -> c_label -> unit val pretty : Format.formatter -> c_label -> unit
open Cil_types open Cil_types
......
...@@ -251,26 +251,43 @@ c. Consolidating the Bench. ...@@ -251,26 +251,43 @@ c. Consolidating the Bench.
This mode replays the automated proofs and the interactive ones, re-running Alt-Ergo on every \textsf{WP} goals and every proof tactic sub-goals. The user scripts are never modified — this is a replay mode only. This mode replays the automated proofs and the interactive ones, re-running Alt-Ergo on every \textsf{WP} goals and every proof tactic sub-goals. The user scripts are never modified — this is a replay mode only.
\clearpage \subsection{Strategies}
\subsection{Available Tactics}
Strategies are heuristics that generate a prioritized bunch of tactics to be tried on the current goal.
Few built-in strategies are provided by the \textsf{WP} plug-in ; however, the user can extends the proof editor with
custom ones, as explained in section~\ref{wp-custom-tactics} below.
To run strategies, the interactive proof editor provide a single button \texttt{Strategies} in the tactic panel.
Configure the heuristics you want to include in your try, then click the button. The generated with highest priority is immediately applied. The proof summary now display \texttt{backtrack} buttons revealing proof nodes where alternative tactics are available. You can use those backtracking button to cycle over the generated tactics.
Of course, strategies are meant to be used multiple times, in sequence. Recall that strategies apply highest priority tactic first, on the current goal. When using strategies several times, you shall see several \texttt{backtrack}ing buttons in your proof script. You backtrack from any point at any time.
You shall also alternate strategies \emph{and} manually triggered tactics. Though, strategies are only used to
\emph{infer} or \emph{suggest} interesting tactics to the user. Once your are finished with your proved, only the tactics are saved in the script, not the strategies used to find them. Hence, replaying a script generated with strategies would not involve backtracking any more. The script will directly replay your chosen alternatives.
It is also possible to call strategies from the command line, with option \texttt{-wp-auto}. The strategies are tried up to some depth, and while a limited number of pending goals
remains unproved by \textsf{Qed} or the selected provers. More precisely:
\begin{description}
\item[\tt -wp-auto s,...] applies strategies \texttt{s,...} recursively to unproved goals.
\item[\tt -wp-auto-depth <$n$>] limit recursive application of strategies to depth $n$ (default is 5).
\item[\tt -wp-auto-width <$n$>] limit application of strategies when there is less than $n$ pending goals (default is 10).
\item[\tt -wp-auto-backtrack <$n$>] when the first tried strategies do not close a branch, allows for backtracking
on $n$ alternative strategies. Backtracking is performed on goals which are closed to the root proof obligation, hence
performing a kind of width-first search strategy, which tends to be more efficient in practice.
Backtracking is deactivated by default ($n=0$) and only used when \verb+-wp-auto+ is set.
\end{description}
The name of registered strategies is printed on console by using \texttt{-wp-auto '?'}. Custom strategies can be loaded by plug-ins, see below.
\newcommand{\TACTIC}[2]{#1\quad\quad\triangleright\quad\quad#2} \newcommand{\TACTIC}[2]{#1\quad\quad\triangleright\quad\quad#2}
\subsection{General Tactics}
\paragraph{Absurd} Contradict a Hypothesis\\ \paragraph{Absurd} Contradict a Hypothesis\\
The user can select a hypothesis $H$, and change the goal to $\neg H$: The user can select a hypothesis $H$, and change the goal to $\neg H$:
$$ \TACTIC{\Delta,H\models\,G}{\Delta\models\,\neg H} $$ $$ \TACTIC{\Delta,H\models\,G}{\Delta\models\,\neg H} $$
\paragraph{Array} Decompose array access-update patterns\\
The use select an expression $e\equiv a[k_1\mapsto v][k_2]$. Then:
$$ \TACTIC{\Delta\models\,G}{%
\begin{array}[t]{ll}
\Delta,\,k_1=k_2,\,e = v &\models G \\
\Delta,\,k_1\neq k_2,\,e = a[k_2] &\models G
\end{array}} $$
\paragraph{Choice} Select a Goal Alternative\\ \paragraph{Choice} Select a Goal Alternative\\
When the goal is a disjunction, the user select one alternative and discard the others: When the goal is a disjunction, the user select one alternative and discard the others:
$$ \TACTIC{\Delta\models\,\Gamma,G}{\Delta\models\,G} $$ $$ \TACTIC{\Delta\models\,\Gamma,G}{\Delta\models\,G} $$
...@@ -280,7 +297,6 @@ When the user select an equality between two records, it is decomposed field by ...@@ -280,7 +297,6 @@ When the user select an equality between two records, it is decomposed field by
$$ \TACTIC{ a = b }{ \bigwedge a.f_i = b.f_i } $$ $$ \TACTIC{ a = b }{ \bigwedge a.f_i = b.f_i } $$
\paragraph{Contrapose} Swap and Negate Hypothesis with Conclusion\\ \paragraph{Contrapose} Swap and Negate Hypothesis with Conclusion\\
The user select a hypothesis (typically, a negation) and swap it with the goal. The user select a hypothesis (typically, a negation) and swap it with the goal.
$$ \TACTIC{\Delta,H\models\,G}{\Delta,\neg G\models\,\neg H} $$ $$ \TACTIC{\Delta,H\models\,G}{\Delta,\neg G\models\,\neg H} $$
...@@ -303,14 +319,14 @@ $$\TACTIC{\Delta\models\,G}{% ...@@ -303,14 +319,14 @@ $$\TACTIC{\Delta\models\,G}{%
\Delta,\neg C \models G \Delta,\neg C \models G
\end{array}} $$ \end{array}} $$
\paragraph{Definition} Unfold predicate and logic function definition\\
The user simply select a term $f(e_1,\ldots,e_n)$ or a predicate $P(e_1,\ldots,e_n)$ which is replaced by its definition, when available.
\paragraph{Filter} Erase Hypotheses \\ \paragraph{Filter} Erase Hypotheses \\
The tactic is always applicable. It removes hypotheses from the goal on a variable used basis. When variables are compounds (record and arrays) a finer heuristics is used to detect which parts of the variable is relevant. A transitive closure of dependencies is also used. However, it is always possible that too many hypotheses are removed. The tactic is always applicable. It removes hypotheses from the goal on a variable used basis. When variables are compounds (record and arrays) a finer heuristics is used to detect which parts of the variable is relevant. A transitive closure of dependencies is also used. However, it is always possible that too many hypotheses are removed.
The tactic also have a variant where only hypotheses \emph{not relevant} to the goal are retained. This is useful to find absurd hypotheses that are completely disjoint from the goal. The tactic also have a variant where only hypotheses \emph{not relevant} to the goal are retained. This is useful to find absurd hypotheses that are completely disjoint from the goal.
\paragraph{Havoc} Go Through Assigns \\
This is a variant of the \texttt{Lemma} tactic dedicated to \texttt{Havoc} predicate generate by complex assigns clause. The user select an address, and if the address is not assigned by the \texttt{Havoc} clause, the memory at this address is unchanged.
\paragraph{Instance} Instantiate properties\\ \paragraph{Instance} Instantiate properties\\
The user selects a hypothesis with one or several $\forall$ quantifiers, or an $\exists$ quantified goal. Then, with the composer, the use choose to instantiate one or several of the quantified parameters. In case of $\forall$ quantifier over integer, a range of values can be instantiated instead. The user selects a hypothesis with one or several $\forall$ quantifiers, or an $\exists$ quantified goal. Then, with the composer, the use choose to instantiate one or several of the quantified parameters. In case of $\forall$ quantifier over integer, a range of values can be instantiated instead.
...@@ -323,22 +339,11 @@ $$\TACTIC{\Delta,\,\forall x\, P(x)\models G}{\Delta,P(n)\ldots P(m)\models G}$$ ...@@ -323,22 +339,11 @@ $$\TACTIC{\Delta,\,\forall x\, P(x)\models G}{\Delta,P(n)\ldots P(m)\models G}$$
When instantiating a goal with an expression $e$: When instantiating a goal with an expression $e$:
$$\TACTIC{\Delta\models \exists x\,G(x)}{\Delta\models G(e)}$$ $$\TACTIC{\Delta\models \exists x\,G(x)}{\Delta\models G(e)}$$
\paragraph{Lemma} Search \& Instantiate Lemma\\
The user start by selecting a term in the goal. Then, the search button in the tactic panel will display a list of lemma related to the term. Then, he can instantiate the parameters of the lemma, like with the Instance tactic.
\paragraph{Intuition} Decompose with Conjunctive/Disjunctive Normal Form\\ \paragraph{Intuition} Decompose with Conjunctive/Disjunctive Normal Form\\
The user can select a hypothesis or a goal with nested conjunctions and disjunctions. The tactics then computes the conjunctive or disjunctive normal form of the selection and split the goal accordingly. The user can select a hypothesis or a goal with nested conjunctions and disjunctions. The tactics then computes the conjunctive or disjunctive normal form of the selection and split the goal accordingly.
\paragraph{Range} Enumerate a range of values for an integer term\\ \paragraph{Lemma} Search \& Instantiate Lemma\\
The user select any integer expression $e$ in the proof, and a range of numerical values $a\ldots b$. The proof goes by case for each $e=a\ldots e=b$, plus the side cases $e<a$ and $e>b$: The user start by selecting a term in the goal. Then, the search button in the tactic panel will display a list of lemma related to the term. Then, he can instantiate the parameters of the lemma, like with the Instance tactic.
$$\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{ll}
\Delta,e<a &\models G \\
\Delta,e=a &\models G \\
&\vdots \\
\Delta,e=b &\models G \\
\Delta,e>b &\models G
\end{array}} $$
\paragraph{Rewrite} Replace Terms\\ \paragraph{Rewrite} Replace Terms\\
This tactic uses an equality in a hypothesis to replace each occurrence of term by another one. This tactic uses an equality in a hypothesis to replace each occurrence of term by another one.
...@@ -348,9 +353,6 @@ The original equality hypothesis is removed from the goal. ...@@ -348,9 +353,6 @@ The original equality hypothesis is removed from the goal.
$$\TACTIC{\Delta,a=b\models\,G}{\Delta[a\leftarrow b]\models\,G[a\leftarrow b]}$$ $$\TACTIC{\Delta,a=b\models\,G}{\Delta[a\leftarrow b]\models\,G[a\leftarrow b]}$$
\paragraph{Separated} Expand Separation Cases\\
This tactic decompose a \texttt{separated}$(a,n,b,m)$ predicate into its four base cases: $a$ and $b$ have different bases, $a+n \leq b$, $b+m \leq a$, and $a[0..n-1]$ and $b[0..m-1]$ overlaps. The regions are separated in the first three cases, and not separated in the overlapping case. This is kind of normal disjunctive form of the separation clause.
\paragraph{Split} Decompose Logical Connectives and Conditionals\\ \paragraph{Split} Decompose Logical Connectives and Conditionals\\
This is the most versatile available tactic. It decompose merely any logical operator following the sequent calculus rules. Typically: This is the most versatile available tactic. It decompose merely any logical operator following the sequent calculus rules. Typically:
...@@ -376,7 +378,8 @@ When the user selects a arbitrary boolean expression $e$, the tactic is similar ...@@ -376,7 +378,8 @@ When the user selects a arbitrary boolean expression $e$, the tactic is similar
\Delta,\neg e\models G \Delta,\neg e\models G
\end{array}} \] \end{array}} \]
Finally, when the user select a arithmetic comparison over $a$ and $b$, the tactics makes a split over $a=b$, $a<b$ and $a>b$: Finally, when the user select a arithmetic comparison over $a$ and $b$,
the tactics makes a split over $a=b$, $a<b$ and $a>b$:
\[\TACTIC{\Delta\models\,G}{% \[\TACTIC{\Delta\models\,G}{%
\begin{array}[t]{ll} \begin{array}[t]{ll}
\Delta,a<b&\models G \\ \Delta,a<b&\models G \\
...@@ -384,49 +387,7 @@ Finally, when the user select a arithmetic comparison over $a$ and $b$, the tact ...@@ -384,49 +387,7 @@ Finally, when the user select a arithmetic comparison over $a$ and $b$, the tact
\Delta,a>b&\models G \Delta,a>b&\models G
\end{array}} \] \end{array}} \]
\paragraph{Definition} Unfold predicate and logic function definition\\ \subsection{Integers \& Bit-wised Tactics}
The user simply select a term $f(e_1,\ldots,e_n)$ or a predicate $P(e_1,\ldots,e_n)$ which is replaced by its definition, when available.
\paragraph{Bitwise} Decompose equalities over $N$-bits\\
The use selects an integer equality and a number of bits.
Providing the two members of the equality are in range $0..2^N-1$,
the equality is decomposed into $N$ bit-tests equalities:
\[\TACTIC{\Delta\models G}{%
\begin{array}[t]{rcl}
\Delta\phantom{)} &\models & 0 \leq a,b < 2^N \\
\sigma(\Delta) & \models & \sigma(G)