Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland


Chronological Thread 
  • From: Bas Spitters <b.a.w.spitters AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] (user experience report) "Proof assistants as routine tools", Neil Strickland
  • Date: Mon, 1 Dec 2014 14:17:24 +0100

Neil makes an interesting observation on the lack of standardization
for even: N,Z,Q
Note that we have several variants of N already.

I know of at least three ways to organize this:
- modules, as in the std lib
- canonical structures, e.g. ssr and refinements CoqEAL
- type classes, e.g. math-classes

I agree that this is an important problem. I don't think we have a solution
yet.
Integration type classes and canonical structures via unification
hints would be a step forwards.
As would be a simpler module system, perhaps learning from agda.


At the MAP Spring School there is important work by the ssreflect team
to present an introduction to their library:
http://www-sop.inria.fr/manifestations/MapSpringSchool/program.html


Regarding the last slide. I am hoping that the new package manager and
regression suite and the new Coq interface can address some of these
problems.

On Mon, Dec 1, 2014 at 1:17 PM, Enrico Tassi
<enrico.tassi AT inria.fr>
wrote:
> On Sun, Nov 30, 2014 at 01:40:18PM +0200, Ilmārs Cīrulis wrote:
>> Probably a bit offtopic.
>>
>> It was easy to prove "(exists n, forall p, prime p -> p <=n) -> False".
>> But I had a problems proving "(forall n, exists p, prime p /\ p > n".
>
> That is exactly what the proof Cyril and myself pointed to shows.
>
> Lemma prime_above m : {p | m < p & prime p}.
>
> Here we have a sigma-type in Type (denoted with {x | P x}) instead of Prop
> (denoted with exists), hence we really construct the witness.
>
>> Do you have any hints? (Also, what does that SSReflect proof do?)
>
> The proof uses some facts from the math comp library, namely
>
> Lemma pdivP n : n > 1 → {p | prime p & p %| n}. (* %| means divides *)
> Lemma gtnNdvd n d : 0 < n → n < d → (d %| n) = false.
>
> The theories used are mostly here:
>
> http://ssr.msr-inria.inria.fr/doc/mathcomp-1.5/MathComp.prime.html
> http://ssr.msr-inria.inria.fr/doc/mathcomp-1.5/MathComp.div.html
>
> I guess you want to look at the pdiv function, that is the one computing
> the witness. Its correctness is not proved directly, but is rather a
> consequence of the correctness of the algorithm producing a prime
> decomposition (pdiv just picks the smallest item in the decomposition).
>
> Best,
> --
> Enrico Tassi



Archive powered by MHonArc 2.6.18.

Top of Page