The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Hi Stéphane

You're right, I did not spot the problem at the right place! It's with
functors that my problem shows up.
Here is an example:

<<<
Require Import Peano_dec.
Class EqDec (A:Type) := {
 eq_dec: forall (x y:A), {x = y} + {x <> y}
}.

Notation "x == y" := (eq_dec x y) (at level 70, no associativity).

Instance EqDec_nat : EqDec nat :={
  eq_dec := eq_nat_dec
}.


Module Type DECIDABLE.
  Parameter t: Type.
  Instance EqDec_t : EqDec t.
End DECIDABLE.

Module DecNat <: DECIDABLE.
  (* notice that in my development, this module is less trivial *)
  Definition t := nat.
  Definition EqDec_t := EqDec_nat.
End DecNat.


Module Foo (X:DECIDABLE).
  Lemma foo : forall (x y:X.t),
    if (x == y) then x = y else x <> y.
  Proof.
    intros. destruct (x == y); auto.
  Qed.
End Foo.

Module FooNat := Foo(DecNat).

Lemma bar : forall (x y: nat), True.
Proof.
  intros x y.
  pose proof (FooNat.foo x y).
  destruct (x == y). (* wrong destruction !! *)
>>>

I have to unfold DecNat.t in H. and unfold DecNat.EqDec_t in H. for
the destruction to work.

If I add

<<<
 Set Printing All. pose (x == y).
>>>
here is what I get:
<<<
H : match @eq_dec DecNat.t DecNat.EqDec_t x y return Prop with
      | left _ => @eq DecNat.t x y
      | right _ => not (@eq DecNat.t x y)
      end
  s := @eq_dec nat EqDec_nat x y : sumbool (@eq nat x y) (not (@eq nat x y))
>>>

Thanks for your help

Alexandre