notnotelim2

Stream: general

[Phiroc]

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]

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]

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]

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]

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

[Kevin Buzzard]

rfl

[Phiroc]

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

[Kevin Buzzard]

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]

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]

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]

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

[Shing Tak Lam]

@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