Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Coinduction on predicate defined wrt other coi...


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.)

  1. 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.

  1. 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.

  1. 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: Mar 29 2024 at 04:18 UTC