The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

Hi,
It seems to me that this problem has been solved in the last version of 
Coq (8.O beta) .
The lemma Nat_1x can be deduced without any problem from the Axiom Nat_1.

> The following code showing there are some problems
> with (at least) the usage of modules in Coq 7.4.
> The problem is that in the proof of  Nat_1x it is impossible to use
> Nat_1, previousely established (in another module).
>
> Best Regards,
> Jevgenijs.
>
> Require Bool.
> Module Type I_Nat.
> Inductive Nat : Set := O : Nat
> | S : Nat->Nat.
>
> Fixpoint eq_Nat [n1:Nat; n2:Nat] : bool :=
> Cases n1 n2 of
> O O         => true
> | O (S k)     => false
> | (S m) O     => false
> | (S m) (S k) => (eq_Nat m k)
> end.
> End I_Nat.
>
>
> Module Type I_Nat2.
> Declare Module NA:I_Nat.
> Import NA.
> Axiom Nat_1 :  (n,m: Nat) ((eq_Nat n m) = true)->(eq Nat n m).
> End I_Nat2.
>
> Module Nat2[NA:I_Nat].
> Import NA.
> Lemma Nat_1 :  (n,m: Nat) ((eq_Nat n m) = true)->(eq Nat n m).
> Proof.
> Intros n.
> Induction n.
> Induction m.
> Auto.
> Simpl.
> Intros.
> Assert False.
> Auto with *.
> Contradiction.
> Simpl.
> Intros.
> Induction m.
> Simpl.
> Intros.
> Assert False.
> Auto with *.
> Contradiction.
> Simpl.
> Intros.
> Replace m with n.
> Auto.
> Auto.
> Qed.
> End Nat2.
>
> Module NatProps [NA:I_Nat][NA2:I_Nat2  with Module NA:=NA].
> Import NA.
> Import NA2.
>
> Lemma Nat_1x :  (n,m: Nat) ((eq_Nat n m) = true)->(eq Nat n m).
> Proof.
> Intros n m H.
> Apply (Nat_1 n m).
> Apply H.
> (*
> Error: Impossible to unify (eq_Nat n m)=true with
> (NA2.NA.eq_Nat n m)=true
> *)
> Qed.
>
> End NatProps.
>
>
>
>
> ________________________________________________
> Message sent using UebiMiau 2.7.2
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
>