Structures: Square root of a natural number

We have seen the following types:

• Universes
• Function types
• Dependent function types

There is only one other basic type construction in Lean: Inductive Types and their generalization, Indexed Inductive Types.

We start with a special class of inductive types: Structures. We will also see how to combine data and proofs and to prove with tactics.

Square root of a natural number

structure NatSqrt (n : Nat) : Type

• val : Nat
• isSqrt : self.val * self.val = n

def sqrt4 : NatSqrt 4

Equations

• sqrt4 = { val := 2, isSqrt := sqrt4.proof_1 }

def sqrt3 : NatSqrt 9

Equations

• sqrt3 = { val := 3, isSqrt := sqrt3.proof_1 }

def sqrt9 : NatSqrt 9

Equations

• sqrt9 = { val := 3, isSqrt := sqrt9.proof_1 }

A lemma

We will define a function that gives the square root of a product of two natural numbers. We will first prove a lemma that will be useful in the definition. This will be proved using tactics.

Note that all the rw tactics can be written as a single tactic with a list of rewrites.

theorem sqrt_mul (a b : Nat) : a * a * (b * b) = a * b * (a * b)

def sqrt_prod {m n : Nat} (sqm : NatSqrt m) (sqn : NatSqrt n) : NatSqrt (m * n)

Equations

• sqrt_prod sqm sqn = { val := sqm.val * sqn.val, isSqrt := ⋯ }