Of course "apply proof_irrelevance" did the trick -- it just didn't work in my case because I had a Require Import ClassicalFacts
up in my script, whereas I would have needed Coq.Logic.ProofIrrelevance
, as a Coq-Club member pointed out.
Proving structural equality of dependent records in Coq
-
01-07-2022 - |
Frage
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?
Lösung
Lizenziert unter: CC-BY-SA mit Zuschreibung
Nicht verbunden mit StackOverflow