coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] injectivity of constructors

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] injectivity of constructors
Date: Fri, 14 Dec 2018 03:14:13 +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:UbBh/BMD3Jgzb2+Re+ol6mtUPXoX/o7sNwtQ0KIMzox0I/z5rarrMEGX3/hxlliBBdydt6oUzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlLiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkHKTA37X3XhMJzgqJVoh2hpgBwzYHbb4yOKPpxZbnQcc8GSWZdXMtcUTFKDIOmb4sICuoMJeJWoJfnp1QQqBu/BRSnCu31xT5GnX/22qs62PkmHA/CwgMgBcwBsHHUrdnvOqkdS+60zLLPzTXFdP5ZwzH96JXSfh8/vP6MQKh8ftDMyUQ2EQ7Ok1ueqYvgPzyP1+QNtXCW7+tmVeK1im4osRt9oja1xsoql4LHhZoVx0jL+Cll2oo5OMG0RUxhbdK5HpZdtjuWO5Z4T84hW21ltyI3xqcbtZO/fCUG0poqyh3FZ/CZa4SI7AzsWeWNLTp9gX9oe7KyihKs/kWl1+LxWNK73VdPoydBndTBuH4A2hnX58WHS/Zy5EGs0iuV2Q/J8OFLO0U0mLLbK5E/xr4wkYIevFjNESHrhEn6kbaaeEIr9OS18ujnZa7pqYGGO49zlwH+Lr8hmsuiAeQ+LwcCRXCb+f671L3/40L2XKlKjvwxkqnfqpzaItkbprK9Aw9S1YYj6AyzACuh0NQdhXUHLVRFdwybj4XxNFzCPOr0Aeqjj1muijtn2v7LM7z7DpnQIHXOk6/tfbNn5E5dzAozw8pf55VRCrwZJPz8RFXxu8LdDh45KQC6zfzoCdtm1oMZX2KCGbWWMKXPsVOS+O0gPvSMaJUPtzbgM/Ql/eLhjWclmV8BeqmkxYcYaHehHvh/P0qZZWfsjcwaHGcRvgs+SfTqh0eYXT5SYXayRaM86SshBIKoF4eQDryq1faK2z7+FZlLbEhHDEqNGDHmbc/MD/wLcWeZJtJruj0CT7moDYE7g0KArgj/nphqNOfR62U0vI340949s8/ejxw35HpYBtuG1GelRmdp2G4EWnk/wfYs8gRG1l6f3P0g0LRjHttJ6qYRC1ZoBdvn1+V/TuvKdEfEd9aNRkyhR4z8Uzg3U5Q8z8JIalsvQoz+3CCG5DKjBvour5LOHIY9q/iO1n7sYctx1jDPyft51gR0co50LWSjw5VH2U3TCorOzxrLvpuRLf1Z+QOUsWCJwCyJoV1SVxN2XePdR3cDa0DKrNP/oETfU7upDrdhOQxEm5eP
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Thanks all for the various replies, but injection doesn't work,
giving error
Ltac call to "injection" failed.
Error: Not a negated primitive equality.

Jeremy

On 12/14/2018 02:07 PM, Jasper Hugunin wrote:
> `injection` seems to fit your description, see
> https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.injection.
>
> - Jasper Hugunin
>
> On Thu, Dec 13, 2018 at 4:54 PM Lily Chung
> <ikdc AT mit.edu
>
> <mailto:ikdc AT mit.edu>>
> wrote:
>
> That follows from general properties of equality, and has nothing to
> do with constructors. Try f_equal.
>

[Coq-Club] injectivity of constructors, Jeremy Dawson, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Pierre Courtieu, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Lily Chung, 12/14/2018
  - Re: [Coq-Club] injectivity of constructors, Jasper Hugunin, 12/14/2018
    - Re: [Coq-Club] injectivity of constructors, Jeremy Dawson, 12/14/2018
      - Re: [Coq-Club] injectivity of constructors, Jasper Hugunin, 12/14/2018
        
        Re: [Coq-Club] injectivity of constructors, Jasper Hugunin, 12/14/2018
      - Re: [Coq-Club] injectivity of constructors, Dominique Larchey-Wendling, 12/14/2018
        
        Re: [Coq-Club] injectivity of constructors, Pierre Courtieu, 12/14/2018
        
        Re: [Coq-Club] injectivity of constructors, Lily Chung, 12/14/2018
        
        Re: [Coq-Club] injectivity of constructors, Elazar, 12/14/2018
        RE: [Coq-Club] injectivity of constructors, Jason -Zhong Sheng- Hu, 12/14/2018
- Re: [Coq-Club] injectivity of constructors, Jay Kruer, 12/14/2018
  - [Coq-Club] compound coercion, richard Dapoigny, 12/16/2018