From c7c28081ce89e65c60d024f3af8a5d376b394354 Mon Sep 17 00:00:00 2001 From: Lorenz Gorse <lorenz.gorse@gmail.com> Date: Fri, 2 Jun 2017 11:37:36 +0200 Subject: [PATCH] Updates... --- cheatsheet.html | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/cheatsheet.html b/cheatsheet.html index 27a0658..2e3520a 100644 --- a/cheatsheet.html +++ b/cheatsheet.html @@ -50,7 +50,7 @@ </tr> <tr> <td>move /evP</td> - <td>...</td> + <td>Rephrase the top of the proof stack using the reflection lemma <code>evP</code>.</td> </tr> <tr> <td>case: m</td> @@ -73,16 +73,20 @@ <td>Destruct <code>m</code> and remember information about the current branch in the hypothesis <code>H</code>.</td> </tr> <tr> - <td>case n.+2 / E</td> - <td>...</td> + <td>case E': n.+2 /</td> + <td>Assume the goal is <code>ev x.+2 -> ev x</code>. Do a case analysis on the arguments of the inductive type <code>ev</code> (Which is defined as <code>Inductive ev: nat -> Prop := ev_0: ev 0 | ev_SS: ev n -> ev n.+2</code>) and remember information about the case analysis in <code>E'</code>. This produces two new goals, one for the constructor <code>ev_0</code> with <code>E: x.+2 = 0</code> and one for the constructor <code>ev_SS</code> with <code>E: x.+2 = n.+2<code> and evidence for <code>ev n</code>.</td> + </tr> + <tr> + <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 n //</td> <td>Do a case analysis on <code>n</code> and resolve the trivial subgoals.</td> </tr> <tr> - <td>case: H1 Hn => <-</td> - <td>...</td> + <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</td> @@ -98,7 +102,7 @@ </tr> <tr> <td>apply/evenP</td> - <td>...</td> + <td>Rephrase the goal using the reflection lemma <code>evenP</code>.</td> </tr> <tr> <td>apply</td> -- GitLab