Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] lset contains unexpected elements

Email Gateway (Aug 22 2022 at 10:55):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Christoph,

Yes. Your lemma is correct. This is a bug in Nitpick. Nitpick was developed before the "codatatype" command was added to Isabelle, and it looks like I forgot to handle set functions properly. I'll look into this.

Cheers,

Jasmin

Email Gateway (Aug 22 2022 at 11:00):

From: Christoph Dittmann <f-isabellelist@yozora.eu>
Dear Jasmin,

Thanks, this is a relief.

Best,
Christoph

Email Gateway (Aug 22 2022 at 11:01):

From: Manuel Eberl <eberlm@in.tum.de>
Just out of curiosity: how does one prove this lemma? I played around
with it yesterday but could not figure it out.

Cheers,

Manuel

Email Gateway (Aug 22 2022 at 11:02):

From: Dmitriy Traytel <traytel@in.tum.de>
Hi Manuel,

the key ingredient is the following lemma proved by induction on the set
function (provided by the codatatype package).

lemma "y ∈ lset w' ⟹ w' = w ⟹ x = y"
by (induct y w' rule: llist.set_induct; subst (asm) w.ctr; simp)

This is the rather general approach. For the special case of lazy lists,
Andreas has a nice alternative characterization of lset in terms of lnth
in Coinductive_LList which might make things simpler (but more index-based).

Dmitriy

Email Gateway (Aug 22 2022 at 11:02):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Manuel,

You have to use the induction rule for lset. Here's the proof:

lemma "lset w = {x}"
proof(intro set_eqI iffI)
fix y :: "'a"
assume "y ∈ lset w"
thus "y ∈ {x}"
by(induction xs=="w :: 'a llist" rule: lset_induct)(subst (asm) w.code; simp)+
qed(subst w.code; simp)

Best,
Andreas

Email Gateway (Aug 22 2022 at 11:10):

From: Christoph Dittmann <f-isabellelist@yozora.eu>
Hello,

I have trouble understanding codatatypes. The AFP entry "coinductive"
defines lazy lists:

codatatype (lset: 'a) llist = LNil | LCons 'a "'a llist"

Then I define the infinite list containing only x (to my understanding,
this list should be unique):

consts x :: 'a
primcorec w where "w = LCons x w"

Then I expected "lset w = {x}" to hold. Turns out it doesn't:

lemma "lset w = {x}" try
(* Nitpick found a counterexample for card 'a = 2: Empty assignment *)

So I guess either my understanding of lset as "the set of all elements
occuring in the list" is wrong or my definition of w is not what I think
it is.

Could someone shed some light on this?

Thanks,
Christoph

Last updated: Apr 24 2024 at 01:07 UTC