Я располагаю список натуральных чисел в порядке убывания. С помощью следующих двух функций я нашел элемент максимального значения в списке.
Теперь вместо fold_ tacti c я хочу использовать свою собственную функцию, потому что обе предназначены для одной и той же цели.
Definition replace (n: nat) (l: list nat) : list nat:=
match l with
| nil => l
| h::tl => if n <? h then l else n::tl
end.
Fixpoint largest (elements: nat) (l: list nat) : nat :=
match l with
| nil => 0
| cons h1 nil => h1
| cons h l => match elements with
| O => h
| S elements' => largest elements' (replace h l)
end
end.
Definition maxvalue (l : list nat) : [] <> l -> nat.
intros.
destruct l.
destruct (H (@erefl (list nat) [])).
apply : (fold_left (fun x y => if x <=? y then y else x) l n).
Defined.
Theorem sub_ordering : forall l n0 n1,
n1 <= n0 ->
fold_left (fun x y : nat => if x <=? y then y else x)
l n1 <= fold_left (fun x y : nat => if x <=? y then y else x) l n0.
Definition maxval (l : list nat) : [] <> l -> nat.
intros.
destruct l.
destruct (H (@erefl (list nat) [])).
apply : ( largest (length elements)(replace h l) l n).
Defined.