coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: David Pereira <dpereira AT liacc.up.pt>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Powerset construction for FSets
- Date: Fri, 23 Jul 2010 16:20:38 +0100
Dear Thomas and Stéphane,
Thanks for the suggestions and pointer to the ATBR library.
Best regards,
David.
On Jul 23, 2010, at 4:08 PM, Stéphane Lescuyer wrote:
> You should probably use [fold] to iterate over the elements in the
> [subset] function (better computational behaviour and easier reasoning
> on the function after its been defined, than with Program Fixpoint).
> Also, using the accumulator in [add] to get rid of the extra [union]
> yields the following code:
>
> Module Powerset (M : FSetInterface.S).
> Module MSet := FSetList.Make(M).
>
> Definition add x (m : MSet.t) : MSet.t :=
> MSet.fold (fun s acc => MSet.add (M.add x s) acc) m m.
>
> Definition powerset (s : M.t) : MSet.t :=
> M.fold add s MSet.empty.
> End Powerset.
>
> With the following invariants for the functions:
> Property add_spec :
> forall x m s, MSet.In s (add x m) <->
> (MSet.In s m \/ exists s', MSet.In s' m /\ M.Equal (M.add x s') s).
>
> Property powerset_spec :
> forall s s', MSet.In s' (powerset s) <-> M.Subset s' s.
>
> Cheers,
>
> Stéphane
> --
> I'm the kind of guy that until it happens, I won't worry about it. -
> R.H. RoY05, MVP06
- [Coq-Club] Powerset construction for FSets, David Pereira
- Re: [Coq-Club] Powerset construction for FSets,
Thomas Braibant
- Re: [Coq-Club] Powerset construction for FSets,
Stéphane Lescuyer
- Re: [Coq-Club] Powerset construction for FSets, David Pereira
- Re: [Coq-Club] Powerset construction for FSets,
Stéphane Lescuyer
- Re: [Coq-Club] Powerset construction for FSets,
Thomas Braibant
Archive powered by MhonArc 2.6.16.