coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [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: Re: [Coq-Club] apply without instantiating
Date: Thu, 24 Jan 2019 04:41:38 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.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-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:b7uuTRfbVuAvCgQCrjdEzzRllGMj4u6mDksu8pMizoh2WeGdxcS9Yh7h7PlgxGXEQZ/co6odzbaO4+a4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYr5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM38H/ZhNFsjKxVoxyhqR5ww4/Ib4+aO/VzZb/dfcoASGZdQspdSyxMD4WhZIUPFeoBOuNYopH5qVQQtxuxGwysBePywTFGnHD307Y60+MnEQrb2wEuG8wBsG7Ko9XwNKYeS+67w7PGzDXYaPNW3yzw55LOchA8u/2DQ69/cdfLxUY1CgPIl1OdopHmMTONzukAvHSX4/B9We6ziWMrsRx9rzauy8s2l4XEiJ4ZxkjZ+Sh53Io5P8O0RFJ1bNK+Dpdcqj2WO5FrTs4sR2xkoCg6xaMFtJKneSUHzZAqyh3EZPGIdoWE/xzuW/iMLjp9inJqZrGyiwq3/ES+0eL8WMa53VBXpSRfiNbMrGoC1xnL58iHVPR9+kCh1C6T2g/d9+9IPV04mbPcJZAu37I8j50Tvl/dESPsn0X2kbOWeV4j+ui17eTof6/qpoeGN49zlgHxLLghmtC+AeQ/NAgCRW+b+fmg1L3n+k35R7ZKgucqnanetZDWPcUbpqinDA9Jyosu5AqzAy273NgEn3QLNk9JdRyGgoTzJl3DLuz0Ae+6g1u2kTdrw/7GPqfmApXINnXNlKnufaxj5E5ZyAs/195R6IhaC7EaJ/LzXFT8u8beDh8kKQC73fvoCMhn2owERGKDGrWZP7/KsV+U+uIvJPGBa5MSuDbkMvQq+/rujWIillIGZqmo3Z4XaGiiEfh8IkWZZ2DsgtYbHmsQsAo+Vr+itFrXGzVUfjO5W782zjA9EoOvS4nZDMj5i7uYmSy/A5d+Z2ZcC1nKH22+JKueXPJZSi+IL8pw2hANSqOmTcd19xy0uQrrjZZuMfHT/AURs4+l2dRooeTOw0JhvQdoBtiQhjneB1p/mXkFEmdvjfJP5Hdlw1LG6pBWxvlRFNhd/fRMC11oPJjBieF2Fpb7R1CYJ4vbeBOdWtyjRAoJYJcp2dZXORR0HcjkgxzemSO3UedMyu67Qacs+6eZ5EDfYsZwz3Gai/sIsmJ+G45qGDTjgaRysQ/OG4TOjkOV0b6wcrgR1zLM82HFyneSuEZfU0h7VqCXBH0=
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Hi Jason,

trivial seems to instantiate the evar in this example

Coq < Goal forall T (y : T), exists x, x=y.
1 subgoal

============================
forall (T : Type) (y : T), exists x : T, x = y

Unnamed_thm < intros.
1 subgoal

T : Type
y : T
============================
exists x : T, x = y

Unnamed_thm < eexists.
1 focused subgoal
(shelved: 1)

T : Type
y : T
============================
?x = y

Unnamed_thm < trivial.
No more subgoals.

Unnamed_thm < Qed.
Unnamed_thm is defined

Coq < Check Unnamed_thm.
Unnamed_thm
: forall (T : Type) (y : T), exists x : T, x = y

Jeremy

On 22/1/19 5:32 pm, Jason -Zhong Sheng- Hu wrote:
> 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