(** An _axiomatic_ approach to real numbers. *)

Parameter R : Set.

Delimit Scope R_scope with R.
Local Open Scope R_scope.

(** We'll start by _declaring_ two real numbers - the important ones. *)
Parameter R0 : R.
Parameter R1 : R.

(** Along with methods for obtaining (some of) the others *)
Parameter Rplus : R -> R -> R.
Parameter Rmult : R -> R -> R.
Parameter Ropp : R -> R.
Parameter Rinv : R -> R.
Parameter Rlt : R -> R -> Prop.

Infix "+" := Rplus : R_scope.
Infix "*" := Rmult : R_scope.
Notation "- x" := (Ropp x) : R_scope.
Notation "/ x" := (Rinv x) : R_scope.

Infix "<" := Rlt : R_scope.

(** Other definitions are shorthand for our axioms *)

Definition Rgt (r1 r2:R) : Prop := r2 < r1.
Definition Rle (r1 r2:R) : Prop := r1 < r2 \/ r1 = r2.
Definition Rge (r1 r2:R) : Prop := Rgt r1 r2 \/ r1 = r2.

Definition Rminus (r1 r2:R) : R := r1 + - r2.
Definition Rdiv (r1 r2:R) : R := r1 * / r2.

Infix "-" := Rminus : R_scope.
Infix "/" := Rdiv : R_scope.

Infix "<=" := Rle : R_scope.
Infix ">=" := Rge : R_scope.
Infix ">" := Rgt : R_scope.

(** We'd like to be able to convert natural numbers to Rs, thereby allowing
    ourselves to write numbers like 0, 1, 2, 3... *)

Fixpoint INR (n : nat) : R :=
  match n with
  | O    => R0
  | S n' => R1 + INR n'
  end.

(** A _coercion_ tells Coq to try applying a given function whenever
   types mismatch. For instance, [Rplus 4 5] will currently give a
   type error. *)

Fail Check (4 + 5).

Coercion INR : nat >-> R.
 
Check 4 + 5.
Compute (4 + 5).

(** The standard library defines a coercion from Z to R which is
    slightly more useful but also more difficult to parse. *)

(* *** *)
(** We can now proceed to the core of the real number library : The axioms *)

Axiom R1_neq_R0 : 1 <> 0.

(** Addition *)

Axiom Rplus_comm : forall r1 r2 : R, r1 + r2 = r2 + r1.

Axiom Rplus_assoc : forall r1 r2 r3 : R, r1 + r2 + r3 = r1 + (r2 + r3).

Axiom Rplus_opp_r : forall r : R, r + - r = 0.

Axiom Rplus_0_l : forall r : R, 0 + r = r.

(** Of course, not everything needs to be an axiom: We've left some things out. *)

Lemma Rplus_0_r : forall r : R, r + 0 = r.
Proof.
  (* WORKINCLASS *)
Admitted.

Lemma Rplus_opp_l : forall r, -r + r = 0.
Proof.
  (* WORKINCLASS *)
Admitted.

Lemma Ropp_0 : -0 = 0.
  (* WORKINCLASS *)
Admitted.
  
(** Multiplicative axioms *)

Axiom Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1.

Axiom Rmult_assoc : forall r1 r2 r3:R, r1 * r2 * r3 = r1 * (r2 * r3).

Axiom Rinv_l : forall r:R, r <> 0 -> / r * r = 1.

Axiom Rmult_1_l : forall r:R, 1 * r = r.

Axiom Rmult_plus_distr_l : forall r1 r2 r3:R, r1 * (r2 + r3) = r1 * r2 + r1 * r3.

Lemma Ropp_mult_distr_l : forall r1 r2, - (r1 * r2) = - r1 * r2.
Proof.
  (* WORKINCLASS *)
Admitted.

Lemma Rmult_0_r : forall r, r * 0 = 0.
Proof.
  (* WORKINCLASS *)
  Admitted.
(* /WORKINCLASS *)

(** The last core axiom of the reals: *)

Definition is_upper_bound (E:R -> Prop) (m:R) := forall x:R, E x -> x <= m.

Definition bound (E:R -> Prop) := exists m : R, is_upper_bound E m.

Definition is_lub (E:R -> Prop) (m:R) :=
  is_upper_bound E m /\ (forall b:R, is_upper_bound E b -> m <= b).

Axiom completeness :
  forall E:R -> Prop,
  bound E -> (exists x : R, E x) -> { m:R | is_lub E m }.