Exercises in Theorem Proving in Lean

Stream: new members

[Alex Zhang]

I am trying to do the following exercise from the book: As exercises, we encourage you to develop a notion of composition for partial functions from α to β and β to γ, and show that it behaves as expected.

open option

def my_comp {α β γ: Type*} (f: α → option β) (g: β → option γ): α → option γ :=
λ a, if f a = none then none
     else sorry

reports error

failed to synthesize type class instance for
α : Type ?,
β : Type ?,
γ : Type ?,
f : α → option β,
g : β → option γ,
a : α
⊢ decidable (f a = none)

How can I fix it?

[Kevin Buzzard]

You can either fix it by assuming that option beta has decidable equality (e.g. with open_locale classical) or you can do the problem the way you're expected to do it, without using if and instead splitting on the constructors, like the way addition is defined on the naturals: we don't write "a+b = if b = 0 then a else ...", we write

add : nat -> nat -> nat
| a 0 := a
| a (succ b) = ...

[Alex Zhang]

It seems that the first approach

open_locale classical

open option

def my_comp {α β γ: Type*} (f: α → option β) (g: β → option γ): α → option γ :=
λ a, if f a = none then none
     else sorry

gives me another error message: command expected for open_locale.

[Kevin Buzzard]

import tactic at the top

[Kevin Buzzard]

but let me stress that this is not the way you are expected to do the problem.

[Alex Zhang]

Yeah Yeah. I am doing the second way.

[Kevin Buzzard]

The difference with the two methods is that the "use the equation compiler" method will give you better definitional equalities; "x = if (true thing) then x else y" is not true by definition, it's true because of the theorem if_pos, whereas using the equation compiler you'll get more stuff true by definition (for example x + 0 = x is true for naturals by definition in Lean).

[Alex Zhang]

I am trying to do the exercise "We also encourage you to show that bool and nat are inhabited, that the product of two inhabited types is inhabited, and that the type of functions to an inhabited type is inhabited".
But I am not sure what "to show that bool and nat are inhabited" exactly asks me to do. Am I expected to write a theorem claiming this or something else?

[Rémy Degenne]

I would say that for the case of nat, the exercise is to replace that sorry:

example : inhabited nat := sorry

[Alex Zhang]

Is there a more concise way to prove the following?

example (α β : Type*) (a: inhabited α) (b: inhabited β)
: inhabited (prod α β) :=
inhabited.mk (inhabited.cases_on a (λ a,a), inhabited.cases_on b (λ b,b))

[Kevin Buzzard]

example (α β : Type*) [inhabited α] [inhabited β] :
  inhabited (α × β) :=
⟨⟨arbitrary α, arbitrary β⟩⟩

[Kevin Buzzard]

inhabited is a class, so the idiomatic thing to do would be to use rectangular brackets and not name the term of type inhabited alpha. Lean gives it some auto-generated name like _inst_37 or something, but more importantly it also adds it to the typeclass system, meaning that functions like arbitrary (which expect to find an inhabited instance using type class inference) will work.

The first pointy brackets is inhabited.mk, the second is prod.mk. This pointy bracket trick is why you see a lot less of mk functions than you might expect.

[Alex Zhang]

Thanks a lot!

[Kevin Buzzard]

example (α β : Type*) [inhabited α] [inhabited β] :
  inhabited (α × β) :=
⟨⟨default α, default β⟩⟩

I have no idea which is the best proof.

[Mario Carneiro]

example (α β : Type*) : ∀ [inhabited α] [inhabited β], inhabited (α × β)
| ⟨a⟩ ⟨b⟩ := ⟨(a, b)⟩

[Mario Carneiro]

kevin's is probably the best proof though

[Eric Wieser]

docs#default is usually better than docs#arbitrary, I think

[Alex Zhang]

Mario Carneiro said:

example (α β : Type*) : ∀ [inhabited α] [inhabited β], inhabited (α × β)
| ⟨a⟩ ⟨b⟩ := ⟨(a, b)⟩

Could you please explain the syntax of | ⟨a⟩ ⟨b⟩ ?

[Kevin Buzzard]

It's the same syntax as

def add : nat -> nat -> nat
| a 0 := a
|a (succ b) := succ (a + b)

It's explained in chapter 8 (IIRC) of #tpil

[Mario Carneiro]

it's a pattern match on inhabited A, which is an inductive type wrapping a single element of type A

[Alex Zhang]

''Under the hood, this definition is compiled down to a single inductive type with an index i in a two-valued type (such as bool), where i encodes which of even or odd is intended. ''

mutual inductive even, odd
with even : ℕ → Prop
| even_zero : even 0
| even_succ : ∀ n, odd n → even (n + 1)
with odd : ℕ → Prop
| odd_succ : ∀ n, even n → odd (n + 1)

