coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] apply without instantiating

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] apply without instantiating
Date: Tue, 22 Jan 2019 07:16:08 +0000
Accept-language: fr-FR, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f45.google.com
Ironport-phdr: 9a23:eN4h0x9Xi4fMmP9uRHKM819IXTAuvvDOBiVQ1KB30uIcTK2v8tzYMVDF4r011RmVBdWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+557ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaKz43/mLZisJyg61Hrx2svAZwz5Lbb4yPKPZyYr7RcNUHTmRBRMZRUClBD5umYYsOEeUBJ/xYoJfgrFYQqhu+GBOsBP/uyjBWm3/9wKo30/wgEQ7YxgwgBcwBvG7Io9XyKacSS/y1zKjWwjXedP5W1jL955LJchAlu/2DQbVwcc/IxEQpCgjLjU2QpJT7Mz+J0ukBqWuW4up6We6ylWIqqBt9rzevy8s0hYTFmpgZxk3Y+Slk2oo4IcC0RFR7bNOqFpZbqjuUOJFsQsw4RmFloCY6xaMCuZ68ZCUKzY4oxx/ba/CefYmI5w/vWP+fITp3hH9pYr2/hxG18Uivzu3zSNO430pNripAitXMt3YN2ALP6sWfVPdx4kOs1SyM2g3T8O1IPF44mKnBJ5MuwrM8jp8Tvl7CHi/ylkX2lqiWdkA89+iw6uTofK/mpoWCOINulg7+NbkumtajAeQ5LAcOQnOW+eu51LL5/E35RK9GgeExkqncqJzaP9gUpralAw9J1YYu8wqwDzC/0NgBgXYHKE9FdwmcgojyO1DOJej4Au2lj1Stljdr3fHGMaf7DpXDNHiQ2IvmKPx27FcZww4ux/he4YhVA/cPOri7DkT2rZnTCgIzGw2y2efuTttngMdWE2mIG+qSNL7YmV6O/OMmZeeWLsdBszHkbvMh+vTGjHkjmFZbc7P/jrUNb3XtJvVrOV+UKVHrn80dEGoX9l4mTeHwklDEWjlOfWqzUr8U6TQyCYbgBoDGENP+yIed1Tu2S8UFLltNDUqBRC+xJte0HswUYSfXGfdP1zkNVLyvUYgkjEj8uwrzyr4hJe3RqHRB6cDTkeNt7uiWrikcsCRuBp3EgW6IRmBw2GgPQm1uhf0tkQlG0l6GlJNArblYGNhUva4bVw47MdvDyrU/BYyvHA3GediNRRCtRdD0WTw=

Did you try simple_apply? One of the differences with apply seems to be more or less what you want. It is not the only difference though.

Best regards

Pierre

De : coq-club-request AT inria.fr de la part de Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
Envoyé : mardi, janvier 22, 2019 7:33 AM
À : coq-club AT inria.fr
Objet : Re: [Coq-Club] apply without instantiating

I believe lots of tactics, e.g. trivial, will eliminate reflexive goals but not instantiating evars.

Thanks,
Jason Hu

On Jan 22, 2019 01:21, Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> wrote:

Hi,

Is there a way of applying a theorem without instantiating existential
variables in a goal?

For example, if you want to eliminate equality goals but not create
phony ones, as with the goals

a ++ b ++ c = ?d ++ ?e
and
f ++ g = f ++ g

I want some variant of

all : try (apply eq_refl).

which would catch the second goal but not the first

thanks

Jeremy

[Coq-Club] apply without instantiating, Jeremy Dawson, 01/22/2019
- Re: [Coq-Club] apply without instantiating, Jason -Zhong Sheng- Hu, 01/22/2019
  - Re: [Coq-Club] apply without instantiating, Pierre Courtieu, 01/22/2019
    - Re: [Coq-Club] apply without instantiating, Jeremy Dawson, 01/28/2019
      - Re: [Coq-Club] apply without instantiating, Pierre Courtieu, 01/28/2019
  - Re: [Coq-Club] apply without instantiating, Jeremy Dawson, 01/24/2019
    - Re: [Coq-Club] apply without instantiating, Théo Zimmermann, 01/24/2019