Library s3_reals

Real numbers

How to define real numbers?

Wikipedia:

The discovery of a suitably rigorous definition of the real numbers — indeed, the realization that a better definition was needed — was one of the most important developments of 19th century mathematics. The currently standard axiomatic definition is that real numbers form the unique Archimedean complete totally ordered field (R,+,·,<), up to isomorphism,1 whereas popular constructive definitions of real numbers include declaring them as equivalence classes of Cauchy sequences of rational numbers, Dedekind cuts, or certain infinite "decimal representations", together with precise interpretations for the arithmetic operations and the order relation. These definitions are equivalent in the realm of classical mathematics.

In Coq, the standard library proposes the axiomatic approach

Require Import Reals.

Check R.
Check Rplus.
Check Rmult.
Check Rgt.

be careful about notations

Check fun x ⇒ x + x.

Open Scope R_scope.

Check fun x ⇒ x + x.

Check fun x ⇒ (x + x)%nat.

Check fun x ⇒ (x + x)%R.

real numbers form a ring

Check R. Check R0. Check R1. Check Rplus. Check Ropp. Print Rminus. Check Rmult. Print Rlt.

four axioms about addition

Check Rplus_comm. Check Rplus_assoc. Check Rplus_opp_l. Check Rplus_0_l.
Fact Rplus_0_r r : r + 0 = r.
Proof.
now rewrite Rplus_comm, Rplus_0_l.
Qed.

four axioms for multiplication

Check Rmult_comm. Check Rmult_assoc. Check Rmult_1_l. Check Rmult_plus_distr_l.

non-triviality

Check R1_neq_R0.

the tactic ring takes care of the ring structure

Fact ex1 x y : x × x - y × y = (x + y) × (x - y).
Proof. ring. Qed.

Fact ex2 : 121 = 11 × 11.
Proof. ring. Qed.

Fact ex3 : ∀ x y, (x = y) ∨ (x = -y) → x × x = y × y.
Proof.
intros ? ? [ → | → ]; ring.
Qed.

be careful about notations, again

Check 6.
Check 3+3.

Eval simpl in 3+3.
Eval compute in 6.
Eval compute in 3+3.
Eval compute in 11.

Eval compute in 3.1416.

injecting natural numbers into R

Print INR.

Compute INR 11.
Check plus_INR.

injecting relative numbers into R

Print IZR.

Compute IZR (-11).
Check plus_IZR.

Goal IZR(-42) = -42.
Proof.
reflexivity. Qed.

Goal INR 42 = 42.
Proof.
simpl. ring.
Qed.

real numbers form a field

Check Rinv. Check Rinv_l. Print Rdiv.

the tactic field proves automatically field equalities

Fact ex4 x y : x ≠ 0 → y ≠ 0 → 1 / x + 1 / y = (x + y) / (x × y).
Proof. intros. field. tauto. Qed.

Fact ex5 : 121 / 11 = 11.
Proof. intros. field. Qed.

Fact ex6 : ∀ x y, x ≠ y → (x × x - y × y) / (x - y) = y + x.
Proof.
  intros x y E. field.
  Search (_ - _ ≠ 0).
  now apply Rminus_eq_contra.
Qed.

total order on reals

Check Rlt. Print Rgt. Print Rle. Print Rge.
Check Rlt_asym. Check Rlt_trans. Check Rplus_lt_compat_l. Check Rmult_lt_compat_l.

tactic lra solves systems of linear inequations

Require Import Psatz.

Fact ex7 x : 0 < x → 2 × x - 1 < 6 × x + 7.
Proof. lra. Qed.

Fact ex8 : 12 / 15 < 37 / 45.
Proof. lra. Qed.

Check total_order_T. Check Rlt_le_dec.

defining new functions

Definition Rmax2 (x y: R): R :=
if Rlt_le_dec x y then y else x.

proving facts about them

Lemma Rmax2_comm x y : Rmax2 x y = Rmax2 y x.
Proof.
  unfold Rmax2.
  case Rlt_le_dec; intro;
    case Rlt_le_dec; intro;
      lra.
Qed.

exercise: define a function returning the maximal element amongs three numbers

Definition Rmax3 x y z := Rmax2 (Rmax2 x y) z.

