PDF UPDATE SCRIPT

software_foundations/bin/1_basics-anki.txt

@@ -37,6 +37,6 @@ What do <tt>Case</tt>/<tt>SCase</tt>/etc do?<br><br>Don't confuse <tt>Case</tt>
 What is the syntax of the <tt>induction</tt> tactic?	Just the same as the <tt>destruct</tt> tactic.
 What do context items like <tt>IHn'</tt> stand for?	Inductive Hypothesis for <tt>n'</tt>
 Name some fundamental facts concerning our definition of <tt>plus</tt> comes up over and over?	<pre>- S (n + m) = (S n) + m<br>- S (n + m) = n + (S m)</pre>
-How can you create sub-theorems without creating a new top-level name?	Use the <tt>assert</tt> tactic.<br><br><pre>assert (H: whatever).<br>  Case "Proof of assertion". whatever.</pre><br>After the proof is done <tt>H</tt> will be added to context.
+How can you create sub-theorems without creating a new top-level name?	Use the <tt>assert</tt> tactic.<br><br><pre>assert (H: whatever).<br>(* or: assert (whatever) as H *)<br>  Case "Proof of assertion". whatever.</pre><br>After the proof is done <tt>H</tt> will be added to context.
 What is a common non-stylistic reason for using <tt>assert</tt>?	You want to use the <tt>rewrite</tt> tactic on an instance of the pattern that is not outermost.<br>In this case you can prove as a sub-theorem exactly the rewrite you want, and then use <tt>rewrite</tt> in terms of this sub-theorem.
 Describe the <tt>replace</tt> tactic.<br><br>When is it often used?	<pre>replace (t) with (u)</pre>replaces (all copies of) expression <tt>t</tt> in the goal with expression <tt>u</tt> and generates <tt>t=u</tt> as an additional subgoal.<br><br>It's often used when <tt>rewrite</tt> acts on the wrong part of the goal.

software_foundations/bin/1_basics-mnemosyne.txt

@@ -37,6 +37,6 @@ What do <tt>Case</tt>/<tt>SCase</tt>/etc do?<br><br>Don't confuse <tt>Case</tt>
 What is the syntax of the <tt>induction</tt> tactic?	Just the same as the <tt>destruct</tt> tactic.
 What do context items like <tt>IHn'</tt> stand for?	Inductive Hypothesis for <tt>n'</tt>
 Name some fundamental facts concerning our definition of <tt>plus</tt> comes up over and over?	<pre>- S (n + m) = (S n) + m<br>- S (n + m) = n + (S m)</pre>
-How can you create sub-theorems without creating a new top-level name?	Use the <tt>assert</tt> tactic.<br><br><pre>assert (H: whatever).<br>  Case "Proof of assertion". whatever.</pre><br>After the proof is done <tt>H</tt> will be added to context.
+How can you create sub-theorems without creating a new top-level name?	Use the <tt>assert</tt> tactic.<br><br><pre>assert (H: whatever).<br>(* or: assert (whatever) as H *)<br>  Case "Proof of assertion". whatever.</pre><br>After the proof is done <tt>H</tt> will be added to context.
 What is a common non-stylistic reason for using <tt>assert</tt>?	You want to use the <tt>rewrite</tt> tactic on an instance of the pattern that is not outermost.<br>In this case you can prove as a sub-theorem exactly the rewrite you want, and then use <tt>rewrite</tt> in terms of this sub-theorem.
 Describe the <tt>replace</tt> tactic.<br><br>When is it often used?	<pre>replace (t) with (u)</pre>replaces (all copies of) expression <tt>t</tt> in the goal with expression <tt>u</tt> and generates <tt>t=u</tt> as an additional subgoal.<br><br>It's often used when <tt>rewrite</tt> acts on the wrong part of the goal.

software_foundations/bin/4_programming_with_propositions-anki.txt

@@ -1,3 +1,4 @@
 Explain the <tt>generalize dependent</tt> tactic.	?
-All propositions in Coq are of what type?	<tt>Prop</tt>
+What is a proposition?<br><br>What is a <tt>Prop</tt>?	A proposition is a mathematical statement expressing a factual claim. It may or may not be provable.<br><br>A <tt>Prop</tt> is the type of expressions that represent propositions.
+Name the two simplest ways to create propositions expression.	- Assert that one expression is equal to another.<br>- Given propositions expressions <tt>P</tt> and <tt>Q</tt>, assert <tt>P->Q</tt>.
 The definition <tt>even</tt> has the type <tt>nat->Prop</tt>. Give three ways to pronounce this.	- <tt>even</tt> is a <em>function</em> from numbers to propositions.<br>- <tt>even</tt> is a <em>family</em> of propositions, indexed by a number <tt>n</tt>.<br>- <tt>even</tt> is a <em>property</em> of numbers.

software_foundations/bin/4_programming_with_propositions-mnemosyne.txt

@@ -1,3 +1,4 @@
 Explain the <tt>generalize dependent</tt> tactic.	?
-All propositions in Coq are of what type?	<tt>Prop</tt>
+What is a proposition?<br><br>What is a <tt>Prop</tt>?	A proposition is a mathematical statement expressing a factual claim. It may or may not be provable.<br><br>A <tt>Prop</tt> is the type of expressions that represent propositions.
+Name the two simplest ways to create propositions expression.	- Assert that one expression is equal to another.<br>- Given propositions expressions <tt>P</tt> and <tt>Q</tt>, assert <tt>P->Q</tt>.
 The definition <tt>even</tt> has the type <tt>nat->Prop</tt>. Give three ways to pronounce this.	- <tt>even</tt> is a <em>function</em> from numbers to propositions.<br>- <tt>even</tt> is a <em>family</em> of propositions, indexed by a number <tt>n</tt>.<br>- <tt>even</tt> is a <em>property</em> of numbers.