What is the single inductive type it is compiled down to?

[Horatiu Cheval]

I think the output of #print even._mut_ is the type that definition compiles to

[Horatiu Cheval]

Of course, that's not very human-friendly. You can write that inductive using a bool index like this

inductive even_odd : bool → ℕ → Prop
| even_zero {even : bool} : even → even_odd tt 0
| even_succ {even : bool} : ∀ n, even_odd ff n → even_odd tt (n + 1)
| odd_succ {even : bool} : ∀ n, even_odd tt n → even_odd ff (n + 1)

[Horatiu Cheval]

Basically, you write even_odd tt for even and even_odd ff for odd

[Kevin Buzzard]

We tend to stay away from mutual inductives in Lean. The reason is this: whilst it no doubt gets compiled down to a single inductive type, it is almost certainly nowhere near as nice as the clean version which Horatiu has posted. Mario's recommendation is always to do the compiling-down yourself. Fortunately our experience in mathematics is that it is quite rare that one needs mutual inductive types, indeed it's surprisingly rare to need inductive types other than structures at all, at least in the kind of mathematics which I have been doing in Lean. Nat itself is a very weird outlier. Even and odd don't need to be defined mutually, and indeed in mathlib they are defined independently.

[Alex Zhang]

mutual inductive even, odd
with even : ℕ → Prop
| even_zero : even 0
| even_succ : ∀ n, odd n → even (n + 1)
with odd : ℕ → Prop
| odd_succ : ∀ n, even n → odd (n + 1)

-- BEGIN
open even odd

theorem not_odd_zero : ¬ odd 0.

Why does this theorem can be closed by a period?

[Kevin Buzzard]

Because the equation compiler, which basically knows something about induction, can do enough calculations dealing with cases itself to realise that no cases need to be dealt with by the human

[Kevin Buzzard]

The logic is this: we need to prove false given an input of odd 0. That term of type odd 0 needs to come from a constructor of odd. The only constructor of odd ultimately makes a term of type odd (n+1) so before we figure out exactly what to ask the user for we had better find all solutions of n+1=0. The definition of n+1 is succ n so we had better ask the user to deal with all n such that succ n is zero. But these are different constructors for nat so there can't be any solutions at all and so we don't have to ask the user to do anything. Some argument of that nature is happening internally

[Alex Zhang]

If I were very stubborn and insist on proving this by myself, what can I do then to close the following proof?

mutual inductive even, odd
with even : ℕ → Prop
| even_zero : even 0
| even_succ : ∀ n, odd n → even (n + 1)
with odd : ℕ → Prop
| odd_succ : ∀ n, even n → odd (n + 1)

-- BEGIN
open even odd

theorem not_odd_zero : ¬ odd 0 :=
begin
  intros h,
  sorry
end

[Eric Wieser]

cases h would be the next step

[Kevin Buzzard]

and presumably the last step?

[Alex Zhang]

Yes!

[Alex Zhang]

This is an example copied from the book:

universe u

inductive vector (α : Type u) : ℕ → Type u
| nil {} : vector 0
| cons   : Π {n}, α → vector n → vector (n+1)

namespace vector
local notation h :: t := cons h t

variable {α : Type u}

-- BEGIN
def add [has_add α] : Π {n : ℕ}, vector α n → vector α n → vector α n
| .(0)   nil                nil        := nil
| .(n+1) (@cons .(α) n a v) (cons b w) := cons (a + b) (add v w)
-- END

end vector

In the line | .(n+1) (@cons .(α) n a v) (cons b w) := cons (a + b) (add v w), is there any difference between using .(α) and α?

[Kevin Buzzard]

If you change .(n+1) to (n+1) then it breaks, so yes. Perhaps the error you get gives you some sort of idea as to the problems going on here.

[Kevin Buzzard]

In this case you can get away with (_+1) by the way.

[Kevin Buzzard]

I will say again that the dependent type vector n implemented as an inductive type is very hard to work with and whilst it's good to struggle and learn what is hard, when you've finished becoming miserable about how difficult Lean is and how it can't do something as simple as vectors, I would urge you to try everything that you're doing with the subtype definition and discover how easy it all is again.

[Alex Zhang]

In the proof of the last theorem, is there a way to match e with the case split in the definition of simp_const? If I do as in the current proof, I will have trouble showing simp_const e = e in the last case.

inductive aexpr : Type
| const : ℕ → aexpr
| var : ℕ → aexpr
| plus : aexpr → aexpr → aexpr
| times : aexpr → aexpr → aexpr

open aexpr

def aeval (v : ℕ → ℕ) : aexpr → ℕ
| (const n)    := n
| (var n)      := v n
| (plus e₁ e₂)  := aeval e₁ + aeval e₂
| (times e₁ e₂) := aeval e₁ * aeval e₂

