How to prove `¬(Even 1)` manually?

Stream: lean4

[y-samuel]

I am wondering how to manually prove some falsity in Lean4, such as proving 0 ≠ 1 and ¬(Even 1).

Although the cases tactic can eliminate those impossible subgoals, I prefer to solve them manually for enjoyment.

-- by simp
example : 1 ≠ 0 := by simp

-- by cases
example : 1 ≠ 0 := by
  intro h
  cases h

I am able to prove 0 ≠ 1 using the rewrite tactic.

-- by rewrite
def is_zero : Nat → Prop
  | .zero => True
  | .succ _ => False

example : (0 = 1) → False := by
  have h_0_eq_0 : is_zero 0 = is_zero 0 := rfl
  intro h_0_eq_1
  conv at h_0_eq_0 => {
    left
    rw [h_0_eq_1]
  }
  have h_false_eq_true : False = True := h_0_eq_0
  rewrite [h_false_eq_true]
  exact trivial

-- even by crazy recOn!
def f : Nat → Prop :=
  @Nat.rec (fun _ => Prop) False (fun _ _ => True)

example (n : Nat) : (.succ n = 0) → False :=
  fun e => @Eq.subst _ f (.succ n) 0 e True.intro

And to prove Even 1 is false by cases.

example : ¬(Even 1) := by
  intro h
  cases h

But I am unsure how to prove ¬(Even 1) manually, can someone show the proof and put some materials about this?

inductive Even : Nat → Prop where
  | zero : Even 0
  | add_two : (k : Nat) → Even k → Even (k + 2)

example : ¬(Even 1) := by
  intro h
  sorry -- How?

Thank you all!

[Eric Rodriguez]

You can always #print a lemma to see the proof. This will be using noConfusion

[y-samuel]

Eric Rodriguez said:

You can always #print a lemma to see the proof. This will be using noConfusion

Magic #print! Thank you!

[y-samuel]

I wonder if there is a method based on typed pattern matching?

[Eric Rodriguez]

If you try pattern match, it will give you type errors. You need to use the nomatch keyword, or the match h with . extension in Std (Std/Tactic/NoMatch)

[Eric Rodriguez]

(sorry, I think nomatch is mathlib/std)

[Eric Rodriguez]

theorem as : ¬(Even 1) := fun h ↦ nomatch h

#print as

[Eric Rodriguez]

Eric Rodriguez said:

(sorry, I think nomatch is mathlib/std)

it's actually the other way round!

[y-samuel]

Eric Rodriguez said:

If you try pattern match, it will give you type errors. You need to use the nomatch keyword, or the match h with . extension in Std (Std/Tactic/NoMatch)

Oh, Very Thank You!
I thought how to turn type errors in pattern matching into some information (like mata-programming, I am not sure) indeed!
I think I should read "The Little Typer" because I remember this book use recursor directly.

[David Thrane Christiansen]

Generally speaking, programming and proving with recursors directly is quite dreadful. Tactics and pattern matching is much easier! But knowing how they work is part of the fun, and that's what you're doing here, so in that spirit I'll translate a bit of code from The Little Typer into Lean for you. Apologies in advance for unidiomatic Lean - I'm trying to connect Lean syntax to the book, rather than follow proper Lean naming conventions.

The first step is getting your hands on a recursor. Lean makes one for each inductive type, and it's used to justify the termination of recursive definitions with pattern matching, but let's pretend that we need to write our own in order to get something that looks more like the one in Pie:

def indNat (mot : Nat → Sort u) (base : mot 0) (step : (n : Nat) → mot n → mot (n + 1)) : (tgt : Nat) → mot tgt
  | 0 => base
  | n + 1 => step n (indNat mot base step n)

It sounds like you understand recursors already, so I won't get into this more. To check your understanding, write the equivalent for lists and binary trees.

To do the kind of thing you want to do, we need to build the "no confusion" lemma for Nat. This states that the constructors of Nat are disjoint (that is, zero never equals successor) and injective (equal successors means their arguments are equal). The way we do this is a bit formulaic, but the explanations in the literature are not so accessible in my opinion - I had a hard time learning them, at least!

Note that "no confusion" says "assume that these Nats are equal" and then after that says what the consequences of that equality are. If they're both zero, there's nothing learned. If they're a mix of zero and successor, then their equality implies falsehood (this is the disjointness bit). If they're both successor, then their equality implies the equality of the smaller Nats under the succ constructor. The "consequences of equality" bit can be captured in this function:

