The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

In the book Pierre Castéran and I wrote, we give an example on binary
search trees (Ch. 11), which should easily be understood by any computer
scientist with enough background in algorithms.  I already had some
positive feedback about this chapter as teaching material.  It might
be too much for 1.5 hour course, though.

The first chapter of the book also seems to correspond to your needs,
in that chapter we use a sorting algorithm as an example for explaining
the process of describing and verifying algorithms.

Aside from this, you can also use functions about arithmetics, like
division, which we used as an example in chapter 9.  The nice part
about arithmetics is that you can specify the functions without need
for too much theory: when describing a sorted list it takes a little
time convincing yourself that you did really specify a sorting
algorithm; when describing a division function it is easier to say that
given n and m (with m non zero), you want q and r such that
n=m*q+r and 0 <= q < r.

When teaching, I usually rely on arithmetics for my examples, 
because it fits the common mathematical background of most audiences.

If you don't have our book, I can send you fragments of the chapters,
as a teaser, if you promise me that you won't make it publicly
available (the restriction is just because I don't want to have any
problems with the publisher).

Cheers,

Yves
-- 
INRIA, 2004 rte des Lucioles B.P.93, F-06902 Valbonne Cedex
tel: 0492387739, http://www-sop.inria.fr/marelle/Yves.Bertot

--- Begin Message ---

• From: coq-club-request AT pauillac.inria.fr
• To: coq-club AT pauillac.inria.fr
• Subject: Coq-club digest, Vol 1 #701 - 5 msgs
• Date: Fri, 30 Jun 2006 12:01:05 +0200 (MET DST)
• List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Send Coq-club mailing list submissions to
        
coq-club AT pauillac.inria.fr

To subscribe or unsubscribe via the World Wide Web, visit
        http://pauillac.inria.fr/mailman/listinfo/coq-club
or, via email, send a message with subject or body 'help' to
        
coq-club-request AT pauillac.inria.fr

You can reach the person managing the list at
        
coq-club-admin AT pauillac.inria.fr

When replying, please edit your Subject line so it is more specific
than "Re: Contents of Coq-club digest..."


Today's Topics:

   1. Re: Re: Coq-club digest, Vol 1 #699 - 5 msgs 
(casteran AT labri.fr)
   2. problems with coercions (Line Jakubiec-Jamet)
   3. Re: problems with coercions 
(roconnor AT theorem.ca)
   4. Re: problems with coercions (Virgile Prevosto)
   5. Examples for a class on Coq? (Adam Chlipala)

--__--__--

Message: 1
From: 
casteran AT labri.fr
Date: Wed, 28 Jun 2006 19:57:56 +0200
To: "Jorge F. Salas O." 
<jfsalaso AT cantv.net>
Cc: 
coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]Re: Coq-club digest, Vol 1 #699 - 5 msgs

Quoting "Jorge F. Salas O." 
<jfsalaso AT cantv.net>:

> Dear Sir,
>
> We, at the Escuela de Computación de la Universidad Central de   
> Venezuela, are beginning to use Coq as a tool for realize proofs and  
>  extract functional programs from them. We are interested in using   
> Coq especifically for proving theorems in the theory of formal   
> languages, mainly in linear and context-free languages. By example,   
> the equivalence between finite automata and linear languagues, the   
> pumping lemma, etc.
>
> We are using Bertot & Castéran book for learning the system and in   
> september we will conduct a seminar in the Calculus of Constructions  
>  and the Curry-Howard isomorphism.
>
> I ask you advice in order to find previous and recent results in this
> class of problems using Coq. Best if we can get a tutorial in using Coq
> for proving theorems in the formal language theory.
>
> Thanking you in advance.
>

  Dear Prof. Salas,

There are interesting contributions on formal language theory:
http://coq.inria.fr/contribs-eng.html

Please look also at the section on Concurrent Systems and Protocols.

The authors of these contributions certainly would tell you how to get
reports on these developments.

Best regards,

Pierre



> -- 
> Prof. Jorge F. Salas O.
> Laboratorio Mefis
> Escuela de Computación
> Facultad de Ciencias - UCV
> Tel. 605.1042/1070
>
>

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.


--__--__--

Message: 2
Date: Thu, 29 Jun 2006 17:18:54 +0200
From: Line Jakubiec-Jamet 
<jakubiec AT lif.univ-mrs.fr>
To: 
coq-club AT pauillac.inria.fr
Subject: [Coq-Club]problems with coercions

   Hello,

I have two questions about coercions in Coq.

* My first problem is illustrated by the following declarations:

Parameters (A B C :Prop).
Parameter Z:{A}+{B}->{A}+{C}.
Coercion  Z:{A}+{B}>->{A}+{C}. (*Syntax error: *)


