Documentation

Bookshelf.Avigad.Chapter_7

Avigad.Chapter7 #

Inductive Types

Exercise 1 #

Try defining other operations on the natural numbers, such as multiplication, the predecessor function (with pred 0 = 0), truncated subtraction (with n - m = 0 when m is greater than or equal to n), and exponentiation. Then try proving some of their basic properties, building on the theorems we have already proved.

Since many of these are already defined in Lean’s core library, you should work within a namespace named hide, or something like that, in order to avoid name clashes.

source
inductive Avigad.Chapter7.ex1.Nat :
Type
Instances For
    source
    def Avigad.Chapter7.ex1.Nat.add (m : Avigad.Chapter7.ex1.Nat) (n : Avigad.Chapter7.ex1.Nat) :
    Avigad.Chapter7.ex1.Nat
    Equations
    Instances For
      source
      instance Avigad.Chapter7.ex1.Nat.instAddNat :
      Add Avigad.Chapter7.ex1.Nat
      Equations
      source
      theorem Avigad.Chapter7.ex1.Nat.add_zero (m : Avigad.Chapter7.ex1.Nat) :
      m + Avigad.Chapter7.ex1.Nat.zero = m
      source
      theorem Avigad.Chapter7.ex1.Nat.add_succ (m : Avigad.Chapter7.ex1.Nat) (n : Avigad.Chapter7.ex1.Nat) :
      m + Avigad.Chapter7.ex1.Nat.succ n = Avigad.Chapter7.ex1.Nat.succ (m + n)
      source
      theorem Avigad.Chapter7.ex1.Nat.zero_add (n : Avigad.Chapter7.ex1.Nat) :
      Avigad.Chapter7.ex1.Nat.zero + n = n
      source
      def Avigad.Chapter7.ex1.Nat.mul (m : Avigad.Chapter7.ex1.Nat) (n : Avigad.Chapter7.ex1.Nat) :
      Avigad.Chapter7.ex1.Nat
      Equations
      Instances For
        source
        def Avigad.Chapter7.ex1.Nat.pred (n : Avigad.Chapter7.ex1.Nat) :
        Avigad.Chapter7.ex1.Nat
        Equations
        Instances For
          source
          def Avigad.Chapter7.ex1.Nat.sub (m : Avigad.Chapter7.ex1.Nat) (n : Avigad.Chapter7.ex1.Nat) :
          Avigad.Chapter7.ex1.Nat
          Equations
          Instances For
            source
            def Avigad.Chapter7.ex1.Nat.exp (m : Avigad.Chapter7.ex1.Nat) (n : Avigad.Chapter7.ex1.Nat) :
            Avigad.Chapter7.ex1.Nat
            Equations
            Instances For

              Exercise 2 #

              Define some operations on lists, like a length function or the reverse function. Prove some properties, such as the following:

              a. length (s ++ t) = length s + length t

              b. length (reverse t) = length t

              c. reverse (reverse t) = t

              source
              theorem Avigad.Chapter7.ex2.length_sum {α : Type u_1} (s : List α) (t : List α) :
              List.length (s ++ t) = List.length s + List.length t
              source
              theorem Avigad.Chapter7.ex2.length_inject_anywhere {α : Type u_1} (x : α) (as : List α) (bs : List α) :
              List.length (as ++ [x] ++ bs) = List.length as + List.length bs + 1
              source
              theorem Avigad.Chapter7.ex2.list_reverse_aux_append {α : Type u_1} (as : List α) (bs : List α) :
              List.reverseAux as bs = List.reverse as ++ bs
              source
              theorem Avigad.Chapter7.ex2.length_reverse {α : Type u_1} (t : List α) :
              List.length (List.reverse t) = List.length t
              source
              theorem Avigad.Chapter7.ex2.reverse_reverse_aux {α : Type u_1} (as : List α) (bs : List α) :
              List.reverse (as ++ bs) = List.reverse bs ++ List.reverse as
              source
              theorem Avigad.Chapter7.ex2.reverse_reverse {α : Type u_1} (t : List α) :
              List.reverse (List.reverse t) = t

              Exercise 3 #

              Define an inductive data type consisting of terms built up from the following constructors:

              • const n, a constant denoting the natural number n

              • var n, a variable, numbered n

              • plus s t, denoting the sum of s and t

              • times s t, denoting the product of s and t

              Recursively define a function that evaluates any such term with respect to an assignment of values to the variables.

              source
              inductive Avigad.Chapter7.ex3.Foo :
              Type
              Instances For
                source
                def Avigad.Chapter7.ex3.value_at :
                Nat → List Nat → Nat
                Equations
                Instances For
                  source
                  def Avigad.Chapter7.ex3.eval_foo :
                  Avigad.Chapter7.ex3.Foo → List Nat → Nat
                  Equations
                  Instances For