def IfEqual : Nat → Nat → Prop
  | 0, 0 => True
  | _+1, 0 => False
  | 0, _+1 => False
  | n+1, k+1 => n = k

Generally, there's $n^2$ cases for $n$ constructors, and all the off-diagonal ones are False while the on-diagonal ones are the conjunction of the equalities of the constructor arguments.

Exercises:

1. Rewrite IfEqual using indNat
2. Create the corresponding IfEqual for lists and for binary trees

The type of "no confusion" is now (n k : Nat) (eq : n = k) : IfEqual n k. Check your understanding by instantiating it with some concrete Nats and see what the resulting statement says.

Proving this by induction on n and k is not the way forward, however - the false cases are simply disjointness, but that's what we're trying to prove! A little trick is needed: prove only the on-diagonal cases!

def ifEqualSelf (n : Nat) : IfEqual n n :=
  indNat (fun k => IfEqual k k) True.intro (fun _ _ => rfl) n

Like IfEqual, this isn't really recursive. Here's another exercise: use indNat to define casesNat, which is like indNat without an induction hypothesis, and then use it here.

Given the diagonal case, substitution can be used with the equality assumption to prove "no confusion" (which I've renamed a bit here to match The Little Typer as best as I remember it - my PDF is on the other computer and the paper version under a pile of stuff right now):

def ifEqualThenWhat (n k : Nat) (eq : n = k) : IfEqual n k :=
  eq ▸ ifEqualSelf n

This says that if two numbers are equal, then the consequences of that equality hold. Expanding out the four cases for n and k, this is injectivity and disjointness of constructors.

This is super annoying to use. Here's some examples:

def zeroNotOne (eq : 0 = 1) : False := ifEqualThenWhat 0 1 eq
def zeroNotTwo (eq : 0 = 2) : False := ifEqualThenWhat 0 2 eq
def oneNotThree (eq : 1 = 3) : False :=
  let h : 0 = 2 := ifEqualThenWhat 1 3 eq
  ifEqualThenWhat 0 2 h

Exercise: prove that eight doesn't equal fifteen. Write it out in full with no underscores.

This can be used with the recursor to implement decidable equality of Nat:

open Decidable in
def decNatEq : (n k : Nat) → Decidable (n = k) :=
  indNat (fun n => ∀ k, Decidable (n = k))
    (indNat (fun k => Decidable (0 = k))
      (isTrue rfl)
      (fun k' _ => isFalse (ifEqualThenWhat 0 (k' + 1))))
    (fun n' ih =>
      indNat (fun k => Decidable (n' + 1 = k))
        (isFalse (ifEqualThenWhat (n' + 1) 0))
        (fun k' _ =>
           match ih k' with
           | isTrue eq => isTrue (congrArg (· + 1) eq)
           | isFalse notEq => isFalse fun (h : n' + 1 = k' + 1) =>
             notEq (ifEqualThenWhat (n' + 1) (k' + 1) h)))

Exercises:

1. Extract the three non-recursive cases into helper lemmas
2. Replace the uses of ▸ and pattern matching on Decidable with recursors a la indNat
3. Use your dependent cases operation from earlier to simplify decNatEq
4. Generalize this definition to List and binary trees - the list case will require an input proof that the elements have decidable equality. Do all this with recursors.

By the time you've done all this, you'll have a good idea of what happens behind the scenes! For more info, read A Few Constructions on Constructors by McBride, Goguen, and McKinna - it's got all this and more, and its techniques are an important part of what goes on in Lean.

[y-samuel]

David Thrane Christiansen said:

Generally speaking, programming and proving with recursors directly is quite dreadful. Tactics and pattern matching is much easier! But knowing how they work is part of the fun, and that's what you're doing here, so in that spirit I'll translate a bit of code from The Little Typer into Lean for you. Apologies in advance for unidiomatic Lean - I'm trying to connect Lean syntax to the book, rather than follow proper Lean naming conventions.

The first step is getting your hands on a recursor. Lean makes one for each inductive type, and it's used to justify the termination of recursive definitions with pattern matching, but let's pretend that we need to write our own in order to get something that looks more like the one in Pie:

def indNat (mot : Nat → Sort u) (base : mot 0) (step : (n : Nat) → mot n → mot (n + 1)) : (tgt : Nat) → mot tgt
  | 0 => base
  | n + 1 => step n (indNat mot base step n)

It sounds like you understand recursors already, so I won't get into this more. To check your understanding, write the equivalent for lists and binary trees.

To do the kind of thing you want to do, we need to build the "no confusion" lemma for Nat. This states that the constructors of Nat are disjoint (that is, zero never equals successor) and injective (equal successors means their arguments are equal). The way we do this is a bit formulaic, but the explanations in the literature are not so accessible in my opinion - I had a hard time learning them, at least!

Note that "no confusion" says "assume that these Nats are equal" and then after that says what the consequences of that equality are. If they're both zero, there's nothing learned. If they're a mix of zero and successor, then their equality implies falsehood (this is the disjointness bit). If they're both successor, then their equality implies the equality of the smaller Nats under the succ constructor. The "consequences of equality" bit can be captured in this function:

def IfEqual : Nat → Nat → Prop
  | 0, 0 => True
  | _+1, 0 => False
  | 0, _+1 => False
  | n+1, k+1 => n = k

Generally, there's $n^2$ cases for $n$ constructors, and all the off-diagonal ones are False while the on-diagonal ones are the conjunction of the equalities of the constructor arguments.

Exercises:

1. Rewrite IfEqual using indNat
2. Create the corresponding IfEqual for lists and for binary trees

The type of "no confusion" is now (n k : Nat) (eq : n = k) : IfEqual n k. Check your understanding by instantiating it with some concrete Nats and see what the resulting statement says.

Proving this by induction on n and k is not the way forward, however - the false cases are simply disjointness, but that's what we're trying to prove! A little trick is needed: prove only the on-diagonal cases!

def ifEqualSelf (n : Nat) : IfEqual n n :=
  indNat (fun k => IfEqual k k) True.intro (fun _ _ => rfl) n

Like IfEqual, this isn't really recursive. Here's another exercise: use indNat to define casesNat, which is like indNat without an induction hypothesis, and then use it here.

Given the diagonal case, substitution can be used with the equality assumption to prove "no confusion" (which I've renamed a bit here to match The Little Typer as best as I remember it - my PDF is on the other computer and the paper version under a pile of stuff right now):

def ifEqualThenWhat (n k : Nat) (eq : n = k) : IfEqual n k :=
  eq ▸ ifEqualSelf n

This says that if two numbers are equal, then the consequences of that equality hold. Expanding out the four cases for n and k, this is injectivity and disjointness of constructors.

This is super annoying to use. Here's some examples:

def zeroNotOne (eq : 0 = 1) : False := ifEqualThenWhat 0 1 eq
def zeroNotTwo (eq : 0 = 2) : False := ifEqualThenWhat 0 2 eq
def oneNotThree (eq : 1 = 3) : False :=
  let h : 0 = 2 := ifEqualThenWhat 1 3 eq
  ifEqualThenWhat 0 2 h

Exercise: prove that eight doesn't equal fifteen. Write it out in full with no underscores.

This can be used with the recursor to implement decidable equality of Nat:

open Decidable in
def decNatEq : (n k : Nat) → Decidable (n = k) :=
  indNat (fun n => ∀ k, Decidable (n = k))
    (indNat (fun k => Decidable (0 = k))
      (isTrue rfl)
      (fun k' _ => isFalse (ifEqualThenWhat 0 (k' + 1))))
    (fun n' ih =>
      indNat (fun k => Decidable (n' + 1 = k))
        (isFalse (ifEqualThenWhat (n' + 1) 0))
        (fun k' _ =>
           match ih k' with
           | isTrue eq => isTrue (congrArg (· + 1) eq)
           | isFalse notEq => isFalse fun (h : n' + 1 = k' + 1) =>
             notEq (ifEqualThenWhat (n' + 1) (k' + 1) h)))

Exercises:

1. Extract the three non-recursive cases into helper lemmas
2. Replace the uses of ▸ and pattern matching on Decidable with recursors a la indNat
3. Use your dependent cases operation from earlier to simplify decNatEq
4. Generalize this definition to List and binary trees - the list case will require an input proof that the elements have decidable equality. Do all this with recursors.

By the time you've done all this, you'll have a good idea of what happens behind the scenes! For more info, read A Few Constructions on Constructors by McBride, Goguen, and McKinna - it's got all this and more, and its techniques are an important part of what goes on in Lean.

Thankkkkkk uuuuuuuuu!
Yes, it is fun for me and I want to know the "details".
I will take the time to exercise your ideas!
Again, thank you!