Stream: Coq users

Topic: ✔ Prove if element (nat) is in list l, list_sum l >= element

view this post on Zulip Roland Coeurjoly Lechuga (Jun 08 2022 at 21:45):

I have the following Lemma I want to prove:

Lemma nat_in_list_le_list_sum: forall (l:list nat) (element: nat), In element l = True -> element <= list_sum l.
Proof. intros l element H. induction l.
       + simpl. inversion H. exfalso. rewrite H1. constructor.
       + simpl.

So far I have proved the base case, but I struggle with the second goal.
I have looked for proofs regarding list_sum but found nothing.

view this post on Zulip Gaëtan Gilbert (Jun 08 2022 at 21:50):

don't use In element l = True, you want just In element l instead

view this post on Zulip Gaëtan Gilbert (Jun 08 2022 at 21:52):

full proof for example

Require Import List PeanoNat.

Lemma nat_in_list_le_list_sum: forall (l:list nat) (element: nat), In element l -> element <= list_sum l.
Proof.
  intros l element H. induction l.
  - simpl. inversion H.
  - simpl. destruct H.
    + subst. apply Nat.le_add_r.
    + transitivity (list_sum l);auto.
      rewrite Nat.add_comm. apply Nat.le_add_r.
Qed.

view this post on Zulip Roland Coeurjoly Lechuga (Jun 08 2022 at 21:59):

Thanks! @Gaëtan Gilbert I am going to study this carefully.

view this post on Zulip Notification Bot (Jun 08 2022 at 21:59):

Roland Coeurjoly has marked this topic as resolved.

Last updated: Sep 23 2023 at 08:01 UTC