Difference between pages "Rodin Platform 2.4 Release Notes" and "Rodin Proof Tactics"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Nicolas
 
imported>Son
m
 
Line 1: Line 1:
{{TOCright}}
+
This page contains descriptions of the available proof tactics within the RODIN Platform.
  
== What's New in Rodin 2.4? ==
+
For each tactic, the descriptions is as follows:
  
From this release on, the Rodin platform is also provided for 64-bit Windows and Linux OSes.
+
* '''Description''': A high-level description of the tactic. This will be the description appeared in the RODIN Platform preferences.
  
* Modelling
+
* '''Additional details''': (Optional) Details explanation of the tactic.
: '''[[Rodin Editor]]''': the Rodin Editor is now part of the Core Platform as the default editor for machines and contexts. The older structured editor is still there though.
 
  
* Building
+
* '''ID''': An unique ID associated with the tactic.
: '''proper build''': the builder now systematically deletes temporary files (*.bcm_tmp and alike); these files were a source of many troubles in further builds
 
  
* Proving
+
* '''Auto-tactic''': ''No'': the tactic cannot be added as an auto-tactic. ''Yes'': the tactic can be added as an auto-tactic. ''Default'': the tactic is a default auto-tactic.
:'''Type Environment View''': this new view shows the type environment for the current node of the proof (free identifiers and their type). It is accessible through "Window > Show View > Type Environment"
 
:'''Proof Simplification''': once proofs are complete, they can be automatically simplified, by removing unneeded steps (mostly: unused inference by post tactic); this feature is however disabled by default, you can enable it by "Window > Preferences > Event-B > Sequent Prover > Simplify complete proofs when saving"
 
:'''Auto Tactic''': a new tactic combinator 'Attempt after Lasso' is available in Auto Tactic profile editor.
 
:'''Import/export profiles''': from the tactic preference page, profiles can be exported and imported to/from the file system
 
:'''Preference Scope''': the shorcut to Auto Tactic Preference in Proof Control now indicates whether the current project has specific tactic settings or uses the global workspace settings
 
  
* Changes for plugin-developers
+
* '''[[The Proving Perspective (Rodin User Manual)#The Automatic Post-tactic|Post-tactic]]''': ''No'': the tactic cannot be added as a post-tactic. ''Yes'': the tactic can be added as a post-tactic. ''Default'': the tactic is a default post-tactic.
:switch to Eclipse 3.7.1 (no impact expected)
 
:'''new XProver API''': external prover providers can now extend XProverReasoner2 along with the ISimpleSequent framework. ProcessMonitor also provides a ''wrapCommand'' method to properly handle external prover process interruption.
 
  
== Requirements - Compatibility ==
+
* '''Preference display''': (Optional) If the tactic can be used as an auto-tactic or a post-tactic, information on how the tactic is displayed in the auto-tactic preference or the post-tactic preference.
  
