Require ZArith.

Section lattice_lemma.

Parameters d0, c1, d1, c2, d2 : Z.

Hypothesis c1_pos : `c1 >= 0`.
Hypothesis c1_geq_d1 : `c1 >= d1`.
Hypothesis c2_pos : `c2 >= 0`.
Hypothesis c2_geq_d2 : `c2 >= d2`.

Hypothesis pre_order : (`d1 <= 0` /\ `d2 >= 0`) \/ (`d1 < 0` /\ `d2 < 0` /\ `c1 <= c2`) \/ (`d1 > 0` /\ `d2 > 0` /\ `c2 + d1 <= c1 + d2`).

(*
Definition Zmax := [x, y : Z] Cases (Zcompare x y) of
  EGAL => x
| SUPERIEUR => x
| INFERIEUR => y
end.  

Definition x1 := (Zmax `0` d0). 
Definition x2 := (Zmax `0` `d0+c1`).
Definition x3 := (Zmax `0` `d0+d1`).
Definition x4 := (Zmax c2 `d0+d1`).
Definition x5 := (Zmax d2 `d0+d1`).

Definition y1 := x1.
Definition y2 := (Zmax c2 `d0`).
Definition y3 := (Zmax d2 `d0`). 
Definition y4 := (Zmax d2 `d0+c1`). 
Definition y5 := x5. *)

Parameters x1, x2, x3, x4, x5, y1, y2, y3, y4, y5 : Z.
Definition is_max := [x, a, b : Z] (`a <= b` /\ `x = b`) \/ (`a >= b` /\ `x = a`).

Hypothesis def_x1 : (is_max x1 `0` d0). 
Hypothesis def_x2 : (is_max x2 `0` `d0+c1`).
Hypothesis def_x3 : (is_max x3 `0` `d0+d1`).
Hypothesis def_x4 : (is_max x4 c2 `d0+d1`).
Hypothesis def_x5 : (is_max x5 d2 `d0+d1`).

Hypothesis def_y1 : `y1 = x1`.
Hypothesis def_y2 : (is_max y2 c2 `d0`).
Hypothesis def_y3 : (is_max y3 d2 `d0`). 
Hypothesis def_y4 : (is_max y4 d2 `d0+c1`). 
Hypothesis def_y5 : `y5 = x5`.

Definition a11 := `x1 <= y1`.
Definition a12 := `x1 <= y2`.
Definition a13 := `x1 <= y3`.
Definition a14 := `x1 <= y4`.
Definition a15 := `x1 <= y5`.

Definition a21 := `x2 <= y1`.
Definition a22 := `x2 <= y2`.
Definition a23 := `x2 <= y3`.
Definition a24 := `x2 <= y4`.
Definition a25 := `x2 <= y5`.

Definition a31 := `x3 <= y1`.
Definition a32 := `x3 <= y2`.
Definition a33 := `x3 <= y3`.
Definition a34 := `x3 <= y4`.
Definition a35 := `x3 <= y5`.

Definition a41 := `x4 <= y1`.
Definition a42 := `x4 <= y2`.
Definition a43 := `x4 <= y3`.
Definition a44 := `x4 <= y4`.
Definition a45 := `x4 <= y5`.

Definition a51 := `x5 <= y1`.
Definition a52 := `x5 <= y2`.
Definition a53 := `x5 <= y3`.
Definition a54 := `x5 <= y4`.
Definition a55 := `x5 <= y5`.

Definition b55 := a55.
Definition b45 := a45 /\ b55.
Definition b35 := a35 /\ b45.
Definition b25 := a25 /\ b35.
Definition b15 := a15 /\ b25.

Definition b54 := a54 /\ b55.
Definition b44 := a44 /\ (b54 \/ b45).
Definition b34 := a34 /\ (b44 \/ b35).
Definition b24 := a24 /\ (b34 \/ b25).
Definition b14 := a14 /\ (b24 \/ b15).

