Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Confusing Isar chained proofs

Email Gateway (Aug 23 2022 at 08:14):

From: Ian Hayes <Ian.Hayes@uq.edu.au>
I have some confusing behaviour in Isar proofs using chains of reasoning.
The theory below abstracts the issue (so that the proofs are (should be)
trivial).

Lemma trans1 is fine (there is a much more direct proof but its the Isar
I'm concerned with).

Lemma trans2 succeeds but looks like it should not.
Looking at the output of the proof state just after "u" it states "have
b ≤ a" and
then in the next step the "..." matches "a" rather than "b"
which is not what I assumed looking at the equivalent step in trans1.

Lemma trans3 fails to prove the second step because
the first step actually shows "have b ≤ a" and hence
the "..." matches "a" rather than (what I assumed) "b".

I think the issue is that "a ≥ b" is an /abbreviation/ that gets
replaced by "b ≤ a"
and that is what the Isar chaining proof sees.

The problem is that in the context I'm working in, I want to use proofs that
are (sometimes long) chains of ≥ steps (which don't work as expected).
I know it is possible to reverse the proofs and use ≤, but in my context
that is not the style of presentation I desire.

Is this really the intended behaviour of chained proofs for ≥ ?
Is there a way to do the chains of ≥ proofs?

Thanks in advance
Ian

theory Scratch
  imports Main

begin

locale test = order
begin

lemma trans1:
  assumes x: "c ≤ b"
  assumes y: "b = a"
  shows "c ≤ a"
proof -
  have u: "c ≤ b"
    by (simp add: x)
  also have v: "… = a"
    by (simp add: y)
  show ?thesis
    using u v by auto
qed

lemma trans2:
  assumes x: "a ≥ b"
  assumes y: "a = c"
  shows "c ≥ b"
proof -
  have u: "a ≥ b"
    by (simp add: x)
  moreover have v: "… = c"
    by (simp add: y)
  show ?thesis
    using u v by auto
qed

lemma trans3:
  assumes x: "a ≥ b"
  assumes y: "b ≥ c"
  shows "a ≥ c"
proof -
  have "a ≥ b"
    by (simp add: x)
  moreover have "… ≥ c"
    sorry

end

Email Gateway (Aug 23 2022 at 08:15):

From: Akihisa Yamada <akihisayamada@nii.ac.jp>
Dear Ian,

Isar's chained proofs are not about "...", but "also" that combines
facts by certain rules (AFAIK theorems given [trans] attribute) and
"finally" that gives the combined result as if you are "using" it.

"..." is just a shorthand for the last argument of the previous
statement (if I understand correctly), so you can be explicit when it
doesn't refer to what you want.

context order begin
lemma trans3:
assumes x: "a ≥ b"
assumes y: "b ≥ c"
shows "a ≥ c"
proof -
have "a ≥ b"
by (simp add: x)
also have "b ≥ c" using y.
finally show ?thesis.
end

Best regards,
Akihisa

Email Gateway (Aug 23 2022 at 08:15):

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

I know a way to do >= style proofs, although I never used it in my own proofs:

notepad
begin
fix a b c d :: int
have "a > b" (is "_ > ?rhs") sorry
also have "?rhs ≥ c" (is "_ ≥ ?rhs") sorry
also (xtrans)have "?rhs = d" sorry
finally (xtrans) have "a > d" .
end

The ‘xtrans’ trick has been briefly described in https://isabelle.in.tum.de/repos/isabelle/file/3ab52e4a8b45/src/HOL/Orderings.thy

Best,
Wenda

Email Gateway (Aug 23 2022 at 08:15):

From: Ian Hayes <Ian.Hayes@uq.edu.au>
Dear Akihisa,

My understanding (like yours) of "..." /was/ that it matches the last
argument of the previous statement
but lemma trans2 shows that in the case of ≥ it matches the first
argument of the previous statement.
I think this is because "a ≥ b" is an abbreviation that gets expanded to
"b ≤ a" and
then it is the last argument of this (i.e. "a" rather than "b") that
"..." matches.
I found this counter intuitive.
The interaction between abbreviations and Isar's "..." seems broken to me.

In our actual application the "b" can be quite large, so the chained
style with "..." makes it much more readable.

Thanks for your feedback
Ian

Email Gateway (Aug 23 2022 at 08:15):

From: Ian Hayes <Ian.Hayes@uq.edu.au>
Dear Wenda,

Many thanks for your feedback and the description of the pattern
matching trick.
Most useful.

The link you gave confirms that "..." stands for the wrong thing for ≥.
It seems to me that the "..." needs to be instantiated with the right
argument
of the previous statement /before/ the abbreviation for ≥ is expanded.
But that is probably a non-trivial modification to Isabelle/Isar.

Your link allowed me to find the following link
<https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-September/msg00034.html>
which is a response from Makarius to the same issue I am having.

Email Gateway (Aug 23 2022 at 08:15):

From: Akihisa Yamada <akihisayamada@nii.ac.jp>
Dear Ian, Wenda,

it seems we don't have to learn the "(xtrans)" trick nowadays, maybe
we've got enough [trans] rules?

And, yes, "..." is the last argument after normalization. What I wanted
to say is that it is so no matter you're in chaining proof or not.
General ways to avoid writing same thing twice (like "is") are
documented in Sec. 4.3.1 of the prog-prove document.

Best regards,
Akihisa

Email Gateway (Aug 23 2022 at 08:16):

From: Akihisa Yamada <akihisayamada@nii.ac.jp>
Dear Ian, Wenda,

it seems we don't have to learn the "(xtrans)" trick nowadays, maybe
we've got enough [trans] rules?

I'm sorry for the confusion, I was on a richer context than Main which
has nicer set of trans rules.

Best regards,
Akihisa

And, yes, "..." is the last argument after normalization. What I wanted
to say is that it is so no matter you're in chaining proof or not.
General ways to avoid writing same thing twice (like "is") are
documented in Sec. 4.3.1 of the prog-prove document.

Best regards,
Akihisa

On 2020/01/30 6:00, Ian Hayes wrote:

Dear Wenda,

Many thanks for your feedback and the description of the pattern
matching trick.
Most useful.

The link you gave confirms that "..." stands for the wrong thing for ≥.
It seems to me that the "..." needs to be instantiated with the right
argument
of the previous statement /before/ the abbreviation for ≥ is expanded.
But that is probably a non-trivial modification to Isabelle/Isar.

Your link allowed me to find the following link
<https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-September/msg00034.html>

which is a response from Makarius to the same issue I am having.

---

On Fri, 9 Sep 2011, Peter Lammich wrote:

I just wondered if it is possible to use the Isar-style transitivity
     reasoning with \ge, i.e.

note a\ge b also note ... \ge c finally have "a\ge c"

There is still no proper way to do it.  When I've introduced the concept
of calculational reasoning in Isar the >= abbreviations did not exist,
and
it was already known that it would not work. (The potential for confusion
when swapping order of concrete vs. abstract syntax was known long before
Isar, which was the reason for avoiding it in early Isabelle/HOL.)

Later >= was introduced nonetheless, when I was not looking / not quick
enough to explain the situation.  Since that time I have an item on my
TODO list to extend the "..." treatment of Isar to accomodate that
extension of the HOL library.  The >= abbreviation is an example where
bug / feature are one and the same thing.

---

I'm hoping this issue is moving up Makarius' TODO list :-)
In the meantime I think it should probably be documented in the Isar
manual
rather than hidden in a comment in Orderings.thy.

Thanks again
Ian

On 29/1/20 21:39, Wenda Li wrote:

Dear Ian,

I know a way to do >= style proofs, although I never used it in my
own proofs:

notepad
begin
   fix a b c d :: int
   have "a > b" (is "_ > ?rhs")  sorry
   also have "?rhs ≥ c" (is "_ ≥ ?rhs") sorry
   also (xtrans)have "?rhs = d" sorry
   finally (xtrans) have "a > d" .
end

The ‘xtrans’ trick has been briefly described in
https://isabelle.in.tum.de/repos/isabelle/file/3ab52e4a8b45/src/HOL/Orderings.thy

Best,
Wenda

On 29 Jan 2020, at 09:35, Ian Hayes <Ian.Hayes@uq.edu.au> wrote:

I have some confusing behaviour in Isar proofs using chains of
reasoning.
The theory below abstracts the issue (so that the proofs are (should
be) trivial).

Lemma trans1 is fine (there is a much more direct proof but its the
Isar I'm concerned with).

Lemma trans2 succeeds but looks like it should not.
Looking at the output of the proof state just after "u" it states
"have b ≤ a" and
then in the next step the "..." matches "a" rather than "b"
which is not what I assumed looking at the equivalent step in trans1.

Lemma trans3 fails to prove the second step because
the first step actually shows "have b ≤ a" and hence
the "..." matches "a" rather than (what I assumed) "b".

I think the issue is that "a ≥ b" is an /abbreviation/ that gets
replaced by "b ≤ a"
and that is what the Isar chaining proof sees.

The problem is that in the context I'm working in, I want to use
proofs that
are (sometimes long) chains of ≥ steps (which don't work as expected).
I know it is possible to reverse the proofs and use ≤, but in my
context
that is not the style of presentation I desire.

Is this really the intended behaviour of chained proofs for ≥ ?
Is there a way to do the chains of ≥ proofs?

Thanks in advance
Ian

---

theory Scratch
   imports Main

begin

locale test = order
begin

lemma trans1:
   assumes x: "c ≤ b"
   assumes y: "b = a"
   shows "c ≤ a"
proof -
   have u: "c ≤ b"
     by (simp add: x)
   also have v: "… = a"
     by (simp add: y)
   show ?thesis
     using u v by auto
qed

lemma trans2:
   assumes x: "a ≥ b"
   assumes y: "a = c"
   shows "c ≥ b"
proof -
   have u: "a ≥ b"
     by (simp add: x)
   moreover have v: "… = c"
     by (simp add: y)
   show ?thesis
     using u v by auto
qed

lemma trans3:
   assumes x: "a ≥ b"
   assumes y: "b ≥ c"
   shows "a ≥ c"
proof -
   have "a ≥ b"
     by (simp add: x)
   moreover have "… ≥ c"
     sorry

end

--
Professor Ian Hayes
Mail: School of Information Technology and Electrical Engineering,
      University of Queensland, Brisbane, Queensland  4072, Australia
CRICOS Provider No: 00025B
E-mail: Ian.Hayes@uq.edu.au
Work: (GMT+10 hours) +61 (7) 3365 2386 FAX: +61 (7) 3365 4999

Email Gateway (Aug 23 2022 at 08:16):

From: Dominique Unruh <unruh@ut.ee>
Hi,

one trick how to fix a situation like this without decreasing
readability is to write   (is "... >= _")  after the have-command. Since
the automatic binding of ... happens before the binding via "is", this
will bind ... to the actual lhs of >=. This way, you get the intuitive
meaning of ... with only small syntactic overhead.

Best wishes,
Dominique.

Email Gateway (Aug 23 2022 at 08:29):

From: Lukas Stevens <lukas.stevens+isabelle-users@in.tum.de>
I just reviewed this thread and played around with some of the suggested
workarounds and encountered the following surprising behavior.

lemma
  fixes a b c d :: int
  assumes "d ≥ c"
  assumes "c ≥ b"
  assumes "b ≥ a"
  shows "d ≥ a"
proof -
  note ‹a ≤ b›
  also note ‹b ≤ c›
  also have ‹… ≤ d› ― ‹Proof obligation: @{prop ‹b ≤ d›}› sorry
  finally show ?thesis sorry
qed

lemma
  fixes a b c d :: int
  assumes "a ≤ b"
  assumes "b ≤ c"
  assumes "c ≤ d"
  shows "a ≤ d"
proof -
  note ‹a ≤ b›
  also note ‹b ≤ c›
  also have ‹… ≤ d› ― ‹Proof obligation: @{prop ‹d ≤ d›}› sorry
  finally show ?thesis sorry
qed

The second proof is just like the first proof but with the direction of
≤ reversed. In the former one, the ellipsis seems to correspond to the
right-hand side of the initial note command (?). In the latter one, the
ellipsis seems to correspond to the right-hand side of the goal a ≤ d.

-- Lukas Stevens

Email Gateway (Aug 23 2022 at 08:30):

From: Manuel Eberl <eberlm@in.tum.de>
In both cases, the … refers to the right-hand side of the last "assumes"
command. The "note" does not change what "…" refers to at all.

I do find that behaviour a bit unfortunate myself. A related problem is
that when I show something like "f ∈ O(g)", then I would of course like
the "…" to refer to the "g" and not the "O(g)". But I can live with it,
and you can always pattern match to get the behaviour you really want.

Manuel

Email Gateway (Aug 23 2022 at 08:30):

From: Makarius <makarius@sketis.net>
That is a consequence of too many features stacking up over time, and not all
interactions have been ironed out yet.

You can replace "note ‹prop›" to "have ‹prop› by fact" to get the standard
discipline of binding the three dots.

Makarius

Last updated: Nov 21 2024 at 12:39 UTC