But we can write:

Parameters (A B C :Prop).
Definition X:={A}+{B}.
Definition Y:={A}+{C}.
Parameter Z:X->Y.
Coercion  Z:X>->Y. (* Ok*)

I don't understand why it is different?


* Secondly, suppose we have :

Parameters (A B C :Prop).
Definition X:={A}+{B}.
Definition Y:={A}+{C}.
Parameter Z:X->Y.
Coercion  Z:X>->Y.

Parameter F:Y->Prop.
Definition f := exists v:B, F (Z (right A v)).

Why we have to use Z in the definition f to make the conversion between
an object of type X to an object of type Y ?
(it should be introduced by the coercion Z?).


Thanks for your help,


   Line

-- 
(**********************************************************)
(* Line Jakubiec-Jamet                                    *)
(* Laboratoire d'Informatique Fondamentale de Marseille   *)
(* Université de la Méditerranée (Aix-Marseille II)       *)
(* Faculté des Sciences de Luminy                         *)
(* 163, Avenue de Luminy                                  *)
(* 13288 - MARSEILLE Cedex 9                              *)
(**********************************************************)


--__--__--

Message: 3
From: 
roconnor AT theorem.ca
Date: Thu, 29 Jun 2006 11:33:16 -0400 (EDT)
To: Line Jakubiec-Jamet 
<jakubiec AT lif.univ-mrs.fr>
cc: 
coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]problems with coercions

On Thu, 29 Jun 2006, Line Jakubiec-Jamet wrote:

>  Hello,
>
> I have two questions about coercions in Coq.
>
> * My first problem is illustrated by the following declarations:
>
> Parameters (A B C :Prop).
> Parameter Z:{A}+{B}->{A}+{C}.
> Coercion  Z:{A}+{B}>->{A}+{C}. (*Syntax error: *)

Coercions are between classes, rather than types.  A class is a defined 
name with type forall (x1:A1)..(xn:An), s whre s is a sort, or Sortclass 
or Funclass.

If you define AB := {A}+{B} and AC := {A}+{C}, then you can make a 
coercion from AB to AC.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''


--__--__--

Message: 4
Date: Thu, 29 Jun 2006 18:01:18 +0200
From: Virgile Prevosto 
<virgile.prevosto AT m4x.org>
To: 
coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]problems with coercions

Hello,

Le Thu, 29 Jun 2006 17:18:54 +0200,
Line Jakubiec-Jamet 
<jakubiec AT lif.univ-mrs.fr>
 a Ã©crit :

> * My first problem is illustrated by the following declarations:
> 
> Parameters (A B C :Prop).
> Parameter Z:{A}+{B}->{A}+{C}.
> Coercion  Z:{A}+{B}>->{A}+{C}. (*Syntax error: *)

as already said, coercions are between classes, not arbitrary types

> * Secondly, suppose we have :
> 
> Parameters (A B C :Prop).
> Definition X:={A}+{B}.
> Definition Y:={A}+{C}.
> Parameter Z:X->Y.
> Coercion  Z:X>->Y.
> 
> Parameter F:Y->Prop.
> Definition f := exists v:B, F (Z (right A v)).
> 
> Why we have to use Z in the definition f to make the conversion
> between an object of type X to an object of type Y ?

I guess this is a side-effect of the above: (right A v) has type
{A}+{B}, not X. If you use a type annotation, the coercion is correctly
inferred:
(* ... *)
Definition f := exists v:B, F ((right A v): X).
Print f.
f = exists v : B, F (right A v:X): Prop
-- 
E tutto per oggi, a la prossima volta.
Virgile


--__--__--

Message: 5
Date: Thu, 29 Jun 2006 13:51:24 -0700
From: Adam Chlipala 
<adamc AT cs.berkeley.edu>
To: 
coq-club AT pauillac.inria.fr
Subject: [Coq-Club]Examples for a class on Coq?

I am looking for examples of practical uses of Coq to present in a 
class.  My big criteria are:

  * Applications outside of pure math are preferable.  I think of many 
developments in programming language semantics as "pure math" for this 
purpose.
  * I would like some small examples that could perhaps be presented in 
a 1.5 hour lecture, including some that are simple enough that they 
could be used early in the class to motivate why the audience should be 
interested in using proof assistants.
  * Some examples that use extraction would be good.

Can anyone point me to any good examples (with source code!) of this kind?

I would also be very interested to learn about any past successful 
doctoral-level classes focused on Coq.

Thanks!



--__--__--

--------------------------------------------------------
Bug reports: http://coq.inria.fr/bin/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

End of Coq-club Digest

--- End Message ---