Less or equal relation with largest element of natural number list

Link:: https://stackoverflow.com/q/67379273

Display all goals and responses

Question

I want to use definition of list_max_le. After applying Search list_max_le. I get nothing. How I can define list_max_le in Coq?

Answer

Require Import List.
Search "list" "max".list_max: list nat -> nat
list_max_le:
  forall (l : list nat) (n : nat),
  list_max l <= n <-> Forall (fun k : nat => k <= n) l
list_max_app:
  forall l1 l2 : list nat,
  list_max (l1 ++ l2) =
  Nat.max (list_max l1) (list_max l2)
list_max_lt:
  forall [l : list nat] (n : nat),
  l <> nil ->
  list_max l < n <-> Forall (fun k : nat => k < n) l

by using quotes "..." you search for definitions with has the specified string in its name.

If you want to see the definition of list_max_le, you use the Print command

Print list_max_le.list_max_le = 
fun l : list nat =>
list_ind
  (fun l0 : list nat =>
   forall n : nat,
   list_max l0 <= n <->
   Forall (fun k : nat => k <= n) l0)
  (fun n : nat =>
   conj
     (fun _ : 0 <= n =>
      Forall_nil (fun k : nat => k <= n))
     (fun _ : Forall (fun k : nat => k <= n) nil =>
      PeanoNat.Nat.le_0_l n))
  (fun (a : nat) (l0 : list nat)
     (IHl : forall n : nat,
            list_max l0 <= n <->
            Forall (fun k : nat => k <= n) l0)
     (n : nat) =>
   conj
     (fun H : Nat.max a (list_max l0) <= n =>
      let H0 :
        forall n0 m p : nat,
        PeanoNat.Nat.max n0 m <= p ->
        n0 <= p /\ m <= p :=
        fun n0 m p : nat =>
        match PeanoNat.Nat.max_lub_iff n0 m p with
        | conj x _ => x
        end in
      let H1 : a <= n /\ list_max l0 <= n :=
        H0 a (list_max l0) n H in
      Forall_cons a
        match H1 with
        | conj H2 _ => H2
        end
        (let H2 :
           forall n0 : nat,
           list_max l0 <= n0 ->
           Forall (fun k : nat => k <= n0) l0 :=
           fun n0 : nat =>
           match IHl n0 with
           | conj x _ => x
           end in
         H2 n match H1 with
              | conj _ H4 => H4
              end))
     (fun H : Forall (fun k : nat => k <= n) (a :: l0)
      =>
      let H0 :
        a :: l0 = a :: l0 ->
        Nat.max a (list_max l0) <= n :=
        match
          H in (Forall _ l1)
          return
            (l1 = a :: l0 ->
             Nat.max a (list_max l0) <= n)
        with
        | Forall_nil _ =>
            fun H0 : nil = a :: l0 =>
            (fun H1 : nil = a :: l0 =>
             let H2 : False :=
               eq_ind nil
                 (fun e : list nat =>
                  match e with
                  | nil => True
                  | _ :: _ => False
                  end) I (a :: l0) H1 in
             False_ind (Nat.max a (list_max l0) <= n)
               H2) H0
        | @Forall_cons _ _ x l1 Hle HF =>
            fun H0 : x :: l1 = a :: l0 =>
            (fun H1 : x :: l1 = a :: l0 =>
             let H2 : l1 = l0 :=
               f_equal
                 (fun e : list nat =>
                  match e with
                  | nil => l1
                  | _ :: l2 => l2
                  end) H1 in
             (let H3 : x = a :=
                f_equal
                  (fun e : list nat =>
                   match ... with
                   | ... => x
                   | ... => n0
                   end) H1 in
              (fun H4 : x = a =>
               let H5 : x = a := H4 in
               eq_ind_r (... => ...) (... => ...) H5)
                H3) H2) H0 Hle HF
        end in
      H0 eq_refl)) l
     : forall (l : list nat) (n : nat),
       list_max l <= n <->
       Forall (fun k : nat => k <= n) l

Arguments list_max_le _%list_scope _%nat_scope

but in this case the definition is not very readable.

If you Search without "...", you search with a pattern that tries to match part of the type definition.

