Coqの `forall i：nat 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. 

は、（特に）私を与える：

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. 

：

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

2を組み合わせることで、あなたはあなたの目標を証明することができるはずです