Rodin Proof Tactics: Difference between revisions

← Older edit Newer edit →

Revision as of 14:28, 18 February 2011

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: Details explanation of the tactic, when it is applicable, give the associated proof rule. See Inference rules list and Rewriting rules list.

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.

True Goal

Description: Discharges any sequent whose goal is '⊤' (logical true).

Additional details:

\frac{}{\mathsf{H} \;\;\vdash \;\; \btrue}

TRUE_GOAL

ID: org.eventb.core.seqprover.trueGoalTac

Auto-tactic: Default

Post-tactic: Default

Preference display: True Goal (Discharge)

Interactive: No

Proving interface display: ⊤ goal

False Hypothesis

Description: Discharges any sequent containing a '⊥' hypothesis

Additional details:

\frac{}{\mathsf{H}, \bfalse \;\;\vdash \;\; \mathit{P}}

FALSE_HYP

ID: org.eventb.core.seqprover.falseHypTac

Auto-tactic: Default

Post-tactic: Default

Preference display: False Hypothesis (Discharge)

Interactive: No

Proving interface display: ⊥ hyp

Goal in Hypotheses

Description: Discharges any sequent whose goal is contained in its hypotheses

Additional details:

\frac{}{\mathsf{H}, \mathit{P} \;\;\vdash \;\; \mathit{P}}

HYP

ID: org.eventb.core.seqprover.goalInHypTac

Auto-tactic: Default

Post-tactic: Default

Preference display: Goal in Hypotheses (Discharge)

Interactive: No

Proving interface display: hyp

Goal Disjunct in Hypothesis

Description: Discharges any sequent whose goal is a disjunction and one of whose disjuncts is present in the hypotheses.

Additional details:

\frac{}{\mathsf{H}, \mathit{Q} \;\;\vdash \;\; \mathit{P} \lor \ldots \lor \mathit{Q} \lor \ldots \lor \mathit{R}}

HYP_OR

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

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. The corresponding proof rule is as follows.

\frac{}{\mathsf{H}, f \in E \; op \; F \;\;\vdash \;\; f \in T_1 \pfun T_2}

FUN_GOAL

where $op$ is either $\pfun, \tfun, \pinj, \tinj, \psur, \tsur, \tbij$ .

ID: org.eventb.core.seqprover.funGoalTac

Auto-tactic: Default

Post-tactic: Default

Preference display: Functional Goal (Discharge)

Interactive: No

Proving interface display: functional goal

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 rewriting rules, which are marked as Automatic.

The corresponding proof rule is as follows.

\frac{\mathsf{H}, \mathsf{H^\prime} \;\;\vdash \;\; \mathit{P^\prime}}{\mathsf{H} \;\;\vdash \;\; \mathit{P}}

SIM

where $\mathsf{H^\prime}$ are the set of new hypotheses obtained by rewriting some of the original hypothesis in $\mathsf{H}$ , and $\mathit{P}$ is the rewriting of the original goal $\mathit{P}$ .

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

After

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.

The rewriting rules are SIMP_TYPE_EQUAL_EMPTY and SIMP_TYPE_IN in the rewriting rules page.

The corresponding proof rule is as follows.

\frac{\mathsf{H}, \mathsf{H^\prime} \;\;\vdash \;\; \mathit{P^\prime}}{\mathsf{H} \;\;\vdash \;\; \mathit{P}}

SIM

where $\mathsf{H^\prime}$ are the set of new hypotheses obtained by rewriting some of the original hypothesis in $\mathsf{H}$ , and $\mathit{P}$ is the rewriting of the original goal $\mathit{P}$ .

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

After

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.

Additional details:

\frac{\mathsf{H}, \mathit{P} \;\;\vdash \;\; \mathit{Q}}{\mathsf{H} \;\;\vdash \;\; \mathit{P} \limp \mathit{Q}}

IMP_R

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.

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

After

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.

\frac{\mathsf{H} \;\;\vdash \;\; \mathit{P(x)}}{\mathsf{H} \;\;\vdash \;\; \forall x \qdot \mathit{P(x)}}

ALL_R

where $x$ does not appear freely in $\mathsf{H}$ .

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.

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

After

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

After

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.

\frac{\mathsf{H}, \mathit{P(x)}, \ldots, \mathit{Q(x)} \;\;\vdash \;\; \mathit{R}}{\mathsf{H}, \exists x \qdot \mathit{P(x)} \land \ldots \land \mathit{Q(x)} \;\;\vdash \;\; \mathit{R}}

