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?

Did you try `Locate list_max`

? You may have more than one function with base name `list_max`

.

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.

It certainly comes from your re-definition of `list_max`

(useless, since it's the same `fold_right`

as 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

Ok,thanks

Last updated: May 18 2024 at 10:02 UTC