(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import ZArith_base.
Require Export Wf_nat.
Require Import Omega.
Local Open Scope Z_scope.

Definition Zwf (c x y:Z) := c <= y /\ x < y.

Section wf_proof.

  Variable c : Z.

  Let f (z:Z) := Z.abs_nat (z - c).

  Lemma Zwf_well_founded : well_founded (Zwf c).
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
well_founded (Zwf c)
    red; intros.
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
Acc (Zwf c) a
    assert (forall (n:nat) (a:Z), (f a < n)%nat \/ a < c -> Acc (Zwf c) a).
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
H:forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
Acc (Zwf c) a
    clear a; simple induction n; intros.
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n:nat
a:Z
H:(f a < 0)%nat \/ a < c
Acc (Zwf c) a
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n, n0:nat
H:forall a0 : Z,
(f a0 < n0)%nat \/ a0 < c -> Acc (Zwf c) a0
a:Z
H0:(f a < S n0)%nat \/ a < c
Acc (Zwf c) a
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
H:forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
Acc (Zwf c) a

    case H; intros.
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n:nat
a:Z
H:(f a < 0)%nat \/ a < c
H0:(f a < 0)%nat
Acc (Zwf c) a
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n:nat
a:Z
H:(f a < 0)%nat \/ a < c
H0:a < c
Acc (Zwf c) a
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n, n0:nat
H:forall a0 : Z,
(f a0 < n0)%nat \/ a0 < c -> Acc (Zwf c) a0
a:Z
H0:(f a < S n0)%nat \/ a < c
Acc (Zwf c) a
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
H:forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
Acc (Zwf c) a
    case (lt_n_O (f a)); auto.
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n:nat
a:Z
H:(f a < 0)%nat \/ a < c
H0:a < c
Acc (Zwf c) a
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n, n0:nat
H:forall a0 : Z,
(f a0 < n0)%nat \/ a0 < c -> Acc (Zwf c) a0
a:Z
H0:(f a < S n0)%nat \/ a < c
Acc (Zwf c) a
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
H:forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
Acc (Zwf c) a
    apply Acc_intro; unfold Zwf; intros.
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n:nat
a:Z
H:(f a < 0)%nat \/ a < c
H0:a < c
y:Z
H1:c <= a /\ y < a
Acc (fun x y0 : Z => c <= y0 /\ x < y0) y
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n, n0:nat
H:forall a0 : Z,
(f a0 < n0)%nat \/ a0 < c -> Acc (Zwf c) a0
a:Z
H0:(f a < S n0)%nat \/ a < c
Acc (Zwf c) a
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
H:forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
Acc (Zwf c) a
    assert False; omega || contradiction.
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n, n0:nat
H:forall a0 : Z,
(f a0 < n0)%nat \/ a0 < c -> Acc (Zwf c) a0
a:Z
H0:(f a < S n0)%nat \/ a < c
Acc (Zwf c) a
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
H:forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
Acc (Zwf c) a

    case H0; clear H0; intro; auto.
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n, n0:nat
H:forall a0 : Z,
(f a0 < n0)%nat \/ a0 < c -> Acc (Zwf c) a0
a:Z
H0:(f a < S n0)%nat
Acc (Zwf c) a
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
H:forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
Acc (Zwf c) a
    apply Acc_intro; intros.
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n, n0:nat
H:forall a0 : Z,
(f a0 < n0)%nat \/ a0 < c -> Acc (Zwf c) a0
a:Z
H0:(f a < S n0)%nat
y:Z
H1:Zwf c y a
Acc (Zwf c) y
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
H:forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
Acc (Zwf c) a
    apply H.
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n, n0:nat
H:forall a0 : Z,
(f a0 < n0)%nat \/ a0 < c -> Acc (Zwf c) a0
a:Z
H0:(f a < S n0)%nat
y:Z
H1:Zwf c y a
(f y < n0)%nat \/ y < c
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
H:forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
Acc (Zwf c) a
    unfold Zwf in H1.
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n, n0:nat
H:forall a0 : Z,
(f a0 < n0)%nat \/ a0 < c -> Acc (Zwf c) a0
a:Z
H0:(f a < S n0)%nat
y:Z
H1:c <= a /\ y < a
(f y < n0)%nat \/ y < c
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
H:forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
Acc (Zwf c) a
    case (Z.le_gt_cases c y); intro; auto with zarith.
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n, n0:nat
H:forall a0 : Z,
(f a0 < n0)%nat \/ a0 < c -> Acc (Zwf c) a0
a:Z
H0:(f a < S n0)%nat
y:Z
H1:c <= a /\ y < a
H2:c <= y
(f y < n0)%nat \/ y < c
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
H:forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
Acc (Zwf c) a
    left.
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n, n0:nat
H:forall a0 : Z,
(f a0 < n0)%nat \/ a0 < c -> Acc (Zwf c) a0
a:Z
H0:(f a < S n0)%nat
y:Z
H1:c <= a /\ y < a
H2:c <= y
(f y < n0)%nat
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
H:forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
Acc (Zwf c) a
    red in H0.
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n, n0:nat
H:forall a0 : Z,
(f a0 < n0)%nat \/ a0 < c -> Acc (Zwf c) a0
a:Z
H0:(S (f a) <= S n0)%nat
y:Z
H1:c <= a /\ y < a
H2:c <= y
(f y < n0)%nat
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
H:forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
Acc (Zwf c) a
    apply lt_le_trans with (f a); auto with arith.
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n, n0:nat
H:forall a0 : Z,
(f a0 < n0)%nat \/ a0 < c -> Acc (Zwf c) a0
a:Z
H0:(S (f a) <= S n0)%nat
y:Z
H1:c <= a /\ y < a
H2:c <= y
(f y < f a)%nat
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
H:forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
Acc (Zwf c) a
    unfold f.
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
n, n0:nat
H:forall a0 : Z,
(f a0 < n0)%nat \/ a0 < c -> Acc (Zwf c) a0
a:Z
H0:(S (f a) <= S n0)%nat
y:Z
H1:c <= a /\ y < a
H2:c <= y
(Z.abs_nat (y - c) < Z.abs_nat (a - c))%nat
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
H:forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
Acc (Zwf c) a
    apply Zabs2Nat.inj_lt; omega.
c:Z
f:=fun z : Z => Z.abs_nat (z - c):Z -> nat
a:Z
H:forall (n : nat) (a0 : Z),
(f a0 < n)%nat \/ a0 < c -> Acc (Zwf c) a0
Acc (Zwf c) a
    apply (H (S (f a))); auto.
  Qed.

End wf_proof.

Hint Resolve Zwf_well_founded: datatypes.

Definition Zwf_up (c x y:Z) := y < x <= c.

Section wf_proof_up.

  Variable c : Z.

  Let f (z:Z) := Z.abs_nat (c - z).

  Lemma Zwf_up_well_founded : well_founded (Zwf_up c).
c:Z
f:=fun z : Z => Z.abs_nat (c - z):Z -> nat
well_founded (Zwf_up c)
  Proof.
c:Z
f:=fun z : Z => Z.abs_nat (c - z):Z -> nat
well_founded (Zwf_up c)
    apply well_founded_lt_compat with (f := f).
c:Z
f:=fun z : Z => Z.abs_nat (c - z):Z -> nat
forall x y : Z, Zwf_up c x y -> (f x < f y)%nat
    unfold Zwf_up, f.
c:Z
f:=fun z : Z => Z.abs_nat (c - z):Z -> nat
forall x y : Z,
y < x <= c ->
(Z.abs_nat (c - x) < Z.abs_nat (c - y))%nat
    intros.
c:Z
f:=fun z : Z => Z.abs_nat (c - z):Z -> nat
x, y:Z
H:y < x <= c
(Z.abs_nat (c - x) < Z.abs_nat (c - y))%nat
    apply Zabs2Nat.inj_lt; try (apply Z.le_0_sub; intuition).
c:Z
f:=fun z : Z => Z.abs_nat (c - z):Z -> nat
x, y:Z
H:y < x <= c
c - x < c - y
    now apply Z.sub_lt_mono_l.
  Qed.

End wf_proof_up.

Hint Resolve Zwf_up_well_founded: datatypes.