The Coq mailing list

["Razvan Voicu" <razvan AT comp.nus.edu.sg>]

Dear all,

I don't understand the following behaviour:

|| Coq < Goal forall n m, n<=m -> S n <= S m.
|| 1 subgoal
||
||  ============================
||   forall n m : nat, n <= m -> S n <= S m
||
|| Unnamed_thm < apply (fun (A:(forall n, S n<= S n)) 
||                     (B:(forall n m : nat, n <= m -> S n <= S (S m))) 
||                     (n m:nat) (H:n<=m) => 
||                        match H in (_ <= n0) return (S n <= S n0) with 
||                          | le_n => A n 
||                          | le_S m0 H0 => B n m0 H0 end).
|| Toplevel input, characters 0-199
|| > apply (fun (A:(forall n, S n<= S n)) (B:(forall n m : nat, n <= m -> S
n <= S
|| (S m))) (n m:nat) (H:n<=m) => match H in (_ <= n0) return (S n <= S n0)
with | l
|| e_n => A n | le_S m0 H0 => B n m0 H0 end).
|| >
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
^^
||
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
^^^^
|| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|| Error: Impossible to unify "S ?6080 <= S ?6081" with
||  "forall n m : nat, n <= m -> S n <= S m"
||
|| Unnamed_thm < Definition D := (* same term here *)
||           (fun (A:(forall n, S n<= S n)) 
||                (B:(forall n m : nat, n <= m -> S n <= S (S m))) 
||                (n m:nat) (H:n<=m) => 
||                   match H in (_ <= n0) return (S n <= S n0) with 
||                     | le_n => A n 
||                     | le_S m0 H0 => B n m0 H0 end).
|| D is defined.
||
|| Unnamed_thm < apply D.
|| 2 subgoals
||
||  ============================
||   forall n : nat, S n <= S n
||
|| subgoal 2 is:
||   forall n m : nat, n <= m -> S n <= S (S m)

I don't understand why when I try to apply the term directly, Coq raises an
error,
whereas when the term is named, the application works. Please help.

Thanks in advance,

Razvan