The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Hello all,

I have a module in which I define a Notation. However, next I cannot use this notation outside the module but inside it is fine. Code is below. The problem occurs in the final Axiom. The error is "The term "i" has type "int32" while it is expected to have type "nat"."

Any hints?

Have a nice Christmas,
Chris


Require Import NArith.

Delimit Scope ord_scope with ord.

Module Type OrderedType.
   Axiom S: Set.
   Axiom lt: S -> S -> Prop.
   Axiom lt_trans: forall i j k: S, lt i j -> lt j k -> lt i k.
End OrderedType.

Module OrderedTypeFacts (M: OrderedType).

   Definition gt (i j: M.S) := M.lt j i.

   Notation "i < j" := (M.lt i j): ord_scope.
   Notation "i > j" := (gt i j): ord_scope.
 
(* Here my axiom is fine, no probs using the notation *)
Axiom int32_lt_to_gt:
   forall i j: M.S,
   (i < j)%ord ->
   (j > i)%ord.

End OrderedTypeFacts.

Definition int32: Set
:= { n: N | (n < 2^32)%N }.

Inductive int32_lt: int32 -> int32 -> Prop
:= mk_int32_lt:
      forall i j: N,
      forall H1: (i < 2^32)%N,
      forall H2: (j < 2^32)%N,
      (i < j)%N ->
      int32_lt (exist _ i H1) (exist _ j H2).

Theorem int32_lt_trans:
   forall i j k: int32,
   int32_lt i j ->
   int32_lt j k ->
   int32_lt i k.
Proof.
intros [i H1] [j H2] [k H3] H4 H5.
inversion H4 as [l m H6 H7 H8 H9 H10].
inversion H5 as [n p H11 H12 H13 H14 H15].
apply mk_int32_lt.
apply Nlt_trans with (m := j); assumption.
Qed.

Module int32_OrderedType <: OrderedType.
   Definition S := int32.
   Definition lt := int32_lt.
   Definition lt_trans := int32_lt_trans.
End int32_OrderedType.

Module int32 := OrderedTypeFacts int32_OrderedType.

(* Here I get an error *)

Axiom int32_lt_to_gt:
   forall i j: int32,
   (i < j)%ord ->
   (j > i)%ord.