docs: add debugging tips for vcg goals

Signed-off-by: Gerwin Klein <[email protected]>

docs/crefine-notes.md

@@ -250,7 +250,40 @@ so a simplification before the `wp`/`vcg` is needed...
 
 This 'last big subgoal' is where we prove that the `P` and `P'` appearing in the lemma statement imply the `?Q` and `?Q'` that have, at that point, been instantiated to a big conjunction of all the preconditions computed to fulfil the Hoare triple for each instruction of the program.
 
-The first thing that may happen here is that you end up needing to prove False. This is due to a simplification along the proof that instantiated a schematic precondition to 'False' to fulfil the goal (e.g. `?Q ⟹ bla`). The only thing to do here is to go back into the proof to see where it is generated and try to avoid it (sorry, not better clue...)
+The first thing that may happen here is that you end up needing to prove
+`False`. This is due to a simplification along the proof that instantiated a
+schematic precondition to 'False' to fulfil the goal (e.g. `?Q ⟹ bla`). One
+debugging technique for this is to replace the invocations of `vcg` that lead to
+the final goal with
+
+```
+apply (rule conseqPre, vcg, rule order.refl)
+```
+
+For a "good" goal, this sequence will succeed and leave a goal to prove which
+has no schematic variables in the assumptions (ideally also not in the
+conclusion, but those should be harmless). If this sequence fails, then there
+most likely is a problem with the parameters of the schematic precondition the
+goal is allowed to depend on, e.g. you have `?P x` in the precondition, but
+`vcg` is generating a goal that depends on some parameter `y`. This can happen
+when new parameters are introduced by `exE`, `clarsimp`, case distinctions, or
+other tactics. For instance you might have `x = Some y` in the assumptions and
+`?P (Some y)` as the schematic precondition, but the `vcg` needs `?P y`.
+Unification is generally not smart enough to figure out that `P (the (Some y))`
+would be a solution. In some cases the tactic `wpfix` can resolve the problem
+and replace `?P` with a new `?P` that is allowed to depend on more parameters.
+Otherwise, there are two remaining strategies:
+
+* go back to the place where the schematic `?P` is introduced and introduce the
+  parameter before the schematic, so `?P` can depend on the parameter. This could
+  happen for instance by using a better case distinction rule that manages
+  schematics, or by performing the relevant `exE`, `clarsimp` etc before the
+  schematic is introduced (not always possible).
+
+* go back to the place where the parameter `y` is introduced and prevent it from
+  being introduced. E.g. instead of using `clarsimp` to generate `x = Some y`
+  and using `y`, use `the x` instead. This is not necessarily nice, but should
+  always be available in principle.
 
 Another problem is to deal with sometimes 40 goals after expansion of this last goal, and usually very similar goals. So this idea is to 'generate' the more useful premises as possible before expanding (by `subgoal_tac` or `frule`).