XST_L

where $x$ does not appear freely in $\mathsf{H}$ and $\mathit{R}$ .

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.

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

After

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

After

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.

\frac{}{\mathsf{H}, \mathit{P}, \neg\mathit{P} \;\;\vdash \;\; \mathit{Q}}

CNTR

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)

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.

\frac{\mathsf{H(E)}, \mathit{x} = \mathit{E} \;\;\vdash \;\; \mathit{P(E)}}{\mathsf{H(x)}, \mathit{x} = \mathit{E} \;\;\vdash \;\; \mathit{P(x)}}

EQL_LR

\frac{\mathsf{H(E)}, \mathit{E} = \mathit{x} \;\;\vdash \;\; \mathit{P(E)}}{\mathsf{H(x)}, \mathit{E} = \mathit{x} \;\;\vdash \;\; \mathit{P(x)}}

EQL_RL

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 $x = y + 1$ and the step just after the second application of the tactic with hypothesis $1 = y$ .

Before

After the first application

After the second application

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: Simplifies the (visible) implicative hypotheses in a sequent by removing predicates from their left hand sides that are (selected) hypotheses.

Additional details:

\frac{ \textbf{H},\textbf{P},\;\textbf{Q}\limp \textbf{R}\;\;\vdash \;\; \textbf{S} }{\textbf{H},\;\textbf{P},\; \textbf{P} \land \textbf{Q} \limp \textbf{R} \;\;\vdash \;\; \textbf{S}}

AUTO_MH

ID: org.eventb.core.seqprover.shrinkImpHypTac

Auto-tactic: Default

Post-tactic: Default

Preference Display: Shrink Implicative Hypotheses (Simplify)

Interactive: No

Proving interface display: auto ImpE

Before

After

Shrink Enumerated Set

Description: Simplifies (selected) hypotheses of the form e ∈ {a,b,c} to e ∈ {a,c} after finding the hypothesis ¬ e = b.

Additional details: TODO

ID: org.eventb.core.seqprover.shrinkEnumHypTac

Auto-tactic: No

Post-tactic: Default

Preference Display: Shrink Enumerated Set (Simplify)

Interactive: No

Proving Interface Display: negEnum <hypotheses names>

Before

After Before

Implicative Hypothesis with Conjunctive RHS

Description: Simplifies all (selected) hypotheses of the form P ⇒ Q ∧ R into multiple implications P ⇒ Q , P ⇒ R.

Additional details:

\frac{\textbf{H},\textbf{P} \limp \textbf{Q}, \textbf{P} \limp \textbf{R}\;\;\vdash \;\; \textbf{S}}{\textbf{H},\;\textbf{P} \limp \textbf{Q} \land \textbf{R} \;\;\vdash \;\; \textbf{S}}

IMP_AND_L

ID: org.eventb.core.seqprover.splitRightConjImpHypTac

Auto-tactic: No

Post-tactic: Yes

Preference Display: Implicative Hypotheses with Conjunctive RHS (Simplify)

Interactive: Hypothesis

The operator ⇒ is redden in the hypotheses. When the mouse hovers the red symbol, the label of the tactic in the context menu is Implication with conjunction rewrites.

Proving Interface Display: ⇒ with ∧ in hyp <hypothesis name>

Before

After

Implicative Hypothesis with Disjunctive LHS

Description: Simplifies all (selected) hypotheses of the form P ∨ Q ⇒ R into multiple implications P ⇒ R , Q ⇒ R.

Additional details:

\frac{ \textbf{H},\textbf{P} \limp \textbf{R}, \textbf{Q} \limp \textbf{R}\;\;\vdash \;\; \textbf{S} }{\textbf{H},\;\textbf{P} \lor \textbf{Q} \limp \textbf{R} \;\;\vdash \;\; \textbf{S}}

IMP_OR_L

ID: org.eventb.core.seqprover.splitLeftDisjImpHypTac

Auto-tactic: No

Post-tactic: Yes

Preference Display: Implicative Hypotheses with Disjunctive LHS (Simplify)

Interactive: Hypothesis

The operator ⇒ is redden in the hypotheses. When the mouse hovers the red symbol, the label of the tactic in the context menu is Implication with disjunction rewrites.

Proving Interface Display: ⇒ with ∨ in hyp <hypothesis name>

Before

After

