Email Gateway (May 04 2024 at 16:33): Email Gateway (May 04 2024 at 16:33):From: Peter Lammich <cl-isabelle-users@lists.cam.ac.uk>
Dear List,
I'm trying to figure out how to prove goals of the form
EX x. P x y
where P is a coinductive predicate, and x,y have coinductive types .
For example (below), consider two functions that select a sublist of a
lazy list. The first selects an arbitrary sublist, the second takes an
additional sequence of Booleans that specifies whether to take the
corresponding elements or not.
Intuitively, for every result of the first one (implicit selection), we
should be able to find a corresponding explicit selection.
Unfortunately, I have no idea how to prove that, or even how to approach
such a proof ... :(
Any help or hints appreciated.
Peter
imports "Coinductive.Coinductive_List"
begin
coinductive is_subl :: "'a llist ⇒ 'a llist ⇒ bool" where
"is_subl xs LNil"
| drop: "is_subl xs ys ⟹ is_subl (LCons x xs) ys"
| take: "is_subl xs ys ⟹ is_subl (LCons x xs) (LCons x ys)"
coinductive is_subl' :: "bool llist ⇒ 'a llist ⇒ 'a llist ⇒ bool" where
"is_subl' ct xs LNil"
| "is_subl' ct xs ys ⟹ is_subl' (LCons False ct) (LCons x xs) ys"
| "is_subl' ct xs ys ⟹ is_subl' (LCons True ct) (LCons x xs) (LCons x
ys)"
(* Easy to show that explicit selection ⟹ implicit selection *)
lemma "is_subl' ct xs ys ⟹ is_subl xs ys"
apply (coinduction arbitrary: ct xs ys)
apply (force elim: is_subl'.cases)
done
(* How to prove the other way round? *)
lemma "is_subl xs ys ⟹ ∃ct. is_subl' ct xs ys"
Email Gateway (May 04 2024 at 18:38):From: Tjark Weber <tjark.weber@it.uu.se>
Peter,
Existential statements are often (best) proved by providing an explicit
witness term. Have you tried something along the lines of
primcorecursive ct :: "'a llist ⇒ 'a llist ⇒ bool llist" where
"ct xs ys = ..."
lemma "is_subl xs ys ⟹ is_subl' (ct xs ys) xs ys"
?
Best,
Tjark
När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/
E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy
Email Gateway (May 04 2024 at 19:29):From: Peter Lammich <cl-isabelle-users@lists.cam.ac.uk>
Thank you very much Tjark!
Of course I had tried the witness approach, and it got very cumbersome.
For my actual example, which is slightly more complex than is_subl (I'm
shuffling two lists), I couldn't get it through.
After writing the mail, I had tried again, more systematically, and got
it through. I didn't share that immediately, as I hoped for a maybe more
concise way to do that.
I'll share my approach here now. I systematically derived the witness.
One additional complication is that the cases of is_subl are not
disjoint, which needs additional work in the proof.
Any comments on whether there is a simpler/more systematic method are
appreciated!
Email Gateway (May 04 2024 at 20:29):From: Andrei Popescu <andrei.h.popescu@gmail.com>
Hi Peter,
I agree with Tijark, and with your own solution as well, which can be
made prettier but the essence will stay the same: The only way (I know
how) to prove such statements is by providing a corecursively
constructed witness.
Side comment: That is not the correct sublist relation for lazy lists
btw, as it allows you to prove that any infinite llist is sublist of
any other llist by just using drop in(de)finitely.
Cheers,
Andrei
Email Gateway (May 05 2024 at 06:55):From: Dmitriy Traytel <traytel@di.ku.dk>
Hi Peter,
Augmenting the previous answers with a pointer to Jasmin’s and mine guest entry on Larry’s blog:
https://lawrencecpaulson.github.io/2023/11/08/CoinductivePuzzle.html
The problem we consider there is different, but similar in spirit (we also construct a corecursive witness to prove an existentially quantified statement about lazy lists). We also use the (right) sublist relation under the name emb (with a small twist ensuring that finite lazy lists are only embedded in finite lazy lists, but this is easy to adjust by dropping that finiteness assumption). The corresponding formalization is in the AFP (Ordered_Resolution_Prover.Lazy_LList_Chain).
Best wishes,
Dmitriy
Last updated: May 19 2024 at 04:18 UTC