The Coq mailing list

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

On Tue, Jan 13, 2004 at 02:00:16PM +0100, Pierre Casteran wrote:
> By the way, I have often to deal with inductive type definitions.
> Is it OK to put the inductive definition in the signature (since
> it is a declaration of the constructors and the _ind, _rec, ...
> theorems), and duplicate the inductive definition in the signature
> and in the module and/or functor ?.
>

On Tue, 13 Jan 2004 16:51:27 +0100, Jacek Chrzaszcz wrote:
>>Yes, it is OK. Apart from having to write everything twice (and making Coq
>>verify that the declaration and definitions correspond) I can see no
>>problem.

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