Conjunctive Goal

Description: Splits a sequent with a conjunctive goal into multiple subgoals.

Additional details:

\frac{\textbf{H} \; \; \vdash \; \; \textbf{P} \qquad \textbf{H} \; \; \vdash \; \; \textbf{Q}}{\textbf{H} \; \; \vdash \; \; \textbf{P} \; \land \; \textbf{Q}}

AND_R

ID: org.eventb.core.seqprover.conjGoalTac

Auto-tactic: No

Post-tactic: Yes

Preference display: Conjunctive Goal (Split)

Interactive: Goal

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

After

Clarify Goal

Description: Clarifies the goal by repeatedly by:
- splitting conjunctions,
- simplifying implications,
- simplifying universal quantifiers,
- discharging sequents with a true goal, a false hypothesis and where the goal is contained in the hypotheses.

Additional details: This tactic applies a composition of tactics #Conjunctive Goal, #Implication Goal and #For-all Goal followed by a looping of tactics #True Goal and #False Hypothesis.

ID: org.eventb.core.seqprover.clarifyGoalTac

Auto-tactic: Default

Post-tactic: Default

Preference Display: Clarify Goal (Mixed)

Interactive: No

Functional Overriding in Goal

Description: TODO

Additional details:

\frac{\textbf{H},\; G \in \dom(g) \;\;\vdash\;\;\textbf{Q}(g(G)) \qquad \textbf{H},\; \neg\, G \in \dom(g) \;\;\vdash\;\;\textbf{Q}((\dom(g) \domsub f)(G))}{\textbf{H} \;\;\vdash \;\; \textbf{Q}((f\ovl g)(G))}

OV_R

\frac{\textbf{H},\; G=E \;\;\vdash\;\;\textbf{Q}(F) \qquad \textbf{H},\; \neg\,(G=E) \;\;\vdash\;\;\textbf{Q}((\{E\}) \domsub f)(G))}{\textbf{H} \;\;\vdash \;\; \textbf{Q}((f\ovl\{E \mapsto F\})(G))}

OV_SETENUM_R

where Q is WD strict.

These inference rules are applied automatically, repeatedly and recursively.

ID: org.eventb.core.seqprover.funOvrGoalTac

Auto-tactic: Default

Post-tactic: No

Preference Display: Functional Overriding in Goal (Split)

Interactive: Goal

When hovering the redden override operator <+, select (f<+{E|->F})(G) from the drop-down menu. (TODO strange menu item)

Proving Interface Display: ovr in goal

Before

First node after application

Second node after application

Functional Overriding in Hypothesis

Description: TODO

Additional details:

\frac{\textbf{H},\; G \in \dom(g) ,\;\textbf{P}(g(G))\;\;\vdash\;\;\textbf{Q} \qquad \textbf{H},\; \neg\,G \in \dom(g) ,\;\textbf{P}((\dom(g) \domsub f)(G))\;\;\vdash\;\;\textbf{Q}}{\textbf{H},\;\textbf{P}((f\ovl g)(G)) \;\;\vdash \;\; \textbf{Q}}

OV_L

\frac{\textbf{H},\; G=E ,\;\textbf{P}(F)\;\;\vdash\;\;\textbf{Q} \qquad \textbf{H},\; \neg\,(G=E) ,\;\textbf{P}((\{E\}) \domsub f)(G))\;\;\vdash\;\;\textbf{Q}}{\textbf{H},\;\textbf{P}((f\ovl\{E \mapsto F\})(G)) \;\;\vdash \;\; \textbf{Q}}

OV_SETENUM_L

where P is WD strict.

These inference rules are applied automatically, repeatedly and recursively.

ID: org.eventb.core.seqprover.funOvrHypTac

Auto-tactic: Yes

Post-tactic: Yes

Preference Display: Functional Overriding in Hypothesis (Split)

Interactive: Hypothesis

When hovering the redden override operator <+, select (f<+{E|->F})(G) from the drop-down menu. (TODO strange menu item)

Proving Interface Display: ovr in <hypothesis name>

Before

First node after application

Second node after application

Partition Rewriter

Description: Simplifies all predicates of the form partition(S, ...) into their expanded form in the goal and all visible hypotheses.

Additional details: TODO

ID: org.eventb.core.seqprover.partitionRewriteTac

Auto-tactic: Default

Post-tactic: No

Preference Display: Partition Rewriter (Simplify)

Interactive: Hypothesis, Goal

