Main Page

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

Objective

Split every goal in the form : $f \ovl{\left\{x \mapsto y\right\}} \in A \to B$ into three sub-goals :

• ${x} \domsub f \in A \smallsetminus \left\{x\right\} \to B$
• $x \in A$
• $y \in B$

Design Decision

Instead of proofing the first sub-goal, it may be more easy to proof $f\in A\to B$ which is a sufficient condition : $(f\in A\to B)\limp ({x} \domsub f \in A \smallsetminus \left\{x\right\} \to B)$.

Implementation

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

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

Then, if the hypothesis $f\in A\to B$ is contained in the hypothesis the goal is splitted as follows :

• $f\in A\to B$
• $x \in A$
• $y \in B$

Else, it is splitted as follows :

• ${x} \domsub f \in A \smallsetminus \left\{x\right\} \to B$
• $x \in A$
• $y \in B$