coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Dealing with equalities in dependent types

From: Anton Trunov <anton.a.trunov AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Dealing with equalities in dependent types
Date: Sat, 21 Jan 2017 00:32:22 +0300
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=anton.a.trunov AT gmail.com; spf=Pass smtp.mailfrom=anton.a.trunov AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f46.google.com
Ironport-phdr: 9a23:cwHFEx0Ip3w/WV73smDT+DRfVm0co7zxezQtwd8ZsesRLPad9pjvdHbS+e9qxAeQG96Kt7QY0KGP7/+oGTRZp83e4DZaKN0EfiRGoPtVtjRoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blItdaymUrLV2s+wzqW5/4DZSwROnju0J71ofzusqgCEn88Kho0qFrwszBzX6i9BffhRwyVhY06JghD7+O+/+Zdi92JbvPd3pJ0IarnzY6ltFe8QNz8hKW1gvMA=

> On 20 Jan 2017, at 17:44, Emilio Jesús Gallego Arias
> <e+coq-club AT x80.org>
> wrote:
>
> The example I like most is that people with plenty of Coq's experience
> still struggle to prove things like "rev nil = nil".

Emilio, thank you for a nice exercise!
The simplest solution I could come up with is like so:

From Coq Require Import Vector.
Fact rev_nil A : rev (nil A) = nil A.
Proof.
generalize (rev (nil A)).
now apply case0.
Qed.

—
kind regards,
Anton

[Coq-Club] Dealing with equalities in dependent types, Klaus Ostermann, 01/20/2017
- Re: [Coq-Club] Dealing with equalities in dependent types, Dominique Larchey-Wendling, 01/20/2017
  - Re: [Coq-Club] Dealing with equalities in dependent types, Anton Trunov, 01/20/2017
  - Re: [Coq-Club] Dealing with equalities in dependent types, Klaus Ostermann, 01/20/2017
- Re: [Coq-Club] Dealing with equalities in dependent types, Emilio Jesús Gallego Arias, 01/20/2017
  - Re: [Coq-Club] Dealing with equalities in dependent types, Anton Trunov, 01/20/2017
    - Re: [Coq-Club] Dealing with equalities in dependent types, Emilio Jesús Gallego Arias, 01/21/2017
  - Re: [Coq-Club] Dealing with equalities in dependent types, Vadim Zaliva, 01/21/2017