The predicate partition is redden in the goal or the hypotheses. When the mouse hovers the red symbol, the label of the tactic in the context menu is Rewrites a partition into its definition.

Proving Interface Display: Partition rewrites in goal / hyp <hypothesis name>

Before

After

One-Point Rule in Goal

Description: Applies automatically the OnePointGoal tactic to the goal.

Additional details:

\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H} \;\;\vdash \;\; \forall x, \ldots, \ldots,z \qdot [y \bcmeq E]\textbf{P} \land \ldots \land \ldots \land [y \bcmeq E]\textbf{Q} \limp [y \bcmeq E]\textbf{R} }{ \textbf{H} \;\;\vdash\;\; \forall x, \ldots, y, \ldots, z \qdot \textbf{P} \land \ldots \land y = E \land \ldots \land \textbf{Q} \limp \textbf{R} }

ONE_POINT_R

The rule can be applied with ∀ as well as with ∃.

ID: org.eventb.core.seqprover.onePointGoalTac

Auto-tactic: Yes

Post-tactic: Yes

Preference Display: One Point Rule in Goal (Split)

Interactive: No

Proving Interface Display: One Point Rule in goal

Before

After

One-Point Rule in Hypothesis

Description: Applies automatically the OnePointHyp tactic to the selected hypotheses.

Additional details:

\frac{\textbf{H} \;\;\vdash \;\; {WD}(E) \qquad \textbf{H}, \forall x, \ldots, \ldots,z \qdot [y \bcmeq E]\textbf{P} \land \ldots \land \ldots \land [y \bcmeq E]\textbf{Q} \limp [y \bcmeq E]\textbf{R} \;\;\vdash \;\; \textbf{G}}{ \textbf{H}, \forall x, \ldots, y, \ldots, z \qdot \textbf{P} \land \ldots \land y = E \land \ldots \land \textbf{Q} \limp \textbf{R} \;\;\vdash\;\; \textbf{G}}

ONE_POINT_L

The rule can be applied with ∀ as well as with ∃.

ID: org.eventb.core.seqprover.onePointHypTac

Auto-tactic: Yes

Post-tactic: Yes

Preference Display: One Point Rule in Hypotheses (Split)

Interactive: No

Proving Interface Display: One Point Rule in hypothesis name

Before

After

Bounded Goal with Finite Hypothesis

Description: Discharges a sequent whose goal states that an expression E has a lower or a upper bound (e.g. ∃n·(∀x·x ∈ S ⇒ x ≤ n)), when there is an hypothesis that states the finiteness of E (i.e. finite(S)).

Additional details:

\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \leq x)}

FIN_L_LOWER_BOUND_L

\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; x \geq n)}

FIN_L_LOWER_BOUND_R

\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; n \geq x)}

FIN_L_UPPER_BOUND_L

\frac{}{\textbf{H},\;\finite(S) \;\;\vdash \;\; \exists n\,\qdot\, (\forall x \,\qdot\, x \in S \;\limp\; x \leq n)}

FIN_L_UPPER_BOUND_R

ID: org.eventb.core.seqprover.finiteHypBoundedGoalTac

Auto-tactic: Default

Post-tactic: Default

Preference Display: Bounded Goal with finite Hypothesis (Discharge)

Interactive: No

Proving Interface Display: Existence of minimum or maximum in goal with finite hypothesis

Before

After

Falsify Goal

Description: Contradicts the goal: the negation of the goal is taken as hypothesis and the goal becomes false.

Additional details:

\frac{\textbf{H},\;\neg\,\textbf{Q} \;\;\vdash \;\; \bfalse}{\textbf{H} \;\;\vdash \;\; \textbf{Q}}

CONTRADICT_R

ID: org.eventb.ui.falsify

Auto-tactic: No

Post-tactic: No

Interactive: Goal

Proving Interface Display: ct

Before

After

Falsify Hypothesis

Description: Contradicts an hypothesis: the negation of the goal is taken as hypothesis and the goal becomes the negation of the contradicted hypothesis.

Additional details:

\frac{\textbf{H},\;\neg\,\textbf{Q} \;\;\vdash \;\; \neg\,\textbf{P}}{\textbf{H},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}}

CONTRADICT_L

ID: org.eventb.ui.falsify

Auto-tactic: No

Post-tactic: No

Interactive: Hyp

Proving Interface Display: ct

Before

After

conjI

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

allI

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

