coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jason Gross <jasongross9 AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] test for term convertibility without instantiation
Date: Sun, 30 Oct 2016 21:21:47 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f182.google.com
Ironport-phdr: 9a23:iVqNCxJpjgWRkAcKjtmcpTZWNBhigK39O0sv0rFitYgULPnxwZ3uMQTl6Ol3ixeRBMOAuqgC1LWd6vy/EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuS9SU0Jv8jrzts7ToICxwzAKnZr1zKBjk5S7wjeIxxbVYF6Aq1xHSqWFJcekFjUlhJFaUggqurpzopM0r221qtvkg789NV7nhN+R9FOQATWduD2dgz8ry/TLHUAHHsnAbSyAdlgdCKwnD9hDzGJnr5HjUrO14jQuTJsrwBZ8uXi+5p/NpQQTvjigdMCUioUnYj8VxiORQpxf39E83+JLdfIzAbKk2RajaZ95PADMZBss=

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