Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] WLOG in Isabelle/HOL


view this post on Zulip Email Gateway (Apr 10 2023 at 17:13):

From: Marco Maggesi <marco.maggesi@unifi.it>
Hello,

I'm new to Isabelle.
I'm trying to do some basic plane Euclidean geometry using the HOL-Analysis
session.

Harrison in HOL Light made some tactics for implementing WLOG reasoning
(Without Loss of Generality https://www.cl.cam.ac.uk/~jrh13/papers/wlog.html
)

Are there similar tactics in Isabelle?

More generally, I'm looking for documents describing the Multivariate
library in Isabelle.
What do you think could be a good place to start?

Thanks,
Marco

view this post on Zulip Email Gateway (Apr 10 2023 at 17:24):

From: Manuel Eberl <manuel@pruvisto.org>
Hello,

there have been ideas to port this to Isabelle, but so far no one has
(to my knowledge). I don't remember in detail how the WLOG tactic works,
but I think it should be quite feasible to do something like this in
Isabelle, perhaps even with an Eisbach method.

I think I also remember that HOL Light's WLOG reminded me a bit of the
transfer method in Isabelle, so perhaps one could even realise it using
that (not sure if it would actually save work though).

As for the Analysis library, I fear there is no actual documentation of
that. There have been ideas to make one for a long time, but it we all
never really found the time to do that. However, what we at least did
was to tag important theorems and definitions with an "important" tag,
so you can try searching the library for that to find out what's there.
There's also a way to generate a PDF document containing all the
important definitions/theorems (which had several hundred pages if I
recall correctly).

There are some documents explaning particular aspects of the library,
e.g. the PDF on type classes and filters (which are crucial for
topological concepts like limits and open sets, but also e..g
derivatives) or the documentation for the real_asymp method (which
automates real asymptotics). I would just suggest that if you have
concrete questions about something, just ask.

Cheers,

Manuel

view this post on Zulip Email Gateway (Apr 11 2023 at 17:47):

From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hello,

I did at some point implement a wlog keyword for Isabelle. (Not a tactic
but a structured wlog command.)

This was some years back, I am not sure this still works in current
Isabelle versions.

If there is interest, I would be happy to go through the code and
resuscitate it.

However, my problem (that maybe the Isabelle core team or AFP editors
can answer) is the following:

What would be a place for such a development? If I just keep a Wlog
theory somewhere on my homepage, it is not going to be useful (bitrot,
hard to find, cannot use it in AFP submissions). Can such a thing be
published on AFP? (Considering that it does not contain actual proofs
except maybe an example or two.)

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Apr 11 2023 at 17:48):

From: Manuel Eberl <manuel@pruvisto.org>
Absolutely! The AFP does have a "Tools" section that is intended
precisely for such entries, and yours would not be the first of its kind.

Manuel

view this post on Zulip Email Gateway (Apr 11 2023 at 18:25):

From: Makarius <makarius@sketis.net>
If this is a structured Isar proof command, I would be interested to see it
(although I am rarely satisfied with such attempts, because it is very
difficult to get right).

Makarius

view this post on Zulip Email Gateway (Apr 11 2023 at 21:02):

From: Marco Maggesi <marco.maggesi@unifi.it>
Thank you Manuel for your quick and informative response.
For now, I'm just learning the system, so I will do my experiment without
using WLOG.

One quick question: I didn't know this mechanism of "keywords".
Is it possible to filter theorems with the "important" tag in the search
mechanism?

Thank you,
Marco

Il giorno lun 10 apr 2023 alle ore 13:47 Manuel Eberl <manuel@pruvisto.org>
ha scritto:

view this post on Zulip Email Gateway (Apr 13 2023 at 19:44):

From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hi,
Then I shall try to resurrect my code.

[Makarius]: If this is a structured Isar proof command, I would be
interested to see it (although I am rarely satisfied with such attempts,
because it is very difficult to get right).

I will post a link to the code here first. I'm open for suggestion how
to fix wrong use of Isar-interna (which there will probably be plenty
of) before posting it to AFP.

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Apr 16 2023 at 17:43):

From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hi,

I went through my wlog-code and made a working (and somewhat documented)
version of my wlog command.

The files are here:
https://github.com/dominique-unruh/isabelle-tidbits/tree/1d00f7f1f2fe76df49f6caeb35d83d2e091470bf/Wlog

And example of how the command works is this:

text ‹The theorem @{thm [source] Complex.card_nth_roots} has the
additional assumption \<^term>‹n > 0›.
  We use exactly the same proof except for stating that w.l.o.g.,
\<^term>‹n > 0›.›
lemma card_nth_roots_strengthened:
  assumes "c ≠ 0"
  shows   "card {z::complex. z ^ n = c} = n"
