GCD: Termination example

As an example of proving termination, we define the function hcf that computes the greatest common divisor of two natural numbers. We prove that hcf terminates by showing that the argument decreases in each recursive call.

@[irreducible]

def hcfSimple (a b : ℕ) : ℕ

Simple version of the GCD function

Equations

• hcfSimple a b = if b = 0 then a else if a < b then hcfSimple b a else hcfSimple (a - b) b

@[irreducible]

def hcf (a b : ℕ) : ℕ

The function hcf computes the greatest common divisor of two natural numbers. We have to prove that it terminates.

Equations

• hcf a b = if h : b = 0 then a else if h' : a < b then hcf b a else let_fun h₁ := ⋯; let_fun this := ⋯; let_fun this := ⋯; hcf (a % b) b

We cannot always make partial definitions.

partial def not_wrong {α : Type} [Nonempty α] (x : ℕ) : α

A recursively defined function that loops forever but is a legal definition as its codomain is empty.

@[irreducible]

theorem hcf_dvd (a b : ℕ) : hcf a b ∣ a ∧ hcf a b ∣ b

structure BezoutPair (a b : ℕ) : Type

• x : ℤ
• y : ℤ
• eqn : self.x * ↑a + self.y * ↑b = ↑(hcf a b)

@[irreducible]

def bezoutPair (a b : ℕ) : BezoutPair a b

Equations

• One or more equations did not get rendered due to their size.