coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proof with as

From: Christopher Ernest Sally <christopherernestsally AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] proof with as
Date: Tue, 18 May 2021 01:01:38 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=christopherernestsally AT gmail.com; spf=Pass smtp.mailfrom=christopherernestsally AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f52.google.com
Ironport-hdrordr: A9a23:FAGTUK1ESx+Em6KXS3f95gqjBKMkLtp133Aq2lEZdPUzSL3+qynOpoV+6faaskdzZJhNo7690cq7MBbhHPxOkOss1N6ZNWGM0gfGEGgI1+vfKlPbehEWKdQx6Ztd
Ironport-phdr: A9a23:1v20gxMxgn3AueRtivol6nasDRdPi9zP1u491JMrhvp0f7i5+Ny6ZQqDvKQr1gGXFtiEo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9AdgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/229pHJfQlFhTuwbbxyIRi0sA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODE38G7VisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8apMCAvQBPeZCron9vEcOrRymBQmsGuzv0CJDiHDs3a08zeshCh3G1xE9Ed0UtHTUqNX0P7oVXO+pzKnI1zTDb+hK2Tf68IjIcg4uoeuSUrJqd8re11IvFx/ejlqKrYzlOzOU2/8Cs2ie9eVgVOavh3Q7pAF2pzii38EhgZTGiYwJ0F7L7zl5wJorKt2iTk52ecCpHZhOuyyUKoZ7Rt0vTWF0tCs6xLAKp4O3cTUExpkjyBDSd+GLfomJ7x/sW+icIzd1iX14dL+ihRu88UqtxvD6W8Kp01hKtjJInsfQun0JzRDe6ciKRuFg8kqg2DuDzQDe5v9CLEspj6TUMYQhzaQ1lpcLsUTMACv2mELuga+TbEok++yo5/3mYrXhu5OQLoF0hwHgPqg0lcy/BuM4MgcKX2eF4+izyLrj/UjhTLVLiP05jLXZvYjEKcgHoqO1GQxY34Y55xqiDjqr0c4UkHkZIF5dfRKIlYnpO1XAIPDiCve/hkyhnytrx/DcP73hGYnNLn/bkLfhY7l98VBTyBA1zd9B/JJUFqoBL+j3Wk/1tN3VFRA5MwmuzObmDNVxzJ8RWWWKAqOBKqPdrUeI5v4zI+mLfIIapDH9K+E86/HyiX85hEQScLKy3ZoXbXC4Bu5pL1+YYXrqmNcBEH0FshAwTOzw2xW+VmtYYG/3VKYh7HlvA4W/SIzHW4qFgbqb3S79EIcANU5cDVXZOnfydp6YXO8MZTjaD9VnnycYHYOoT4swnUWltBX70KZgNurZ4CACs5/4yMN84+nCvR43/D1wSc+a1jfeHClPgmoUSmpuj+hEqktnxwLbuUCZq/lRFNgW5vQQFwlnb9jTyOt1D920UQXELI/hoLmOTdCvADV3RdU0kYZmi6NVFNCrjxSF1C2vUed9qg==

Hi Patricia

There is only one proof of equality in coq, eq_refl, so H0 should be eq_refl.

However, you might encounter some other problems, depending on the structure of your proof.

Regards

Chris

On Mon, 17 May 2021 at 22:43, Patricia Peratto <psperatto AT vera.com.uy> wrote:

I have proved a theorem:

Theorem neq_nil_cons (A:Type(x:A)(y:list A)(z:list A)(p:cons x y = z): not (z=nil).

I have a Fixpoint:

Fixpoint proof1 (A:Type)(l:list A) :=
match l with
| x :: (y :: s) as ys => neq_nil_cons A y s ys H0
| _ => something
end.

In the place of H0 I need a proof that (cons y s)=ys.

How I can do this?

Regards,
Patricia

[Coq-Club] proof with as, Patricia Peratto, 05/17/2021
- Re: [Coq-Club] proof with as, Dominique Larchey-Wendling, 05/18/2021
- Re: [Coq-Club] proof with as, Christopher Ernest Sally, 05/18/2021