The Coq mailing list

["Jevgenijs Sallinens" <jevgenijs AT dva.lv>]

> On Thu, 15 Jan 2004 16:41
> Pierre Courtieu  wrote:
>
>
>
> Lemma Nat_1x :  (n,m: Nat) ((eq_Nat n m) = true)->(eq Nat n m).
>
> If you put NA2.NA.eq_Nat instead of eq_Nat in the type of the lemme, then
> the script works works... Don't understand why this is necessary.

Dear Pierre,

I suspect there is some fundamental difference with the case when inductive
types and fixponts are not used in module types. In the latter case I havn't
found similar problems.

Writing like NA2.NA. is a bit ugly, but what is worth, this could became
unmanageble when there are many related modules.
In the example below, I have added yet another module I_Nat3 without its
implementation.
Now in Nat_Test one result should be taken from I_Nat2 and another from
I_Nat3. I suspect, now it is impossuble to finish the proof of Nat_Test
without introducing new module where both I_Nat2 and I_Nat3 are
imported. (NA3.NA and NA2.NA are conflicting)

Yet another problem, I have discovered after sent original mail, is that
lemma Nat_2 not recognized as having the same type as Axiom Nat_2
in the module type I_Nat2,  if  verification like
Module Nat2[NA:I_Nat]:I_Nat2 with Module NA:=NA.
is imposed.

If these problems are real, I think the usage of inductive definitions
in module types are not reliable for large projects.
Instead in module types there should placed only properties
of such definitions,but definitions themselves should be
within implementation modules.

Sorry if this trouble all is only due to my little experience with modules.

Thanks,
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_2 : (n,m: Nat) ((eq_Nat n m) = true)->(eq Nat n m).
End I_Nat2.

Module Nat2[NA:I_Nat].
(* The following  dosn't work
:I_Nat2 with Module NA:=NA.
*)
Import NA.
Axiom Nat_2 : (n,m: Nat) ((eq_Nat n m) = true)->(eq Nat n m).
(* no proof given for shortnest *)

Module NA:=NA.
End Nat2.

Module Type I_Nat3.
Declare Module NA:I_Nat.
Import NA.
Parameter eq_Nat2:Nat->Nat->bool.
Axiom Nat_3 : (n,m: Nat) ((eq_Nat2 n m) = true)->((eq_Nat n m) = true).
End I_Nat3.


Module NatProps [NA:I_Nat][NA2:I_Nat2 with Module NA:=NA]
[NA3:I_Nat3 with Module NA:=NA].
Import NA.
Import NA2.
Import NA3.

Lemma Nat_Test : (n,m:Nat) ((eq_Nat2 n m) = true)->(eq Nat n m).
Proof.
Intros n m H.
Apply (NA2.Nat_2 n m).
(*Goal  (NA2.NA.eq_Nat n m)=true*)
Apply (Nat_3 n m).
(*
Error: Impossible to unify (NA3.NA.eq_Nat n m)=true with
(NA2.NA.eq_Nat n m)=true
*)
Apply H.
Qed.

End NatProps.



________________________________________________
Message sent using UebiMiau 2.7.2