Email Gateway (Jan 11 2023 at 10:44): Email Gateway (Jan 11 2023 at 10:44):From: amarin.uiuc@gmail.com
Hello,
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 re-formatting, 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.
To show that "le (min n m) n" was formed by leN, I need to find an x such that
This makes sense.
I'm a bit confused by the second case, which is to show that "le (min n m) n"
was formed by leS.
It makes sense that I need to find an x and y such that
But I'm missing where
exists x' y'. x = min x' y' /\ x = x'
came from.
Is it the coinduction hypothesis?
And also as a related question, I've been reading
https://xavierleroy.org/CdF/2018-2019/9.pdf. Page 16 discusses the coinduction
principle. Those slides are based on Coq, but the concepts are relevant to
helping me understand coinduction and the following question.
From page 16, I'm trying to map the coinduction principle to the proof
obligation that Isabelle generates.
What is the P(n) for "le (min n m) n"? The slides don't explicitly mention
anything about the coinduction hypothesis either.
Can somebody help me connect the dots, please?
Thank you,
Amarin
Last updated: Apr 25 2024 at 04:18 UTC