Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Mutually recursive coinductive predicates


view this post on Zulip Email Gateway (Aug 18 2022 at 15:45):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hello all,

I am having trouble understanding the coinduction rule that the
(co)inductive package produces for mutually recursive definitions.
Here's an example:

theory Test imports Nat_Infinity begin

coinductive even :: "inat set"
and odd :: "inat set"
where
"even 0"
| "odd n ==> even (iSuc n)"
| "even n ==> odd (iSuc n)"

The only coinduction theorem I was able to find, was even_odd.coinduct,
but it looks like this:

[| ?X ?x ?xa;
!!x xa.
?X x xa
==> ~ x & xa = 0 |
(EX n. ~ x & xa = iSuc n & (?X True n | odd n)) |
(EX n. x & xa = iSuc n & (?X False n | even n)) |]
==> even_odd ?x ?xa

Here are my troubles with this rule;

  1. Why is there a boolean parameter x to even_odd and similarly to X?
    (In case I have three mutually recursive predicates, there are even
    more booleans floating around!)

  2. How can I use this rule to ever prove anything about even or odd
    (e.g. that Infty is both even and add)?
    The conclusion only mentions the combined predicate even_odd.
    Searching for "even" or "odd" with find_theorems does not produce any
    theorems that relate even or odd with even_odd other than
    even_odd.coinduct.

Thanks in advance for any help,

Andreas

view this post on Zulip Email Gateway (Aug 18 2022 at 15:45):

From: Tambet <qtvali@gmail.com>
I replace ?X with function name "EO" and add some parentheses:

[| EO ?x ?xa;
!!x xa.
EO x xa
==> ~ x & xa = 0 |
(EX n. ~ x & xa = iSuc n & (EO True n | odd n)) |
(EX n. x & xa = iSuc n & (EO False n | even n)) |]
==> even_odd ?x ?xa

For me it seems that ?x is boolean and ?xa is number. Thus, I do the
corresponding replacement (for readability, not compileability):

[| EO isodd n;
!!isodd n.
EO isodd n
==> (~ isodd) & (n = 0) |
(EX m. (~ isodd) & (n = iSuc m) & ((EO True m) | (odd m))) |
(EX m. (isodd) & (n = iSuc m) & ((EO False m) | (even m))) |]
==> even_odd isodd n

This ((EO True m) | (odd m)) is odd rule then, but it basically says that
((odd m+1) | (odd m)). As m+1 is n, it's also a conclusion
(~(odd n - 1) ==> (EO True n)) or, in other words, (~(odd n - 1) ==> (odd
n)).

Tambet


Last updated: Mar 28 2024 at 16:17 UTC