The Coq mailing list

[Filou Vincent <vincent.filou AT labri.fr>]

Hi all,

I  was wondering if there was any way to prove the lemma stated at the 
end of this mail.
I suppose the fact that FMaps implementations carry proofs prevents it.
I have proven a weaker version with an equivalence relation, but I'd 
rather use the coq equality version.
Would adding a proof irrelevance axiom in the FMapList module solve the 
problem?
(if so, has anybody implemented such a solution?)
What would be the consequences of the adjonction of this axiom?
In other words, would I "break something" by adding it?

Thanks

Vincent Filou


Require Import FMaps.
Require Import FMapList.
Require Import FSets.

Module Map := FMapList.Make(Nat_as_DT).
Module MapFacts:= FMapFacts.Facts(Map).

Parameters (I A B:Type)
          (RA:relation (Map.t A)).

Let C := (A*B)%type.

Definition MapI := Map.t I.
Definition MapA := Map.t A.
Definition MapC := Map.t C.
Definition projection (x:C):= fst x.

Parameter (R:relation MapC)
         (I_to_A: I->A)
         (I_to_C: I->C).

Hypothesis Inverses: forall (x:I), (projection (I_to_C x)) = (I_to_A x).

Definition big_projection (s: MapC ):MapA := @Map.map C A projection s.
Definition init_A (s: MapI ):MapA := @Map.map I A I_to_A s.
Definition init_B (s: MapI ):MapC := @Map.map I C I_to_C s.

Lemma Big_Inverses: forall x, big_projection (init_B x) = init_A x.
Proof.
Admitted.