Discussion:
[isabelle] Mutual coinduction
Thomas Sternagel
2016-09-26 11:07:49 UTC
Raw Message
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
Dmitriy Traytel
2016-09-26 13:33:54 UTC
Raw Message
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
Post by Thomas Sternagel
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'.
theory Tmp
imports
Main
begin
coinductive_set X and Y where
"n ∈ Y ⟹ Suc n ∈ X"
| "n ∈ X ⟹ Suc n ∈ Y"
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
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
Thomas Sternagel
2016-09-26 13:43:29 UTC
Raw Message
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.
Post by Dmitriy Traytel
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).
?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
Post by Thomas Sternagel
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'.
theory Tmp
imports
Main
begin
coinductive_set X and Y where
"n ∈ Y ⟹ Suc n ∈ X"
| "n ∈ X ⟹ Suc n ∈ Y"
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
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