notnotelim

Stream: general

[Phiroc]

Good morning,

I'm try to translate the following theorem from Agda to Lean :

notnotelim : forall (b : bool) -> not not b = b
notnotelim : tt = refl
notnotelim : ff = refl

cf. Verified Functional Programming in Agda, Aarun Stump, p. 22

Here's my first attempt, which doesn't work:

theorem notnotelim2 (b : bool):
    ¬¬ b = b :=
begin
    induction b,
    case tt { reflection },
    case ff { reflection }
end

However, this works:

theorem notnotelim (b : bool):
    ¬¬ b = b :=
begin
    induction b,
    case tt { contradiction },
    case ff { contradiction }
end

I've no idea why.

In Idris, this works (just as in Agda):

notNotTT : not (not True) = True
notNotTT = Refl

I can't figure out how to prove the same theorem, but with a "forall":

theorem notnotelim2 :
    ∀b: bool, ¬¬ b = b :=
begin
    -- proof
end

Any help would be much appreciated.

Many thanks.

Philip

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

Note that not works on Props, not on bools

[Yury G. Kudryashov]

bnot works on bools

[Phiroc]

Many thanks Yury.