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.

sara lee (Aug 26 2021 at 16:39):

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 Listlibrary: list_max_le, Forall_foralland 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: Sep 26 2023 at 13:01 UTC