Почему разворачивание не работает на lt (меньше) в Coq?

Question

Я хотел бы доказать lt n m -> le n m, поскольку он не существует в стандартной библиотеке Coq.

Хотя в Coq.Init.Peano, lt m n определяется как S m <= n, я не могу unfold lt в гипотезе использовать такое определение.

Почему разворачивание не работает? Кажется, что только inversion может работать.

Answer 1

Я не знаю, какую версию Coq вы используете, но по моему, unfold работает просто отлично: если я unfold lt in h. в

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

Я получаю следующую цель:

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

Кстати, лемма, которую вы ищете, находится в Nat.lt_le_incl.

Answer 2

Использование Coq 8.5pl3 она разворачивается просто прекрасно:

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. 

Вы, возможно, используя другое определение 'лт'. Вы можете проверить, какой из них вы используете:

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

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