Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] injectivity of constructors

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] injectivity of constructors


Chronological Thread 
  • From: Jasper Hugunin <jasperh AT cs.washington.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] injectivity of constructors
  • Date: Thu, 13 Dec 2018 19:55:37 -0800
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasperh AT cs.washington.edu; spf=None smtp.mailfrom=jasperh AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-ot1-f42.google.com
  • Ironport-phdr: 9a23:U2crixEONH4C6lNmwnBByZ1GYnF86YWxBRYc798ds5kLTJ78osSwAkXT6L1XgUPTWs2DsrQY07qQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDmwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODE38G7VisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8apMCAe4bMuZDt4nyuUEOpga8CwmxC+Pv1zlIhn7w3aYn1OkhExvJ3Bc4H90QqnTUrM74O7sJUeyvwqjH1y7Db/NX2Tf754jIbhchofeWUb1ubMXR1FAiGgXYhVuerozlOima1uULs2WD7upgU/ivi289pA1rrDiv3MEhgZTKiIIN0l3I6zl1zYIvKdC7SEN3e8CoHIZMuy2AOIZ6XMUvSHxytikg0L0Jo5u7cTAKyJs5wx7fbOSKc42S7RLiUOadODB4hG54dL6miRa//lasxvfzVsmz11ZKoS5FncfWun8R0BzT79CLSvp7/ki/xTaCzx7f5v1ALEwulqfWK4QtzqAtmpYPq0jOETH6lF3zjKCMd0Uk/uao6/7gYrXjvpKcNZV7ihrmMqswgMy/Af81PRQVX2SB9+Wzzqbj/U34QLVMgf02jq7ZsJbAKcsFu6G5HhdZ0pw/5BanEzemzNMYkGEbI1JCYRKLlpTmO1XTIP/jFvq/mFStkDJzx//cJLHhA5PNLmLCkLj7Z7p95VRcm0IPyoVU4IsRAbUcKtryXFXwvZrWFEwXKQuxlsTuE81wzMs+RG2SBK6fePfQuESQ6/gvC+KXIpAcozb8Lfc54PiogHMkzwxONZK11IcaPSjrVs9tJF+UNCK104UxVFwStw97d9TEzViLUDpdfXG3BvNu7Sp9F4u9DYbFSZyqhvqM0DrpRsQKNFADMUiFFDLTT6vBQ+0FMXPAKdQnjTUfVbmnRJMm01ejuBKok+M6fNqRwTURsNfY7PYw5+DXkktvpzl9DsDY1H3UCm8oxCUHQDg52K05qkt4mA+O
To use injection in the way you want to, you need to specify a term. Please do check the docs. Here is a minimal working example:
```
Goal forall a b c d : nat, pair a b = pair c d -> (a = c) * (b = d).
intros a b c d H.
injection H.
intros e2 e1.
exact (pair e1 e2).
Qed.
```

- Jasper Hugunin

On Thu, Dec 13, 2018 at 7:15 PM Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> wrote:
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.
>

Archive powered by MHonArc 2.6.18.

Top of Page