Discussion:
[isabelle] Continuing with a proof after a failed 'done'
(too old to reply)
Lars Hupel
2016-08-02 14:41:21 UTC
Permalink
Raw Message
Dear list,

I'm currently working on refactoring a rather large Isar proof. In
there, I have a small number of short 'apply' scripts. When these break,
I get "Failed to finish proof" as expected on 'done'. However, unlike a
failed 'by' proof, I can't continue with the rest of the proof.

Consider this small example:

lemma
assumes P Q
shows "P ∧ Q"
proof
show P
by rule
next
show Q
sorry
qed

Here, the "show Q" part can be checked as normal. However:

lemma
assumes P Q
shows "P ∧ Q"
proof
show P
apply rule
done
next
show Q
sorry
qed

.. everything after 'done' is red.

(I guess this counts as a "feature request".)

Cheers
Lars
Andreas Lochbihler
2016-08-02 14:53:00 UTC
Permalink
Raw Message
Hi Lars,

Just insert a "sorry" after the failing "done" and you can go on.

Andreas
Post by Lars Hupel
Dear list,
I'm currently working on refactoring a rather large Isar proof. In
there, I have a small number of short 'apply' scripts. When these break,
I get "Failed to finish proof" as expected on 'done'. However, unlike a
failed 'by' proof, I can't continue with the rest of the proof.
lemma
assumes P Q
shows "P ∧ Q"
proof
show P
by rule
next
show Q
sorry
qed
lemma
assumes P Q
shows "P ∧ Q"
proof
show P
apply rule
done
next
show Q
sorry
qed
... everything after 'done' is red.
(I guess this counts as a "feature request".)
Cheers
Lars
Lars Hupel
2016-08-02 14:54:15 UTC
Permalink
Raw Message
Hi Andreas,
Post by Andreas Lochbihler
Just insert a "sorry" after the failing "done" and you can go on.
of course, that's a possibility, but I don't understand why 'done' and
'by' behave differently there in the first place.

Cheers
Lars
Lars Hupel
2016-08-02 14:59:15 UTC
Permalink
Raw Message
Neither do I understand why they behave differently. Probably only
Makarius knows. The short forms "." and ".." also behave like done and
differently from their long forms "by this" and "by rule". It looks like
"by" is the outsider, because "proof(rule) qed" does not close the proof
block, either.
Right, I forgot about 'qed'. This one is not as easy to work around
using a single strategically placed 'sorry'.
Andreas Lochbihler
2016-08-02 15:01:28 UTC
Permalink
Raw Message
Hi Lars,

Neither do I understand why they behave differently. Probably only Makarius knows. The
short forms "." and ".." also behave like done and differently from their long forms "by
this" and "by rule". It looks like "by" is the outsider, because "proof(rule) qed" does
not close the proof block, either.

Andreas
Post by Lars Hupel
Hi Andreas,
Post by Andreas Lochbihler
Just insert a "sorry" after the failing "done" and you can go on.
of course, that's a possibility, but I don't understand why 'done' and
'by' behave differently there in the first place.
Cheers
Lars
Makarius
2016-08-02 15:26:52 UTC
Permalink
Raw Message
Post by Lars Hupel
Hi Andreas,
Post by Andreas Lochbihler
Just insert a "sorry" after the failing "done" and you can go on.
of course, that's a possibility, but I don't understand why 'done' and
'by' behave differently there in the first place.
After so many years, PIDE document editing still lacks substructural
error-recovery.

The 'by' command is based on a special trick, using
Proof.future_terminal_proof: it pretends to be finished on the toplevel
and forks the actual work.

The 'sorry' and '\<proof>' commands always finish, imitating the same
behaviour.

All other proof commands just work sequentially on the surface.


Only recently, I have started to introduce some formal source structure
for indentation in the editor. More will come eventually, and error
handling in continuous checking should somehow participate.


Makarius

Loading...