/-! # Avigad.Chapter2

Dependent Type Theory
-/

/-! ### Exercise 1

Define the function `Do_Twice`, as described in Section 2.4.
-/

namespace 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 Avigad.Chapter2