Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] rewriting without instantiating

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] rewriting without instantiating


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page