So if you search

Search list_max.list_max_le:
  forall (l : list nat) (n : nat),
  list_max l <= n <-> Forall (fun k : nat => k <= n) l
list_max_app:
  forall l1 l2 : list nat,
  list_max (l1 ++ l2) =
  Nat.max (list_max l1) (list_max l2)
list_max_lt:
  forall [l : list nat] (n : nat),
  l <> nil ->
  list_max l < n <-> Forall (fun k : nat => k < n) l

You search for all definitions that contains the term list_max.

You can have many strings and terms to refine your search. As an example, if you want some lemma about induction on lists, it is probably called something with "ind" in its name, and has the list term in its type (not necessarily in its name). So you can try

Search "ind" list.find:
  forall [A : Type], (A -> bool) -> list A -> option A
list_sind:
  forall [A : Type] (P : list A -> SProp),
  P nil ->
  (forall (a : A) (l : list A), P l -> P (a :: l)) ->
  forall l : list A, P l
list_ind:
  forall [A : Type] (P : list A -> Prop),
  P nil ->
  (forall (a : A) (l : list A), P l -> P (a :: l)) ->
  forall l : list A, P l
nth_indep:
  forall [A : Type] (l : list A) [n : nat] (d d' : A),
  n < length l -> nth n l d = nth n l d'
rev_ind:
  forall [A : Type] (P : list A -> Prop),
  P nil ->
  (forall (x : A) (l : list A),
   P l -> P (l ++ x :: nil)) -> forall l : list A, P l
rev_list_ind:
  forall [A : Type] (P : list A -> Prop),
  P nil ->
  (forall (a : A) (l : list A),
   P (rev l) -> P (rev (a :: l))) ->
  forall l : list A, P (rev l)
find_none:
  forall [A : Type] (f : A -> bool) (l : list A),
  find f l = None ->
  forall x : A, In x l -> f x = false
find_some:
  forall [A : Type] (f : A -> bool) (l : list A)
    [x : A], find f l = Some x -> In x l /\ f x = true
Forall_ind:
  forall [A : Type] [P : A -> Prop]
    (P0 : list A -> Prop),
  P0 nil ->
  (forall (x : A) (l : list A),
   P x -> Forall P l -> P0 l -> P0 (x :: l)) ->
  forall l : list A, Forall P l -> P0 l
Forall_sind:
  forall [A : Type] [P : A -> Prop]
    (P0 : list A -> SProp),
  P0 nil ->
  (forall (x : A) (l : list A),
   P x -> Forall P l -> P0 l -> P0 (x :: l)) ->
  forall l : list A, Forall P l -> P0 l
NoDup_ind:
  forall [A : Type] (P : list A -> Prop),
  P nil ->
  (forall (x : A) (l : list A),
   ~ In x l -> NoDup l -> P l -> P (x :: l)) ->
  forall l : list A, NoDup l -> P l
NoDup_sind:
  forall [A : Type] (P : list A -> SProp),
  P nil ->
  (forall (x : A) (l : list A),
   ~ In x l -> NoDup l -> P l -> P (x :: l)) ->
  forall l : list A, NoDup l -> P l
Exists_ind:
  forall [A : Type] [P : A -> Prop]
    (P0 : list A -> Prop),
  (forall (x : A) (l : list A), P x -> P0 (x :: l)) ->
  (forall (x : A) (l : list A),
   Exists P l -> P0 l -> P0 (x :: l)) ->
  forall l : list A, Exists P l -> P0 l
Exists_sind:
  forall [A : Type] [P : A -> Prop]
    (P0 : list A -> SProp),
  (forall (x : A) (l : list A), P x -> P0 (x :: l)) ->
  (forall (x : A) (l : list A),
   Exists P l -> P0 l -> P0 (x :: l)) ->
  forall l : list A, Exists P l -> P0 l
ForallOrdPairs_sind:
  forall [A : Type] [R : A -> A -> Prop]
    (P : list A -> SProp),
  P nil ->
  (forall (a : A) (l : list A),
   Forall (R a) l ->
   ForallOrdPairs R l -> P l -> P (a :: l)) ->
  forall l : list A, ForallOrdPairs R l -> P l
ForallOrdPairs_ind:
  forall [A : Type] [R : A -> A -> Prop]
    (P : list A -> Prop),
  P nil ->
  (forall (a : A) (l : list A),
   Forall (R a) l ->
   ForallOrdPairs R l -> P l -> P (a :: l)) ->
  forall l : list A, ForallOrdPairs R l -> P l
Add_ind:
  forall [A : Type] [a : A]
    (P : list A -> list A -> Prop),
  (forall l : list A, P l (a :: l)) ->
  (forall (x : A) (l l' : list A),
   Add a l l' -> P l l' -> P (x :: l) (x :: l')) ->
  forall l l0 : list A, Add a l l0 -> P l l0
Add_sind:
  forall [A : Type] [a : A]
    (P : list A -> list A -> SProp),
  (forall l : list A, P l (a :: l)) ->
  (forall (x : A) (l l' : list A),
   Add a l l' -> P l l' -> P (x :: l) (x :: l')) ->
  forall l l0 : list A, Add a l l0 -> P l l0
Forall2_ind:
  forall [A B : Type] [R : A -> B -> Prop]
    (P : list A -> list B -> Prop),
  P nil nil ->
  (forall (x : A) (y : B) (l : list A) (l' : list B),
   R x y ->
   Forall2 R l l' -> P l l' -> P (x :: l) (y :: l')) ->
  forall (l : list A) (l0 : list B),
  Forall2 R l l0 -> P l l0
Forall2_sind:
  forall [A B : Type] [R : A -> B -> Prop]
    (P : list A -> list B -> SProp),
  P nil nil ->
  (forall (x : A) (y : B) (l : list A) (l' : list B),
   R x y ->
   Forall2 R l l' -> P l l' -> P (x :: l) (y :: l')) ->
  forall (l : list A) (l0 : list B),
  Forall2 R l l0 -> P l l0
Relation_Operators.Ltl_ind:
  forall (A : Set) (leA : A -> A -> Prop)
    (P : list A -> list A -> Prop),
  (forall (a : A) (x : list A), P nil (a :: x)) ->
  (forall a b : A,
   leA a b -> forall x y : list A, P (a :: x) (b :: y)) ->
  (forall (a : A) (x y : list A),
   Relation_Operators.Ltl A leA x y ->
   P x y -> P (a :: x) (a :: y)) ->
  forall l l0 : list A,
  Relation_Operators.Ltl A leA l l0 -> P l l0
Relation_Operators.Ltl_sind:
  forall (A : Set) (leA : A -> A -> Prop)
    (P : list A -> list A -> SProp),
  (forall (a : A) (x : list A), P nil (a :: x)) ->
  (forall a b : A,
   leA a b -> forall x y : list A, P (a :: x) (b :: y)) ->
  (forall (a : A) (x y : list A),
   Relation_Operators.Ltl A leA x y ->
   P x y -> P (a :: x) (a :: y)) ->
  forall l l0 : list A,
  Relation_Operators.Ltl A leA l l0 -> P l l0
Relation_Operators.Desc_sind:
  forall (A : Set) (leA : A -> A -> Prop)
    (P : list A -> SProp),
  P nil ->
  (forall x : A, P (x :: nil)) ->
  (forall (x y : A) (l : list A),
   Relation_Operators.clos_refl A leA x y ->
   Relation_Operators.Desc A leA (l ++ y :: nil) ->
   P (l ++ y :: nil) ->
   P ((l ++ y :: nil) ++ x :: nil)) ->
  forall l : list A,
  Relation_Operators.Desc A leA l -> P l
Relation_Operators.Desc_ind:
  forall (A : Set) (leA : A -> A -> Prop)
    (P : list A -> Prop),
  P nil ->
  (forall x : A, P (x :: nil)) ->
  (forall (x y : A) (l : list A),
   Relation_Operators.clos_refl A leA x y ->
   Relation_Operators.Desc A leA (l ++ y :: nil) ->
   P (l ++ y :: nil) ->
   P ((l ++ y :: nil) ++ x :: nil)) ->
  forall l : list A,
  Relation_Operators.Desc A leA l -> P l