coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] rewriting without instantiating
- Date: Mon, 3 Dec 2018 10:23:24 +0000
- Accept-language: de-DE, en-US
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga14.intel.com
- Dlp-product: dlpe-windows
- Dlp-reaction: no-action
- Dlp-version: 11.0.400.15
- Ironport-phdr: 9a23:Z09EHxQ4+DiTJvWHpoevs+Gpxdpsv+yvbD5Q0YIujvd0So/mwa6yYBKN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHJhMJtkKJVrhGvpxJ9zI7VfI6aO/Vwc7jBfdwBQWdNQtpdWzBDD466coABD/ABPeFdr4TlqVcAsBy+ChejBOPz0D9IgWf20bUn2OomEAHJwAwgEMgQv3TQotn+KaAfUeW0zKbUzTXMde1Z2TPn5IjTdRAuv/6MXa5qccrW0UkiDALFjlOMqYP7OzOZzPgCs2+e7+d5U++klmApqwZ0oje1x8csjJHEhoMTylDY6yp5xJw5KsCmR0N9fNWqE4NQujmHO4ZyXM8uWWFltSYgxrAGp5K3ZjUGxIknyhLHdvCKcoaF7gjtWeufOzt0mnxodbalixqv8kWs1vXwWtS13VtOtCZJjNnBu38X2xDN8MSLV/lw80G80jiVzQ/T8PtLIUUsmKrbNZEhxrkwm4IWsUTMBCD6hUr7gLWXdkUi5uin9eDnbq/6qZ+bMo94kgD+MqIwlcyjGek0LwwDU3aB9em81LDv5030TKtQgvErj6XUsIjWJcEBqa64Bw9V3Jwj6xG6Dzq+1dQYnGUILFJfdx2Zi4jlIUrOIPfmAvewn1SsijBrx+jdM73gBJXNMmbMkLP7cblh7E5czRI/zcpD6JJMFrEBPPXzV1ftu9zfFx81KhC7w+L6CNpmzY4eQmKOAqqBMKzIq1OI5+QvI/ONZIAPojr9JeIltLbSiipzklgEOKKtwJE/aXaiH/0gLV/TKS7nhc5EGmMXtCI/SvbrgRuMS2gASWy1Wvd23TY2B568Cp+HDqWsi7yI0SPxVslTZ2tGA12IV2zveoqYQfAUQCOUPsJl1DcDUO7yGMcayRiyuVqimPJcJe3O93hA7MOx5J1O/+TW0CoK23lxBsWZ3XuKSjgtzGIOWzIymqt4pB4kkwvR4e1Dm/VdUOdrybZRSA5jbMzdyfB3D5b5XQeTJo7UGmbjec2vBHQKdvx0w9IKZB8iSdCth0mfmSusH7IR0beMAc5s/w==
Dear Jermeny,
Dear Coq Experts,
I thought an easy solution would be to use rewrite giving the evar as
argument like this:
Require Import List.
Include List.ListNotations.
Goal forall T:Type, True.
Proof.
intro T.
evar (Φ1:list T).
evar (Φ2:list T).
assert(?Φ1 ++ [] ++ ?Φ2 = ?Φ1 ++ ?Φ2).
rewrite -> (app_nil_l ?Φ2).
But this doesn't work - Coq seems to ignore the argument. I would consider
this to be a bug.
It does work if I give Φ2 rather than ?Φ2:
rewrite -> (app_nil_l Φ2).
reflexivity.
Another thing I don't understand is why I can't use the evar name if I create
the goal in the way suggested by Armael:
Goal forall T:Type, exists (Φ1 Φ2 : list T),
Φ1 ++ [] ++ Φ2 = Φ1 ++ Φ2.
Proof.
do 2 eexists.
Fail rewrite -> (@app_nil_l T ?Φ2).
Can someone explain why the name ?Φ2 cannot be used here?
Best regards,
Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928
- [Coq-Club] rewriting without instantiating, Jeremy Dawson, 12/03/2018
- Re: [Coq-Club] rewriting without instantiating, Dominique Larchey-Wendling, 12/03/2018
- Re: [Coq-Club] rewriting without instantiating, Jeremy Dawson, 12/03/2018
- Re: [Coq-Club] rewriting without instantiating, Robbert Krebbers, 12/03/2018
- Re: [Coq-Club] rewriting without instantiating, Emilio Jesús Gallego Arias, 12/03/2018
- Re: [Coq-Club] rewriting without instantiating, Jason Gross, 12/04/2018
- Re: [Coq-Club] rewriting without instantiating, Emilio Jesús Gallego Arias, 12/03/2018
- Re: [Coq-Club] rewriting without instantiating, Armaël Guéneau, 12/03/2018
- Re: [Coq-Club] rewriting without instantiating, Robbert Krebbers, 12/03/2018
- Re: [Coq-Club] rewriting without instantiating, Jeremy Dawson, 12/03/2018
- RE: [Coq-Club] rewriting without instantiating, Soegtrop, Michael, 12/03/2018
- Re: [Coq-Club] rewriting without instantiating, Dominique Larchey-Wendling, 12/03/2018
Archive powered by MHonArc 2.6.18.