def simp_const : aexpr → aexpr
| (plus (const n₁) (const n₂))  := const (n₁ + n₂)
| (times (const n₁) (const n₂)) := const (n₁ * n₂)
| e                             := e

def fuse : aexpr → aexpr
| (const n)    := const n
| (var n)      := var n
| (plus e₁ e₂)  := simp_const (plus (fuse e₁) (fuse e₂))
| (times e₁ e₂) := simp_const (times (fuse e₁) (fuse e₂))


theorem simp_const_eq (v : ℕ → ℕ) :
  ∀ e : aexpr, aeval v (simp_const e) = aeval v e :=
λ e, match e with
| (plus (const n₁) (const n₂))  := by simp [aeval,simp_const]
| (times (const n₁) (const n₂)) := by simp [aeval,simp_const]
| e                             := by {have h:simp_const e = e,{sorry},rw h,}
end

[Kevin Buzzard]

Instead of match (which does cases) you could use the induction tactic. Does this help?

[Alex Zhang]

Thanks for the suggestion, but not quite.. (the actual problem is concerning using the third case in the defn of simp_const as the sorry indicates in the above code)

[Alex Zhang]

In the third case of the proof, Lean seems not clever enough to know that e is not in the first two cases.

[Kevin Buzzard]

Yes that's correct, Lean doesn't know. If you want it to know then you will need to do induction on e. But it is not clear to me that you are proving the right thing. My instinct is that you should just prove "the big theorem" following e.g. the example at the beginning of chapter 2 of "Certified Programming with Dependent Types" by Chlipala (it's written for Coq but a very early exercise I did in Lean was to port this example over to Lean) and then I would imagine that you will be able to deduce everything relatively easily.

If there's one thing I've learnt from examples like this, it's that this kind of structural induction is much harder than a mathematician imagines. Fortunately I also learnt that there are plenty of computer scientists around here who know the tricks, and also that in practice in the kind of mathematics done by most working mathematicians, this sort of complex induction procedure is rarely if ever needed.

[Kevin Buzzard]

If you really want to push this forward, then you need to remember that every definition comes with a cost, and the cost is that you have to make an API for the definition. You have made four definitions without any API at all, and are now trying to prove a theorem relating three of them. What you should be doing is that the moment you have defined simp_const (which, as I've said above, does not look to me like a useful definition, you really want the theorem which says "my compiler is correct" rather than some weaker partial versions) you need to make an API for it, proving things like simp_const (var n) = var n and many other things (you will have to deal with the case simp_const (plus (const n) (times e f)) etc etc, it will be horrible). Once you have a robust API for simp_const you can press on. Every definition you make, you need to pay for.

[Kevin Buzzard]

Oh I see -- this is an actual exercise in TPIL? :-/ Then probably what I'm saying is inaccurate. Apart from the bit when I said "I worked through the example in CPDT and it taught me a lot".

[Kevin Buzzard]

So yes, on further experimentation, you can absolutely do this by doing induction on everything. I don't see how to do it using the method you're using.

[Kevin Buzzard]

Solution

theorem simp_const_eq (v : ℕ → ℕ) :
  ∀ e : aexpr, aeval v (simp_const e) = aeval v e :=
begin
  intro e,
  induction e with _ _ a b _ _ a b _ _,
  { refl },
  { refl },
  { cases a,
    cases b,
    { refl },
    { refl },
    { refl },
    { refl },
    { refl },
    { refl },
    { refl } },
  { cases a,
    cases b,
    { refl },
    { refl },
    { refl },
    { refl },
    { refl },
    { refl },
    { refl },
  }
end

[Alex Zhang]

Thanks for your long explanation, Kevin! Could you let me know what "API" here stands for?

[Alex Zhang]

A shorter solution using repeat:

theorem simp_const_eq (v : ℕ → ℕ) :
  ∀ e : aexpr, aeval v (simp_const e) = aeval v e :=
begin
  intro e,
  induction e with _ _ a b _ _ a b _ _,
  repeat { refl },
  repeat { cases a, cases b, repeat { refl }},
end

[Kevin Buzzard]

Yes, I thought I'd leave the refls all in there just to show you that at the end of the day we really did have to take it apart into cases. API means "interface". For example you make the reals real as Dedekind cuts or Cauchy sequences (who knows which, the user is not supposed to know) and then you define real.add and real.mul and real.a_non_empty_bounded_set_has_a_LUB and real.field and the proofs of course depend on the definition but the user doesn't look at the proofs. The definition (real) comes with the cost (proving it's a complete archimedean ordered field) and then the user doesn't look at the innards of the definition but just uses the interface you've made for them.