Difference between revisions of "Maplet Overriding in Goal"

From Event-B
Jump to navigationJump to search
imported>Billaude
imported>Billaude
Line 3: Line 3:
 
= Objective =
 
= Objective =
  
Split every goal in the form : <math> f \ovl{\{x \mapsto y\}} \in A \to B </math> into three sub-goals :
+
Split every goal in the form : <math>f\ovl{\{x\mapsto y\}}\in A\to B </math> into three sub-goals if and only if the sequent contains that hypothesis <math>f\in A\;op\;B</math> :
:*<math>\{x\} \domsub f \in A \smallsetminus \{x\} \to B</math>
+
:*<math>f\in A\;op\;B</math>
:*<math>x \in A</math>
+
:*<math>x\in A</math>
:*<math>y \in B</math>
+
:*<math>y\in B</math>
 +
Where <math>op</math> denote either a Relation <math>\left(\rel\right)</math>, or a Total Relation <math>\left(\trel\right)</math>, or a Partial Function <math>\left(\pfun\right)</math>, or a Total Function <math>\left(\tfun\right)</math>.
  
 
= Design Decision =
 
= Design Decision =
  
Instead of proofing the first sub-goal, it may be more easy to proof <math>f\in A\to B</math> which is a sufficient condition : <math>(f\in A\to B)\limp (\{x\} \domsub f \in A \smallsetminus \{x\} \to B)</math>.
+
Those three subgoals are not equivalent to the goal from which they are inferred. In order to get the equivalence, we should write <math>\{x\}\domsub f\in A\setminus\{x\}\;op\;B</math>. But this has the drawback of writing twice the expression ''x''. If this expression is big, then it can make the proof rule hard to read.
 +
 
 +
But, we know that <math>\left(f\in A\;op\;B\right)\limp \left(\{x\}\domsub f\in A\setminus\{x\}\;op\;B\right)</math>. By ensuring that this predicate is among the hypotheses of the sequent, we are sure that it will be proofed. Indeed, if this check was not done, the proof obligation may be unprovable since there are a loss of informations by writing <math>f\in A\;op\;B</math> instead of <math>\{x\}\domsub f\in A\setminus\{x\}\;op\;B</math>.
  
 
= Implementation =
 
= Implementation =
Line 22: Line 25:
 
  │            ├── x
 
  │            ├── x
 
  │            └── y
 
  │            └── y
  └── <math>\to</math>
+
  └── <math>op</math>
 
     ├── A
 
     ├── A
 
     └── B
 
     └── B
 
Then, if the hypothesis <math>f\in A\to B</math> is present, the goal is split as follows :
 
Then, if the hypothesis <math>f\in A\to B</math> is present, the goal is split as follows :
:*<math>f\in A\to B</math>
+
:*<math>f\in A\;op\;B</math>
:*<math>x \in A</math>
 
:*<math>y \in B</math>
 
Else, it is split as follows :
 
:*<math>\{x\} \domsub f \in A \smallsetminus \{x\} \to B</math>
 
 
:*<math>x \in A</math>
 
:*<math>x \in A</math>
 
:*<math>y \in B</math>
 
:*<math>y \in B</math>
 +
Else nothing is proceeded.
  
 
[[Category:Design proposal]]
 
[[Category:Design proposal]]

Revision as of 14:41, 19 August 2011

This page describes the design of a tactic requested here : Feature Request #3306228

Objective

Split every goal in the form : f\ovl{\{x\mapsto y\}}\in A\to B into three sub-goals if and only if the sequent contains that hypothesis f\in A\;op\;B :

  • f\in A\;op\;B
  • x\in A
  • y\in B

Where op denote either a Relation \left(\rel\right), or a Total Relation \left(\trel\right), or a Partial Function \left(\pfun\right), or a Total Function \left(\tfun\right).

Design Decision

Those three subgoals are not equivalent to the goal from which they are inferred. In order to get the equivalence, we should write \{x\}\domsub f\in A\setminus\{x\}\;op\;B. But this has the drawback of writing twice the expression x. If this expression is big, then it can make the proof rule hard to read.

But, we know that \left(f\in A\;op\;B\right)\limp \left(\{x\}\domsub f\in A\setminus\{x\}\;op\;B\right). By ensuring that this predicate is among the hypotheses of the sequent, we are sure that it will be proofed. Indeed, if this check was not done, the proof obligation may be unprovable since there are a loss of informations by writing f\in A\;op\;B instead of \{x\}\domsub f\in A\setminus\{x\}\;op\;B.

Implementation

First, the goal is checked. Its tree structure must match the following one :

\in
├── \ovl
│   ├── f
│   └── {}
│       └──  \mapsto
│            ├── x
│            └── y
└── op
    ├── A
    └── B

Then, if the hypothesis f\in A\to B is present, the goal is split as follows :

  • f\in A\;op\;B
  • x \in A
  • y \in B

Else nothing is proceeded.