exI

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Remove Negation

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Review

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Proof by cases

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Add Hypothesis

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Abstract Expression

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Automatic Prover

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Post tactic

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Lasoo

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Back Tracking

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Prune

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Search Hypothesis

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Cache Hypothesis

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Information

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Modus Ponens

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

conjE

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

disjE

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

allE

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

exE

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Double Implication Hypothesis

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

cont Implication Hypothesis

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Functional Overriding

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Modus Tollens

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Remove Membership

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Remove Inclusion

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Remove Strict-Inclusion

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Inclusion Set Minus Right

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Remove Inclusion Universal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Implication Introduction

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Disjunction to Implication

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Forall Modus Ponens

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Next Pending Sub-goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Next Reviewed Sub-goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

impAndHyp

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

impAndGoal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

impOrHyp

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

impOrGoal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

relImgUnionRight

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

relImgUnionLeft

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Set Equality

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Equivalent

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Functional Intersection Image

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Functional Set Minus Image

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Functional Singleton Image

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Converse Relation

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Domain Distribution to the Left

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Domain Distribution to the Right

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Range Distribution to the Left

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Range Distribution to the Right

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Set Minus

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Conjunction and Disjunction Distribution

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Union Conjunction Distribution

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

compUnionDist

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Domain/Range Union Distribution

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Relational Overriding

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Composition Image

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Domain Composition

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Range Composition

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Functional Composition Image

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Finite Set in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Finite Intersection in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Finite Set Minus in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Finite Relation in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Finite Relation Image in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Finite Domain in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Finite Range in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Finite Function in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Finite Function Converse in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Finite Functional Relational Image in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Finite Functional Range in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Finite Functional Domain in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Finite Minimum in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Finite Maximum in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Finite Negative in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Finite Positive in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Cardinality Comparison in Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Cardinality Up to

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Partition Rewrite

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Arithmetic Rewrite

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

Total Domain in Hypothesis / Goal

Description:

Additional details:

ID:

Auto-tactic:

Post-tactic:

Preference Display:

Interactive:

Proving Interface Display:

Before [[Image: ]]

After [[Image: ]]

@@ Line 671: / Line 671: @@
 After [[Image: ctGoalAfter.png]]
+== Falsify Hypothesis ==
+* '''Description''': Contradicts an hypothesis: the negation of the goal is taken as hypothesis and the goal becomes the negation of the contradicted hypothesis.
+* '''Additional details''':
+{{InfRule|CONTRADICT_L| <math>\frac{\textbf{H},\;\neg\,\textbf{Q} \;\;\vdash \;\; \neg\,\textbf{P}}{\textbf{H},\;\textbf{P} \;\;\vdash \;\; \textbf{Q}}</math>}}
+* '''ID''': org.eventb.ui.falsify
+* '''Auto-tactic''': ''No''
+* '''Post-tactic''': ''No''
+* '''Interactive''': ''Hyp''
+* '''Proving Interface Display''': ''ct''
+Before [[Image: ctHypBefore.png]]
+After [[Image: ctHypAfter.png]]
 == conjI ==
@@ Line 1,047: / Line 1,069: @@
 == Information ==
-* '''Description''':
-* '''Additional details''':
-* '''ID''':
-* '''Auto-tactic''':
-* '''Post-tactic''':
-* '''Preference Display''':
-* '''Interactive''':
-* '''Proving Interface Display''':
-Before [[Image: ]]
-After [[Image: ]]
-== Falsify Hypothesis ==
 * '''Description''':

Rodin Proof Tactics: Difference between revisions

Revision as of 14:28, 18 February 2011

True Goal

False Hypothesis

Goal in Hypotheses

Goal Disjunct in Hypothesis

Functional Goal

Simplification Rewriter

Type Rewriter

Implication Goal

For-all Goal

Exists Hypothesis

Find Contradictory Hypothesis

Use Equality Hypothesis

Use Equality Hypothesis from Left to Right

Shrink Implicative Hypothesis

Shrink Enumerated Set

Implicative Hypothesis with Conjunctive RHS

Implicative Hypothesis with Disjunctive LHS

Conjunctive Goal

Clarify Goal

Functional Overriding in Goal

Functional Overriding in Hypothesis

Partition Rewriter

One-Point Rule in Goal

One-Point Rule in Hypothesis

Bounded Goal with Finite Hypothesis

Falsify Goal

Falsify Hypothesis

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

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