Skip to content

stylistic fixes #1

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

stylistic fixes #1

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f0f6569
stylistic fixes
clayrat Sep 7, 2022
85f1908
whitespace
clayrat Sep 7, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
209 changes: 104 additions & 105 deletions lecture1.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,27 +7,27 @@


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

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.
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, real numbers are axiomatised
(*
In Coq, real numbers are axiomatised
*)

Require Import Reals.
Expand All @@ -40,8 +40,8 @@ Check Rmult.
Check Rgt.

(*
We want to use the usual notations but the default interpretion is the one
for natural numbers nat
We want to use the usual notations but the default interpretion is the one
for natural numbers (nat)
*)

Check fun x => x + x.
Expand All @@ -61,19 +61,19 @@ Check fun x => (x + x)%R.
(******************************************************************************)

Check R. (* the reals *)
Check R0. (* zero *)
Check R1. (* one *)
Check R0. (* zero *)
Check R1. (* one *)
Check Rplus. (* addition *)
Check Ropp. (* opposite *)
Print Rminus. (* subtraction *)
Check Rmult. (* multiplication *)

(* Addition 4 axioms *)

Check Rplus_comm. (* commutativity *)
Check Rplus_assoc. (* associativity *)
Check Rplus_opp_l. (* right inverse *)
Check Rplus_0_l. (* left neutral element *)
Check Rplus_comm. (* commutativity *)
Check Rplus_assoc. (* associativity *)
Check Rplus_opp_l. (* right inverse *)
Check Rplus_0_l. (* left neutral element *)

(* We can already derive some facts *)

Expand All @@ -86,12 +86,12 @@ Qed.

(* Multiplication 4 axioms *)

Check Rmult_comm. (* commutativity *)
Check Rmult_assoc. (* associativity *)
Check Rmult_1_l. (* left neutral element *)
Check Rmult_plus_distr_l. (* right distributivity *)
Check Rmult_comm. (* commutativity *)
Check Rmult_assoc. (* associativity *)
Check Rmult_1_l. (* left neutral element *)
Check Rmult_plus_distr_l. (* right distributivity *)

(* Non triviality 1 axiome *)
(* Non triviality 1 axiom *)

Check R1_neq_R0.

Expand All @@ -104,7 +104,7 @@ Fact ex2 : 121 = 11 * 11.
Proof. ring. Qed.


