asd

Require Import Coq.omega.Omega.

(** an integer as a pair of nats *)
Inductive integer : Type :=
| pair : nat -> nat -> integer.

Notation "( x , y )" := (pair x y).

(** first component of the pair *)
Definition fst (x: integer): nat :=
match x with
| (m, n) => m
end.

(** second component of the pair *)
Definition snd (x: integer): nat :=
match x with
| (m, n) => n
end.

(** equality as an axiom *)
Axiom Z_eq: forall (x y: integer), fst x + snd y = snd x + fst y <-> x = y.

(** addition *)
Definition Z_plus (x: integer) (y: integer): integer :=
match x with
| (a1, a2) =>
  match y with
  | (b1, b2) => (a1 + b1, a2 + b2)
  end
end.

Notation "z '+Z' w" := (Z_plus z w) (at level 50, left associativity) : type_scope.

(** subtraction *)
Definition Z_minus (x: integer) (y: integer): integer :=
match x with
| (a1, a2) =>
  match y with
  | (b1, b2) => (a1 + b2, a2 + b1)
  end
end.

Notation "z '-Z' w" := (Z_minus z w) (at level 50, left associativity) : type_scope.

(** negation of an integer: z |-> -z *)
Definition Z_neg (x: integer): integer :=
match x with
| (a1, a2) => (a2, a1)
end.

Notation "'-Z' w" := (Z_neg w) (at level 35, right associativity) : type_scope.

(** multiplication *)
Definition Z_mult (x: integer) (y: integer): integer :=
match x with
| (a1, a2) =>
  match y with
  | (b1, b2) => (a1 * b1 + a2 * b2, a1 * b2 + a2 * b1)
  end
end.

Notation "z '*Z' w" := (Z_mult z w) (at level 40, left associativity) : type_scope.

(** zero and one *)
Definition Z0: integer := (0, 0).
Definition Z1: integer := (1, 0).

(** plus_assoc *)
Theorem Z_1: forall x y z: integer, (x +Z y) +Z z = x +Z (y +Z z).
Proof. destruct x, y, z. simpl. rewrite <- Z_eq. simpl. omega. Qed.

(** plus_comm *)
Theorem Z_2: forall x y: integer, x +Z y = y +Z x.
Proof. destruct x, y. simpl. rewrite <- Z_eq. simpl. omega. Qed.

(** zero as an identity for plus *)
Theorem Z_3: forall x: integer, x +Z Z0 = x.
Proof. destruct x. simpl. rewrite <- Z_eq. simpl. omega. Qed.

(** inverse element for plus *)
Theorem Z_4: forall x: integer, x +Z -Z x = Z0.
Proof. destruct x. simpl. rewrite <- Z_eq. simpl. omega. Qed.

(** mult_assoc *)
Theorem Z_5: forall x y z: integer, (x *Z y) *Z z = x *Z (y *Z z).
Proof. Admitted.

(** mult_comm *)
Theorem Z_6: forall x y: integer, x *Z y = y *Z x.
Proof. Admitted.

(** one as an identity for mult *)
Theorem Z_7: forall x: integer, x *Z Z1 = x.
Proof. Admitted.

(** left distribution law *)
Theorem Z_8: forall x y z: integer, x *Z (y +Z z) = x *Z y +Z x *Z z.
Proof. Admitted.

(** Z is an integral domain *)
Theorem Z_9: forall x y: integer, x *Z y = Z0 -> x = Z0 \/ y = Z0.
Proof. Admitted.

(** natural order for Z *)
Definition Z_leb (x y: integer) := (** x <= y iff *)
match x with
| (a1, a2) =>
  match y with
  | (b1, b2) => (a1 + b2 <= b1 + a2)
  end
end.

Notation "z '<=Z' w" := (Z_leb z w) (at level 70, no associativity) : type_scope.
Notation "z '<Z' w" := (~ Z_leb w z) (at level 70, no associativity) : type_scope.
Notation "z '>=Z' w" := (Z_leb w z) (at level 70, no associativity) : type_scope.
Notation "z '>Z' w" := (~ Z_leb z w) (at level 70, no associativity) : type_scope.

(** trichotomy *)
Theorem Z_10: forall x y: integer,
  (  x <Z y /\ ~ x = y /\ ~ x >Z y) \/
  (~ x <Z y /\   x = y /\ ~ x >Z y) \/
  (~ x <Z y /\ ~ x = y /\   x >Z y).
Proof. Admitted.

(** transitivity *)
Theorem Z_11: forall x y z: integer, x <Z y /\ y <Z z -> x <Z z.
Proof. Admitted.

(** addition preserves the order *)
Theorem Z_12: forall x y z: integer, x <Z y -> x +Z z <Z y +Z z.
Proof. Admitted.

(** mult by positive number preserves the order *)
Theorem Z_13: forall x y z: integer, x <Z y /\ z >Z Z0 -> x *Z z <Z y *Z z.
Proof. Admitted.

(** Z is not a trivial ring *)
Theorem Z_14: Z0 <> Z1.
Proof. unfold not. rewrite <- Z_eq. simpl. intros. inversion H. Qed.