Avigad.Chapter2

Dependent Type Theory

Exercise 1

Define the function Do_Twice, as described in Section 2.4.

def Avigad.Chapter2.ex1.double (x : Nat) : Nat

Equations

• Avigad.Chapter2.ex1.double x = x + x

def Avigad.Chapter2.ex1.doTwice (f : Nat → Nat) (x : Nat) : Nat

Equations

• Avigad.Chapter2.ex1.doTwice f x = f (f x)

def Avigad.Chapter2.ex1.doTwiceTwice (f : (Nat → Nat) → Nat → Nat) (x : Nat → Nat) : Nat → Nat

Equations

• Avigad.Chapter2.ex1.doTwiceTwice f x = f (f x)

Exercise 2

Define the functions curry and uncurry, as described in Section 2.4.

def Avigad.Chapter2.ex2.curry {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α × β → γ) : α → β → γ

Equations

• Avigad.Chapter2.ex2.curry f α β = f (α, β)

def Avigad.Chapter2.ex2.uncurry {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → β → γ) : α × β → γ

Equations

• Avigad.Chapter2.ex2.uncurry f x = f x.fst x.snd

Exercise 3

Above, we used the example vec α n for vectors of elements of type α of length n. Declare a constant vec_add that could represent a function that adds two vectors of natural numbers of the same length, and a constant vec_reverse that can represent a function that reverses its argument. Use implicit arguments for parameters that can be inferred. Declare some variables nd check some expressions involving the constants that you have declared.

axiom Avigad.Chapter2.ex3.vec : Type u → Nat → Type u

axiom Avigad.Chapter2.ex3.vec.empty (α : Type u) : Avigad.Chapter2.ex3.vec α 0

axiom Avigad.Chapter2.ex3.vec.cons (α : Type u) (n : Nat) : α → Avigad.Chapter2.ex3.vec α n → Avigad.Chapter2.ex3.vec α (n + 1)

axiom Avigad.Chapter2.ex3.vec.append (α : Type u) (n : Nat) (m : Nat) : Avigad.Chapter2.ex3.vec α m → Avigad.Chapter2.ex3.vec α n → Avigad.Chapter2.ex3.vec α (n + m)

axiom Avigad.Chapter2.ex3.vec.add {α : Type u} {n : Nat} : Avigad.Chapter2.ex3.vec α n → Avigad.Chapter2.ex3.vec α n → Avigad.Chapter2.ex3.vec α n

axiom Avigad.Chapter2.ex3.vec.reverse {α : Type u} {n : Nat} : Avigad.Chapter2.ex3.vec α n → Avigad.Chapter2.ex3.vec α n

Exercise 4

Similarly, declare a constant matrix so that matrix α m n could represent the type of m by n matrices. Declare some constants to represent functions on this type, such as matrix addition and multiplication, and (using vec) multiplication of a matrix by a vector. Once again, declare some variables and check some expressions involving the constants that you have declared.

axiom Avigad.Chapter2.ex4.matrix : Type u → Nat → Nat → Type u

axiom Avigad.Chapter2.ex4.matrix.add {α : Type u} {m : Nat} {n : Nat} : Avigad.Chapter2.ex4.matrix α m n → Avigad.Chapter2.ex4.matrix α m n → Avigad.Chapter2.ex4.matrix α m n

axiom Avigad.Chapter2.ex4.matrix.mul {α : Type u} {m : Nat} {n : Nat} {p : Nat} : Avigad.Chapter2.ex4.matrix α m n → Avigad.Chapter2.ex4.matrix α n p → Avigad.Chapter2.ex4.matrix α m p

axiom Avigad.Chapter2.ex4.matrix.app {α : Type u} {m : Nat} {n : Nat} : Avigad.Chapter2.ex4.matrix α m n → Avigad.Chapter2.ex3.vec α n → Avigad.Chapter2.ex3.vec α m