coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] apply without instantiating

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] apply without instantiating
Date: Tue, 22 Jan 2019 06:21:06 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:GhbOmh+PGtn/zP9uRHKM819IXTAuvvDOBiVQ1KB31OgcTK2v8tzYMVDF4r011RmVBdWds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+557ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaKz43/mLZis1sg6xUrx2svAB/zJXObY2JKPZyYqHQcNUHTmRBRMZRUClBD5u4YYQRFeoOI+NYrongrFUAtxS/CxKsBOTpyjRVgXL42bM10/4/HgHD3A0sBdwAv27ardXuM6cSV/u4w7POzTXedf9Zxyry6JXSfh87vPGBRLR9etfSx0k3Dw7IgUmcpZb4Mz+J1OkBqXWX4uRiWO61lmIrtRx9riCyysosloXFnJwZxkzK+Clj3oo5OMG0RFRmbdOqFJZcry+aOJV1T88+RmxlvSg3xqEHtJO/eSUF1JUqyADEZPGCfYiF4hzuWPiULDhiinJldrayihCv+ka60OL8TNO70FNSoypFjNbMsncN2gTP58eJV/Vx4lqt1S+S2Q/R5OxIOEc0mrHFJJI7xb4wi4YTvl/EHi/rnkX5kbWadl0++uiv9+TofKnppoOdN49zjAHyKKMumtGjAeQ8NQgOWGub9f6g273k+E31WLRKjvsonanFqJ3XKtgXqrSkDwNJ0Isv8QuzAjmk3dgCgHULMk9JdAqCj4fzOlHOJP74De24g1SpiDplw+7JPqf/DZXILnnPirnvcqxz6k5Hzwozy8tS6IhSCrEcOv78RFL+tMHCAhAjLgy42/znB8ll1oMCRWKPBbeUP7/VsV+R/+4gP+2MZJIOtzvmMPgk5/vujWcjllMHfKmp24EXaHGiEfh8LUWZeymkvtBUW2wNp081SPHgoFyESz9aIXioFepo7TYiTYmiEI3rR4a3gbXH0j3tTbNMYWUTKF2WHHL5P6mNROwLbmrGAMJ7nzkVE5SoVJQm0zmnshK8xrZ6aOPJrH5L/an/3cR4srWA3So58iZ5WpzEgjO9Clpsl2ZNfAcYmaV2oEhz0FCGiPIqivpFU9Ff+rVAT1VjbMKO/6lBE9n3Hzn5UJKRUl//GIevByx3Q94shdYTMR4kRoeSyyvb1i/vOIc70ryGAJtorfD14kOpfoNG+i2D06MsyV47XsFIKGuqwLZl8BTeDJLIlEPfkLu2caMb32jG82LRlGc=
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

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