# [isabelle] Coinduction on predicate defined wrt other coinductive predicates

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

theory Test_Coinduction imports "Coinductive.Coinductive" begin
typedecl state
typedecl abs
consts
transition :: "state \<Rightarrow> state \<Rightarrow> bool"
state_abs :: "state \<Rightarrow> abs"
abs_equiv :: "abs \<Rightarrow> abs \<Rightarrow> bool"
coinductive abs_trace :: "state \<Rightarrow> abs llist \<Rightarrow> bool" where
base:"\<lbrakk> \<forall>s2. \<not>transition s1 s2\<rbrakk> \<Longrightarrow> abs_trace s1 (LNil)"
| step:"\<lbrakk> transition s1 s2; abs_trace s2 l; state_abs s1 = as1\<rbrakk> \<Longrightarrow> abs_trace s1 (LCons as1 l)"
definition P :: "state \<Rightarrow> abs llist \<Rightarrow> bool" where
"P s l \<equiv> \<exists>l'. abs_trace s l' \<and> llist_all2 abs_equiv l l'"
coinductive P_co :: "state \<Rightarrow> abs llist \<Rightarrow> bool" where
base:"\<lbrakk> \<forall>s2. \<not>transition s1 s2\<rbrakk> \<Longrightarrow> P_co s1 (LNil)"
| step:"\<lbrakk> transition s1 s2; P_co s2 l; state_abs s1 = as1; abs_equiv as as1 \<rbrakk> \<Longrightarrow> P_co s1 (LCons as l)"
lemma P_co_imp_P:
assumes "P_co s al"
shows "P s al"
sorry
thm P_co.coinduct
lemma P_coinduct:
assumes "X xa xb"
and "(\<And>x1 x2.
X x1 x2 \<Longrightarrow>
(\<exists>a. x1 = a \<and> x2 = LNil \<and> (\<forall>b. \<not> transition a b)) \<or>
(\<exists>a b l aa' aa.
x1 = a \<and>
x2 = LCons aa l \<and>
transition a b \<and>
(X b l \<or> P b l) \<and>
state_abs a = aa' \<and> abs_equiv aa aa'))"
shows "P xa xb"
sorry
end

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