Mercurial > cpdt > repo
diff src/StackMachine.v @ 22:91e247c68ee8
Template generation
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 05 Sep 2008 16:46:32 -0400 |
parents | c0cbf324ec7d |
children | 26ad686e68f2 |
line wrap: on
line diff
--- a/src/StackMachine.v Wed Sep 03 16:37:51 2008 -0400 +++ b/src/StackMachine.v Fri Sep 05 16:46:32 2008 -0400 @@ -198,6 +198,7 @@ (* begin hide *) Abort. (* end hide *) +(* begin thide *) (** Though a pencil-and-paper proof might clock out at this point, writing "by a routine induction on [e]," it turns out not to make sense to attack this proof directly. We need to use the standard trick of %\textit{%#<i>#strengthening the induction hypothesis#</i>#%}%. We do that by proving an auxiliary lemma: *) @@ -511,6 +512,7 @@ reflexivity. Qed. +(* end thide *) (** * Typed Expressions *) @@ -793,6 +795,7 @@ (* begin hide *) Abort. (* end hide *) +(* begin thide *) (** Again, we need to strengthen the theorem statement so that the induction will go through. This time, I will develop an alternative approach to this kind of proof, stating the key lemma as: *) @@ -851,3 +854,4 @@ Theorem tcompileCorrect : forall t (e : texp t), tprogDenote (tcompile e nil) tt = (texpDenote e, tt). crush. Qed. +(* end thide *)