Why unfold does not work on lt(less-than) in Coq?

1
votes

I'd like to prove lt n m -> le n m since it does not exist in Coq's standard library.

Though in Coq.Init.Peano, lt m n is defined as S m <= n, I cannot unfold lt in the hypothesis to use such definition.

Why unfold does not work? It seems that only inversion could work.

2
coq

2 Answers

1
votes

I don't know what version of Coq you are using, but on mine, unfold works just fine: if I do unfold lt in h. in 

1 subgoal
n : nat
m : nat
h : n < m
______________________________________(1/1)
n <= m

I get the following goal:

1 subgoal
n : nat
m : nat
h : S n <= m
______________________________________(1/1)
n <= m

By the way, the lemma you are looking for is in Nat.lt_le_incl.

0
votes

Using Coq 8.5pl3 it unfolds just fine:

Require Import Coq.Init.Peano.

Goal forall m n, lt n m -> le n m.
Proof.
  intros m n H.
  unfold lt in H.
  apply le_S_n, le_S, H.
Qed.

You maybe using different 'lt' definition. You can check which one you are using as follows:

Coq < About lt.
lt : nat -> nat -> Prop

Argument scopes are [nat_scope nat_scope]
lt is transparent
Expands to: Constant Coq.Init.Peano.lt