Set Implicit Arguments.
Require Import List Arith Lia Morphisms Wf.
Import ListNotations.
Definition funcomp {X Y Z} (g : Y -> Z) (f : X -> Y) :=
fun x => g (f x).
Notation "f >> g" := (funcomp g f) (at level 50).
Fixpoint it (n: nat) {X: Type} (f: X -> X) (s: X) :=
match n with
| 0 => s
| S n => f (it n f s)
end.
Lemma it_plus n m X f (s: X):
it (n + m) f s = it n f (it m f s).
Proof.
induction n; cbn; congruence.
Qed.
Lemma it_commute n X f (s: X):
f (it n f s) = it n f (f s).
Proof.
induction n; cbn; congruence.
Qed.
(* step up the <= game *)
Instance max_proper: Proper (le ++> le ++> le) max.
Proof.
intros a b ? c d ?; transitivity (max a d);
eauto using Nat.max_le_compat_l, Nat.max_le_compat_r.
Qed.
Instance plus_proper: Proper (le ++> le ++> le) plus.
Proof.
intros a b ? c d ?; transitivity (a + d);
eauto using plus_le_compat_l, plus_le_compat_r.
Qed.
Instance lt_le_subrel: subrelation lt le.
Proof.
intros ?? H; unfold lt in *; transitivity (S x); eauto.
Qed.
Fixpoint Sum (N: list nat) :=
match N with
| nil => 0
| n :: N => n + Sum N
end.
Lemma Sum_in x N:
In x N -> x <= Sum N.
Proof.
induction N; cbn; intuition; lia.
Qed.
Lemma Sum_app N1 N2:
Sum (N1 ++ N2) = Sum N1 + Sum N2.
Proof.
induction N1; cbn; lia.
Qed.
Hint Rewrite Sum_app : listdb.
Definition cast {X: Type} {P: X -> Type} {x y: X} (A: P x) (H: x = y): P y :=
@eq_rect X x P A y H.
Require Import List Arith Lia Morphisms Wf.
Import ListNotations.
Definition funcomp {X Y Z} (g : Y -> Z) (f : X -> Y) :=
fun x => g (f x).
Notation "f >> g" := (funcomp g f) (at level 50).
Fixpoint it (n: nat) {X: Type} (f: X -> X) (s: X) :=
match n with
| 0 => s
| S n => f (it n f s)
end.
Lemma it_plus n m X f (s: X):
it (n + m) f s = it n f (it m f s).
Proof.
induction n; cbn; congruence.
Qed.
Lemma it_commute n X f (s: X):
f (it n f s) = it n f (f s).
Proof.
induction n; cbn; congruence.
Qed.
(* step up the <= game *)
Instance max_proper: Proper (le ++> le ++> le) max.
Proof.
intros a b ? c d ?; transitivity (max a d);
eauto using Nat.max_le_compat_l, Nat.max_le_compat_r.
Qed.
Instance plus_proper: Proper (le ++> le ++> le) plus.
Proof.
intros a b ? c d ?; transitivity (a + d);
eauto using plus_le_compat_l, plus_le_compat_r.
Qed.
Instance lt_le_subrel: subrelation lt le.
Proof.
intros ?? H; unfold lt in *; transitivity (S x); eauto.
Qed.
Fixpoint Sum (N: list nat) :=
match N with
| nil => 0
| n :: N => n + Sum N
end.
Lemma Sum_in x N:
In x N -> x <= Sum N.
Proof.
induction N; cbn; intuition; lia.
Qed.
Lemma Sum_app N1 N2:
Sum (N1 ++ N2) = Sum N1 + Sum N2.
Proof.
induction N1; cbn; lia.
Qed.
Hint Rewrite Sum_app : listdb.
Definition cast {X: Type} {P: X -> Type} {x y: X} (A: P x) (H: x = y): P y :=
@eq_rect X x P A y H.