Library Coq.ZArith.Zminmax


Require Import Zmin Zmax.

Require Import BinInt Zorder.




Open Local Scope Z_scope.

Lattice properties of min and max on Z

Absorption





Lemma Zmin_max_absorption_r_r : forall n m, Zmax n (Zmin n m) = n.

Proof.

  intros; apply Zmin_case_strong; intro; apply Zmax_case_strong; intro; 

    reflexivity || apply Zle_antisym; trivial.

Qed.




Lemma Zmax_min_absorption_r_r : forall n m, Zmin n (Zmax n m) = n.

Proof.

  intros; apply Zmax_case_strong; intro; apply Zmin_case_strong; intro; 

    reflexivity || apply Zle_antisym; trivial.

Qed.

Distributivity





Lemma Zmax_min_distr_r : 

  forall n m p, Zmax n (Zmin m p) = Zmin (Zmax n m) (Zmax n p).

Proof.

  intros.

  repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; 

    reflexivity ||

      apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).

Qed.




Lemma Zmin_max_distr_r : 

  forall n m p, Zmin n (Zmax m p) = Zmax (Zmin n m) (Zmin n p).

Proof.

  intros.

  repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros; 

    reflexivity ||

      apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).

Qed.

Modularity





Lemma Zmax_min_modular_r :

  forall n m p, Zmax n (Zmin m (Zmax n p)) = Zmin (Zmax n m) (Zmax n p).

Proof.

  intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;

    reflexivity ||

      apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).

Qed.




Lemma Zmin_max_modular_r :

  forall n m p, Zmin n (Zmax m (Zmin n p)) = Zmax (Zmin n m) (Zmin n p).

Proof.

  intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;

    reflexivity ||

      apply Zle_antisym; (assumption || eapply Zle_trans; eassumption).

Qed.

Disassociativity





Lemma max_min_disassoc : forall n m p, Zmin n (Zmax m p) <= Zmax (Zmin n m) p.

Proof.

  intros; repeat apply Zmax_case_strong; repeat apply Zmin_case_strong; intros;

    apply Zle_refl || (assumption || eapply Zle_trans; eassumption).

Qed.