asgaf

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.

Lemma dist_l: forall a b c: nat, c * (a + b) = c * a + c * b.
Proof. induction c.
  - auto.
  - simpl. rewrite -> plus_assoc. rewrite <- (plus_assoc a (c * a) b). rewrite (plus_comm (c * a) b). omega.
Qed.

Lemma dist_r: forall a b c: nat, (a + b) * c = a * c + b * c.
Proof. induction a.
  - auto.
  - simpl. intros. rewrite <- plus_assoc. rewrite <- (IHa b c). reflexivity.
Qed.

(** mult_assoc *)
Theorem Z_5: 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.
  repeat rewrite dist_l. repeat rewrite dist_r. repeat rewrite plus_assoc. repeat rewrite mult_assoc. omega.
Qed.

(** mult_comm *)
Theorem Z_6: forall x y: integer, x *Z y = y *Z x.
Proof. destruct x, y. simpl. rewrite <- Z_eq. simpl. repeat rewrite plus_assoc.
rewrite (mult_comm n1 n), (mult_comm n0 n2), (mult_comm n1 n0), (mult_comm n n2). omega. Qed.

(** one as an identity for mult *)
Theorem Z_7: forall x: integer, x *Z Z1 = x.
Proof. destruct x. simpl. rewrite <- Z_eq. simpl. omega. Qed.

(** left distribution law *)
Theorem Z_8: forall x y z: integer, x *Z (y +Z z) = x *Z y +Z x *Z z.
Proof. destruct x, y, z. simpl. rewrite <- Z_eq. simpl.
  repeat rewrite dist_l. repeat rewrite dist_r. repeat rewrite plus_assoc. repeat rewrite mult_assoc. omega. Qed.

(** Z is an integral domain *)
Theorem Z_9: forall x y: integer, x *Z y = Z0 -> x = Z0 \/ y = Z0.
Proof. destruct x. remember (beq_nat n n0) as b. destruct b.
  - intros. left. rewrite <- Z_eq. simpl. symmetry in Heqb.
    rewrite beq_nat_true_iff in Heqb. rewrite Heqb. omega.
  - intros. right. rewrite <- Z_eq. simpl. symmetry in Heqb.
    rewrite beq_nat_false_iff in Heqb. rewrite <- Z_eq in H.
    destruct y. simpl in H. repeat (rewrite <- plus_n_O in H).
    simpl. repeat (rewrite <- plus_n_O).
    assert (forall a b: nat, a <> b -> minus a b <> 0 \/ minus b a <> 0).
    { induction a.
      - intros. simpl. right. omega.
      - destruct b. intros. left. omega. intros.
        assert (forall c d: nat, c = d -> S c = S d).
        { intros. rewrite H1. reflexivity. }
        assert (a <> b).
        { unfold not. intros. apply H1 in H2. apply H0 in H2. inversion H2. }
        apply IHa in H2. destruct H2. left. omega. right. omega. }

    apply H0 in Heqb.
    assert (forall q r, q - r <> 0 /\ q * n1 + r * n2 = q * n2 + r * n1 -> n1 = n2).
    { intros. destruct H1.
      assert (q * n1 - r * n1 = q * n2 - r * n2). { omega. }
      assert (forall n n0, n - n0 <> 0 -> (n - n0) + n0 = n).
      { intros. omega. }
      rewrite <- (H4 q r) in H3.
      assert (forall x y: nat, x + y - y = x).
      { intros. omega. }
      repeat rewrite dist_r in H3.
      repeat rewrite H5 in H3.
      assert (forall z x y: nat, S z * x = S z * y -> x = y).
      { assert (S_inj: forall k l: nat, S k = S l -> k = l). { intros. omega. }
        assert (S_surj: forall k l: nat, k = l -> S k = S l). { intros. rewrite H6. reflexivity. }
        induction z. intros. omega. induction x. simpl. destruct y. reflexivity. intros.
        rewrite <- mult_n_O in H6. inversion H6.
        assert (forall a b, a * S b = a + a * b).
        { intros. induction a. omega. simpl. rewrite IHa. omega. }
        destruct y. intros. rewrite <- mult_n_O in H7. inversion H7.
        repeat rewrite (H6 (S(S z)) _). intros.
        apply S_surj. apply IHx. omega. }
      remember (q - r) as k. destruct k. omega. apply (H6 k). apply H3.
      apply H1.
    }
    destruct Heqb.
    apply (H1 n n0). split. apply H2. apply H.
    apply (H1 n0 n). split. apply H2. omega. Qed.

