Search code examples
coqcoq-tactic

How can I break `forall i: nat i < S k -> H` in Coq into `i < k and i=k`?

I have to prove:

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

I have a separate hypothesis for i < Datatypes.length l0 and i = Datatypes.length l0.

Solution 
  • Require Import Arith.

SearchAbout lt le.

    gives me (among other things):

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

    Now. You have i < S k which is equivalent to S i <= S k and you want i <= k. So you need to peel-off S on each side.

    SearchAbout le S.

    gives me (among other things):

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

    By combining the two, you should be able to prove your goal:

    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.