Search code examples
coqssreflect

Coq - prove that there exists a maximal element in a non empty sequence

As an exercise I want to prove that there is always exists a maximum element in a non-empty sequence.

Theorem largest_el_in_list (s: seq rat) x : x \in s -> exists y, y \in s /\ forall z, z \in s -> y >= z.

My idea was to go by induction on s, and then to destruct x. The largest element in this first case is the only element in the list. However, in the second case I'm getting quite confused. Am I supposed to use the inductive hypothesis? My idea was that we can get rid of the existential by exists max a a1, where a is the maximal element we found in the previous step, and a1 is the new element being added to the sequence. But if I do this, then I can't use the inductive hypothesis and I get completely stuck.

I've been stuck for hours and would love to know if I have the right idea.

Edit: Here is the proof so far, with the current proof state below:

Theorem largest_el_in_list (s: seq rat) x : x \in s -> exists y, y \in s /\ forall z, z \in s -> y >= z.
Proof.
  elim/last_ind : s => //= s x0 IH x_in_rcons.
  case : s IH x_in_rcons.
  move => _ x_in_sx0.
  exists x0. split.
  rewrite in_cons. apply/orP. left. by apply/eqP.
  rewrite in_cons in x_in_sx0. case/orP : x_in_sx0 => //= xeqx0 z z_in_sx0.
  rewrite in_cons in z_in_sx0. case/orP : z_in_sx0 => //= zeqx0. case/eqP : zeqx0 => zeqx0.
  by rewrite zeqx0.
  move => a l IH x_in_rcons. 
  exists (maxr x0 a). split.
  have [agex0 | x0gta] := (lerP x0 a).
  by rewrite mem_head.
  rewrite rcons_cons in_cons. apply/orP. right. by rewrite in_rcons.
  move => z z_in_rcons.
Admitted.

Proof state:

x: rat_eqType
x0, a: rat
l: seq rat
IH: x \in a :: l ->
     exists y : rat, y \in a :: l /\ (forall z : rat, z \in a :: l -> z <= y)
x_in_rcons: x \in rcons (a :: l) x0
z: rat
z_in_rcons: z \in rcons (a :: l) x0
-------------------------------
(1/1)
z <= maxr x0 a

ANOTHER EDIT:

Imports:

From finprob Require Import prob.
From mathcomp Require Import all_ssreflect all_algebra seq.
From extructures Require Import ord fset fmap ffun.
Import Num.Theory.
Import GRing. 
Import Bool. 
Import Num.Def.

You can find extructures here https://github.com/arthuraa/extructures And finprob here https://github.com/arthuraa/finprob

UPDATE:

Although changing the definition clears the path, there is still an issue. Here is the updated proof and proof state:

Theorem largest_el_in_list (s: seq rat) : s != [::] -> exists y, y \in s /\ forall z, z \in s -> y >= z.
Proof.
  elim/last_ind : s => //= s x0 IH x_in_rcons.
  case : s IH x_in_rcons.
  move => _ x_in_sx0.
  exists x0. split.
  rewrite in_cons. apply/orP. left. by apply/eqP.

  move => z z_in_cons.
  rewrite in_cons in z_in_cons.
  case/orP : z_in_cons => //= zeqx0.
  case/eqP : zeqx0 => zeqx0. by rewrite zeqx0.
  
  move => a l IH cons_nempty.
  case IH => //= x [x_in_cons IH'].
  exists x.
  split.
  rewrite in_cons in x_in_cons.
  rewrite in_cons. 
  case/orP : x_in_cons => [xeqa | x_in_l].
  by rewrite xeqa orTb. apply/orP. right. rewrite in_rcons. apply/orP. by right.
  move => z z_in_cons.
  apply IH'.
  rewrite in_cons. rewrite in_cons in z_in_cons.
  case/orP : z_in_cons => [zeqa | z_in_cons].
  by rewrite zeqa orTb.
Admitted.

x0, a: rat
l: seq rat
IH: a :: l != [::] ->
     exists y : rat, y \in a :: l /\ (forall z : rat, z \in a :: l -> z <= y)
cons_nempty: rcons (a :: l) x0 != [::]
x: rat
x_in_cons: x \in a :: l
IH': forall z : rat, z \in a :: l -> z <= x
z: rat
z_in_cons: z \in rcons l x0
-------------------------
(1/1)
(z == a) || (z \in l)

I don't see how this can be true, because we know from z_in_cons that z is either equal to x0, or it is in l. Thus, if we go by cases, the first case is impossible because we are lacking some information about x0.

Solution

  • Another approach would be to explicitly provide, right from the start, a value for y, the existence of which you are looking for. This should be the maximum of the list, which you could either specify yourself, via a Fixpoint definition, or be the maximum as defined in Coq.

    But if you want to keep the proof by induction, as you suggest in your comment, here is one way (I suppose one can write it in a more concise manner). I'm using here nat instead of rat, for convenience:

    Theorem largest_el_in_list (s: seq nat) : 
  s != [::] -> exists y, y \in s /\ forall z, z \in s -> y >= z.
Proof.
elim: s => [//=|n s IH _].
have [/eqP ->|/IH [max [maxins ismax]]] := boolP (s == nil).
- exists n.
  split=> [|y]; first by rewrite in_cons eq_refl orTb.
  by rewrite in_cons ?in_nil => /orP [/eqP ->|].
- have [lenx|] := boolP (n <= max).
  - exists max. 
    split=> [|z]; first by rewrite in_cons maxins orbT.
    by rewrite in_cons => /orP [/eqP ->|/ismax]. 
  - rewrite -ltnNge.
    exists n.
    split=> [|z]; first by rewrite in_cons eq_refl orTb.
    rewrite in_cons => /orP [/eqP -> //|/ismax ltzx].
    by rewrite (@leq_trans max) // ltnW.
Qed.