coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proving UIP on decidable domains

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] proving UIP on decidable domains
Date: Thu, 15 Dec 2016 14:42:51 -0500
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-f171.google.com
Ironport-phdr: 9a23:0/EgZBBlxIrwkkTZFMsRUyQJP3N1i/DPJgcQr6AfoPdwSPv/rsbcNUDSrc9gkEXOFd2CrakV0KyI4uu7ACQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9GiTe5b75+NhS7oAHeusQYnIdpN7o8xAbOrnZUYepd2HlmJUiUnxby58ew+IBs/iFNsP8/9MBOTLv3cb0gQbNXEDopPWY15Nb2tRbYVguA+mEcUmQNnRVWBQXO8Qz3UY3wsiv+sep9xTWaMMjrRr06RTiu86FmQwLuhSwaNTA27XvXh9RtgqxFrhKvpx9xzYDab46aNvVxYqzTcMgGRWdDRMtdSzBND42+YoYJEuEPPfxYr474p1YWqRW+Ag+sC/nzyj9InHD227Ax3eI/HgHHwgwvAdQOsGjJp9jyNqcSVua1zKjLzTrda/NZxyny5ZPHchAku/6MXLZwfdDNxkkoEgPIl1OdopHmMTONzukBrXSX4u56We+si2MrsR99riazyss2l4XEhJ8ZxkjG+Clk2oo5O9O1RUFhbdK5HpZcqzuWO5V4T84gRWxjpTw0xaccuZGheSgH0JQnyADba/yAa4WI5wjsVOeVITthnXJle66ziw+88US9yODwS9O40FlNripCndnMsm4C2wbP5ciAT/tx5kah2TCR2ADP8uxIP1w4mK7BJ5MiwrM8jIQfvVrfEiPshUn7jrKael0h+uey6uTnZrvmpoWbN49xkgz+MKMumsq+AeQ7LAcOW3aU9vqn2b3s+E32WrRKjvksnqbFt5DaINwXprSlDA9NzoYj9xG/Ai+639QfhHkLNU5KeBaaj4fyIFzOO/D5DfKng1u2ijtrxvbGPqfgAprXNHTDnq3hLv5B7BtXzxN2xtRC7bpVDKsAKbT9QBzfrtvdWz0+NQWow+/hQPFw150TX37HVq2eNqLRvFuF68ogJuCNYMkevzOreKtt3OLnkXJswQxVRqKux5ZCMH0=

On 12/15/2016 02:28 PM, Gabriel Scherer wrote:

For the (Foo tt) example, note that there *is* a trivial proof... term.
(Because inference of depend pattern matching annotations is good enough.)

Goal forall f g : Foo tt, f = g.
refine (fun f g =>
match f, g with
| foo, foo => eq_refl
end).
Qed.

That's great! Inference of pattern matching annotations is nice, although I'm confused about when to anticipate them. Also, too bad I can't get similar support via destruct f, g - which is what I end up doing most of the time anyway.

-- Jonathan

[Coq-Club] proving UIP on decidable domains, Chunhui He, 12/15/2016
- Re: [Coq-Club] proving UIP on decidable domains, ikdc, 12/15/2016
  - Re: [Coq-Club] proving UIP on decidable domains, Cyprien Mangin, 12/15/2016
    - Re: [Coq-Club] proving UIP on decidable domains, Chunhui He, 12/15/2016
- Re: [Coq-Club] proving UIP on decidable domains, Thorsten Altenkirch, 12/15/2016
- Re: [Coq-Club] proving UIP on decidable domains, Jonathan Leivent, 12/15/2016
  - Re: [Coq-Club] proving UIP on decidable domains, Gabriel Scherer, 12/15/2016
    - Re: [Coq-Club] proving UIP on decidable domains, Jonathan Leivent, 12/15/2016
      - Re: [Coq-Club] proving UIP on decidable domains, Emilio Jesús Gallego Arias, 12/15/2016