<td>Move the assumption A from the context to the goal. If the goal was <code>G</code> before, it will be <code>A -> G</code> afterwards and <code>A</code> won't appear in the context anymore.</td>
<td>Move the assumption <code>A</code> from the context to the goal. If the goal was <code>G</code> before, it will be <code>A -> G</code> afterwards and <code>A</code> won't appear in the context anymore.</td>
</tr>
<tr>
<td>move /evP</td>
<td>Rephrase the top of the proof stack using the reflection lemma <code>evP</code>.</td>
</tr>
<tr>
<td>move /evP: H => H'</td>
<td>Rephrase the hypothesis <code>H</code> using the reflection lemma <code>evP</code> and store the result in the hypothesis <code>H'</code>.</td>
</tr>
<tr>
<td>move: {H}</td>
<td>Clear hypothesis <code>H</code>.</td>
</tr>
<tr>
<td>move Eq: expr => alias</td>
<td>Replace <code>expr</code> with the name <code>alias</code> and store the according equation in the new hypothesis <code>Eq</code>.</td>
</tr>
<tr>
<td>case: m</td>
<td>Destruct <code>m</code>, which must be inductively defined (This includes propositions). Creates one subgoal for every constructor. Note: <code>m</code> may be a complex expression, as long as its type is inductive. TODO: <code>case</code> also calls <code>injection</code>.</td>
...
...
@@ -84,6 +92,10 @@
<td>case E': n.+2 / E</td>
<td>Like <code>case E': n.+2 /</code>, but performs the case analysis in hypothesis <code>E</code></tr>
</tr>
<tr>
<td>case H: _ _ _ /</td>
<td>TODO</td>
</tr>
<tr>
<td>case n //</td>
<td>Do a case analysis on <code>n</code> and resolve the trivial subgoals.</td>
...
...
@@ -220,6 +232,34 @@
<td>omega</td>
<td>Solve most arithmetic expressions with <code>+</code>, <code>-</code>, and <code>*</code>.</td>
</tr>
<tr>
<td>invas</td>
<td>Invert and substitute.</td>
</tr>
<tr>
<td>eauto</td>
<td>Try to solve the goal by applying lemmas, unfolding definitions.</td>
</tr>
<tr>
<td>eauto with ImpDB</td>
<td>Try to solve the goal by applying lemmas, unfolding definitions. Take hints from <code>ImpDB</code>.</td>
</tr>
<tr>
<td>eauto using lemma1, lemma2</td>
<td>Try to solve the goal by applying lemmas, unfolding definitions. Add <code>lemma1</code>, <code>lemma2</code> to the lists of lemmas to apply.</td>
