The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Maybe I am confused, but it seems to me that the induction principle
you wish for is not stronger, but weaker than the available induction
principle. If you look for instance at [fold_rec_bis]:

Theorem fold_rec_bis :
    forall (A:Type)(P : t elt -> A -> Type)(f : key -> elt -> A -> A),
     forall (i:A)(m:t elt),
     (forall m m' a, Equal m m' -> P m a -> P m' a) ->  (* HP *)
     (P (empty _) i) ->
     (forall k e a m', MapsTo k e m -> ~In k m' ->         (* Hstep *)
       P m' a -> P (add k e m') (f k e a)) ->
     P m (fold f m i).

and if P is such that it is compatible with [Equiv elt_eq] where
[elt_eq] is your custom equivalence relation on elements, and [f] is
compatible with [elt_eq] as well, then both are a fortiori compatible
with [Equal] and Leibniz. Therefore introducing [elt_eq] in hypotheses
HP and Hstep would strenghten the hypotheses, and weaken the induction
principle altogether.

Another way to look at this is, you say that the signature of Maps is
not general enough, but [elements_1] and [elements_2], for instance,
are the strongest results that one can have on the results of
[elements]. I can prove strictly more things knowing that if I put 1/2
in a map, I get 1/2 when I look it up, than only knowing that I might
get any amongst 2/4, 6/12, 21/42 etc. Maybe I am missing something ?

Stéphane

On Fri, Mar 4, 2011 at 5:15 AM, Frederic Blanqui
<frederic.blanqui AT inria.fr>
 wrote:
> 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.
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06