爲什麼在Coq中lt（小於）展開不起作用？

Question

我想證明lt n m -> le n m，因爲它不存在於Coq的標準庫中。

雖然在Coq.Init.Peano，lt m n被定義爲S m <= n，但我不能在unfold lt這個假設中使用這樣的定義。

爲什麼展開不起作用？似乎只有inversion可以工作。

Answer 1

我不知道你用的是什麼版本的勒柯克的，但在礦山，unfold作品就好了：如果我在

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

做unfold lt in h.我得到以下目標：

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

順便說一句，你正在尋找的引理是在Nat.lt_le_incl。

Answer 2

使用勒柯克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. 

您可能使用不同的 'LT' 的定義。您可以檢查使用哪一個，如下所示：

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

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