pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-27 23:06:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Revising for next lecture

Browse source
This commit is contained in:
Adam Chlipala 2021-03-07 14:21:30 -05:00
parent bc9ab2a9bc
commit 3c419e5072
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
IntroToProofScripting.v
View file

@ -220,7 +220,7 @@ Proof.
apply Inc2Inv; assumption. apply Inc2Inv; assumption.
Qed. Qed.
(* OK, HERE is where prove the main theorem. This source file doesn't leave a (* OK, HERE is where we prove the main theorem. This source file doesn't leave a
* record of the trail of intermediate, less-automated versions, but we develop * record of the trail of intermediate, less-automated versions, but we develop
* it step-by-step in class. *) * it step-by-step in class. *)
@ -483,9 +483,9 @@ Goal False.
length (1 :: 2 :: 3 :: nil) ltac:(fun n => pose n). length (1 :: 2 :: 3 :: nil) ltac:(fun n => pose n).
Abort. Abort.
(* However, it's not always convenient to use continuation passing style (* However, it's not always convenient to use continuation-passing style
* everywhere, so cool kids use the following hack to sneak side effects * everywhere, so cool kids use the following hack to sneak side effects
* into otherwise functional Ltac code: *) * into otherwise functional Ltac code. *)
Module Import WithPrintingFixedWithoutContinuations. Module Import WithPrintingFixedWithoutContinuations.
Ltac length ls := Ltac length ls :=
let __ := match constr:(Set) with let __ := match constr:(Set) with
@ -793,7 +793,7 @@ Section t6.
apply H2. apply H2.
exact H. exact H.
exact p. exact p.
(* In two weeks, we'll meet [eauto], which can do these last steps (* Next week, we'll meet [eauto], which can do these last steps
* automatically. *) * automatically. *)
Qed. Qed.
End t6. End t6.

2
IntroToProofScripting_template.v
View file

@ -157,7 +157,7 @@ Proof.
apply Inc2Inv; assumption. apply Inc2Inv; assumption.
Qed. Qed.
(* OK, HERE is where prove the main theorem. *) (* OK, HERE is where we prove the main theorem. *)
Theorem increment2_invariant_ok : invariantFor increment2_sys increment2_invariant. Theorem increment2_invariant_ok : invariantFor increment2_sys increment2_invariant.
Proof. Proof.