我怎樣才能將Coq中的``I'< S k -> H`分成`i <k和i = k`？

Question

我必須證明：

i < Datatypes.length (l0 ++ f :: nil) -> H 

我有一個單獨的假說i < Datatypes.length l0和i = Datatypes.length l0。

Answer 1

Require Import Arith. 

SearchAbout lt le. 

給我（除其他事項外）：

le_lt_or_eq: forall n m : nat, n <= m -> n < m \/ n = m 

現在。您有i < S k相當於S i <= S k，並且您需要i <= k。所以你需要在每邊剝離S。

SearchAbout le S. 

給我（除其他事項外）：

le_S_n: forall n m : nat, S n <= S m -> n <= m 

通過結合兩個，你應該能夠證明你的目標：

Goal forall i k, i < S k -> i < k \/ i = k. 
intros i k iltSk. 
apply le_lt_or_eq. 
apply le_S_n. 
assumption. 
Qed.