The Coq mailing list

["Lucian M. Patcas" <lucian.patcas AT gmail.com>]

Hello,

How can I prove this theorem without using "auto with arith"?

Lemma silly : forall t : nat, t >=2 -> t <= 2 -> t = 2.

When proved using "auto with arith", the proof term is 

silly = 
fun (t : nat) (H1 : t >= 2) (H2 : t <= 2) => le_antisym t 2 H2 H1
     : forall t : nat, t >= 2 -> t <= 2 -> t = 2

I didn't even know le_antisym existed, not to mention how ugly this term looks:

le_antisym = 
fun (n m : nat) (H : n <= m) =>
match H in (_ <= n0) return (n0 <= n -> n = n0) with
| le_n => fun _ : n <= n => eq_refl n
| le_S m' H0 =>
    fun H1 : S m' <= n =>

    False_ind (n = S m')
      (let H2 := le_trans (S m') n m' H1 H0 in
       (let H3 := le_Sn_n m' in fun H4 : S m' <= m' => H3 H4) H2)
end
     : forall n m : nat, n <= m -> m <= n -> n = m

... one surely needs to master the dark side of the force to come up with such a proof term... Is there a standard trick to deal with such proofs, but without using "auto with arith"?

Thanks,
Lucian