2
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ What is this for? Homework for a class? Something else? You'll need to use induction here. Try starting your proof with induction m as [ | m IHm]. $\endgroup$
    – djao
    Commented Apr 12, 2023 at 13:14

1 Answer 1

1
$\begingroup$

as @djao said, you need to use induction.

Below you will find one possible proof for your Theorem (without ssreflect). The strategy is essentially induction on lst (note the generalized H and m to strengthen de induction hypothesis).

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 X n m lst H; revert H; generalize m.
  induction lst; [ simpl; reflexivity | ].

  intros; simpl.
  destruct m0; [ discriminate | ].
  specialize (IHlst m0).

  apply IHlst, Nat.ltb_ge; apply Nat.ltb_ge in H.
  simpl in H; apply le_S_n in H.

  exact H.
Qed.
```
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.