Email Gateway (Aug 22 2022 at 14:09): Email Gateway (Aug 22 2022 at 14:09):From: Thomas Sternagel <Thomas.Sternagel@uibk.ac.at>
Dear List,
I'm trying to figure out mutual coinduction in a development version of
Isabelle/HOL (d4b89572ae71). In particular I want to use the coinduction
scheme for two sets defined by mutual coinduction, but I'm not even able
to formulate my goal in a way that I can use 'coinduct'.
Consider the following minimal example:
theory Tmp
imports
Main
begin
coinductive_set X and Y where
"n ∈ Y ⟹ Suc n ∈ X"
| "n ∈ X ⟹ Suc n ∈ Y"
lemma tmp:
shows "(∀x. P x ⟶ x ∈ X) ∧ (∀x. Q x ⟶ x ∈ Y)"
proof (coinduct rule: X_Y.coinduct)
sorry
end
In the first line of the proof of lemma 'tmp' the following exception is
raised
exception TERM raised (line 80 of "Isar/rule_cases.ML"):
Expected 2 binop arguments
∃n. B.0 = Suc n ∧ (Q n ∨ n ∈ Y)
What am I doing wrong? What is 'B.0'? I don't understand what's
happening here.
Tom
Email Gateway (Aug 22 2022 at 14:09):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Tom,
I fear that currently neither coinduct nor coinduction work properly with mutually coinductive predicates. Thus, in your example I would just use rule (+ goal_cases for the case names).
Note that few weeks ago the coinductive was generating a different (non-mutual) rule, that was exposing the internal construction (see NEWS). In your example this old rule looked like:
?X ?x ?xa ⟹
(⋀x xa. ?X x xa ⟹
(∃n. ¬ x ∧ xa = Suc n ∧ (?X True n ∨ n ∈ Y)) ∨
(∃n. x ∧ xa = Suc n ∧ (?X False n ∨ n ∈ X))) ⟹
Xp_Yp ?x ?xa
This rule may have worked better with coinduct(ion), but getting from Xp_Yp to X and Y was tedious in turn.
When I changed coinductive to produce the new rule, I haven’t seen any uses of mutually coinductive predicates in isabelle + AFP. Is your use-case a new development, or is it one that used to work with the old rule?
Cheers,
Dmitriy
Email Gateway (Aug 22 2022 at 14:10):From: Thomas Sternagel <Thomas.Sternagel@uibk.ac.at>
Its a new development.
Actually, I started with Isabelle/HOL 2016 where I encountered the 'old'
rule you describe below, but could also not figure out how to use it, so
I switched to development version d4b89572ae71, because the coinduction
scheme looked more promising there.
Thanks for the information, anyway.
Last updated: May 01 2024 at 20:18 UTC