Skip to content

Instantly share code, notes, and snippets.

@larsr

larsr/dotnineninenine_is_one

Last active November 22, 2019 10:16
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save larsr/8695938f4622b7ed2b09e1662e18ffa9 to your computer and use it in GitHub Desktop.
Save larsr/8695938f4622b7ed2b09e1662e18ffa9 to your computer and use it in GitHub Desktop.
Download ZIP
Coq proof that 0.9999999999 = 1
Raw
dotnineninenine_is_one
(* Proof that 0.9999999999... = 1 *)
Require Import Reals.
From Coquelicot Require Import Coquelicot.
Require Import Psatz.
Definition nine i := (9/10)*(1/10)^i.
Example e1: sum_n nine 3 = 9/10 + 9/100 + 9/1000 + 9/10000.
unfold nine.
repeat rewrite sum_Sn, ?sum_O.
unfold plus; simpl; lra.
Qed.
Lemma nines: Series nine = 1.
unfold nine.
rewrite Series_scal_l.
enough ( Series (pow (1 / 10)) = 10 / 9) by lra.
apply is_series_unique.
evar (e:R).
replace (10/9) with e.
apply is_series_geom.
unfold Rabs; case Rcase_abs; lra.
unfold e; lra.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment