bookshelf/Exercises/Avigad/Chapter2.lean

109 lines
2.7 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

/-! # Exercises.Avigad.Chapter2
Dependent Type Theory
-/
/-! #### Exercise 1
Define the function `Do_Twice`, as described in Section 2.4.
-/
namespace Exercises.Avigad.Chapter2
namespace ex1
def double (x : Nat) := x + x
def doTwice (f : Nat → Nat) (x : Nat) : Nat := f (f x)
def doTwiceTwice (f : (Nat → Nat) → (Nat → Nat)) (x : Nat → Nat) := f (f x)
#reduce doTwiceTwice doTwice double 2
end ex1
/-! #### Exercise 2
Define the functions `curry` and `uncurry`, as described in Section 2.4.
-/
namespace ex2
def curry (f : α × β → γ) : (α → β → γ) :=
fun α β => f (α, β)
def uncurry (f : α → β → γ) : (α × β → γ) :=
fun x => f x.1 x.2
end ex2
/-! #### 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.
-/
namespace ex3
universe u
axiom vec : Type u → Nat → Type u
namespace vec
axiom empty : ∀ (α : Type u), vec α 0
axiom cons : ∀ (α : Type u) (n : Nat), α → vec α n → vec α (n + 1)
axiom append : ∀ (α : Type u) (n m : Nat), vec α m → vec α n → vec α (n + m)
axiom add : ∀ {α : Type u} {n : Nat}, vec α n → vec α n → vec α n
axiom reverse : ∀ {α : Type u} {n : Nat}, vec α n → vec α n
end vec
-- Check results.
variable (a b : vec Prop 1)
variable (c d : vec Prop 2)
#check vec.add a b
-- #check vec.add a c
#check vec.reverse a
end ex3
/-! #### 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.
-/
namespace ex4
universe u
axiom matrix : Type u → Nat → Nat → Type u
namespace matrix
axiom add : ∀ {α : Type u} {m n : Nat},
matrix α m n → matrix α m n → matrix α m n
axiom mul : ∀ {α : Type u} {m n p : Nat},
matrix α m n → matrix α n p → matrix α m p
axiom app : ∀ {α : Type u} {m n : Nat},
matrix α m n → ex3.vec α n → ex3.vec α m
end matrix
variable (a b : matrix Prop 5 7)
variable (c : matrix Prop 7 3)
variable (d : ex3.vec Prop 3)
#check matrix.add a b
-- #check matrix.add a c
#check matrix.mul a c
#check matrix.app c d
end ex4
end Exercises.Avigad.Chapter2