Stream: Coq users

Topic: max value


view this post on Zulip pianke (Jul 08 2022 at 07:51):

I am applying command

pose proof list_max_le l (list_max l) as H. Then H become
H : List.list_max l <=     list_max l ->    Forall (fun k : nat =>   k <= list_max l) l   instead of

  list_max l <= list_max l <->  Forall  (fun k : nat => k <= list_max l) l .

How i can remove List . from above H?

view this post on Zulip Pierre Castéran (Jul 08 2022 at 09:42):

Did you try Locate list_max ? You may have more than one function with base name list_max.

view this post on Zulip pianke (Jul 08 2022 at 11:40):

Against :Locate list_max .
I get this message "Constant filename_v.list_max Constant Coq.Lists.List.list_max shorter name to refer to it in current context is List.list_max))
I am using these two definitions only
Definition list_max l := fold_right max 0 l.
Lemma list_maxs b l : In b l -> b <= list_max l.

view this post on Zulip Pierre Castéran (Jul 08 2022 at 12:05):

It certainly comes from your re-definition of list_max (useless, since it's the same fold_rightas in the List library).
In your context, you have two different constants : List.list_max(from standard library) and your function list_max. They are clearly (extensionally) equivalent, but not identical. And lemmas in Coq.Lists.List talk about Coq's list_max, not yours. You may remove your definition of list_max, otherwise, you'd have to adapt standard library's lemmas to your definition :scream:

https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.Locate

view this post on Zulip pianke (Jul 13 2022 at 18:17):

Ok,thanks


Last updated: Sep 26 2023 at 13:01 UTC