coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Primitive Projections and Inversion

From: Chung-Kil Hur <gil.hur AT gmail.com>
To: Coq-Club <coq-club AT inria.fr>
Subject: [Coq-Club] Primitive Projections and Inversion
Date: Thu, 28 Jul 2016 20:55:43 +0900
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gil.hur AT gmail.com; spf=Pass smtp.mailfrom=gil.hur AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw0-f169.google.com
Ironport-phdr: 9a23:/aIblRWa7syMZz1b8rRJ9JaK2DnV8LGtZVwlr6E/grcLSJyIuqrYZheOt8tkgFKBZ4jH8fUM07OQ6PG4HzJfqsrZ+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLshrj0pcKYP10ArQH+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6Lpyv/JHBI79ZuETSaFSRGAtNHlw78n2vzHCSxGO7z0SSDNFvABPBl3u7Az8UdLSsy+ylvdnkH2VPMmwTa0ucTun5qZvDhTvjXFUZHYC7GjLh5ko3+pgqxW7qkknzg==

Hi coq-club,

I am trying to use the new feature "primitive projections".

But, the inversion and dependent destruction tactics do not seem to work for records with primitive projections though it is possible to do inversion manually.

Here is an example.

=====================

Require Import Program.

Set Primitive Projections.

Record test := mk {

a : nat;

b : nat

Goal forall a b a' b', mk a b = mk a' b' -> a = a'.

intros.

inversion H. (* does not work *)

dependent destruction H. (* does not work *)

Abort.

Goal forall a b a' b', mk a b = mk a' b' -> a = a'.

intros.

apply (f_equal a) in H.

simpl in H. subst. reflexivity.

Qed.

======================

I wonder whether the inversion tactic will support primitive projections in near future, or there is other ways to do inversion for such records.

Thanks.

Best,

Gil

[Coq-Club] Primitive Projections and Inversion, Chung-Kil Hur, 07/28/2016