Lemma Rmax3_copy x y: Rmax3 x y x = Rmax2 x y.
Proof.
unfold Rmax3, Rmax2.
case Rlt_le_dec; case Rlt_le_dec; lra.
Qed.

one can test two real numbers for equality

Check Req_dec.

and R is integral

Check Rmult_integral.

this is actually derivable from the axioms listed above

Lemma Rmult_integral' (x y: R): x×y = 0 → x=0 ∨ y=0.
Proof.
  intro H.
  destruct (Req_dec x 0). tauto.
  destruct (Req_dec y 0). tauto.
  destruct R1_neq_R0.
  transitivity (x×y/x/y). field; tauto.
  rewrite H. field. tauto.
Qed.

Fact ex9 x : x ^ 2 - 2 × x + 1 = 0 ↔ x = 1.
Proof.
  split; intros H.
  - assert (H': (x-1)*(x-1) = 0) by lra.
    apply Rmult_integral in H'. lra.
  - rewrite H; ring.
Qed.

absolute value

Check Rabs.
Print Rabs.
Check Rcase_abs.

the tactic split_Rabs removes all absolute values appearing in the goal, generating all possible cases

Fact ex10 x y z : Rabs (x - z) ≤ Rabs (x - y) + Rabs (y - z).
Proof. split_Rabs. lra. lra. lra. lra. lra. lra. lra. lra. Qed.

Goal ∀ x y, x × x = y × y ↔ Rabs x = Rabs y.
Proof.
  split.
  - intro H. assert (H':(x+y)*(x-y) = 0) by lra.
    apply Rmult_integral in H'.
    split_Rabs; lra.
  - split_Rabs; try (subst; lra).
    replace x with y; lra.
Qed.

R is archimedian

Check up. Check archimed.

R is complete

Check is_upper_bound. Print is_upper_bound.
Check bound. Print bound.
Check is_lub. Print is_lub.
Check completeness.

from the above 24 axioms, one can construct all usual functions

Check IVT. Check cos_plus.

Looking for lemmas in the loaded libraries

Search sqrt.
Search sqrt (_ × _).
Search (0 < _) (_ × _).
Search (0 < _) (_ × _) outside Fourier_util.
SearchPattern (0 < _ × _).

** Summary

although we cannot compute with them, we can play with real numbers.
several automatic tactics : ring for ring equations field for field equations lra for linear systems of inequations split_Rabs to do case analyses on absolute values
case Re_dec to perform case analyses
unfold def to unfold a definition
set (x := ....) to name a subterm
assert (H : ....) to introduce a lemma.
Search, SearchPattern to look for lemmas in the libraries.

Exercise: show that given two real numbers x,y such that 0 < x < y, if A is their arithmetic mean and G their geometric mean, then x < G < A < y

Lemma lt_sqrt_l x y: 0<=x → 0<=y → sqrt x < y ↔ x < y^2.
Proof.
  intros Hx Hy. split; intro H.
  apply sqrt_lt_0_alt. rewrite sqrt_pow2; lra.
  apply Rlt_le_trans with (sqrt (y^2)).
  apply sqrt_lt_1; lra.
  rewrite sqrt_pow2; lra.
Qed.

Lemma lt_sqrt_r x y: 0<=x → 0<=y → x < sqrt y ↔ x^2 < y.
Proof.
  intros Hx Hy. split; intro H.
  apply sqrt_lt_0_alt. rewrite sqrt_pow2; lra.
  apply Rle_lt_trans with (sqrt (x^2)).
  rewrite sqrt_pow2; lra.
  apply sqrt_lt_1. apply pow2_ge_0. lra. assumption.
Qed.

Goal ∀ x y, 0<x<y → x < sqrt(x×y).
Proof.
  intros. apply lt_sqrt_r.
  lra.
   apply Rmult_le_pos; lra.
  apply Rmult_lt_compat_l; lra.
Qed.

Goal ∀ x y, 0<x<y → sqrt(x×y) < (x+y)/2 .
Proof.
  intros. apply lt_sqrt_l.
   apply Rmult_le_pos; lra.
   lra.
  rewrite <-Rlt_0_minus.
  replace (_ - _) with (((y-x)/2)^2) by field.
  apply Rmult_lt_0_compat; lra.
Qed.

Goal ∀ x y, 0<x<y → (x+y)/2 < y.
Proof. intros. lra. Qed.

This page has been generated by coqdoc