From 02fc826ead2e58363a65b8f38ad4c3dd75e50436 Mon Sep 17 00:00:00 2001
From: Lorenz Gorse <lorenz.gorse@gmail.com>
Date: Sun, 16 Jul 2017 14:04:42 +0200
Subject: [PATCH] Changes.
---
cheatsheet.html | 42 +++++++++++++++++++++++++++++++++++++++++-
1 file changed, 41 insertions(+), 1 deletion(-)
diff --git a/cheatsheet.html b/cheatsheet.html
index ac21afd..ceac4d5 100644
--- a/cheatsheet.html
+++ b/cheatsheet.html
@@ -46,16 +46,24 @@
</tr>
<tr>
<td>move: A</td>
- <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>
+ </tr>
+ <tr>
+ <td>tauto</td>
+ <td>TODO</td>
+ </tr>
+ <tr>
+ <td>solve</td>
+ <td>TODO</td>
+ </tr>
+ <tr>
+ <td>eexists</td>
+ <td>Apply constructor of exists with holes.</td>
+ </tr>
</table>
<h1>Tacticals</h1>
--
GitLab