(* Easy exercise
(* Easy exercise

Fact ex3 : forall x y, (x = y) \/ (x = -y) -> x * x = y * y.
Proof.
Expand Down Expand Up @@ -138,12 +138,12 @@ Print IZR.
Compute IZR (-11).
Check plus_IZR.

(*
Easy exercise: Prove that INR 42 = 42.
(*
Easy exercise: Prove that INR 42 = 42.
*)

(*
Easy exercise: Prove that IZR(-42) = -42.
(*
Easy exercise: Prove that IZR(-42) = -42.
*)

(******************************************************************************)
Expand All @@ -162,57 +162,57 @@ Proof. intros. field. auto. Qed.
Fact ex5 : 121 / 11 = 11.
Proof. intros. field. Qed.

(*
Exercise
Fact ex6 : forall x y, x <> y -> (x * x - y * y) / (x - y) = y + x.
Proof.
....
Qed.
Hint : given a goal
H : ~ a
-----------------
~ b
the tactic contradict returns the contrapose of a goal
contradict H
H : b
-----------------
a
(*
Exercise

Fact ex6 : forall x y, x <> y -> (x * x - y * y) / (x - y) = y + x.
Proof.
....
Qed.

Hint : given a goal

H : ~ a
-----------------
~ b

the tactic "contradict" returns the contrapose of a goal

contradict H

H : b
-----------------
a


*)

(******************************************************************************)
(* Ordering *)
(******************************************************************************)

Check Rlt. (* strictly smaller *)
Print Rgt. (* strictly greater *)
Print Rle. (* smaller or equal *)
Print Rge. (* greater or equal *)
Check Rlt. (* strictly smaller *)
Print Rgt. (* strictly greater *)
Print Rle. (* smaller or equal *)
Print Rge. (* greater or equal *)

Check Rlt_asym. (* antisymmetry *)
Check Rlt_trans. (* transitivity *)
Check Rplus_lt_compat_l. (* left compatibility *)
(* with addition *)
Check Rmult_lt_compat_l. (* left compatibility *)
(* with multiplication *)
Check Rlt_asym. (* antisymmetry *)
Check Rlt_trans. (* transitivity *)
Check Rplus_lt_compat_l. (* left compatibility *)
(* with addition *)
Check Rmult_lt_compat_l. (* left compatibility *)
(* with multiplication *)


(* The tactic "lra" let us prove linear inequalities *)
(* The tactic "lra" lets us prove linear inequalities *)

Require Import Psatz.

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

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

Check total_order_T. (* The order is total *)
Print sumbool.
Expand All @@ -233,27 +233,27 @@ Print Rmax2.
Lemma Rmax2_comm x y : Rmax2 x y = Rmax2 y x.
Proof.
unfold Rmax2.
destruct (total_order_T x y) as [[xLy |xEy] | xGy];
destruct (total_order_T x y) as [[xLy |xEy] | xGy];
destruct (total_order_T y x) as [[yLx |yEx] | yGx]; lra.
Qed.

(*
Exercise : define Rmax3 that takes 3 numbers and returns the greates of
three
(*
Exercise : define Rmax3 that takes 3 numbers and returns the greatest of
three
*)

(* We can test equality on real number. Propositional version *)
(* We can test equality on real numbers. Propositional version *)
Check Req_dec.

(*
Exercise : Build a computation version of Req_dec
(*
Exercise : Build a computational version of Req_dec
*)

(* Integrality of R can be proved *)
Check Rmult_integral.

(*
Exercise : Reprove integrality without using Rmult_integral
(*
Exercise : Reprove integrality without using Rmult_integral
*)

Fact ex9 x : x ^ 2 - 2 * x + 1 = 0 <-> x = 1.
Expand All @@ -273,35 +273,35 @@ Check Rabs.
Check Rcase_abs.
Print Rabs.

(*
The tactic split_Rabs let us remove the absolute value by generating
all the possible cases
(*
The tactic "split_Rabs" lets us remove the absolute value by generating
all the 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.

(*
Exercise : Prove that (x * x = y * y) is equivalent to (Rabs x = Rabs y)
(*
Exercise : Prove that (x * x = y * y) is equivalent to (Rabs x = Rabs y)
*)

(* Property of being archimedian *)
(* Property of being archimedean *)

Check up. (* an uppper bound *)
Check archimed. (* the characteristic property *)

(* Completness *)
(* Completeness *)

Check is_upper_bound. (* to be an upper bound *)
Print is_upper_bound.
Check bound. (* to be bounded *)
Print bound.
Check is_lub. (* to be the smallest bound *)
Check is_lub. (* to be the least bound *)
Print is_lub.
Check completeness. (* completness *)
Check completeness. (* completeness *)


(* From this 24 axioms we can build the usual functions *)
(* From these 24 axioms we can build the usual functions *)

Check IVT. (* intermediate value theorem *)
Check cos_plus. (* some trigonometry *)
Expand All @@ -318,24 +318,23 @@ Search _ (0 < _) (_ * _) outside Fourier_util. (* without fourier *)

SearchPattern (0 < _ * _). (* filtering the conclusion *)

(*
Resume
- we can play formally with the reals
- two automatic tactics
field to prove equalities
lra to prove linear inequalities
- split_Rabs to remove the absolute values
- set (x := ....) to name a subterm
- assert (H : ....) to introduce an intermediate result
- Search, SearchPattern to search in the library
(*
Resume
- we can play formally with the reals
- two automatic tactics
field to prove equalities
lra to prove linear inequalities
- split_Rabs to remove the absolute values
- set (x := ....) to name a subterm
- assert (H : ....) to introduce an intermediate result
- Search, SearchPattern to search in the library
*)

(*
Exercise,
given two real numbers x and y such that 0 < x < y, show that
if A is the arithmetic mean and G the geometric one then we have
x < G < A < y
(*
Exercise,
given two real numbers x and y such that 0 < x < y, show that
if A is the arithmetic mean and G the geometric one then we have
x < G < A < y
*)

End Lecture1.

Loading