Stream: Coq users

Topic: next command?

zohaze (Aug 15 2021 at 17:07):

What next command I should apply ?

``````Lemma max_greater  : forall m h l, In m (h :: l) ->
m <= list_max (h :: l).
Proof.
intros.
apply (Forall_forall (fun k : nat => k <= (list_max (h::l))) l).
apply (list_max_le l (list_max (h::l))). simpl in H.
``````

Olivier Laurent (Aug 19 2021 at 11:28):

First goal will be OK but not the second one.
You should probably use `apply (Forall_forall (fun k : nat => k <= (list_max (h::l))) (h::l)).` in the second line of your proof.

Thank you.

pianke (Jul 02 2022 at 13:42):

``````c k: nat l : list nat
H : k < length (c :: l)
H1 : list_max (c :: l) <= c
Goal: nth k (c :: l) 0 > c -> False
``````

In want to write goal statement in term of list_max (c :: l) ,is it possible?

Pierre Castéran (Jul 02 2022 at 16:17):

With three lemmas of the `List`library: `list_max_le`, `Forall_forall`and `nth_In`, you can infer `nth k (c :: l) 0 <= c` from your hypotheses. Then your proof is completed with `lia`.
May be you should write the proof on paper before writing the formal proof script.

Last updated: Jun 15 2024 at 09:01 UTC