我怎样才能将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.