Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Powerset construction for FSets

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Powerset construction for FSets


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page