Latest revision as of 16:05, 18 March 2014

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\;op_1\;B$ into two sub-goals if and only if the sequent contains a hypothesis such as $f\in A\;op_2\;B$ :

$x\in A$
$y\in B$

Where $op_1$ 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)$ , and $op_2$ is such as $f\in A\;op_2\;B\limp f\in A\;op_1\;B$ .

Design Decision

Those two subgoals and the predicate are not equivalent to the goal. Indeed, in the case $op_1$ is a Relation, the goal is equivalent to $\{x\}\domsub f\in A\setminus\{x\}\rel B\land x\in A\land y\in B$ . But this has the drawback of writing three times 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_1\;B\right)\limp \left(\{x\}\domsub f\in A\setminus\{x\}\;op_1\;B\right)$ for all the relation given in Objective. By ensuring that $f\in A\;op_2\;B$ is among the hypotheses of the sequent, we ensure that the first predicate of the conjunction is provable. 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_2\;B$ instead of $\{x\}\domsub f\in A\setminus\{x\}\;op_1\;B$ .

Table

$f\in A\;op_2\;B\limp f\in A\;op_1 B$
$op_1\;\backslash\;op_2$	$\rel$	$\trel$	$\srel$	$\strel$	$\pfun$	$\tfun$	$\pinj$	$\tinj$	$\psur$	$\tsur$	$\tbij$
$\rel$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$
$\trel$	$-$	$\checkmark$	$-$	$\checkmark$	$-$	$\checkmark$	$-$	$\checkmark$	$-$	$\checkmark$	$\checkmark$
$\srel$	$-$	$-$	$\checkmark$	$\checkmark$	$-$	$-$	$-$	$-$	$\checkmark$	$\checkmark$	$\checkmark$
$\strel$	$-$	$-$	$-$	$\checkmark$	$-$	$-$	$-$	$-$	$-$	$\checkmark$	$\checkmark$
$\pfun$	$-$	$-$	$-$	$-$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$	$\checkmark$
$\tfun$	$-$	$-$	$-$	$-$	$-$	$\checkmark$	$-$	$\checkmark$	$-$	$\checkmark$	$\checkmark$
$\pinj$	$-$	$-$	$-$	$-$	$-$	$-$	$\checkmark$	$\checkmark$	$-$	$-$	$\checkmark$
$\tinj$	$-$	$-$	$-$	$-$	$-$	$-$	$-$	$\checkmark$	$-$	$-$	$\checkmark$
$\psur$	$-$	$-$	$-$	$-$	$-$	$-$	$-$	$-$	$\checkmark$	$\checkmark$	$\checkmark$
$\tsur$	$-$	$-$	$-$	$-$	$-$	$-$	$-$	$-$	$-$	$\checkmark$	$\checkmark$
$\tbij$	$-$	$-$	$-$	$-$	$-$	$-$	$-$	$-$	$-$	$-$	$\checkmark$

@@ Line 3: / Line 3: @@
 = 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\;op_1\;B </math> into two sub-goals if and only if the sequent contains a hypothesis such as <math>f\in A\;op_2\;B</math> :
-:*<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>
+Where <math>op_1</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>, and <math>op_2</math> is such as <math>f\in A\;op_2\;B\limp f\in A\;op_1\;B</math>.
 = 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 two subgoals and the predicate are not equivalent to the goal. Indeed, in the case <math>op_1</math> is a Relation, the goal is equivalent to <math>\{x\}\domsub f\in A\setminus\{x\}\rel B\land x\in A\land y\in B</math>. But this has the drawback of writing three times the expression ''x''. If this expression is big, then it can make the proof rule hard to read.
-= Implementation =
+But, we know that <math>\left(f\in A\;op_1\;B\right)\limp \left(\{x\}\domsub f\in A\setminus\{x\}\;op_1\;B\right)</math> for all the relation given in Objective. By ensuring that <math>f\in A\;op_2\;B</math> is among the hypotheses of the sequent, we ensure that the first predicate of the conjunction is provable. 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_2\;B</math> instead of <math>\{x\}\domsub f\in A\setminus\{x\}\;op_1\;B</math>.
-First, the goal is checked. Its tree structure must match the following one :
+= Table =
- <math>\in</math>
- ├── <math>\ovl</math>
- │   ├── f
- │   └── {}
- │       └──  <math>\mapsto</math>
- │            ├── x
- │            └── y
- └── <math>\to</math>
-     ├── A
-     └── B
-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>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>y \in B</math>
-[[Category:Design proposal]]
+{| class="wikitable alternance" style="text-align:center; width:80%;"
+|+ <math>f\in A\;op_2\;B\limp f\in A\;op_1 B</math>
+|-
+|<math>op_1\;\backslash\;op_2</math>
+! scope=col | <math>\rel</math>
+! scope=col | <math>\trel</math>
+! scope=col | <math>\srel</math>
+! scope=col | <math>\strel</math>
+! scope=col | <math>\pfun</math>
+! scope=col | <math>\tfun</math>
+! scope=col | <math>\pinj</math>
+! scope=col | <math>\tinj</math>
+! scope=col | <math>\psur</math>
+! scope=col | <math>\tsur</math>
+! scope=col | <math>\tbij</math>
+|-
+! scope=row | <math>\rel</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|-
+! scope=row | <math>\trel</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|-
+! scope=row | <math>\srel</math>
+|<math>-</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|-
+! scope=row | <math>\strel</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|-
+! scope=row | <math>\pfun</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|-
+! scope=row | <math>\tfun</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|-
+! scope=row | <math>\pinj</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>-</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|-
+! scope=row | <math>\tinj</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>-</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|-
+! scope=row | <math>\psur</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|-
+! scope=row | <math>\tsur</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|<math>\checkmark</math>
+|-
+! scope=row | <math>\tbij</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>-</math>
+|<math>\checkmark</math>
+|-
+|}
+[[Category:Design]]

Maplet Overriding in Goal: Difference between revisions

Latest revision as of 16:05, 18 March 2014

Objective

Design Decision

Table

Navigation menu

Page actions

Page actions

Personal tools

Navigation

Search

Contribute

Tools