coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] apply without instantiating

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] apply without instantiating
Date: Tue, 22 Jan 2019 06:32:48 +0000
Accept-language: en-CA, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM02-CY1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:5GgBxxQ65PX0Mbj9yY9hn4wm5Npsv+yvbD5Q0YIujvd0So/mwa6yYBSN2/xhgRfzUJnB7Loc0qyK6/CmATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbB/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHJhMJtkKJVrhGvpxJ9zIHIb46YL+Bxcr/Bcd4AWWZNQthdWipcCY28dYsPCO8BMP5coYbnvFsOqh2+DhS1COzsyj9IgXn23aIn2Oo8EQHJwgogH90XvH/Jrtv1KboZXOe7zKbVzTXCbuhW1Snh5ITVbhwsuvGMXbVsccrU00YvFgfFgk+MpoziOjOYz+IAuHWY4ep4Te+ihHIrpxt1rzSx3MshhZPFip8JxlzY7Sl5zpg6KN6kREN+ZNOrDpRduDuEO4ZzQM4vTG9luCg/x70ItpO0YCsHxZE6yxHCZPGKco6F6Q/5WumLOzd3nndldaq/hxms9UigzfXxWNGo3VhNsiZJjMDAu24P2BDO88SHTeBy8Vm71TaIygDT9vpLIUcplardNpEt2KYwloAUsUTfACD5hFn2jK6RdkUi4OSo7PnnYqnipp+bMI90iRvyPbgpmsy6Geg4Mw4OUHaH+emk27Dv4Vf1TbFUgvEsnaTVqo3WKdgHqqKhBg9ayIcj6xKxDze819QYmGEKLFxYdxKHjonpIE/CLOzlAfujmFmskDBrx+zDPrL7A5XNKmLPn6vmfbZ480Jc0hY8zchD55JIDbEMOO78WkjotNDBEhA5NxG0zP38BdVm1oIeXHqPDbWDPKPTt1+I/OMvLPOWaI8bojauY8QisrTlimZ8klsAd4Go24EWYTa2BL4ud06eeD/nhsoLOWYMpAs3CuLw3g6sSzlWMlS7RKU6rnQJCIWgAs/4Ro2rj/nJ/DrzSpNaZnJdUAjVSV/ocJmBUvYILimVJ5kywXQ/SbG9Rtp5hlmVvwjgxu8/d7uGymgjrZvmkeNNyajWnBA2+yZzCp3GgWGKU2R9n2dOTDgzjvkm/R5Nj2yb2K09uMR2UMRJ7qoSAAc9KZvVzug8ANf3CFqYI4W5DW2+S9DjOgkfC9I8x9hSPBRbMvD61FXo7nPvBLUY0buWGJYz76TQmWDrINpwwGrH069niEQ6RsxINiutgastrgU=

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