The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Hello. I come back to this post. It works well for [add] and various 
other functions like [find]. But it does not seem possible to do it for 
[fold] because the provided induction principles are based on [Equal] 
and hence Leibniz equality. And it does not seem possible to prove 
stronger induction principles because various FMapSignature parameters 
explicitly use Leibniz equality which makes the whole FMap development 
incompatible with setoid equalities (see for instance the types of 
fold_1, find_[12], or elements_[12] which uses eq_key_elt based on 
Leibniz equality)... :-( Frederic.

Le 28/01/2011 02:24, AUGER Cedric a écrit :
> Le Thu, 27 Jan 2011 22:48:01 +0800,
> Frederic 
> Blanqui<frederic.blanqui AT inria.fr>
>   a écrit :
>
> > Hello Cedric.
> >
> > I guess that for having M=M', you assume that the equality on A is
> > also = (Leibniz equality). But what if the equality on A is an
> > arbitrary equivalence relation?...
> Of course I assume that (else Coq would probably be inconsistant).
>
> Else you can try to complete the following code for your purpouse; it
> is a functor which will add some lemmas you want.
>
> I may have bad tastes for notations (particulary in using UTF8 even if
> people are used to ascii); for people who would like to have easy ways
> to input them and are using an X window system, I advise them to take a
> look at XCompose; for the others they can try some input method (such
> as uim; or some provided by emacs if they use proof general)
> Require Import FMapInterface.
> Require Import Utf8_core.
> Set Implicit Arguments.
>
> Notation "⊤" := (True).
> Notation "⊥" := (False).
>
> (* Abstraction *)
> Notation "'λ'  x .. y · t" := (fun x =>  .. (fun y =>  t) ..)
>    (at level 200, x binder, y binder, right associativity).
>
> Delimit Scope init_scope with init.
> Open Scope init_scope.
> Notation "'ℕ'" := nat: init_scope.
> Notation "'𝟘'" := Empty_set: init_scope.
> Notation "'𝟙'" := unit: init_scope.
> Notation "'𝟚'" := bool: init_scope.
> Notation "'𝕠'" := tt: init_scope.
> Notation "'𝕥'" := true: init_scope.
> Notation "'𝕗'" := false: init_scope.
> Notation "x ₁" := (let (y, _) := x in y) (at level 5).
> Notation "x ₂" := (let (_, y) := x in y) (at level 5).
>
> Module MapEquiv (M: S).
>   Definition elt_equiv A (elt_eq: A → A → 𝟚): relation A :=
>              λ x y·elt_eq x y = 𝕥.
>   Lemma t_morphism:
>   ∀ A elt_eq, equivalence A (elt_equiv elt_eq) →
>               equivalence (M.t A) (M.Equivb elt_eq).
>    Proof.
>    intros A elt_eq [Refl Trans Sym]; split.
>      intro m; split.
>       now split; auto.
>      intros k e e' H H'.
>      generalize (M.find_1 H').
>      rewrite (M.find_1 H).
>      intro Heq; inversion_clear Heq.
>      exact (Refl e').
>     intros m1 m2 m3 [H12 K12] [H23 K23]; split; intro.
>      generalize (H23 k); generalize (H12 k); clear.
>      now intros [] []; split; auto.
>     intros e e' H H'.
>     destruct ((H12 k)₁ (ex_intro (λ _ · _) e H)) as [e_ He_].
>     generalize (Trans e e_ e').
>     generalize (K23 _ _ _ He_ H').
>     generalize (K12 _ _ _ H He_).
>     clear; unfold Cmp, elt_equiv.
>     now auto.
>    intros m1 m2 [K H]; split.
>     intro k; split; intro L.
>      exact ((K k)₂ L).
>     exact ((K k)₁ L).
>    intros k e e' H1 H2.
>    generalize (Sym e' e).
>    generalize (H _ _ _ H2 H1).
>    clear; unfold Cmp, elt_equiv.
>    now auto.
>   Qed.
>
>   Instance add_m : ∀ A elt_eq,
>   Proper (M.E.eq ==>
>           elt_equiv elt_eq ==>
>           M.Equiv (elt_equiv elt_eq) ==>
>           M.Equiv (elt_equiv elt_eq))
>   (@M.add A).
>    Proof.
>    intros A elt_eq k1 k2 Hk e1 e2 He m1 m2 Hm.
>    split.
>     intro k.
>     generalize (Hm ₁ k); clear -Hm Hk.
>     intros [Hm1 Hm2]; split; intros [a_ Ha_].
>      destruct (M.E.eq_dec k2 k).
>       split with e2.
>       now apply M.add_1.
>      destruct Hm1.
>       split with a_.
>       apply M.add_3 with k1 e1; auto.
>       intro H; destruct n.
>       now apply M.E.eq_trans with k1; auto.
>      split with x.
>      now apply M.add_2; auto.
>     destruct (M.E.eq_dec k1 k).
>      split with e1.
>      now apply M.add_1.
>     destruct Hm2.
>      split with a_.
>      apply M.add_3 with k2 e2; auto.
>      intro H; destruct n.
>      now apply M.E.eq_trans with k2; auto.
>     split with x.
>     now apply M.add_2; auto.
>    intro k.
>    destruct (M.E.eq_dec k2 k).
>     intros e_ e_' H H'.
>     revert He.
>     generalize (M.find_1 H').
>     rewrite (M.find_1 (M.add_1 _ _ e)).
>     generalize (M.find_1 H).
>     rewrite (M.find_1 (M.add_1 _ _ (M.E.eq_trans Hk e))).
>     clear.
>     intro H; inversion_clear H.
>     intro H; inversion_clear H.
>     now auto.
>    intros e_ e_' H H'.
>    generalize (M.add_3 n H').
>    cut (¬M.E.eq k1 k).
>     intro n'; generalize (M.add_3 n' H).
>     exact (Hm ₂ k e_ e_').
>    clear -n Hk.
>    intro H; destruct n.
>    now apply M.E.eq_trans with k1; auto.
>   Qed.
>   End MapEquiv.