Library Max_ext
Require Import Max Omega List.
Require Import ssreflect ssrbool.
Export Max.
Lemma max_lemma1: forall x1 x2 x3, x2 <= x1 -> max x2 x3 <= max x1 x3.
Lemma max_max : forall a b c d, a <= c -> b <= d ->
max a b <= max c d.
Lemma lt_max_inv : forall x1 x2 x3, max x2 x3 < x1 -> x2 < x1 /\ x3 < x1.
Lemma lt_max : forall x1 x2 x3, x2 < x1 /\ x3 < x1 -> max x2 x3 < x1.
Lemma le_max : forall x1 x2 x3, x2 <= x1 /\ x3 <= x1 -> max x2 x3 <= x1.
Lemma le_max_l : forall x y, x <= max x y.
Lemma le_max_l_trans : forall x y z, x <= z -> x <= max z y.
Lemma le_max_r_trans : forall x y z, x <= z -> x <= max y z.
Ltac Resolve_le_max :=
match goal with
| |- max ?y ?z <= ?x =>
apply le_max; split; [Resolve_le_max | Resolve_le_max]
| |- ?z <= max ?x ?y =>
apply le_max_l_trans; Resolve_le_max
| |- ?z <= max ?x ?y =>
apply le_max_r_trans; Resolve_le_max
| |- ?z < ?x + (S ?y) =>
cut (z <= x); [omega | Resolve_le_max]
| _ => omega
end.
Lemma le_max_inv : forall a b n, max a b <= n -> a <= n /\ b <= n.
Definition max_list l def := fold_left max l def.
Lemma max_list_max_comm : forall a b c, max_list a (max b c) = max b (max_list a c).
Lemma le_max_list_R : forall l x def, x <= def -> x <= max_list l def.
Lemma In_le_max_list : forall l def x, In x l -> x <= max_list l def.
Lemma le_max_list_def : forall l x, x <= max_list l x.
Lemma max_list_inv : forall a b n, max_list a b <= n -> b <= n.
Lemma max_list_inv2 : forall a b n, max_list a b <= n ->
forall x, In x a -> x <= n.
Lemma lt_max_list : forall l x y z, max_list l y < x -> z < x -> max_list l (max y z) < x.
Lemma lt_max_list_inv : forall l x def, max_list l def < x -> def < x.
Lemma lt_max_list_inv2 : forall l x def, max_list l def < x ->
forall y, In y l -> y < x.
Lemma max_list_app_inv_new : forall a b x def, max_list (a ++ b) def < x ->
max_list a def < x /\ max_list b def < x.
Lemma max_list_app_new : forall a b x def, max_list a def < x /\ max_list b def < x ->
max_list (a ++ b) def < x.
Definition max_lst l := max_list l O.
Lemma max_lst_inv : forall a b x, max_lst (a ++ b) < x -> max_lst a < x /\ max_lst b < x.
Lemma max_lst_app : forall a b x, max_lst a < x /\ max_lst b < x -> max_lst (a ++ b) < x.
Ltac Resolve_lt_max :=
Resolve_lt_max_hypo; Resolve_lt_max_goal
with
Resolve_lt_max_hypo := match goal with
| H: (max ?y ?z < ?x)%nat |- _ =>
generalize (lt_max_inv _ _ _ H); intro X; inversion_clear X; clear H; Resolve_lt_max_hypo
| H: (max_lst (?y ++ ?z) < ?x)%nat |- _ =>
generalize (max_lst_inv _ _ _ H); intro X; inversion_clear X; clear H; Resolve_lt_max_hypo
| H: ( max_lst nil < ?x)%nat |- _ => rewrite /max_lst /= in H; Resolve_lt_max_hypo
| |- _ => idtac
end
with
Resolve_lt_max_goal := match goal with
| |- (max ?y ?z < ?x)%nat =>
apply lt_max; split; [Resolve_lt_max_goal | Resolve_lt_max_goal]
| |- (max_lst (?y ++ ?z) < ?x)%nat =>
apply max_lst_app; split; [Resolve_lt_max_goal | Resolve_lt_max_goal]
| |- (max_lst nil < ?x)%nat => rewrite /max_lst /=; Resolve_lt_max_goal
| |- _ => omega || tauto
end.
Require Import ssreflect ssrbool.
Export Max.
Lemma max_lemma1: forall x1 x2 x3, x2 <= x1 -> max x2 x3 <= max x1 x3.
Lemma max_max : forall a b c d, a <= c -> b <= d ->
max a b <= max c d.
Lemma lt_max_inv : forall x1 x2 x3, max x2 x3 < x1 -> x2 < x1 /\ x3 < x1.
Lemma lt_max : forall x1 x2 x3, x2 < x1 /\ x3 < x1 -> max x2 x3 < x1.
Lemma le_max : forall x1 x2 x3, x2 <= x1 /\ x3 <= x1 -> max x2 x3 <= x1.
Lemma le_max_l : forall x y, x <= max x y.
Lemma le_max_l_trans : forall x y z, x <= z -> x <= max z y.
Lemma le_max_r_trans : forall x y z, x <= z -> x <= max y z.
Ltac Resolve_le_max :=
match goal with
| |- max ?y ?z <= ?x =>
apply le_max; split; [Resolve_le_max | Resolve_le_max]
| |- ?z <= max ?x ?y =>
apply le_max_l_trans; Resolve_le_max
| |- ?z <= max ?x ?y =>
apply le_max_r_trans; Resolve_le_max
| |- ?z < ?x + (S ?y) =>
cut (z <= x); [omega | Resolve_le_max]
| _ => omega
end.
Lemma le_max_inv : forall a b n, max a b <= n -> a <= n /\ b <= n.
Definition max_list l def := fold_left max l def.
Lemma max_list_max_comm : forall a b c, max_list a (max b c) = max b (max_list a c).
Lemma le_max_list_R : forall l x def, x <= def -> x <= max_list l def.
Lemma In_le_max_list : forall l def x, In x l -> x <= max_list l def.
Lemma le_max_list_def : forall l x, x <= max_list l x.
Lemma max_list_inv : forall a b n, max_list a b <= n -> b <= n.
Lemma max_list_inv2 : forall a b n, max_list a b <= n ->
forall x, In x a -> x <= n.
Lemma lt_max_list : forall l x y z, max_list l y < x -> z < x -> max_list l (max y z) < x.
Lemma lt_max_list_inv : forall l x def, max_list l def < x -> def < x.
Lemma lt_max_list_inv2 : forall l x def, max_list l def < x ->
forall y, In y l -> y < x.
Lemma max_list_app_inv_new : forall a b x def, max_list (a ++ b) def < x ->
max_list a def < x /\ max_list b def < x.
Lemma max_list_app_new : forall a b x def, max_list a def < x /\ max_list b def < x ->
max_list (a ++ b) def < x.
Definition max_lst l := max_list l O.
Lemma max_lst_inv : forall a b x, max_lst (a ++ b) < x -> max_lst a < x /\ max_lst b < x.
Lemma max_lst_app : forall a b x, max_lst a < x /\ max_lst b < x -> max_lst (a ++ b) < x.
Ltac Resolve_lt_max :=
Resolve_lt_max_hypo; Resolve_lt_max_goal
with
Resolve_lt_max_hypo := match goal with
| H: (max ?y ?z < ?x)%nat |- _ =>
generalize (lt_max_inv _ _ _ H); intro X; inversion_clear X; clear H; Resolve_lt_max_hypo
| H: (max_lst (?y ++ ?z) < ?x)%nat |- _ =>
generalize (max_lst_inv _ _ _ H); intro X; inversion_clear X; clear H; Resolve_lt_max_hypo
| H: ( max_lst nil < ?x)%nat |- _ => rewrite /max_lst /= in H; Resolve_lt_max_hypo
| |- _ => idtac
end
with
Resolve_lt_max_goal := match goal with
| |- (max ?y ?z < ?x)%nat =>
apply lt_max; split; [Resolve_lt_max_goal | Resolve_lt_max_goal]
| |- (max_lst (?y ++ ?z) < ?x)%nat =>
apply max_lst_app; split; [Resolve_lt_max_goal | Resolve_lt_max_goal]
| |- (max_lst nil < ?x)%nat => rewrite /max_lst /=; Resolve_lt_max_goal
| |- _ => omega || tauto
end.