Set Implicit Arguments.

Require Import LogicUtil.
Require Export ZArith.

Open Local Scope Z_scope.

Lemma zeql : ∀ x, match x with Z0 ⇒ 0 | Zpos y' ⇒ Zpos y'
  | Zneg y' ⇒ Zneg y' end = x.

Proof.
intro. destruct x; refl.
Qed.

Lemma zeqr : ∀ x, x = match x with Z0 ⇒ 0 | Zpos y' ⇒ Zpos y'
  | Zneg y' ⇒ Zneg y' end.

Proof.
intro. destruct x; refl.
Qed.

Lemma pos_lt : ∀ x y : Z, 0 ≤ y-x-1 → x < y.

Proof.
intros. omega.
Qed.

Lemma pos_le : ∀ x y : Z, 0 ≤ y-x → x ≤ y.

Proof.
intros. omega.
Qed.

Fixpoint power (x : Z) (n : nat) {struct n} : Z :=
  match n with
    | O ⇒ 1
    | S n' ⇒ x × power x n'
  end.

Infix "^" := power.

Lemma power_plus : ∀ x n1 n2, power x (n1+n2) = power x n1 × power x n2.

Proof.
induction n1; intros; simpl. apply zeqr. rewrite IHn1. ring.
Qed.

Lemma power_one : ∀ n, power 1 n = 1.

Proof.
induction n; simpl. refl. rewrite IHn. refl.
Qed.

Lemma power_succ : ∀ x n, power x (S n) = x × power x n.

Proof.
refl.
Qed.

Lemma power_mult : ∀ x n1 n2, power x (n1×n2) = power (power x n1) n2.

Proof.
induction n1; induction n2; intros. refl. rewrite power_one. refl.
rewrite mult_0_r. refl. rewrite power_succ. rewrite <- IHn2.
rewrite <- mult_n_Sm. simpl. repeat rewrite power_plus. simpl. ring.
Qed.

Lemma pos_power : ∀ x n, 0 ≤ x → 0 ≤ power x n.

Proof.
induction n; intros; simpl. omega. apply Zmult_le_0_compat. assumption.
apply IHn. assumption.
Qed.

Lemma spos_power : ∀ x n, 0 < x → 0 < power x n.

Proof.
induction n; intros; simpl. omega. apply Zmult_lt_O_compat. assumption.
apply IHn. assumption.
Qed.

Lemma power_le_compat : ∀ x y n, 0≤x → x≤y → power x n ≤ power y n.

Proof.
induction n; intros; simpl. omega. apply Zmult_le_compat. assumption.
apply IHn; assumption. assumption. apply pos_power. assumption.
Qed.

Definition is_pos z :=
  match z with
    | Zpos _ ⇒ true
    | _ ⇒ false
  end.

Notation pos := (fun z ⇒ 0 ≤ z).
Notation D := (sig pos).
Notation val := (@proj1_sig Z pos).
Notation inj := (@exist Z pos _).

Lemma Zero_in_D : pos 0.

Proof.
simpl. omega.
Qed.

Notation D0 := (inj Zero_in_D).

Lemma pos_power_val : ∀ x n, pos (power (val x) n).

Proof.
intros. destruct x. apply pos_power. assumption.
Qed.

Definition Dlt x y := Zlt (val x) (val y).
Definition Dle x y := Zle (val x) (val y).

Require Import RelUtil.

Definition Dgt := transp Dlt.
Definition Dge := transp Dle.

Require Import Zwf.
Require Import Wellfounded.

Lemma Dlt_well_founded : well_founded Dlt.

Proof.
unfold Dlt. apply wf_incl with (R2 := (fun x y : D ⇒ Zwf 0 (val x) (val y))).
unfold inclusion, Zwf. intros (x,Hx) (y,Hy). simpl. intuition omega.
apply (wf_inverse_image D Z (Zwf 0) val). apply Zwf_well_founded.
Qed.

Require Import SN.

Lemma WF_Dgt : WF Dgt.

Proof.
apply wf_transp_WF. apply Dlt_well_founded.
Qed.

Lemma power_Dlt_compat : ∀ x y n,
  Dlt x y → Dlt (inj (pos_power_val x (S n))) (inj (pos_power_val y (S n))).

Proof.
intros x y. destruct x. destruct y. unfold Dlt. simpl.
induction n; simpl; intros. omega. ded (IHn H).
apply Zle_lt_trans with (m := x × (x0 × power x0 n)). apply Zmult_le_compat_l.
omega. assumption. apply Zmult_gt_0_lt_compat_r. apply Zlt_gt.
apply Zmult_lt_O_compat. omega. apply spos_power. omega. assumption.
Qed.

Lemma Zmax_gub : ∀ m n k, m ≥ k → n ≥ k → Zmax m n ≥ k.

Proof.
intros. apply Zmax_case; assumption.
Qed.

Lemma elim_Zmax_l : ∀ x y z, x ≤ y → x ≤ Zmax y z.

Proof.
intros. eapply Zle_trans. apply H. apply Zle_max_l.
Qed.

Lemma elim_lt_Zmax_l : ∀ x y z, x < y → x < Zmax y z.

Proof.
intros. eapply Zlt_le_trans. eexact H. apply Zle_max_l.
Qed.

Lemma elim_Zmax_r : ∀ x y z, x ≤ z → x ≤ Zmax y z.

Proof.
intros. eapply Zle_trans. apply H. apply Zle_max_r.
Qed.

Lemma elim_lt_Zmax_r : ∀ x y z, x < z → x < Zmax y z.

Proof.
intros. rewrite Zmax_comm. apply elim_lt_Zmax_l. assumption.
Qed.

Lemma Zmax_l : ∀ x y, x ≥ y → Zmax x y = x.

Proof.
intros. unfold Zmax.
destruct (Dcompare_inf (x ?= y)) as [[xy | xy] | xy]; rewrite xy; try refl.
assert (x < y). assumption. omega.
Qed.

Lemma Zmax_r : ∀ x y, y ≥ x → Zmax x y = y.

Proof.
intros. rewrite Zmax_comm. apply Zmax_l. assumption.
Qed.

Lemma Zmax_ge_compat : ∀ x y x' y',
  x ≥ x' → y ≥ y' → Zmax x y ≥ Zmax x' y'.

Proof.
intros. destruct (Zmax_irreducible_inf x' y') as [H1|H1] ; rewrite H1; unfold ge.
rewrite Zmax_comm. apply Zle_ge. apply elim_Zmax_r. omega.
apply Zle_ge. apply elim_Zmax_r. omega.
Qed.

Lemma Zmax_gt_compat : ∀ x y x' y',
  x > x' → y > y' → Zmax x y > Zmax x' y'.

Proof.
intros. destruct (Z_ge_dec x y); destruct (Z_ge_dec x' y');
  do 2 first
    [ rewrite Zmax_r; [idtac | omega]
    | rewrite Zmax_l; [idtac | omega]
      | idtac
    ];
    omega.
Qed.

Lemma Zge_refl : ∀ k, k ≥ k.

Proof.
intros. omega.
Qed.