## Stream: general

### Topic: notnotelim2

#### Phiroc (Apr 06 2020 at 11:04):

Hello,
I'm trying to implement the following theorems described in Verified Functional
Programming in Agda, p. 22-23, but to no avail:

theorem notnotelim2 :
∀b: bool, bnot (bnot b) = b
| tt := bnot (bnot tt)
| ff := bnot (bnot ff)

theorem notnotttprime :
bnot (bnot tt) = tt
| tt := rfl {lzero} {bool} {tt}

theorem notnotffprime :
bnot (bnot ff) = ff
| ff := rfl {lzero} {bool} {ff}


Any help would be much appreciated.

#### Kevin Buzzard (Apr 06 2020 at 11:17):

theorem notnotelim2 :
∀b: bool, bnot (bnot b) = b
| tt := _
| ff := _


If you use underscores then you can see what is missing. In the first one, Lean is expecting a proof of bnot (bnot tt) = tt, but your term bnot (bnot tt) is not a proof of anything, it's just the term tt of type bool.

#### Kevin Buzzard (Apr 06 2020 at 11:18):

In notnotelim2 you are trying to construct a function which eats a bool and spits out a proof. Hence for each possibility for bool, you need to give the proof for this possibility.

#### Kevin Buzzard (Apr 06 2020 at 11:19):

For the second one, you are just trying to prove a theorem. There is no input of a bool. You are attempting to imput a bool with your line | tt := rfl {lzero} {bool} {tt}. You just need to supply a proof. Same for the third.

#### Phiroc (Apr 06 2020 at 11:23):

Sorry, I was saying, could you please provide a hint as to how the proofs should be written?

#### Kevin Buzzard (Apr 06 2020 at 11:23):

rfl

#### Phiroc (Apr 06 2020 at 11:25):

So the Agda variants provided in Agda by Aaron Stump all boil down to rfl?

#### Kevin Buzzard (Apr 06 2020 at 11:31):

I don't know anything about the book you're reading, or Agda. Lean has a proof-irrelevant Prop if that makes any difference.

#### Phiroc (Apr 06 2020 at 11:36):

Here's the book, if you're interested: https://dl.acm.org/doi/book/10.1145/2841316
I am using the theorems defined in it to learn Lean

#### Phiroc (Apr 06 2020 at 11:37):

And here are the above theorems, revisited.

Many thanks, Kevin, for your help.

theorem notnotelim :
∀b: bool, bnot (bnot b) = b
| tt := rfl
| ff := rfl

theorem notnotelim2 :
∀b: bool, bnot (bnot b) = b
| tt := rfl
| ff := rfl

theorem notnotttprime :
bnot (bnot tt) = tt := rfl

theorem notnotffprime :
bnot (bnot ff) = ff := rfl


#### Kevin Buzzard (Apr 06 2020 at 11:39):

The topic of chapter 3 in that book is what I try to cover in the natural number game.

#### Shing Tak Lam (Apr 06 2020 at 11:42):

@Phiroc

Just for reference, strictly speaking your notnotelim2 is not the same as the one in the book, which would be

theorem notnotelim : ∀ (b : bool), bnot (bnot b) = b
| tt := rfl
| ff := rfl

theorem notnottt : bnot (bnot tt) = tt := rfl
theorem notnotff : bnot (bnot ff) = ff := rfl

theorem notnotelim2 : ∀ (b : bool), bnot (bnot b) = b
| tt := notnottt
| ff := notnotff


Last updated: May 13 2021 at 23:16 UTC