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.
x \in a :: l
seems to cause issues. I also tried to do it without IH, and hit a dead end everytime, because I end up having to show that z < x0 or a with no information.