(************************************************************************)
(*         *   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 Export Field.
Require Export QArith_base.
Require Import NArithRing.

Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq.
ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq
Proof.
ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq
  constructor.
forall x : Q, 0 + x == x
forall x y : Q, x + y == y + x
forall x y z : Q, x + (y + z) == x + y + z
forall x : Q, 1 * x == x
forall x y : Q, x * y == y * x
forall x y z : Q, x * (y * z) == x * y * z
forall x y z : Q, (x + y) * z == x * z + y * z
forall x y : Q, x - y == x + - y
forall x : Q, x + - x == 0
  exact Qplus_0_l.
forall x y : Q, x + y == y + x
forall x y z : Q, x + (y + z) == x + y + z
forall x : Q, 1 * x == x
forall x y : Q, x * y == y * x
forall x y z : Q, x * (y * z) == x * y * z
forall x y z : Q, (x + y) * z == x * z + y * z
forall x y : Q, x - y == x + - y
forall x : Q, x + - x == 0
  exact Qplus_comm.
forall x y z : Q, x + (y + z) == x + y + z
forall x : Q, 1 * x == x
forall x y : Q, x * y == y * x
forall x y z : Q, x * (y * z) == x * y * z
forall x y z : Q, (x + y) * z == x * z + y * z
forall x y : Q, x - y == x + - y
forall x : Q, x + - x == 0
  exact Qplus_assoc.
forall x : Q, 1 * x == x
forall x y : Q, x * y == y * x
forall x y z : Q, x * (y * z) == x * y * z
forall x y z : Q, (x + y) * z == x * z + y * z
forall x y : Q, x - y == x + - y
forall x : Q, x + - x == 0
  exact Qmult_1_l.
forall x y : Q, x * y == y * x
forall x y z : Q, x * (y * z) == x * y * z
forall x y z : Q, (x + y) * z == x * z + y * z
forall x y : Q, x - y == x + - y
forall x : Q, x + - x == 0
  exact Qmult_comm.
forall x y z : Q, x * (y * z) == x * y * z
forall x y z : Q, (x + y) * z == x * z + y * z
forall x y : Q, x - y == x + - y
forall x : Q, x + - x == 0
  exact Qmult_assoc.
forall x y z : Q, (x + y) * z == x * z + y * z
forall x y : Q, x - y == x + - y
forall x : Q, x + - x == 0
  exact Qmult_plus_distr_l.
forall x y : Q, x - y == x + - y
forall x : Q, x + - x == 0
  reflexivity.
forall x : Q, x + - x == 0
  exact Qplus_opp_r.
Qed.

Definition Qsft : field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq.
field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq
Proof.
field_theory 0 1 Qplus Qmult Qminus Qopp Qdiv Qinv Qeq
  constructor.
ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq
~ 1 == 0
forall p q : Q, p / q == p * / q
forall p : Q, ~ p == 0 -> / p * p == 1
  exact Qsrt.
~ 1 == 0
forall p q : Q, p / q == p * / q
forall p : Q, ~ p == 0 -> / p * p == 1
  discriminate.
forall p q : Q, p / q == p * / q
forall p : Q, ~ p == 0 -> / p * p == 1
  reflexivity.
forall p : Q, ~ p == 0 -> / p * p == 1
  intros p Hp.
p:Q
Hp:~ p == 0
/ p * p == 1
  rewrite Qmult_comm.
p:Q
Hp:~ p == 0
p * / p == 1
  apply Qmult_inv_r.
p:Q
Hp:~ p == 0
~ p == 0
  exact Hp.
Qed.

Lemma Qpower_theory : power_theory 1 Qmult Qeq Z.of_N Qpower.
power_theory 1 Qmult Qeq Z.of_N Qpower
Proof.
power_theory 1 Qmult Qeq Z.of_N Qpower
constructor.
forall (r : Q) (n : N),
r ^ Z.of_N n == pow_N 1 Qmult r n
intros r [|n];
reflexivity.
Qed.

Ltac isQcst t :=
  match t with
  | inject_Z ?z => isZcst z
  | Qmake ?n ?d =>
    match isZcst n with
      true => isPcst d
    | _ => false
    end
  | _ => false
  end.

Ltac Qcst t :=
  match isQcst t with
    true => t
    | _ => NotConstant
  end.

Ltac Qpow_tac t :=
  match t with
  | Z0 => N0
  | Zpos ?n => Ncst (Npos n)
  | Z.of_N ?n => Ncst n
  | NtoZ ?n => Ncst n
  | _ => NotConstant
  end.

Add Field Qfield : Qsft
 (decidable Qeq_bool_eq,
  completeness Qeq_eq_bool,
  constants [Qcst],
  power_tac Qpower_theory [Qpow_tac]).

Section Examples.

Let ex1 : forall x y z : Q, (x+y)*z ==  (x*z)+(y*z).
forall x y z : Q, (x + y) * z == x * z + y * z
  intros.
x, y, z:Q
(x + y) * z == x * z + y * z
  ring.
Qed.

Let ex2 : forall x y : Q, x+y == y+x.
ex1:forall x y z : Q, (x + y) * z == x * z + y * z
forall x y : Q, x + y == y + x
  intros.
ex1:forall x0 y0 z : Q, (x0 + y0) * z == x0 * z + y0 * z
x, y:Q
x + y == y + x
  ring.
Qed.

Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z).
ex1:forall x y z : Q, (x + y) * z == x * z + y * z
ex2:forall x y : Q, x + y == y + x
forall x y z : Q, x + y + z == x + (y + z)
  intros.
