1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
(* Nested Proofs, and backtrack mechanism in general.
BUGS:
- Still will be one buggy case, when kill-goal command is
assumed to be good enough to kill off current goal without
calculating the Back commands to do inside. Needs tweaking
of PG undo mechanism to allow a single undo function, without
forcing the split.
Exercise: produce a test case showing this bug(!).
======= Below here fixed [?]
- Retract 7a -> 6 needs to do 3 sorts of undo commands!
Abort, Undo, Back.
Algorithm is to use current search-forwards from target span
mechanism, which has to cover the whole range of undo to count
all the Backs. However, only the initial Undo's which appear
before an Abort need to be counted. (See coq-find-and-forget).
- Undo of "Require Omega" in proof uses Undo instead of Back.
[ coq-count-undos needs fixing to use Back as well as Undo ? ]
- once point 12 is reached, sould have one
block from 3 to 12. With the goalsave test :
OK but the reset command is wrong.
- From point 5, retract to point 1: "Abort. Back 5." Argl
Wrong, tactics and line 3 are counted for Back!!
This comes from my modification of coq-find-and-forget
function.
- point 7 is not well backtracked, but this can be solved easily
in coq.el.
*)
Require Logic. (* 1 This needs "Back 1" to be retracted *)
Require List. (* 2 This needs "Back 1" to be retracted *)
Fixpoint f [n:nat] : nat := Cases n of O => O | (S m)=> (f m) end. (*7*)
Lemma t1: (n: nat ) {n=O} + {(EX y | n = (S y))}.
(* 3 This needs "Restart" to be retracted if inside the proof, and
"Reset t1. Back 4." if outside (after point 12). 3 because of the
Require and the two lemmas inside the proof. If only "Reset t1", like
with the current version of PG, then t2 and t3 are still in the
environment. Try this with the current version and with my patch *)
(* da: Back command seems much better behaved than "Reset", which
always clears proof state, I think. Should PG always use Back? *)
Intros. (* 4 This needs "Undo" to be retracted *)
Case n. (* 5 "Undo" *)
EAuto. (* 6 "Undo" *)
Require Omega. (* 7 This needs "Back 1" to be retracted. *)
Lemma t2 : O=O. (* 7a. -> 6: "Abort. Back 1. Undo 1." *)
Auto.
Lemma t4 : O=O.
Auto. (* 7b. -> 6: "Abort. [Undo.] Abort. Back 1. Undo 1." *)
(* 7b. -> 2: "Abort. Abort. Abort. Back 1."
This is a useful test case because PG splits
undo calculation into phases: outwith
top-level proof and within top-level proof. *)
Save.
Save. (* 8 "Back 1" or "Reset t2". *)
Intros. (* 9 "Undo": example of retraction 9->6: Undo 2. Back 3. *)
Fixpoint f [n:nat] : nat := Cases n of O => O | (S m)=> (f m) end. (*7*)
Lemma t3 : O=O. Auto. Save. (* 10 "Back 1" or "Reset t3" *)
EAuto. (* 11 "Undo" *)
Save. (* 12 *)
|
