Re: [isabelle] Coinduction on predicate defined wrt other coinductive predicates



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

On 2018-06-19 21:47, Andreas Lochbihler wrote:
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.

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

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.