The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT polytechnique.org>]

OK I see your problem.
There is no "direct" solution in the sense that definitions which are
made in the functor use the instance brought in the module parameter,
and on functor application these are not inlined.

There is an indirect, practical, solution nonetheless. Your issue
arises when you try to reason on ==, an instance member, and this
reasoning does not depend on the functor and should not be done in the
functor. Lemma "foo" for instance should be an instance-parameterized
definition:
<<<
Lemma myfoo `{EqDec A} (x y : A) : if x == y then x = y else x <> y.
Proof.
  intros; destruct (x == y); assumption.
Qed.
>>>
You can then do what you wanted to:
<<<
Lemma bar : forall (x y: nat), True.
Proof.
  intros x y.
  pose proof (myfoo x y).
  destruct (x == y). (* works *)
>>>>
It works because the instances for myfoo and for (x == y) are resolved
in the same context and therefore will be the same. The rule of thumb
is: consequences of a class should be defined as functions/lemmas
parameterized by instances.

In practice, I imagine that Foo also contains lemmas which are not
only related to EqDec, in that case reasoning on these functions
should be done in the functor Foo itself, where only one instance of
EqDec is available. The only case where you can't avoid the issue
should be quite rare: it is if you need to prove something on a
function f defined in the functor Foo, but only on a particular
instantiation, e.g. FooNat.f. In that case, try using DecNat.t instead
of nat when introducing x and y, so that (x == y) uses the correct
instance.

Hope this helps,
Stéphane

PS : This is unrelated to your issue, but for the formalization of
your EqDec class, it's usually simpler to use a boolean test with an
inductive specification:
<<<
Inductive equal_spec {A} (x y : A) : bool -> Prop :=
| equal_true : x = y -> equal_spec x y true
| equal_false : x <> y -> equal_spec x y false.
Class EqDec (A:Type) := {
  equal : A -> A -> bool;
  eq_dec : forall x y, equal_spec x y (equal x y)
}.
Notation "x == y" := (equal x y) (at level 70, no associativity).
>>>
You have a pure equality test and you can perform case analysis for x
== y by calling "destruct (eq_dec x y)".

2010/10/1 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
>
>



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