The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Cody Roux a écrit :
> You could take a look at:
> Interactive Theorem Proving and Program Development
> Coq'art:The Calculus of Inductive Constructions
> from Yves Bertot and Pierre Casteran
> (Springer)
>
> This covers the subject in some detail. The short answer, though, is:
>
> (1) Any tactic works just as well for a goal of type Prop or of type Set
> exept eventually the elimination of the existential quantifier (for
> technical reasons).
>
> (2) You can use these techniques for programm building: if you "prouve"
> the goal of type: forall l:list, Sorted_list(l). With Sorted_list(l) the
> type of all sorted lists of l (i.e. sorted lists with the same elements
> than l), than you have built a programm that sorts a list, and in the
> same time proven it's correctness.
>   

Yes, but consider also  that, if you build a term of such a type by 
using automatic tactics,
you may not control the underlying algorithm, and obtain a very 
inefficient sorting algorithm.
restrict the  use of automatic tactics to subterms of type Prop.

Pierre


> Hope this helps
>
> Cody
>
> On Wed, 2007-12-19 at 15:17 +0100, Areski Nait Abdallah wrote:
>   
> > Hello,
> >
> > I am looking for a reference which discusses 
> >
> > 	(1) which tactis can be used for solving a goal of type Set, and 
> >
> >         (2) covers the rationale for such tactics.
> >
> > Thank you for your help,
> >
> > Areski
> >
> > --------------------------------------------------------
> > Bug reports: http://logical.futurs.inria.fr/coq-bugs
> > Archives: http://pauillac.inria.fr/pipermail/coq-club
> >           http://pauillac.inria.fr/bin/wilma/coq-club
> > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
> >     
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>