Email Gateway (Aug 22 2022 at 17:24): Email Gateway (Aug 22 2022 at 17:24):From: "C.A. Watt" <caw77@cam.ac.uk>
Hi Andreas
Thanks for your detailed answer! It was a steep learning curve, but I
now have the proofs I want. The secret ingredient was the function using
Hilbert choice in the style of the JinjaThreads Runs_into_Runs_table.
Thanks again for your help!
Best wishes
Conrad
Email Gateway (Aug 22 2022 at 17:39):From: "C.A. Watt" <caw77@cam.ac.uk>
Hello
I've been attempting some coinductive proofs, and I've hit a situation
where I'm not sure to proceed. Any help would be greatly appreciated.
I've tried to make the situation as abstract as possible in the attached
theory file.
In this setting, I have a predicate P defined in terms of two
coinductive predicates. I would like to be able to perform coinduction
on it. I can define a variant of P, P_co, directly as a coinduction,
effectively unfolding the two underlying predicates simultaneously, and
this allows me to prove everything I want to coinductively.
In other areas of my proof, I would strongly prefer to use P's
representation. I want to either derive a coinduction rule for P so that
I no longer need P_co, or to prove that P_co implies P, whichever is
easier. However I've not been able to complete either proof.
I imagine this has some relation to the discussion/solutions presented
below, but I've not been able to follow through the connection myself.
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-November/msg00045.html
https://isabelle.in.tum.de/dist/Isabelle2017/doc/corec.pdf
Thanks in advance for any comments or suggestions. I'm new to
coinduction in Isabelle (and in general), so apologies if there is
something fundamental that I've missed.
Best wishes
Conrad Watt
Test_Coinduction.thy
Email Gateway (Aug 22 2022 at 17:39):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Conrad,
Let me first summarize how I understand your abstract example. transition describes a
transition system between states, and state_abs is an abstraction function on states.
abs_equiv is a relation on abstract states (possibly an equivalence relation).
The relation abs_trace associates with a start state all complete runs of the transition
system starting in this state, as a sequence of abstracted states. P is then the relation
composition of the abs_trace relation with the lifted abs_equiv relation.
All the functions and predicates in here are "primitively corecursive" in that they only
peel off one constructor at a time. So you don't need coinduction upto friends here. I'd
recommend to actually split the abs_trace definition into two. (Warning: I haven't worked
out the following in detail; it's just a sketch.)
Define a relation "trace" from states to complete runs of concrete states. Then prove that
trace s l' ==> EX l. abs_trace s l & l = lmap state_abs l'
and
abs_trace s l ==> EX l'. trace s l' & l = lmap state_abs l'
For the second implication, you want to define a primitively recursive function that
construct a concrete run from an abstract run using Hilbert choice. In my AFP entry
JinjaThreads, the theory LTS provides a bunch of examples in a similar context, e.g., the
lemma Runs_into_Runs_table.
The property l = lmap state_abs l' is equivalent to saying "llist_all2 (BNF_Def.Grp
UNIV state_abs) l l'". So we have
P s l ==>
EX l'. trace s l' &
(llist_all2 (BNF_Def.Grp UNIV state_abs) OO llist_all2 abs_equiv) l l'
and vice versa.
Now, the crucial bit is the lemma llist.rel_Grp. With that, you can transform
llist_all2 (BNF_Def.Grp UNIV state_abs) OO llist_all2 abs_equiv
into
llist_all2 (BNF_Def.Grp UNIV state_abs OO abs_equiv)
i.e., the equivalence closure of the abstraction function. With that characterisation, you
should be able to prove a suitable coinduction rule for starting from trace's.
As I mentioned earlier, my theory LTS in JinjaThreads does many such hops (except for the
llist.rel_Grp part), so you may go and look for some inspiration there.
Hope this helps,
Andreas
Last updated: Nov 21 2024 at 12:39 UTC