proof -
wlog n_pos: "n > 0"*
**    using negation by (simp add: infinite_UNIV_char_0)*
  have "card {z. z ^ n = c} = card {z::complex. z ^ n = 1}"
    by (rule sym, rule bij_betw_same_card, rule
bij_betw_nth_root_unity) fact+
  also have "… = n" by (rule card_roots_unity_eq) fact+
  finally show ?thesis .
qed

Another example is given in the file Wlog_Examples.thy. (It does not
have a ROOT file at the moment. Just download the files into the current
directory for testing.)

Small syntax explanation: wlog name: "assumption" adds the assumption
assumption without loss of generality. Sometime (e.g., when you want
to make use of symmetries), you need to make some of the variables in
the theorem general. Add generalizing x1 x2 ... for this. (This
affects the proof obligation for the wlog-command.) And finally,
assumptions (using the assume command) you made will vanish, unless you
mark them explicitly as something you want to keep (*keeping assmname1
assmname2 ...*). This is because sometimes dropping some assumptions
while introducing others wlog can make the proof obligation simpler.
Notice also that in the state window of Isabelle, the wlog-command
outputs some additional helpful information for the proof obligation proof.

I'm happy to hear any feedback (also about the ML-interna and the
realization of the structured command). If it is something that seems
feasible to me, I can then incorporate it in the AFP submission when I
make one.

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Apr 17 2023 at 07:14):

From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hi,

great to hear that it works in your cases. :)

Yes, that is some leftover debug output. I'll remove it before making
the Wlog-theories "official".

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Apr 17 2023 at 07:21):

From: Stepan Holub <holub@karlin.mff.cuni.cz>
Hi, Dominique,

of course, it would be lovely to have wlog!

I have been solving the problem by a not very nice scheme:

lemma fact_aux: <with the wlog assumption>
lemma fact: <using fact_aux>
hide_fact fact_aux

I have tried your code to two such cases, and it works well.

Small issue: after wlog is proved I am getting something like
([...], 3) (line 95 of "~/wlog.ML")
([...], 2) (line 95 of "~/wlog.ML")
([...], 1) (line 95 of "~/wlog.ML")

where ... is filled with assumptions that I  kept by
keeping assms

Stepan

view this post on Zulip Email Gateway (Apr 17 2023 at 07:50):

From: Stepan Holub <holub@karlin.mff.cuni.cz>
BTW, would it be better, to use standard
from ....
wlog ...
for ...
instead of the new keywords "keeping" and "generalizing"?

Stepan

view this post on Zulip Email Gateway (Apr 17 2023 at 08:01):

From: Dominique Unruh <cl-isabelle-users@lists.cam.ac.uk>
Hi,

Using "for" instead of "generalizing" is possible. But I think it is
still somewhat confusing because "for" usually binds names locally for a
command in Isabelle convention. (I.e., whenever I have a "for x", I
could just replace all the x's in the command by y's, and I would get
the more or less the same effect. But the "generalizing" refers to
existing variables (like arbitrary: in the induction command), and you
cannot change them unless you change the variable names also /before and
after/ the wlog command.)

Using "from" is problematic for two reasons:

* The technical reason is that "from xxx" does not remember the name
"xxx", only the term of that fact, while the wlog-command needs to
know the name of the fact. (In order to make the fact available
again under the same name.)  It's possible to heuristically figure
out which fact it might have been from the term, but that's a bit of
a hack.

* And I also feel that "from" does not capture what is happening here.
"from xxx" usually means "make xxx available for the proof of the
following theorem", so you would expect the proof of the wlog to
become /easier/ with more theorems in the from. However, the keeping
says which assumptions should still be available /after/ the wlog.
Adding more facts in "keeping" makes the proof of the wlog itself
/harder!/

But I'm definitely open for ideas for better names. (I tried using the
existing keywords such as "for" etc., but I ended up with something I
could hardly understand myself. The current words aren't optimal but
definitely better than what I had before in terms of understandability.)

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Apr 17 2023 at 08:39):

From: Stepan Holub <holub@karlin.mff.cuni.cz>
Hi,

concerning names, I think what you say is not true. The generalized
variables are changed from free to skolem. So, on the contrary, a user
expecting to be able to use the old names will be confused (blue changed
to brown).
Similar remark concerns the kept assumptions (including facts proved
before the use of wlog): unless they are kept explicitly, they are lost.
This a well known trap from induction, where "using" has to be used
before induction method is invoked.

Stepan

view this post on Zulip Email Gateway (Apr 17 2023 at 08:43):

From: Stepan Holub <holub@karlin.mff.cuni.cz>
P.S.: I was referring to names of facts. Concerning the names of
variables, we are in agreement, it indeed is the same as "arbitrary". So
perhaps "arbitrary" could be used as the keyword.

Stepan


Last updated: Mar 29 2024 at 04:18 UTC