coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] decide equality on more types

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] decide equality on more types
Date: Fri, 8 Jul 2016 12:14:54 -0400
Authentication-results: mail2-smtp-roc.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-f193.google.com
Ironport-phdr: 9a23:EY9SRxMUX/nSJUr+sSkl6mtUPXoX/o7sNwtQ0KIMzox0KPj8rarrMEGX3/hxlliBBdydsKMczbGO+PG5EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuS9aU1Jz8hrn60qaQSj0AvCC6b7J2IUf+hiTqne5Sv7FfLL0swADCuHpCdrce72ppIVWOg0S0vZ/or9ZV2n8P4Ld5q4YADP27LOwESulTCy1jOGQo7uXqswPCRE2B/CgySGITxzhPBQHZ7Bj8FrP8szX3sPY1jCudO8z1QLQ5VByt6q5qTFnjjyJRZG1xy33elsEl1PETmxmmvREqntbZ

On 07/08/2016 11:56 AM, Matthieu Sozeau wrote:

Hi Jonathan,

...
Both fin_eqdec and Fin3_eqdec are closed under the global context, as they
are using instances of decidable equality for nat and fin.
This eqdec_proof tactic is not able to handle your Finx example currently
though, it's also work in progress. How did you implement your tactic?

I am close to having a standalone demo version that uses the standard Eqdec_dep. So I will send this to you as soon I have it, which should be quite soon. It is not very big or complex.

I was about to put in a JMeq detector (see https://coq.inria.fr/bugs/show_bug.cgi?id=4908) to leverage JMeq only if it was both needed and previously Required, but PMP warned me about it possibly being a bug, so I won't bother. Although, to PMP, all of my Ltac scribbles look like bugs. ;-)

-- Jonathan

[Coq-Club] decide equality on more types, Jonathan Leivent, 07/05/2016
- Re: [Coq-Club] decide equality on more types, Jason Gross, 07/05/2016
  - Re: [Coq-Club] decide equality on more types, Jonathan Leivent, 07/05/2016
    - Re: [Coq-Club] decide equality on more types, Jason Gross, 07/05/2016
      - Re: [Coq-Club] decide equality on more types, Jonathan Leivent, 07/06/2016
        
        [Coq-Club] Ltac way to detect symbol definedness (was Re: decide equality on more types), Jonathan Leivent, 07/06/2016
        
        Re: [Coq-Club] decide equality on more types, Matthieu Sozeau, 07/08/2016
        
        Re: [Coq-Club] decide equality on more types, Jonathan Leivent, 07/08/2016
        
        Re: [Coq-Club] decide equality on more types, Jonathan Leivent, 07/08/2016
        Re: [Coq-Club] decide equality on more types, Jonathan Leivent, 07/08/2016