feat(algebra/continued_fractions): add termination iff rat lemmas (#4867

)

### What

Show that the computation of a continued fraction terminates if and only if we compute the continued fraction of a rational number.

### How

1. Show that every intermediate operation involved in the computation of a continued fraction returns a value that has a rational counterpart. This then shows that a terminating continued fraction corresponds to a rational value.
2. Show that the operations involved in the computation of a continued fraction for rational numbers only return results that can be lifted to the result of the same operations done on an equal value in a suitable linear ordered, archimedean field with a floor function.
3. Show that the continued fraction of a rational number terminates.
4. Set up the needed coercions to express the results above starting from [here](https://github.com/leanprover-community/mathlib/compare/kappelmann_termination_iff_rat?expand=1#diff-1dbcf8473152b2d8fca024352bd899af37669b8af18792262c2d5d6f31148971R129). I did not know where to put these lemmas. Please let me know your opinion.
4. Extract 4 auxiliary lemmas that are not specific to continued fraction but more generally about rational numbers, integers, and natural numbers starting from [here](https://github.com/leanprover-community/mathlib/compare/kappelmann_termination_iff_rat?expand=1#diff-1dbcf8473152b2d8fca024352bd899af37669b8af18792262c2d5d6f31148971R28). Again, I did not know where to put these. Please let me know your opinion.

Co-authored-by: Kevin Kappelmann <kappelmann@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

src/algebra/continued_fractions/basic.lean

@@ -49,18 +49,25 @@ protected structure generalized_continued_fraction.pair := (a : α) (b : α)
 namespace generalized_continued_fraction.pair
 open generalized_continued_fraction as gcf
 
-/-- Make a gcf.pair printable. -/
+variable {α}
+
+/-- Make a `gcf.pair` printable. -/
 instance [has_repr α] : has_repr (gcf.pair α) :=
 ⟨λ p, "(a : " ++ (repr p.a) ++ ", b : " ++ (repr p.b) ++ ")"⟩
 
+/-- Maps a function `f` on both components of a given pair. -/
+def map {β : Type*} (f : α → β) (gp : gcf.pair α) : gcf.pair β :=
+⟨f gp.a, f gp.b⟩
+
 section coe
 /-! Interlude: define some expected coercions. -/
-/- Fix another type `β` and assume `α` can be converted to `β`. -/
-variables {α} {β : Type*} [has_coe α β]
+/- Fix another type `β` which we will convert to. -/
+variables {β : Type*} [has_coe α β]
 
 /-- Coerce a pair by elementwise coercion. -/
-instance has_coe_to_generalized_continued_fraction_pair : has_coe (gcf.pair α) (gcf.pair β) :=
-⟨λ ⟨a, b⟩, ⟨(a : β), (b : β)⟩⟩
+instance has_coe_to_generalized_continued_fraction_pair :
+  has_coe (gcf.pair α) (gcf.pair β) :=
+⟨map coe⟩
 
 @[simp, norm_cast]
 lemma coe_to_generalized_continued_fraction_pair {a b : α} :
@@ -70,6 +77,8 @@ rfl
 end coe
 end generalized_continued_fraction.pair
 
+variable (α)
+
 /--
 A *generalised continued fraction* (gcf) is a potentially infinite expression of the form
 
@@ -120,22 +129,17 @@ def terminates (g : gcf α) : Prop := g.s.terminates
 
 section coe
 /-! Interlude: define some expected coercions. -/
--- Fix another type `β` and assume `α` can be converted to `β`.
+/- Fix another type `β` which we will convert to. -/
 variables {β : Type*} [has_coe α β]
 
-/-- Coerce a sequence by elementwise coercion. -/
-def seq.coe_to_seq : has_coe (seq α) (seq β) := ⟨seq.map (λ a, (a : β))⟩
-
-local attribute [instance] seq.coe_to_seq
-
 /-- Coerce a gcf by elementwise coercion. -/
 instance has_coe_to_generalized_continued_fraction : has_coe (gcf α) (gcf β) :=
-⟨λ ⟨h, s⟩, ⟨(h : β), (s : seq $ gcf.pair β)⟩⟩
+⟨λ g, ⟨(g.h : β), (g.s.map coe : seq $ gcf.pair β)⟩⟩
 
 @[simp, norm_cast]
 lemma coe_to_generalized_continued_fraction {g : gcf α} :
-  (↑(g : gcf α) : gcf β) = ⟨(g.h : β), (g.s : seq $ gcf.pair β)⟩ :=
-by { cases g, refl }
+  (↑(g : gcf α) : gcf β) = ⟨(g.h : β), (g.s.map coe : seq $ gcf.pair β)⟩ :=
+rfl
 
 end coe
 end generalized_continued_fraction

src/algebra/continued_fractions/computation/basic.lean

@@ -72,6 +72,8 @@ We collect an integer part `b = ⌊v⌋` and fractional part `fr = v - ⌊v⌋`
 -/
 structure int_fract_pair := (b : ℤ) (fr : K)
 
+variable {K}
+
 /-! Interlude: define some expected coercions and instances. -/
 namespace int_fract_pair
 
@@ -81,17 +83,20 @@ instance [has_repr K] : has_repr (int_fract_pair K) :=
 
 instance inhabited [inhabited K] : inhabited (int_fract_pair K) := ⟨⟨0, (default _)⟩⟩
 
-variable {K}
+/--
+Maps a function `f` on the fractional components of a given pair.
+-/
+def mapFr {β : Type*} (f : K → β) (gp : int_fract_pair K) : int_fract_pair β :=
+⟨gp.b, f gp.fr⟩
 
 section coe
 /-! Interlude: define some expected coercions. -/
-/- Fix another type `β` and assume `K` can be converted to `β`. -/
+/- Fix another type `β` which we will convert to. -/
 variables {β : Type*} [has_coe K β]
 
 /-- Coerce a pair by coercing the fractional component. -/
 instance has_coe_to_int_fract_pair : has_coe (int_fract_pair K) (int_fract_pair β) :=
-⟨λ ⟨b, fr⟩, ⟨b, (fr : β)⟩⟩
-
+⟨mapFr coe⟩
 
 @[simp, norm_cast]
 lemma coe_to_int_fract_pair {b : ℤ} {fr : K} :
@@ -153,16 +158,14 @@ protected def seq1 (v : K) : seq1 $ int_fract_pair K :=
 
 end int_fract_pair
 
-variable {K}
-
 /--
 Returns the `generalized_continued_fraction` of a value. In fact, the returned gcf is also
 a `continued_fraction` that terminates if and only if `v` is rational (those proofs will be
 added in a future commit).
 
 The continued fraction representation of `v` is given by `[⌊v⌋; b₀, b₁, b₂,...]`, where
 `[b₀; b₁, b₂,...]` recursively is the continued fraction representation of `1 / (v − ⌊v⌋)`. This
-process stops when the fractional part `v- ⌊v⌋` hits 0 at some step.
+process stops when the fractional part `v - ⌊v⌋` hits 0 at some step.
 
 The implementation uses `int_fract_pair.stream` to obtain the partial denominators of the continued
 fraction. Refer to said function for more details about the computation process.