Definition b53 := a53 /\ b54.
Definition b43 := a43 /\ (b53 \/ b44).
Definition b33 := a33 /\ (b43 \/ b34).
Definition b23 := a23 /\ (b33 \/ b24).
Definition b13 := a13 /\ (b23 \/ b14).

Definition b52 := a52 /\ b53.
Definition b42 := a42 /\ (b52 \/ b43).
Definition b32 := a32 /\ (b42 \/ b33).
Definition b22 := a22 /\ (b32 \/ b23).
Definition b12 := a12 /\ (b22 \/ b13).

Definition b51 := a51 /\ b52.
Definition b41 := a41 /\ (b51 \/ b42).
Definition b31 := a31 /\ (b41 \/ b32).
Definition b21 := a21 /\ (b31 \/ b22).
Definition b11 := a11 /\ (b21 \/ b12).

Require Omega.

Lemma latt_lemma : b11.

Tactic Definition absurd :=
  Cut False; Contradiction; (Repeat Match Context With [H:?1=?2 |- ?] -> Clear H); Omega.

Tactic Definition show_one_a a :=
  Assert a; [
  Unfold a11 a12 a13 a14 a15 a21 a22 a23 a24 a25 a31 a32 a33 a34 a35 a41 a42 a43 a44 a45 a51 a52 a53 a54 a55;
 (Repeat Match Context With [H:?1=?2 |- ?] -> Rewrite H);
 (Repeat Match Context With [H:?1=?2 |- ?] -> Clear H);
  Omega | Idtac].

Tactic Definition show_all_a :=
  (Try show_one_a a11);
  (Try show_one_a a12);
  (Try show_one_a a13);
  (Try show_one_a a14);
  (Try show_one_a a15);
  (Try show_one_a a21);
  (Try show_one_a a22);
  (Try show_one_a a23);
  (Try show_one_a a24);
  (Try show_one_a a25);
  (Try show_one_a a31);
  (Try show_one_a a32);
  (Try show_one_a a33);
  (Try show_one_a a34);
  (Try show_one_a a35);
  (Try show_one_a a41);
  (Try show_one_a a42);
  (Try show_one_a a43);
  (Try show_one_a a44);
  (Try show_one_a a45);
  (Try show_one_a a51);
  (Try show_one_a a52);
  (Try show_one_a a53);
  (Try show_one_a a54);
  (Try show_one_a a55);
  (Try show_one_a '(a22\/a44)).

Tactic Definition path :=
   show_all_a;
  (Repeat Match Context With [H:?1=?2 |- ?] -> Clear H);
  (Repeat Match Context With [H:(Zle ?1 ?2) |- ?] -> Clear H);
  (Repeat Match Context With [H:(Zlt ?1 ?2) |- ?] -> Clear H);
  (Repeat Match Context With [H:(Zge ?1 ?2) |- ?] -> Clear H);
   Unfold b11 b12 b13 b14 b15 b21 b22 b23 b24 b25 b31 b32 b33 b34 b35 b41 b42 b43 b44 b45 b51 b52 b53 b54 b55;
   Tauto.

Proof.
Elim pre_order; [Idtac | Intro H; Elim H]; Intro H01; NewDestruct H01; Clear pre_order;
Elim def_x1; Intros [Hx1a Hx1b]; Clear def_x1;
Elim def_x2; Intros [Hx2a Hx2b]; Clear def_x2;
Elim def_x3; Intros [Hx3a Hx3b]; Clear def_x3;
Elim def_x4; Intros [Hx4a Hx4b]; Clear def_x4;
Elim def_x5; Intros [Hx5a Hx5b]; Clear def_x5;
Elim def_y2; Intros [Hy2a Hy2b]; Clear def_y2;
Elim def_y3; Intros [Hy3a Hy3b]; Clear def_y3;
Elim def_y4; Intros [Hy4a Hy4b]; Clear def_y4;
First [absurd | path].
Qed.

End Lattice_lemma.
