diff --git a/cheatsheet.html b/cheatsheet.html index 2e3520abd62493c1b2cdd4a1ad4cb56688fa242a..38dfa9ae4786d03fb0e191e255bb7f5497d2c03a 100644 --- a/cheatsheet.html +++ b/cheatsheet.html @@ -52,6 +52,10 @@ <td>move /evP</td> <td>Rephrase the top of the proof stack using the reflection lemma <code>evP</code>.</td> </tr> + <tr> + <td>move: {H}</td> + <td>Clear hypothesis <code>H</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> @@ -88,6 +92,10 @@ <td>case: H => <-</td> <td>Do a case analysis on the equation <code>H</code>, move the result to the context, rewrite with it, and forget about it.</td> </tr> + <tr> + <td>case: eqnP</td> + <td>TODO</td> + </tr> <tr> <td>case</td> <td>Use case on the first variable in the proof tree.</td> @@ -156,6 +164,14 @@ <td>rewrite /function</td> <td>Unfold the definition of <code>function</code>.</td> </tr> + <tr> + <td>subst x</td> + <td>Find an assumption of the form <code>x=e</code> or <code>e=x</code>, use it for rewriting and clear the assumption.</td> + </tr> + <tr> + <td>subst</td> + <tr>Substitute everything.</tr> + </tr> <tr> <td>have H2 := (H1 a b)</td> <td>Adds a new hypothesis <code>H2</code> to the context which is <code>H1</code> applied to <code>a</code> and <code>b</code>.</td> @@ -200,6 +216,22 @@ <td>constructor</td> <td>Apply the first matching constructor.</td> </tr> + <tr> + <td>omega</td> + <td>Solve most arithmetic expressions with <code>+</code>, <code>-</code>, and <code>*</code>.</td> + </tr> +</table> + +<h1>Tacticals</h1> +<table> + <tr> + <td>try [tactic]</td> + <td>Execute <code>tactic</code> if this would work, do nothing if this would fail (Useful in conjunction with the <code>;</code> tactical).</td> + </tr> + <tr> + <td>do</td> + <td>TODO</td> + </tr> </table> <h1>Commands</h1>