ex1:forall x0 y0 z0 : Q, (x0 + y0) * z0 == x0 * z0 + y0 * z0
ex2:forall x0 y0 : Q, x0 + y0 == y0 + x0
x, y, z:Q
x + y + z == x + (y + z)
  ring.
Qed.

Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2).
ex1:forall x y z : Q, (x + y) * z == x * z + y * z
ex2:forall x y : Q, x + y == y + x
ex3:forall x y z : Q, x + y + z == x + (y + z)
inject_Z 1 + inject_Z 1 == inject_Z 2
  ring.
Qed.

Let ex5 : 1+1 == 2#1.
ex1:forall x y z : Q, (x + y) * z == x * z + y * z
ex2:forall x y : Q, x + y == y + x
ex3:forall x y z : Q, x + y + z == x + (y + z)
ex4:inject_Z 1 + inject_Z 1 == inject_Z 2
1 + 1 == 2
  ring.
Qed.

Let ex6 : (1#1)+(1#1) == 2#1.
ex1:forall x y z : Q, (x + y) * z == x * z + y * z
ex2:forall x y : Q, x + y == y + x
ex3:forall x y z : Q, x + y + z == x + (y + z)
ex4:inject_Z 1 + inject_Z 1 == inject_Z 2
ex5:1 + 1 == 2
1 + 1 == 2
  ring.
Qed.

Let ex7 : forall x : Q, x-x== 0.
ex1:forall x y z : Q, (x + y) * z == x * z + y * z
ex2:forall x y : Q, x + y == y + x
ex3:forall x y z : Q, x + y + z == x + (y + z)
ex4:inject_Z 1 + inject_Z 1 == inject_Z 2
ex5, ex6:1 + 1 == 2
forall x : Q, x - x == 0
  intro.
ex1:forall x0 y z : Q, (x0 + y) * z == x0 * z + y * z
ex2:forall x0 y : Q, x0 + y == y + x0
ex3:forall x0 y z : Q, x0 + y + z == x0 + (y + z)
ex4:inject_Z 1 + inject_Z 1 == inject_Z 2
ex5, ex6:1 + 1 == 2
x:Q
x - x == 0
  ring.
Qed.

Let ex8 : forall x : Q, x^1 == x.
ex1:forall x y z : Q, (x + y) * z == x * z + y * z
ex2:forall x y : Q, x + y == y + x
ex3:forall x y z : Q, x + y + z == x + (y + z)
ex4:inject_Z 1 + inject_Z 1 == inject_Z 2
ex5, ex6:1 + 1 == 2
ex7:forall x : Q, x - x == 0
forall x : Q, x ^ 1 == x
  intro.
ex1:forall x0 y z : Q, (x0 + y) * z == x0 * z + y * z
ex2:forall x0 y : Q, x0 + y == y + x0
ex3:forall x0 y z : Q, x0 + y + z == x0 + (y + z)
ex4:inject_Z 1 + inject_Z 1 == inject_Z 2
ex5, ex6:1 + 1 == 2
ex7:forall x0 : Q, x0 - x0 == 0
x:Q
x ^ 1 == x
  ring.
Qed.

Let ex9 : forall x : Q, x^0 == 1.
ex1:forall x y z : Q, (x + y) * z == x * z + y * z
ex2:forall x y : Q, x + y == y + x
ex3:forall x y z : Q, x + y + z == x + (y + z)
ex4:inject_Z 1 + inject_Z 1 == inject_Z 2
ex5, ex6:1 + 1 == 2
ex7:forall x : Q, x - x == 0
ex8:forall x : Q, x ^ 1 == x
forall x : Q, x ^ 0 == 1
  intro.
ex1:forall x0 y z : Q, (x0 + y) * z == x0 * z + y * z
ex2:forall x0 y : Q, x0 + y == y + x0
ex3:forall x0 y z : Q, x0 + y + z == x0 + (y + z)
ex4:inject_Z 1 + inject_Z 1 == inject_Z 2
ex5, ex6:1 + 1 == 2
ex7:forall x0 : Q, x0 - x0 == 0
ex8:forall x0 : Q, x0 ^ 1 == x0
x:Q
x ^ 0 == 1
  ring.
Qed.

Let ex10 : forall x y : Q, ~(y==0) -> (x/y)*y == x.
ex1:forall x y z : Q, (x + y) * z == x * z + y * z
ex2:forall x y : Q, x + y == y + x
ex3:forall x y z : Q, x + y + z == x + (y + z)
ex4:inject_Z 1 + inject_Z 1 == inject_Z 2
ex5, ex6:1 + 1 == 2
ex7:forall x : Q, x - x == 0
ex8:forall x : Q, x ^ 1 == x
ex9:forall x : Q, x ^ 0 == 1
forall x y : Q, ~ y == 0 -> x / y * y == x
intros.
ex1:forall x0 y0 z : Q, (x0 + y0) * z == x0 * z + y0 * z
ex2:forall x0 y0 : Q, x0 + y0 == y0 + x0
ex3:forall x0 y0 z : Q, x0 + y0 + z == x0 + (y0 + z)
ex4:inject_Z 1 + inject_Z 1 == inject_Z 2
ex5, ex6:1 + 1 == 2
ex7:forall x0 : Q, x0 - x0 == 0
ex8:forall x0 : Q, x0 ^ 1 == x0
ex9:forall x0 : Q, x0 ^ 0 == 1
x, y:Q
H:~ y == 0
x / y * y == x
field.
ex1:forall x0 y0 z : Q, (x0 + y0) * z == x0 * z + y0 * z
ex2:forall x0 y0 : Q, x0 + y0 == y0 + x0
ex3:forall x0 y0 z : Q, x0 + y0 + z == x0 + (y0 + z)
ex4:inject_Z 1 + inject_Z 1 == inject_Z 2
ex5, ex6:1 + 1 == 2
ex7:forall x0 : Q, x0 - x0 == 0
ex8:forall x0 : Q, x0 ^ 1 == x0
ex9:forall x0 : Q, x0 ^ 0 == 1
x, y:Q
H:~ y == 0
~ y == 0
auto.
Qed.

End Examples.

Lemma Qopp_plus : forall a b,  -(a+b) == -a + -b.
forall a b : Q, - (a + b) == - a + - b
Proof.
forall a b : Q, - (a + b) == - a + - b
  intros; ring.
Qed.

Lemma Qopp_opp : forall q, - -q==q.
forall q : Q, - - q == q
Proof.
forall q : Q, - - q == q
  intros; ring.
Qed.