Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] coinduction proof method

Email Gateway (Jan 09 2023 at 16:31):

From: Amarin Phaosawasdi <amarin.uiuc@gmail.com>
Hello,

(Apologies if you received this twice. I tried sending this to the mailing
list yesterday but I'm not sure it got through.)

I'm reading the coinduction example from this blog post:
https://www.joachim-breitner.de/blog/726-Coinduction_in_Coq_and_Isabelle

In particular, the Isabelle section that defines

coinductive le where
leN: "le N m"
| leS: "le n m => le (S n) (S m)"

and tries to prove

lemma min_le: "le (min n m) n"

The first step applies the coinduction proof method and shows this proof
obligation.

forall n m. (exists x. min n m = N /\ n = x) \/
(exists x y.
min n m = S x /\
n = S y /\
((exists x' y'. x = min x' y' ∧ x = x') ∨ le x y))

(I did a bit of renaming and using ascii here.)

To prove by coinduction, I need to show that "le (min n m) n" was formed by
the rules that define le. So it's either leN or leS.

For the leN case, I need to find an x such that

• min n m = N (the first argument of le)
• n = x (the second argument of le)

This makes sense.

For the leS case, I need to find an x and y such that

• min n m = S x (the first argument of le)
• n = S y (the second argument of le)
• le x y (the assumption of leS)

But I'm missing where
exists x' y'. x = min x' y' ∧ x = x'
came from.

I've found some helpful resources online:

• https://www.andreipopescu.uk/MGS2021/Lecture3_Coinductive_Predicates.pdf
• https://xavierleroy.org/CdF/2018-2019/9.pdf
  but neither of them seem to discuss any thing that maps to this extra
  exists x' y'. x = min x' y' ∧ x = x'
  clause. Or I'm not pattern matching the predicate P correctly.

Is it something along the lines of the coinduction hypothesis?

Thank you so much,
Amarin

Email Gateway (Jan 09 2023 at 16:58):

From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Amarin,

The coinduction rule for le is as follows:

X a b ⟹
(⋀x1 x2.
X x1 x2 ⟹
(∃m. x1 = N ∧ x2 = m) ∨ (∃n m. x1 = S n ∧ x2 = S m ∧ (X n m ∨ le n m))) ⟹
le a b

To use coinduction, you need to exhibit the relation X that is closed under the application of the introduction rules (in case of equality this would be the bisimulation witness). The disjunction with "le n m” is actually a small strengthening (not actually stronger than the rule without this disjunct, but convenient) that I would assume to be omitted in the tutorials you cite below. For many examples it will not be relevant.

Now the coinduction proof method instantiates X in your example with the relation "λa b. ∃n m. a = min n m ∧ b = m”. This is what you see below. Our ITP’14 paper (https://doi.org/10.1007/978-3-319-08970-6_7) describes this behavior of coinduction in Section 7.

Best wishes,
Dmitriy

Email Gateway (Jan 09 2023 at 17:27):

From: Amarin Phaosawasdi <amarin.uiuc@gmail.com>
Ah, thanks so much, also for the link to the paper!

Last updated: Apr 25 2024 at 08:20 UTC