(** 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.

Lemma LT: forall x y: integer, x -Z y <Z Z0 <-> x <Z y.
  Proof. intros. destruct x, y. split; unfold Z_leb; simpl; omega. Qed.
Lemma SM: forall x y: integer, x -Z y = Z0 <-> x = y.
  Proof. intros. destruct x, y. split; repeat rewrite <- Z_eq; simpl; omega. Qed.
Lemma GT: forall x y: integer, x -Z y >Z Z0 <-> x >Z y.
  Proof. intros. destruct x, y. split; unfold Z_leb; simpl; omega. Qed.


(** 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.
  assert (Z_10_0: forall x: integer,
    (  x <Z Z0 /\ ~ x = Z0 /\ ~ x >Z Z0) \/
    (~ x <Z Z0 /\   x = Z0 /\ ~ x >Z Z0) \/
    (~ x <Z Z0 /\ ~ x = Z0 /\   x >Z Z0)).
  { destruct x. remember (n - n0) as d1. destruct d1.
    - remember (n0 - n) as d2. destruct d2.
      + right. left. split.
        unfold Z_leb. simpl. omega.
        split. rewrite <- Z_eq. simpl. omega.
        unfold Z_leb. simpl. omega.
      + left. split.
        unfold Z_leb. simpl. omega.
        split. unfold not. rewrite <- Z_eq. simpl. omega.
        unfold Z_leb. simpl. omega.
    - right. right. split.
      unfold Z_leb. simpl. omega.
      split. unfold not. rewrite<- Z_eq. simpl. omega.
      unfold Z_leb. simpl. omega.
  }

  intros. rewrite <- LT. rewrite <- SM. rewrite <- (GT x y).
  apply Z_10_0.
Qed.

(** transitivity *)
Theorem Z_11: forall x y z: integer, x <Z y /\ y <Z z -> x <Z z.
Proof. intros x y z. rewrite <- (LT x y). rewrite <- (LT x z). rewrite <- (LT y z).
  assert (forall a b: integer, a <Z Z0 /\ b <Z Z0 -> a +Z b <Z Z0).
  { destruct a, b. intros. simpl in H; destruct H. simpl. omega. }
  assert ((x -Z y) +Z (y -Z z) = x -Z z).
  { destruct x, y, z. simpl. rewrite <- Z_eq. simpl. omega. }
  intros. rewrite <- H0. apply (H (x -Z y) (y -Z z)). apply H1. Qed.

(** addition preserves the order *)
Theorem Z_12: forall x y z: integer, x <Z y -> x +Z z <Z y +Z z.
Proof. intros x y z. rewrite <- GT. destruct x, y, z. simpl. omega. Qed.

(** 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.
  intros x y z. rewrite <- GT. rewrite <- (GT (y *Z z) _).
  assert (forall n m: nat, ~ n <= m <-> n > m).
  { induction n. intros. omega. intros. destruct m. omega. omega. }
  assert (L: forall a b c d: nat, a >= b /\ c > d -> a + c > b + d).
  { induction a. intros. destruct H0. inversion H0. destruct b. intros.
    simpl. apply H1. simpl. apply H1.
    assert (forall a b: nat, S a >= S b <-> a >= b). { intros. omega. }
    destruct b. intros. simpl. omega.
    intros. rewrite H0 in H1. simpl. apply H0. apply IHa. apply H1. }
  assert (forall a b, a * S b = a + a * b).
  { intros. induction a. omega. simpl. rewrite IHa. omega. }
  assert (C: forall a b c: nat, a > b -> a * S c > b * S c).
  { induction c. omega. intros.
    rewrite H0. rewrite (H0 _ (S c)). assert (a * S c > b * S c). apply IHc in H1; apply H1.
    apply (L a b _ _). split. omega. apply H2. }
  assert (forall a b: integer, a >Z Z0 /\ b >Z Z0 -> a *Z b >Z Z0).
  { destruct a, b. simpl. repeat rewrite <- plus_n_O.
    repeat rewrite H.
    generalize dependent n0.
    induction n. intros. inversion H1. inversion H2. simpl. intros.
    destruct H1. destruct n0. simpl. repeat rewrite <- plus_n_O.
    rewrite mult_comm. rewrite (mult_comm n n2). repeat rewrite <- H0.
    auto. simpl. repeat rewrite -> plus_assoc.
    rewrite -> (plus_comm _ n2). repeat rewrite <- (plus_assoc n2 _ _).
    rewrite -> (plus_comm _ n1). repeat rewrite -> plus_assoc.
    repeat rewrite <- (plus_assoc (n2 + n1)).
    apply L. split. omega. apply IHn. split. omega. omega. }
  assert (forall v w: integer, v +Z -Z w = v -Z w).
  { destruct v, w. simpl. rewrite <- Z_eq. simpl. omega. }
  assert (forall v w: integer, v *Z -Z w = -Z (v *Z w)).
  { destruct v, w. simpl. rewrite <- Z_eq. simpl. omega. }
  assert (y *Z z -Z x *Z z = (y -Z x) *Z z).
  { rewrite (Z_6 y z), (Z_6 x z), (Z_6 _ z).
    repeat rewrite <- H2. symmetry. rewrite <- H3. apply Z_8. }
  rewrite H4. apply H1. Qed.


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