* Configuration
+
* '''Interactive''': ''No'': the tactic cannot be invoked interactively from the [[The Proving Perspective (Rodin User Manual)|proving interface]]. ''Global'': The tactic can be invoked interactively from the [[The Proving Perspective (Rodin User Manual)#The Proof Control Window|Proof Control View]]. ''Goal'': The tactic can be invoked from the [[The Proving Perspective (Rodin User Manual)#Goal and Selected Hypotheses|Goal view]]. ''Hypothesis'': The tactic can be invoked from the [[The Proving Perspective (Rodin User Manual)#Goal and Selected Hypotheses| Hypothesis view]].  If the tactic can be invoked interactively (i.e. either ''Global'', ''Goal'' or ''Hypothesis''), more information about how this could be done will be given. Note that since the '''Post-tactics''' can be launched manually, any tactics that can be included in the post-tactic in principle can be invoked interactively via the post-tactic. Here ''No'' only means that there is no separate invocation for this specific tactic.
** ? Only a '''32-bit''' version of the Rodin platform is provided for '''PC'''s ?
 
** Only a '''64-bit''' version of the Rodin platform is provided for '''MAC'''
 
  
* You need to have a Java JRE (6.0 or later) installed on your computer. The Rodin product will not work with a previous version.
+
* '''Proving interface display''': Example(s) on how applications of this tactic can be seen from the [[The Proving Perspective (Rodin User Manual)|proving interface]] of the RODIN Platform.
  
* To enhance your proving experience, the eclipse font settings (size, aspect...) are available from the preferences (General > Appearance > Colors and Fonts > Rodin). These settings allow you to modify the properties set on the Event-B Keyboard Text Font which is used in many views of the Proving UI. However, to enjoy these functionnalities, you need to install the Brave Sans Mono font on your system. You can download this font from the link [http://sourceforge.net/projects/rodin-b-sharp/files/Font_%20Brave%20Sans%20Mono/0.12/ here].
+
== True Goal ==
 +
* '''Description''': Discharges any sequent whose goal is '⊤' (logical true).
  
* Linux: the internal browser does not work with xulrunner-2.0 (for instance, it causes the welcome page to display a link instead of a html page); xulrunner-1.9.x must be installed.
+
* '''ID''': org.eventb.core.seqprover.trueGoalTac
  
== Installing ==
+
* '''Auto-tactic''': ''Default''
  
=== Upgrading from Rodin 2.3.x ===
+
* '''Post-tactic''': ''Default''
  
Use rodin-2.4-repo.zip:
+
* '''Preference display''': True Goal (Discharge)
  
* download archive [http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.4/rodin-2.4-repo.zip/download rodin-2.4-repo.zip]
+
* '''Interactive''': ''No''
* launch Rodin 2.3.x
 
* Help > Install New Software... > Add... > enter a name (for instance "Rodin 2.4") then
 
: Archive... > select the rodin-2.4-repo.zip archive
 
: Mac users may have to use Local... then point to archive root directory, in case the archive was automatically unzipped
 
* set options in the bottom of the page:
 
:* check
 
:** "Show only the latest versions of available software"
 
:** "Hide items that are already installed"
 
:* uncheck
 
:** "Group items by category"
 
:** "Contact all update sites..."
 
: the central area should now list many entries
 
* select "Rodin Platform", click "Next"
 
: a message informs "Your original request has been modified.  See the details."
 
: "Rodin Platform" is already installed, so an update will be performed instead.
 
* click Next, accept license, finish and restart
 
  
=== Downloading ===
+
* '''Proving interface display''': ⊤ goal
  
[http://sourceforge.net/projects/rodin-b-sharp/files/Core_Rodin_Platform/2.4/ Download Rodin 2.4 now !]
+
[[Image:TrueGoalExp1.png]]
  
== External plug-ins ==
+
== False Hypothesis ==
 +
* '''Description''': Discharges any sequent containing a '⊥' hypothesis
  
{{:Rodin_Platform_2.4_External_Plug-ins}}
+
* '''ID''': org.eventb.core.seqprover.falseHypTac
  
== Fixed Bugs and Implemented Feature Requests ==
+
* '''Auto-tactic''': ''Default''
  
 +
* '''Post-tactic''': ''Default''
  
== Known Issues ==
+
* '''Preference display''': False Hypothesis (Discharge)
  
[https://sourceforge.net/tracker/?group_id=108850&atid=651669&status=1 Bugs on SourceForge]
+
* '''Interactive''': ''No''
  
ClassCastException when uninstalling a feature: this is a known eclipse bug [https://bugs.eclipse.org/bugs/show_bug.cgi?id=348986]
+
* '''Proving interface display''': ⊥ hyp
  
== Disclaimer ==
+
[[Image: FalseHypExp1.png]]
Since Rodin is continuously maintained, several unsoundness bugs which have been encountered were investigated and fixed. However, despite the total commitment of our teams to insure the soundness of the platform, some unexpected and unknown soundness issues could remain. We would be grateful if you would report these issues to the [mailto:rodin-b-sharp-devel@lists.sourceforge.net development mailing list].
 
  
== About ==
+
== Goal in Hypotheses ==
Rodin Platform up to r14093.<br>
+
* '''Description''': Discharges any sequent whose goal is contained in its hypotheses
Developer Release date : 2012/01/12.<br>
 
User Release date : 2012/01/31.
 
  
[[Category:Rodin Platform Release Notes]]
+
* '''ID''': org.eventb.core.seqprover.goalInHypTac
 +
 
 +
* '''Auto-tactic''': ''Default''
 +
 
 +
* '''Post-tactic''': ''Default''
 +
 
 +
* '''Preference display''': Goal in Hypotheses (Discharge)
 +
 
 +
* '''Interactive''': ''No''
 +
 
 +
* '''Proving interface display''': hyp
 +
 
 +
[[Image: GoalInHypExp1.png]]
 +
 
 +
== Goal Disjunct in Hypothesis ==
 +
* '''Description''': Discharges any sequent whose goal is a disjunction and one of whose disjuncts is present in the hypotheses.
 +
 
 +
* '''ID''': org.eventb.core.seqprover.goalDisjInHypTac
 +
 
 +
* '''Auto-tactic''': ''No''
 +
 
 +
* '''Post-tactic''': ''Default''
 +
 
 +
* '''Preference display''': Goal Disjunct in Hypotheses (Discharge)
 +
 
 +
* '''Interactive''': ''No''
 +
 
 +
* '''Proving interface display''': ∨ goal in hyp
 +
 
 +
[[Image: GoalDisjInHypExp1.png]]
 +
 
 +
== Functional Goal ==
 +
* '''Description''': Tries to discharge a sequent whose goal states that an expression is a function (i.e. f ∈ T1 ⇸ T2, where T1 and T2 are type expressions).
 +
 
 +
* '''Additional details''': The sequent is discharged if there is a hypothesis specifying that f is a function of any kind (i.e. partial function, total function, partial injection, total injection, partial surjection,  total surjection, bijection). More information about type expressions in Event-B is in the [[FAQ#What are type expressions in Event-B?|FAQ]] page.
 +
 
 +
* '''ID''': org.eventb.core.seqprover.funGoalTac
 +
 
 +
* '''Auto-tactic''': ''Default''
 +
 
 +
* '''Post-tactic''': ''Default''
 +
 
 +
* '''Preference display''': Functional Goal (Discharge)
 +
 
 +
* '''Interactive''': ''No''
 +
 
 +
* '''Proving interface display''': functional goal
 +
 
 +
[[Image:FunctionalGoalExp1.png]]
 +
 
 +
== Simplification Rewriter ==
 +
* '''Description''': Tries to simplify all predicates in a sequent using pre-defined simplification rewriting rules.
 +
 
 +
* '''Additional details''': The list of rewriting rules are in the following page [[All Rewrite Rules | http://wiki.event-b.org/index.php/All_Rewrite_Rules]], which are marked as ''Automatic''.
 +
 
 +
* '''ID''': org.eventb.core.seqprover.autoRewriteTac
 +
 
 +
* '''Auto-tactic''': ''Default''
 +
 
 +
* '''Post-tactic''': ''Default''
 +
 
 +
* '''Preference display''': Simplification Rewriter (Simplify)
 +
 
 +
* '''Interactive''': ''No''
 +
 
 +
* '''Proving interface display''': simplification rewrites
 +
 
 +
The example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic.  There are 3 rewritings have been done as follows.
 +
 
 +
<math>
 +
\begin{array}{rcl}
 +
a + 0  & \Longrightarrow & a \\
 +
a = a & \Longrightarrow & \btrue \\
 +
c * 1 & \Longrightarrow & c \\
 +
\end{array}
 +
</math>
 +
 
 +
Note that <math>\btrue</math> hypothesis is always ''dropped'' in the RODIN Platform.
 +
 
 +
Before [[Image:SimplifcationRewritesExp1.png]]
 +
 
 +
After [[Image:SimplifcationRewritesExp2.png]]
 +
 
 +
== Type Rewriter ==
 +
* '''Description''': Simplifies predicates containing type expressions such as E ∈ T to ⊤ and T = ∅ to ⊥.
 +
 
 +
* '''Additional details''': More information about type expressions in Event-B is in the [[FAQ#What are type expressions in Event-B?|FAQ]] page.
 +
 
 +
* '''ID''': org.eventb.core.seqprover.typeRewriteTac
 +
 
 +
* '''Auto-tactic''': ''Default''
 +
 
 +
* '''Post-tactic''': ''Default''
 +
 
 +
* '''Preference display''': Type Rewriter (Simplify)
 +
 
 +
* '''Interactive''': ''No''
 +
 
 +
* '''Proving interface display''': type rewrites
 +
 
 +
The example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic.
 +
 
 +
Before [[Image: TypeRewritesExp1.png]]
 +
 
 +
After [[Image: TypeRewritesExp2.png]]
 +
 
 +
== Implication Goal ==
 +
* '''Description''': Simplifies any sequent with an implicative goal by adding the left hand side of the implication to the hypotheses and making its right hand side the new goal.
 +
 
 +
* '''ID''': org.eventb.core.seqprover.impGoalTac
 +
 
 +
* '''Auto-tactic''': ''No''
 +
 
 +
* '''Post-tactic''': ''Default''
 +
 
 +
* '''Preference display''': Implicative Goal (Simplify)
 +
 
 +
* '''Interactive''': ''Goal''. The <math>\limp</math> symbol in the implicative goal is <font color=red>''redden''</font>. When the mouse hovers the red symbol, the label of the tactic in the context menu is ''Deduction''.
 +
 
 +
[[Image: ImpGoalInteractive1.png]]
 +
 
 +
* '''Proving interface display''': ⇒ goal
 +
 
 +
The example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic.
 +
 
 +
Before [[Image: ImpGoalExp1.png]]
 +
 
 +
After [[Image: ImpGoalExp2.png]]
 +
 
 +
== For-all Goal ==
 +
* '''Description''': Simplifies any sequent with a universally quantified goal by freeing all its bound variables.
 +
 
 +
* '''Additional details''': The bound variables will be renaming accordingly to avoid name collision.
 +
 
 +
* '''ID''': org.eventb.core.seqprover.forallGoalTac
 +
 
 +
* '''Auto-tactic''': ''No''
 +
 
 +
* '''Post-tactic''': ''Yes''
 +
 
 +
* '''Preference display''': For-all Goal (Simplify)
 +
 
 +
* '''Interactive''': ''Goal''. The  symbol <math>\forall</math> in the universal quantified goal is <font color=red>''redden''</font>. When the mouse hovers the red symbol, the label of the tactic in the context menu is ''Forall instantiation''.
 +
 
 +
[[Image: ForallGoalInteractive1.png]]
 +
 
 +
* '''Proving interface display''': ∀ goal (frees ''list-of-bounded-identifiers'')
 +
 
 +
The first example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic.  There is no renaming of the bound variable.
 +
 
 +
Before [[Image: ForallGoalExp1.png]]
 +
 
 +
After [[Image: ForallGoalExp2.png]]
 +
 
 +
The second example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic. The bound variable <math>x</math> is not renamed, but the bound variable <math>z</math> is renamed to <math>z0</math> to avoid capture of the existing variable <math>z</math>.
 +
 
 +
Before [[Image: ForallGoalExp3.png]]
 +
 
 +
After [[Image: ForallGoalExp4.png]]
 +
 
 +
== Exists Hypothesis ==
 +
* '''Description''': In automatic mode (as an auto-tactic or post-tactic), this tactic simplifies any sequent containing existentially quantified hypotheses by freeing their bound variables. In interactive mode, only the selected hypothesis is simplified by freeing its bound variables.
 +
 
 +
* '''Additional details''': The bound variables will be renaming if necessary to avoid name collision. After freeing their bound variables, if the resulting predicate is a conjunction then it is split into several hypotheses.
 +
 
 +
* '''ID''': org.eventb.core.seqprover.existHypTac
 +
 
 +
* '''Auto-tactic''': ''No''
 +
 
 +
* '''Post-tactic''': ''Default''
 +
 
 +
* '''Preference display''': Exists Hypotheses (Simplify)
 +
 
 +
* '''Interactive''': ''Hypothesis''. The symbol <math>\exists</math> in the existential quantified hypothesis is redden. When the mouse hovers the red symbol, the label of the tactic in the context menu is ''Free existential variables''.
 +
 
 +
[[Image: ExistsHypInteractive1.png]]
 +
 
 +
* '''Proving interface display''':
 +
 
 +
The first example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic. There is no renaming of the bound variable.
 +
 
 +
Before [[Image: ExistHypExp1.png]]
 +
 
 +
After [[Image: ExistHypExp2.png]]
 +
 
 +
The second example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic. The bound variable x is not renamed, but the bound variable z is renamed to z0 to avoid capture of the existing variable z.
 +
 
 +
Before [[Image: ExistHypExp3.png]]
 +
 
 +
After [[Image: ExistHypExp4.png]]
 +
 
 +
== Find Contradictory Hypothesis ==
 +
* '''Description''': Discharges a sequent by finding contradictory hypotheses, i.e. <math>P</math> and <math>\neg P </math>.
 +
 
 +
* '''Additional details''': This tactic tries to find a contradiction using each selected hypothesis that is a negation.
 +
 
 +
* '''ID''': org.eventb.core.seqprover.findContrHypsTac
 +
 
 +
* '''Auto-tactic''': ''Default''
 +
 
 +
* '''Post-tactic''': ''Default''
 +
 
 +
* '''Preference display''': Find Contradictory Hypotheses (Discharge)
 +
 
 +
* '''Interactive''': ''No''
 +
 
 +
* '''Proving interface display''': ct in hyps (''the negated hypothesis'')
 +
 
 +
[[Image: FindContrHypsExp1.png]]
 +
 
 +
== Use Equality Hypothesis ==
 +
* '''Description''': Simplifies a sequent by rewriting all selected hypotheses and the goal using a (selected) hypothesis that is an equality between a free variable and an expression that does not contain the free variable. The used equality remains in the selected hypotheses to be used again.
 +
 
 +
* '''Additional details''': Each application of the tactic take only one equality hypothesis into account. If there are several equality hypotheses, they require several applications of the tactic. Moreover, in the case where there are several equality hypotheses, the choice of which hypothesis will be chosen is non-deterministic.  This tactic behaves as [[#Use Equality Hypothesis from Left to Right]] or [[#Use Equality Hypothesis from Right to Left]] depending on if the free variable is on the left or on the right of the equality.
 +
 
 +
* '''ID''': org.eventb.core.seqprover.eqHypTac
 +
 
 +
* '''Auto-tactic''': ''Default''
 +
 
 +
* '''Post-tactic''': ''Default''
 +
 
 +
* '''Preference display'': Use Equals Hypotheses (Simplify)
 +
 
 +
* '''Interactive''': ''Hypothesis''. See [[#Use Equality Hypothesis from Left to Right]] and [[#Use Equality Hypothesis from Right to Left]]
 +
 
 +
* '''Proving interface display''': eh (''the equal hypothesis'') in the case where the free variable is on the left-hand side or he (''the equal hypothesis'') in the case where the free variable is on the right-hand side.
 +
 
 +
The  example below shows the screen-shots of the step before the application of the tactic, the step after the first application of the tactic with hypothesis <math>x = y + 1</math> and the step just after the second application of the tactic with hypothesis <math>1 = y</math>.
 +
 
 +
Before [[Image:UseEqualityHypExp1.png]]
 +
 
 +
After the first application [[Image:UseEqualityHypExp2.png]]
 +
 
 +
After the second application [[Image:UseEqualityHypExp3.png]]
 +
 
 +
== Use Equality Hypothesis from Left to Right ==
 +
 
 +
* '''Description''': Rewriting all selected hypotheses and the goal using a (selected) hypothesis that is an equality between two expressions. The used equality remains in the selected hypotheses to be used again.
 +
 
 +
* '''ID''':
 +
 
 +
* '''Auto-tactic''': See [[#Use Equality Hypothesis]]
 +
 
 +
* '''Post-tactic''': See [[#Use Equality Hypothesis]]
 +
 
 +
* '''Interactive''': ''Hypothesis''
 +
 
 +
* '''Proving interface display''':
 +
 
 +
== Shrink Implicative Hypothesis ==
 +
* '''Description''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== Shrink Enumerated Set ==
 +
* '''Description''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== Implicative Hypothesis with Conjunctive RHS ==
 +
* '''Description''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== Implicative Hypothesis with Disjunctive LHS ==
 +
* '''Description''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== Conjunctive Goal ==
 +
* '''Description''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== Clarify Goal ==
 +
* '''Description''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== Functional Overriding in Goal ==
 +
* '''Description''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== Functional Overriding in Hypothesis ==
 +
* '''Description''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== Partition Rewriter ==
 +
* '''Description''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== One-Point Rule in Goal ==
 +
* '''Description''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== One-Point Rule in Hypothesis ==
 +
* '''Description''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== Bounded Goal with Finite Hypothesis ==
 +
* '''Description''': TODO
 +
 
 +
* '''ID''': TODO
 +
 
 +
* '''Display''': TODO
 +
 
 +
* '''Auto-tactic''': TODO
 +
 
 +
* '''Post-tactic''': TODO
 +
 
 +
* '''Interactive''': TODO
 +
 
 +
* '''Example''': TODO
 +
 
 +
== Falsify Goal ==
 +
 
 +
== conjI ==
 +
 
 +
== allI ==
 +
 
 +
== exI ==
 +
 
 +
== Remove Negation ==
 +
 
 +
== Review ==
 +
 
 +
== Proof by cases ==
 +
 
 +
== Add Hypothesis ==
 +
 
 +
== Abstract Expression ==
 +
 
 +
== Automatic Prover ==
 +
 
 +
== Post tactic ==
 +
 
 +
== Lasoo ==
 +
 
 +
== Back Tracking ==
 +
 
 +
== Prune ==
 +
 
 +
== Search Hypothesis ==
 +
 
 +
== Cache Hypothesis ==
 +
 
 +
== Previous ==
 +
 
 +
== Next ==
 +
 
 +
== Information ==
 +
 
 +
== Falsify Hypothesis ==
 +
 
 +
== Modus Ponens ==
 +
 
 +
== conjE ==
 +
 
 +
== disjE ==
 +
 
 +
== allE ==
 +
 
 +
== exE ==
 +
 
 +
 
 +
 
 +
== Double Implication Hypothesis ==
 +
 
 +
== cont Implication Hypothesis ==
 +
 
 +
== Functional Overriding ==
 +
 
 +
 
 +
 
 +
== Modus Tollens ==
 +
 
 +
== Remove Membership ==
 +
 
 +
== Remove Inclusion ==
 +
 
 +
== Remove Strict-Inclusion ==
 +
 
 +
== Inclusion Set Minus Right ==
 +
 
 +
== Remove Inclusion Universal ==
 +
 
 +
== Implication Introduction ==
 +
 
 +
== Disjunction to Implication ==
 +
 
 +
== Forall Modus Ponens ==
 +
 
 +
== Next Pending Sub-goal ==
 +
 
 +
== Next Reviewed Sub-goal ==
 +
 
 +
== impAndHyp ==
 +
 
 +
== impAndGoal ==
 +
 
 +
== impOrHyp ==
 +
 
 +
== impOrGoal ==
 +
 
 +
== relImgUnionRight ==
 +
 
 +
== relImgUnionLeft ==
 +
 
 +
== Set Equality ==
 +
 
 +
== Equivalent ==
 +
 
 +
== Functional Intersection Image ==
 +
 
 +
== Functional Set Minus Image ==
 +
 
 +
== Functional Singleton Image ==
 +
 
 +
== Converse Relation ==
 +
 
 +
== Domain Distribution to the Left ==
 +
 
 +
== Domain Distribution to the Right ==
 +
 
 +
== Range Distribution to the Left ==
 +
 
 +
== Range Distribution to the Right ==
 +
 
 +
== Set Minus ==
 +
 
 +
== Conjunction and Disjunction Distribution ==
 +
 
 +
== Union Conjunction Distribution ==
 +
 
 +
== compUnionDist ==
 +
 
 +
== Domain/Range Union Distribution ==
 +
 
 +
== Relational Overriding ==
 +
 
 +
== Composition Image ==
 +
 
 +
== Domain Composition ==
 +
 
 +
== Range Composition ==
 +
 
 +
== Functional Composition Image ==
 +
 
 +
== Finite Set in Goal ==
 +
 
 +
== Finite Intersection in Goal ==
 +
 
 +
== Finite Set Minus in Goal ==
 +
 
 +
== Finite Relation in Goal ==
 +
 
 +
== Finite Relation Image in Goal ==
 +
 
 +
== Finite Domain in Goal ==
 +
 
 +
== Finite Range in Goal ==
 +
 
 +
== Finite Function in Goal ==
 +
 
 +
== Finite Function Converse in Goal ==
 +
 
 +
== Finite Functional Relational Image in Goal ==
 +
 
 +
== Finite Functional Range in Goal ==
 +
 
 +
== Finite Functional Domain in Goal ==
 +
 
 +
== Finite Minimum in Goal ==
 +
 
 +
== Finite Maximum in Goal ==
 +
 
 +
== Finite Negative in Goal ==
 +
 
 +
== Finite Positive in Goal ==
 +
 
 +
== Cardinality Comparison in Goal ==
 +
 
 +
== Cardinality Up to ==
 +
 
 +
== Partition Rewrite ==
 +
 
 +
== Arithmetic Rewrite ==
 +
 
 +
== Total Domain in Hypothesis / Goal ==

Revision as of 16:10, 10 March 2010

This page contains descriptions of the available proof tactics within the RODIN Platform.

For each tactic, the descriptions is as follows:

  • Description: A high-level description of the tactic. This will be the description appeared in the RODIN Platform preferences.
  • Additional details: (Optional) Details explanation of the tactic.
  • ID: An unique ID associated with the tactic.
  • Auto-tactic: No: the tactic cannot be added as an auto-tactic. Yes: the tactic can be added as an auto-tactic. Default: the tactic is a default auto-tactic.
  • Post-tactic: No: the tactic cannot be added as a post-tactic. Yes: the tactic can be added as a post-tactic. Default: the tactic is a default post-tactic.
  • Preference display: (Optional) If the tactic can be used as an auto-tactic or a post-tactic, information on how the tactic is displayed in the auto-tactic preference or the post-tactic preference.
  • Interactive: No: the tactic cannot be invoked interactively from the proving interface. Global: The tactic can be invoked interactively from the Proof Control View. Goal: The tactic can be invoked from the Goal view. Hypothesis: The tactic can be invoked from the Hypothesis view. If the tactic can be invoked interactively (i.e. either Global, Goal or Hypothesis), more information about how this could be done will be given. Note that since the Post-tactics can be launched manually, any tactics that can be included in the post-tactic in principle can be invoked interactively via the post-tactic. Here No only means that there is no separate invocation for this specific tactic.
  • Proving interface display: Example(s) on how applications of this tactic can be seen from the proving interface of the RODIN Platform.

Contents

True Goal

  • Description: Discharges any sequent whose goal is '⊤' (logical true).
  • ID: org.eventb.core.seqprover.trueGoalTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • Preference display: True Goal (Discharge)
  • Interactive: No
  • Proving interface display: ⊤ goal

TrueGoalExp1.png

False Hypothesis

  • Description: Discharges any sequent containing a '⊥' hypothesis
  • ID: org.eventb.core.seqprover.falseHypTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • Preference display: False Hypothesis (Discharge)
  • Interactive: No
  • Proving interface display: ⊥ hyp

FalseHypExp1.png

Goal in Hypotheses

  • Description: Discharges any sequent whose goal is contained in its hypotheses
  • ID: org.eventb.core.seqprover.goalInHypTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • Preference display: Goal in Hypotheses (Discharge)
  • Interactive: No
  • Proving interface display: hyp

GoalInHypExp1.png

Goal Disjunct in Hypothesis

  • Description: Discharges any sequent whose goal is a disjunction and one of whose disjuncts is present in the hypotheses.
  • ID: org.eventb.core.seqprover.goalDisjInHypTac
  • Auto-tactic: No
  • Post-tactic: Default
  • Preference display: Goal Disjunct in Hypotheses (Discharge)
  • Interactive: No
  • Proving interface display: ∨ goal in hyp

GoalDisjInHypExp1.png

Functional Goal

  • Description: Tries to discharge a sequent whose goal states that an expression is a function (i.e. f ∈ T1 ⇸ T2, where T1 and T2 are type expressions).
  • Additional details: The sequent is discharged if there is a hypothesis specifying that f is a function of any kind (i.e. partial function, total function, partial injection, total injection, partial surjection, total surjection, bijection). More information about type expressions in Event-B is in the FAQ page.
  • ID: org.eventb.core.seqprover.funGoalTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • Preference display: Functional Goal (Discharge)
  • Interactive: No
  • Proving interface display: functional goal

FunctionalGoalExp1.png

Simplification Rewriter

  • Description: Tries to simplify all predicates in a sequent using pre-defined simplification rewriting rules.
  • ID: org.eventb.core.seqprover.autoRewriteTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • Preference display: Simplification Rewriter (Simplify)
  • Interactive: No
  • Proving interface display: simplification rewrites

The example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic. There are 3 rewritings have been done as follows.


\begin{array}{rcl}
 a + 0  & \Longrightarrow & a \\
 a = a & \Longrightarrow & \btrue \\
 c * 1 & \Longrightarrow & c \\
\end{array}

Note that \btrue hypothesis is always dropped in the RODIN Platform.

Before SimplifcationRewritesExp1.png

After SimplifcationRewritesExp2.png

Type Rewriter

  • Description: Simplifies predicates containing type expressions such as E ∈ T to ⊤ and T = ∅ to ⊥.
  • Additional details: More information about type expressions in Event-B is in the FAQ page.
  • ID: org.eventb.core.seqprover.typeRewriteTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • Preference display: Type Rewriter (Simplify)
  • Interactive: No
  • Proving interface display: type rewrites

The example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic.

Before TypeRewritesExp1.png

After TypeRewritesExp2.png

Implication Goal

  • Description: Simplifies any sequent with an implicative goal by adding the left hand side of the implication to the hypotheses and making its right hand side the new goal.
  • ID: org.eventb.core.seqprover.impGoalTac
  • Auto-tactic: No
  • Post-tactic: Default
  • Preference display: Implicative Goal (Simplify)
  • Interactive: Goal. The \limp symbol in the implicative goal is redden. When the mouse hovers the red symbol, the label of the tactic in the context menu is Deduction.

ImpGoalInteractive1.png

  • Proving interface display: ⇒ goal

The example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic.

Before ImpGoalExp1.png

After ImpGoalExp2.png

For-all Goal

  • Description: Simplifies any sequent with a universally quantified goal by freeing all its bound variables.
  • Additional details: The bound variables will be renaming accordingly to avoid name collision.
  • ID: org.eventb.core.seqprover.forallGoalTac
  • Auto-tactic: No
  • Post-tactic: Yes
  • Preference display: For-all Goal (Simplify)
  • Interactive: Goal. The symbol \forall in the universal quantified goal is redden. When the mouse hovers the red symbol, the label of the tactic in the context menu is Forall instantiation.

ForallGoalInteractive1.png

  • Proving interface display: ∀ goal (frees list-of-bounded-identifiers)

The first example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic. There is no renaming of the bound variable.

Before ForallGoalExp1.png

After ForallGoalExp2.png

The second example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic. The bound variable x is not renamed, but the bound variable z is renamed to z0 to avoid capture of the existing variable z.

Before ForallGoalExp3.png

After ForallGoalExp4.png

Exists Hypothesis

  • Description: In automatic mode (as an auto-tactic or post-tactic), this tactic simplifies any sequent containing existentially quantified hypotheses by freeing their bound variables. In interactive mode, only the selected hypothesis is simplified by freeing its bound variables.
  • Additional details: The bound variables will be renaming if necessary to avoid name collision. After freeing their bound variables, if the resulting predicate is a conjunction then it is split into several hypotheses.
  • ID: org.eventb.core.seqprover.existHypTac
  • Auto-tactic: No
  • Post-tactic: Default
  • Preference display: Exists Hypotheses (Simplify)
  • Interactive: Hypothesis. The symbol \exists in the existential quantified hypothesis is redden. When the mouse hovers the red symbol, the label of the tactic in the context menu is Free existential variables.

ExistsHypInteractive1.png

  • Proving interface display:

The first example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic. There is no renaming of the bound variable.

Before ExistHypExp1.png

After ExistHypExp2.png

The second example below shows the screen-shots of the step before the application of the tactic and the step just after the application of the tactic. The bound variable x is not renamed, but the bound variable z is renamed to z0 to avoid capture of the existing variable z.

Before ExistHypExp3.png

After ExistHypExp4.png

Find Contradictory Hypothesis

  • Description: Discharges a sequent by finding contradictory hypotheses, i.e. P and \neg P .
  • Additional details: This tactic tries to find a contradiction using each selected hypothesis that is a negation.
  • ID: org.eventb.core.seqprover.findContrHypsTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • Preference display: Find Contradictory Hypotheses (Discharge)
  • Interactive: No
  • Proving interface display: ct in hyps (the negated hypothesis)

FindContrHypsExp1.png

Use Equality Hypothesis

  • Description: Simplifies a sequent by rewriting all selected hypotheses and the goal using a (selected) hypothesis that is an equality between a free variable and an expression that does not contain the free variable. The used equality remains in the selected hypotheses to be used again.
  • Additional details: Each application of the tactic take only one equality hypothesis into account. If there are several equality hypotheses, they require several applications of the tactic. Moreover, in the case where there are several equality hypotheses, the choice of which hypothesis will be chosen is non-deterministic. This tactic behaves as #Use Equality Hypothesis from Left to Right or #Use Equality Hypothesis from Right to Left depending on if the free variable is on the left or on the right of the equality.
  • ID: org.eventb.core.seqprover.eqHypTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • 'Preference display: Use Equals Hypotheses (Simplify)
  • Proving interface display: eh (the equal hypothesis) in the case where the free variable is on the left-hand side or he (the equal hypothesis) in the case where the free variable is on the right-hand side.

The example below shows the screen-shots of the step before the application of the tactic, the step after the first application of the tactic with hypothesis x = y + 1 and the step just after the second application of the tactic with hypothesis 1 = y.

Before UseEqualityHypExp1.png

After the first application UseEqualityHypExp2.png

After the second application UseEqualityHypExp3.png

Use Equality Hypothesis from Left to Right

  • Description: Rewriting all selected hypotheses and the goal using a (selected) hypothesis that is an equality between two expressions. The used equality remains in the selected hypotheses to be used again.
  • ID:
  • Interactive: Hypothesis
  • Proving interface display:

Shrink Implicative Hypothesis

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Shrink Enumerated Set

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Implicative Hypothesis with Conjunctive RHS

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Implicative Hypothesis with Disjunctive LHS

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Conjunctive Goal

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Clarify Goal

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Functional Overriding in Goal

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Functional Overriding in Hypothesis

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Partition Rewriter

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

One-Point Rule in Goal

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

One-Point Rule in Hypothesis

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Bounded Goal with Finite Hypothesis

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Falsify Goal

conjI

allI

exI

Remove Negation

Review

Proof by cases

Add Hypothesis

Abstract Expression

Automatic Prover

Post tactic

Lasoo

Back Tracking

Prune

Search Hypothesis

Cache Hypothesis

Previous

Next

Information

Falsify Hypothesis

Modus Ponens

conjE

disjE

allE

exE

Double Implication Hypothesis

cont Implication Hypothesis

Functional Overriding

Modus Tollens

Remove Membership

Remove Inclusion

Remove Strict-Inclusion

Inclusion Set Minus Right

Remove Inclusion Universal

Implication Introduction

Disjunction to Implication

Forall Modus Ponens

Next Pending Sub-goal

Next Reviewed Sub-goal

impAndHyp

impAndGoal

impOrHyp

impOrGoal

relImgUnionRight

relImgUnionLeft

Set Equality

Equivalent

Functional Intersection Image

Functional Set Minus Image

Functional Singleton Image

Converse Relation

Domain Distribution to the Left

Domain Distribution to the Right

Range Distribution to the Left

Range Distribution to the Right

Set Minus

Conjunction and Disjunction Distribution

Union Conjunction Distribution

compUnionDist

Domain/Range Union Distribution

Relational Overriding

Composition Image

Domain Composition

Range Composition

Functional Composition Image

Finite Set in Goal

Finite Intersection in Goal

Finite Set Minus in Goal

Finite Relation in Goal

Finite Relation Image in Goal

Finite Domain in Goal

Finite Range in Goal

Finite Function in Goal

Finite Function Converse in Goal

Finite Functional Relational Image in Goal

Finite Functional Range in Goal

Finite Functional Domain in Goal

Finite Minimum in Goal

Finite Maximum in Goal

Finite Negative in Goal

Finite Positive in Goal

Cardinality Comparison in Goal

Cardinality Up to

Partition Rewrite

Arithmetic Rewrite

Total Domain in Hypothesis / Goal