coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] test for term convertibility without instantiation

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] test for term convertibility without instantiation
Date: Sun, 30 Oct 2016 17:59:24 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f175.google.com
Ironport-phdr: 9a23:KZSAghAl0+hZq6DmFF1wUyQJP3N1i/DPJgcQr6AfoPdwSP74osbcNUDSrc9gkEXOFd2CrakV0ayJ7Ou5BDNIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TWM5DIfUi/yKRBybrysXNWD1YLoiKvrpsKbSj4LrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt+PxshyWbwyJ72ccW2NethdJHQXD8FmuXJD3syj3sudw8CafNMzyC7szXGLxvO9QVBb0hXJfZHYC+2bNh5kogQ==

That would work for top-level evars, but it would be harder to do if there are evars under binders.

--Jonathan

On 10/30/2016 05:21 PM, Jason Gross wrote:

You can assert the goal [term1 = term2], generalize over all of the evars,
and then see if [reflexivity] solves your goal. Is this what you're
looking for?

On Sun, Oct 30, 2016 at 4:38 PM Jonathan Leivent
<jonikelee AT gmail.com>
wrote:

Is there any way in Ltac to test if two terms are convertible without
inducing any evar instantiation, and without doing unnecessary reduction?

-- Jonathan

[Coq-Club] test for term convertibility without instantiation, Jonathan Leivent, 10/30/2016
- Re: [Coq-Club] test for term convertibility without instantiation, Jason Gross, 10/30/2016
  - Re: [Coq-Club] test for term convertibility without instantiation, Jonathan Leivent, 10/30/2016
    - Re: [Coq-Club] test for term convertibility without instantiation, Jonathan Leivent, 10/31/2016