I create sublist from list in this way:
Fixpoint sublist {X : Type} (n : nat) (m : nat) (lst : list X) : list X :=
match lst with
| [] => []
| h :: t => match m with
| O => match n with
| O => []
| S n' => h :: sublist n' O t
end
| S m' => sublist n m' t
end
end.
I want to prove that if m
is greater or equal to the length of lst
, then sublist n m lst
will return empty list:
Theorem sublist_list_after_m : forall X : Type, forall n m : nat, forall lst :list X ,
m <? (length lst) = false -> length (sublist n m lst) =? 0 = true.
Proof.
intros.
destruct lst as [|h t].
- simpl. reflexivity.
- simpl. destruct n as [|n'].
+ simpl. reflexivity.
+ destruct m as [|m'].
-- Admitted.
But I not sure what I'm doing wrong.
induction m as [ | m IHm].
$\endgroup$