Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Implicitly referring to previous facts in the ...

Email Gateway (Aug 22 2022 at 16:58):

From: Wenda Li <wl302@cam.ac.uk>
Dear Isabelle users,

In the from-have paradigm, we can implicitly refer to the previous proved fact(s) using the “this” keyword. I was wondering if we can similarly refer to collected results implicitly in the moreover-ultimately paradigm? If not, would that be a good feature for future Isabelle?

Here is a minimal example:

notepad
begin
fix A B D::bool
assume foo:"A ⟹ B ⟹ D"

have "A" "B" sorry
from foo[OF this(1) this(2)] (*here, we can implicitly refer to the previous facts
using the "this" keyword*)
have "D" .

have "A" sorry
moreover have "B" sorry
ultimately have "D"
using foo[OF (*I wish to implicitly refer to A and B here,
like using the "this" keyword previously*)]

Many thanks,
Wenda

Email Gateway (Aug 22 2022 at 16:58):

From: Peter Lammich <lammich@in.tum.de>
Hi Wenda,

there is "calculation", but it seems to be removed by ultimately ...

notepad 
begin
  fix A B D::bool
  assume foo:"A ⟹ B ⟹ D" 

have "A" "B" sorry
  from foo[OF this(1) this(2)] (*here, we can implicitly refer to the
previous facts 
                                    using the "this" keyword*)
  have "D" .

have "A" sorry
  moreover have "B" sorry
  moreover have "D" using foo[OF calculation] .

^^ not very nice though to end a proof with moreover ...

Email Gateway (Aug 22 2022 at 16:58):

From: Wenda Li <wl302@cam.ac.uk>
Dear Peter,

have "A" sorry
moreover have "B" sorry
moreover have "D" using foo[OF calculation] .

Thanks for your quick reply. This is indeed one solution, despite of the slightly misleading syntax :-)

fix A B D::bool
assume foo:"A ⟹ B ⟹ D"

have "A" sorry
moreover have "B" sorry
ultimately have "D"
using foo

My main motivation for this is that when “A” and “B” are complex, we may want to perform some manual forward reasoning in the “ultimately” step, rather than solely relying on automatic tactics. Explicit naming “A” and “B” will do the job, but it seems a little unnatural and unnecessary.

Best,
Wenda

On 19 Mar 2018, at 14:43, Peter Lammich <lammich@in.tum.de> wrote:

Hi Wenda,

there is "calculation", but it seems to be removed by ultimately ...

notepad
begin
fix A B D::bool
assume foo:"A ⟹ B ⟹ D"

have "A" "B" sorry
from foo[OF this(1) this(2)] (*here, we can implicitly refer to the
previous facts
using the "this" keyword*)
have "D" .

have "A" sorry
moreover have "B" sorry
moreover have "D" using foo[OF calculation] .

^^ not very nice though to end a proof with moreover ...

--
Peter

On Mo, 2018-03-19 at 14:08 +0000, Wenda Li wrote:

notepad
begin
fix A B D::bool
assume foo:"A ⟹ B ⟹ D"

have "A" "B" sorry
from foo[OF this(1) this(2)] (*here, we can implicitly refer to the
previous facts
using the "this" keyword*)
have "D" .

have "A" sorry
moreover have "B" sorry
ultimately have "D"
using foo[OF (*I wish to implicitly refer to A and B here,
like using the "this" keyword previously*)]

Email Gateway (Aug 22 2022 at 17:00):

From: Makarius <makarius@sketis.net>
Naming facts that are referenced later in a non-local / non-linear
manner is the normal way in the Isar proof language. In practice about
5-10% of facts mightr require explicit names.

I don't see anything unnatural or unnecessary about it. On the contrary
too much implicit fact management can make Isar proofs hard to read and
hard to maintain, also hard to explain to casual readers who are not
familiar with the language.

Makarius

Email Gateway (Aug 22 2022 at 17:00):

From: Peter Lammich <lammich@in.tum.de>
In my opinion, it is indeed a bit strange that the moreover-ultimately
construction chains the implicit facts (so they are available for your
last proof) but you cannot name them.

ultimately have "D" by (blast intro: foo)

which the more experienced Isabelle user might be tempted to write is
not exactly clearer than

using foo[OF ...] .

So we have a construct that provides some nice implicit fact management
for the complicated cases, but not for the simpler cases, where a
simple forward proof does work.

Email Gateway (Aug 22 2022 at 17:00):

From: Makarius <makarius@sketis.net>
We are talking about the final step of a calculational proof here, i.e.
'finally' or 'ultimately'. The proof following that can be more than
just 'by', but there is no systematic way to refer to the chained facts
in a complex proof here.

This is not a problem of the calculation, but of what can be done with
"proof method ... qed method". I've once had something like this in the
pipeline:

<chained facts>
<goal>
proof -
case facts
then show ?thesis sorry
qed

I.e. the proof method "-" provides a case that "notes" the chained facts
for later use in the subproof. It did not emerge so far, because "notes"
cannot be part of proof method cases -- just by accident: it was not
required so far, and these things have some complexities internally.

Moreover, prospective applications for that have been too rare so far.
As a rule of thumb there need to be 2-3 good reasons to add more
features (read: complexity), not just half a reason. Alternatively, it
is possible to "trade" features: removing historic things that are not
really needed, and using the freed conceptual space to add new things.

Makarius

Last updated: Nov 21 2024 at 12:39 UTC