coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proving structural equality of dependent records in Coq

From: Rui Baptista <rpgcbaptista AT gmail.com>
To: Volker Stolz <stolz AT ifi.uio.no>
Cc: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Proving structural equality of dependent records in Coq
Date: Wed, 23 Oct 2013 09:32:41 +0100

The idea is you use ConfigStructureEq everywhere instead of eq, so that you're never faced with that question.

On Tue, Oct 22, 2013 at 12:59 PM, Volker Stolz <stolz AT ifi.uio.no> wrote:

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On 22.10.13 13.34, Rui Baptista wrote:
> You could also define a custom equality for ConfigStructure and
> use setoid rewriting.
>
> Definition ConfigStructureEq {T : Type} (cs1 cs2 : @ConfigStructure
> T) : Prop := cs1.(E) = cs2.(E) /\ cs1.(C) = cs2.(C).
>
> http://coq.inria.fr/distrib/current/refman/Reference-Manual029.html

Thank
>
you for your suggestion -- how would I use that definition when
facing the question

{| .. |} = {| .. |}

?

Volker (coq-club elided)
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.11 (Darwin)

iQCVAwUBUmZokRLpPok/0ba1AQIORwQAqP4U/nJXYObgIbAtSR3f2qwAGzAx60r+
kx3bEOufj13uNNl3s+yA6eQN5RR/FYYJftP8hNtNcEuBmpTVBNXg6FuS1ogUo5LO
IeLTuRrwpxG5yotnZOLBaNNlIms9UKDLz0+RqjAgXO81tlLviqAJ8PKkajX/Xfja
J0w/YrthAsw=
=hW7f
-----END PGP SIGNATURE-----

[Coq-Club] Proving structural equality of dependent records in Coq, stolz+coq, 10/21/2013
- Re: [Coq-Club] Proving structural equality of dependent records in Coq, Arnaud Spiwack, 10/21/2013
  - Re: [Coq-Club] Proving structural equality of dependent records in Coq, Rui Baptista, 10/22/2013
    - Message not available
      - Re: [Coq-Club] Proving structural equality of dependent records in Coq, Rui Baptista, 10/23/2013