The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

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

On Mon, Oct 21, 2013 at 2:05 PM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

Well, it's pretty much how you guessed: you cannot prove wf1=wf2 without assuming a proof irrelevance axiom. You can do that by writing

Require Import Coq.Logic.ProofIrrelevance.

( http://coq.inria.fr/distrib/current/stdlib/Coq.Logic.ProofIrrelevance.html )

On 21 October 2013 13:36, <stolz+coq AT ifi.uio.no> wrote:

[My programmer instinct made me ask first on
http://stackoverflow.com/q/19479716/60462 -- apologies for missing out on the
coq-club so far!]

I have defined a simple structure:

Require Import Ensembles.

Record ConfigStructure {T:Type} : Type := mkCS {
  E: Ensemble T;
  C: Ensemble (Ensemble T);
  CS_wf : forall x y, In _ C x -> In _ x y -> In _ E y;
  rooted := In (Ensemble T) C (Empty_set T)
}.

CS_wf enforces a semantic well-formedness property upon construction, based on
the two arguments. Now later, I need to compare two records for equality --
what do I with the proof-component?

I started out with the following---I guess the two well-formedness should also
occur on the lhs?

Lemma CS_split: forall T e1 c1 wf1 e2 c2 wf2,
e1 = e2 /\ c1 = c2 -> mkCS T e1 c1 wf1 = mkCS T e2 c2 wf2.
Proof.
intros.
destruct H as [He Hc].
destruct He; destruct Hc.
f_equal.
Abort.

which takes me up to:

T : Type
e1 : Ensemble T
c1 : Ensemble (Ensemble T)
wf1 : forall (x : Ensemble T) (y : T),
      In (Ensemble T) c1 x -> In T x y -> In T e1 y
wf2 : forall (x : Ensemble T) (y : T),
      In (Ensemble T) c1 x -> In T x y -> In T e1 y
============================
 wf1 = wf2

I guess proof irrelevance also comes into play?

Grateful for any advice,
   Volker