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!

[David Thrane Christiansen]

I'm back from vacation. How did the exercises go?

[y-samuel]

Hi David! I am suprised and happy that you wait my homeworks!Good evening!
I apologize for the delay. Please forgive me! :sob:

I recently read your book, The Little Typer, and found it to be an excellent resource on dependent types.
I regret not finishing it a few years ago. However, I am fortunate to have completed it now.
The proof of 'front' and 'nat=?' in The Little Typer was astonishing to me until now.
What a creative thinking!

After reading the little typer, the homework you left become more easier to me.
Please let me know if there are any errors.
Thank you very much!

Nat.lean
List.lean
Binary.lean

[y-samuel]

Oops, I have discovered how to manually prove 'Even 1 -> False' using the same technique you used to prove 'front'!!!
NotEven1.lean

[y-samuel]

y-samuel said:

Oops, I have discovered how to manually prove 'Even 1 -> False' using the same technique you used to prove 'front'!!!
NotEven1.lean

I apply the recursor method and your technique again to generalize this example.
This is difficult for me to say!
NotEvenOdd.lean

[Kevin Buzzard]

you can post code within triple back-ticks ( ``` ) on this Zulip. It's much better than uploading Lean files (for example I cannot read your messages on mobile).

[y-samuel]

Kevin Buzzard said:

you can post code within triple back-ticks ( ``` ) on this Zulip. It's much better than uploading Lean files (for example I cannot read your messages on mobile).

Got it, please wait a minute

[y-samuel]

exercises about Binary:

inductive Binary (α : Type u) where
  | empty : Binary α
  | single (value : α) : Binary α
  | branch (left : Binary α) (right : Binary α) : Binary α

def Binary.IfEqualRef {α : Type u} : Binary α → Binary α → Prop
  | .empty, .empty => True
  | .empty, .single _ => False
  | .empty, .branch _ _ => False
  | .single _, .empty => False
  | .single a, .single b => a = b
  | .single _, .branch _ _ => False
  | .branch _ _, .empty => False
  | .branch _ _, .single _ => False
  | .branch al ar, .branch bl br => al = bl ∧  ar = br

def indBinary
  {α : Type u}
  (motive : Binary α → Sort u1)
  (empty : motive .empty)
  (single : (value : α) → motive (.single value))
  (branch :
    (left : Binary α) →
    (right : Binary α) →
    motive left →
    motive right →
    motive (.branch left right))
    : (target : Binary α) → motive target
  | .empty => empty
  | .single value => single value
  | .branch left right =>
    branch left right
      (indBinary motive empty single branch left)
      (indBinary motive empty single branch right)
def casesBinary
  {α : Type u}
  (motive : Binary α → Sort u1)
  (empty : motive .empty)
  (single : (value : α) → motive (.single value))
  (branch :
    (left : Binary α) →
    (right : Binary α) →
    motive (.branch left right))
    : (target : Binary α) → motive target :=
  indBinary
    motive
    empty
    single
    (fun left right __almost₁ __almost₂ => branch left right)

def IfEqual {α : Type u} (left : Binary α) (right : Binary α) : Prop :=
  casesBinary (fun __k => Prop)
    (casesBinary (fun __k => Prop)
      True
      (fun __value => False)
      (fun __left __right => False)
      right)
    (fun lv => casesBinary (fun __k => Prop)
      False
      (fun rv => lv = rv)
      (fun __left __right => False)
      right)
    (fun ll lr =>
      casesBinary (fun __k => Prop)
        False
        (fun __value => False)
        (fun rl rr =>
          ll = rl ∧ lr = rr)
        right)
    left

def IfEqualSelf {α : Type u} : (tree : Binary α) → IfEqual tree tree :=
  casesBinary
    (fun k => IfEqual k k)
    True.intro
    (fun v => Eq.refl v)
    (fun left right => And.intro (Eq.refl left) (Eq.refl right))

def ifEqualThenWhat {α : Type u} (t1 t2 : Binary α) : (eq : t1 = t2) → IfEqual t1 t2 :=
  Eq.ndrec (motive := fun k => IfEqual t1 k) (IfEqualSelf t1)

def emptyNotSingle {α : Type u} (value : α)
    : Binary.empty = .single value → False :=
  ifEqualThenWhat Binary.empty (.single value)
def emptyNotBranch {α : Type u} (t1 t2 : Binary α)
    : Binary.empty = .branch t1 t2 → False :=
  ifEqualThenWhat Binary.empty (.branch t1 t2)
def singleNotEmpty {α : Type u} (v : α)
    : Binary.single v = .empty → False :=
  ifEqualThenWhat (Binary.single v) .empty
def singleNotBranch {α : Type u} (v : α) (t1 t2 : Binary α)
    : Binary.single v = .branch t1 t2 → False :=
  ifEqualThenWhat (Binary.single v) (.branch t1 t2)
def branchNotEmpty {α : Type u} (t1 t2 : Binary α)
    : Binary.branch t1 t2 = .empty → False :=
  ifEqualThenWhat (.branch t1 t2) Binary.empty
def branchNotSingle {α : Type u} (t1 t2 : Binary α) (v : α)
    : Binary.branch t1 t2 = .single v → False :=
  ifEqualThenWhat (Binary.branch t1 t2) (.single v)

open Decidable in
def decBinaryEq
    (α : Type u)
    [DecidableEq α]
    : (t1 t2 : Binary α) → Decidable (t1 = t2) :=
  indBinary
    (fun t1 => ∀ k, Decidable (t1 = k))
    -- empty
    (fun k => casesBinary (fun k => Decidable (.empty = k))
      (isTrue (Eq.refl Binary.empty))
      (fun v => isFalse (emptyNotSingle v))
      (fun rl rr => isFalse (emptyNotBranch rl rr))
      k)
    -- single
    (fun v k => casesBinary (fun k => Decidable (.single v = k))
      (isFalse (singleNotEmpty v))
      (fun v' => @Decidable.casesOn (v = v')
        (fun __k => Decidable (Binary.single v = .single v'))
        (decEq v v')
        (fun neq => isFalse (fun eqSingle =>
          neq (ifEqualThenWhat (.single v) (.single v') eqSingle)))
        (fun eq => isTrue (congrArg (Binary.single) eq)))
      (fun rl rr => isFalse (singleNotBranch v rl rr))
      k)
    -- branch
    (fun ll lr ihl ihr k => casesBinary (fun k => Decidable (.branch ll lr = k))
      (isFalse (branchNotEmpty ll lr))
      (fun v' => isFalse (branchNotSingle ll lr v'))
      (fun rl rr => @Decidable.casesOn (ll = rl)
        (fun __k => Decidable (Binary.branch ll lr = .branch rl rr))
        (ihl rl)
        (fun neq : ¬ ll = rl => @Decidable.casesOn (lr = rr)
          (fun __k => Decidable (Binary.branch  ll lr = .branch rl rr))
          (ihr rr)
          (fun neq' : ¬ lr = rr => isFalse (fun notEq : Binary.branch ll lr = Binary.branch rl rr =>
            neq' (ifEqualThenWhat (Binary.branch ll lr) (.branch rl rr) notEq).right))
          (fun __eq : lr = rr => isFalse (fun notEq : Binary.branch ll lr = Binary.branch rl rr =>
            neq (ifEqualThenWhat (Binary.branch ll lr) (.branch rl rr) notEq).left)))
        (fun eq : ll = rl => @Decidable.casesOn (lr = rr)
          (fun __k => Decidable (Binary.branch ll lr = .branch rl rr))
          (ihr rr)
          (fun neq' : ¬ lr = rr => isFalse (fun notEq : Binary.branch ll lr = Binary.branch rl rr =>
            neq' (ifEqualThenWhat (Binary.branch ll lr) (.branch rl rr) notEq).right))
          (fun eq' : lr = rr => isTrue (Eq.ndrec
            (motive := fun k => Binary.branch ll lr = .branch k rr)
            (congrArg (Binary.branch ll) eq')
            eq))))
      k)

[y-samuel]

For all odd n, Even n is False:

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

def IfEqual (a : Nat) (b : Nat) : Prop :=
  (@Nat.casesOn (fun __k => Prop) a
    (@Nat.casesOn (fun __k => Prop) b
      True
      (fun __k' => False))
    (fun n =>
      @Nat.casesOn (fun __k => Prop) b
        False
        (fun j => n = j)))

def ifEqualSelf (n : Nat) : IfEqual n n :=
  @Nat.casesOn (fun k => IfEqual k k) n
    True.intro
    (fun n' => Eq.refl n')

def ifEqualThenWhat (n k : Nat) : (eq : n = k) → IfEqual n k :=
  Eq.ndrec (motive := fun k => IfEqual n k) (ifEqualSelf n)

def zeroNotSucc (k : Nat) : 0 = k + 1 → False :=
  ifEqualThenWhat 0 (k + 1)
def succNotZero (k : Nat) : k + 1 = 0 → False :=
  ifEqualThenWhat (k + 1) 0
def succInjective (n k : Nat) : n + 1 = k + 1 → n = k :=
  ifEqualThenWhat (n + 1) (k + 1)
def numberNotSucc (n : Nat) : n = n + 1 → False :=
  indNat
    (fun k => k = k + 1 → False)
    (zeroNotSucc 0)
    (fun n' ih =>
      fun eq => ih (succInjective n' (n' + 1) eq))
    n

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

def notEven1 : ¬(Even 1) :=
  fun h : Even 1 =>
    @Even.casesOn
      (fun k __ek => k = 1 → False)
      1 h
      (fun eq => zeroNotSucc 0 eq)
      (fun k __ek eq => succNotZero k (succInjective (k + 1) 0 eq))
      (Eq.refl 1)

def notEven3 : ¬(Even 3) :=
  fun h : Even 3 =>
    @Even.casesOn
      (fun k __ek => k = 3 → False)
      3 h
      (fun eq => zeroNotSucc 2 eq)
      (fun k ek eq =>
        let kEq1 : k = 1 := succInjective k 1 (succInjective (k + 1) 2 eq)
        let even1 : Even 1 := Eq.ndrec (motive := fun k => Even k) ek kEq1
        notEven1 even1)
      (Eq.refl 3)

def Even.ind
    (motive : (k : Nat) → Even k → Prop)
    (base : motive Nat.zero Even.zero)
    (step : (k : Nat) → (ek : Even k) → motive k ek → motive (k + 2) (.add_two k ek))
    (k : Nat)
    : (target : Even k) → motive k target
  | Even.zero => base
  | Even.add_two k ek => step k ek (Even.ind motive base step k ek)

def notEvenOdd (n : Nat) : (Even (2 * n + 1)) → False :=
  fun h : Even (2 * n + 1) =>
    Even.ind
      (fun k __ek => ∀ (i : Nat), k = 2 * i + 1 → False)
      (fun i eq => zeroNotSucc (2 * i) eq)
      (fun k __ek almost i eq => @Nat.casesOn
        (fun k1 => i = k1 → False)
        i
        (fun i_is_0 =>
          let h₀ : k + 2 = 1 :=
            Eq.ndrec
              (motive := fun k1 => k + 2 = 2 * k1 + 1)
              eq i_is_0
          succNotZero k (succInjective (k + 1) 0 h₀))
        (fun i₁ i_is_succ_i₁ =>
          let h₁ : k + 2 = 2 * i₁ + 3 :=
            Eq.ndrec
              (motive := fun k1 => k + 2 = 2 * k1 + 1)
              eq i_is_succ_i₁
          let h₂ : k = 2 * i₁ + 1 :=
            succInjective k (2 * i₁ + 1)
              (succInjective (k + 1) (2 * i₁ + 2) h₁)
          almost i₁ h₂)
        (Eq.refl i))
      (2 * n + 1) h
      n (Eq.refl (2 * n + 1))

[y-samuel]

exercises about List:

  | .nil, .nil => True
  | .cons _ _, .nil => False
  | .nil, .cons _ _ => False
  | .cons a as, .cons b bs => a = b ∧ as = bs

def indList
    {α : Type u}
    (motive : List α → Sort u1)
    (base : motive .nil)
    (step : (a : α) → (as : List α) → motive as → motive (.cons a as))
    : (target : List α) → motive target
  | .nil => base
  | .cons a as => step a as (indList motive base step as)
def casesList
    {α : Type u}
    (motive : List α → Sort u1)
    (base : motive .nil)
    (step : (a : α) → (as : List α) → motive (.cons a as))
    : (target : List α) → motive target :=
  indList motive base (fun a as __almost => step a as)

def IfEqual₁ {α : Type u} (as : List α) (bs : List α) : Prop :=
  indList (fun __k => Prop)
    (indList (fun __k => Prop)
      True
      (fun __b __bs __almost => False)
      bs)
    (fun a as __almost =>
      indList (fun __k => Prop)
        False
        (fun b bs __almost => a = b ∧ as = bs)
        bs)
    as

def IfEqual {α : Type u} (as : List α) (bs : List α) : Prop :=
  casesList (fun __k => Prop)
    (casesList (fun __k => Prop)
      True
      (fun __b __bs => False)
      bs)
    (fun a as =>
      casesList (fun __k => Prop)
        False
        (fun b bs => a = b ∧ as = bs)
        bs)
    as

def IfEqualSelf {α : Type u} : (ns : List α) → IfEqual ns ns :=
  casesList
    (fun k => IfEqual k k)
    True.intro
    (fun x xs => And.intro (Eq.refl x) (Eq.refl xs))

def ifEqualThenWhat
    {α : Type u}
    (xs ys : List α)
    : (eq : xs = ys) → IfEqual xs ys :=
  Eq.ndrec (motive := fun k => IfEqual xs k)
    (IfEqualSelf xs)

def nilNotCons
    {α : Type u}
    (x : α)
    (xs : List α)
    : List.nil = .cons x xs → False :=
  ifEqualThenWhat .nil (.cons x xs)
def consNotNil
    {α : Type u}
    (x : α)
    (xs : List α)
    : List.cons x xs = .nil → False :=
  ifEqualThenWhat (.cons x xs) .nil
def consInjective
    {α : Type u}
    (x y : α)
    (xs ys : List α)
    : List.cons x xs = List.cons y ys → x = y ∧ xs = ys :=
  ifEqualThenWhat (.cons x xs) (.cons y ys)

open Decidable in
def decListEq (α : Type u) [DecidableEq α] : (as bs : List α) → Decidable (as = bs) :=
  indList (fun xs => ∀ k, Decidable (xs = k))
    (casesList (fun k => Decidable (.nil = k))
      (isTrue rfl)
      (fun y ys => isFalse (nilNotCons y ys)))
    (fun x xs ih =>
      casesList (fun k => Decidable (.cons x xs = k))
        (isFalse (consNotNil x xs))
        (fun y ys => @Decidable.casesOn (xs = ys)
          (fun __k => Decidable (List.cons x xs = .cons y ys))
          (ih ys)
          (fun neq => isFalse
            fun (h : List.cons x xs = .cons y ys) =>
              neq (consInjective x y xs ys h).right)
          (fun eqxs => @Decidable.casesOn (x = y)
            (fun __k => Decidable (List.cons x xs = .cons y ys))
            (decEq x y)
            (fun neq => isFalse
              fun (h : List.cons x xs = .cons y ys) =>
                neq (consInjective x y xs ys h).left)
            (fun eqx => isTrue
              (Eq.ndrec
                (motive := fun k => List.cons x xs = List.cons k ys)
                (congrArg (List.cons x ·) eqxs)
                eqx)))))

[y-samuel]

exercises about Nat:

def IfEqual₀ : Nat → Nat → Prop
  | .zero, .zero => True
  | .succ _, .zero => False
  | .zero, .succ _ => False
  | .succ n, .succ k => n = k

def indNat
    (motive : Nat → Sort u)
    (base : motive 0)
    (step : (n : Nat) → motive n → motive (n + 1))
    : (target : Nat) → motive target
  | 0 => base
  | n + 1 => step n (indNat motive base step n)
def casesNat
    (motive : Nat → Sort u)
    (base : motive 0)
    (step : (n : Nat) → motive (n + 1))
    : (target : Nat) → motive target :=
  indNat motive base (fun n __almost => step n)

def IfEqual (a : Nat) (b : Nat) : Prop :=
  (casesNat (fun __k => Prop)
    (casesNat (fun __k => Prop)
      True
      (fun __k' => False)
      b)
    (fun n =>
      casesNat (fun __k => Prop)
        False
        (fun j => n = j)
        b)
    a)

def ifEqualSelfIndNat : (n : Nat) → IfEqual n n :=
  indNat (fun k => IfEqual k k)
    True.intro
    (fun smaller _ => Eq.refl smaller)

def ifEqualSelf : (n : Nat) → IfEqual n n :=
  casesNat (fun k => IfEqual k k)
    True.intro
    (fun n' => Eq.refl n')

def ifEqualThenWhat (n k : Nat) : (eq : n = k) → IfEqual n k :=
  -- eq ▸ ifEqualSelf n
  Eq.ndrec (motive := fun k => IfEqual n k) (ifEqualSelf n)

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
def eightNoFifteen (eq : 8 = 15) : False :=
  let h₇ : 7 = 14 := ifEqualThenWhat 8 15 eq
  let h₆ : 6 = 13 := ifEqualThenWhat 7 14 h₇
  let h₅ : 5 = 12 := ifEqualThenWhat 6 13 h₆
  let h₄ : 4 = 11 := ifEqualThenWhat 5 12 h₅
  let h₃ : 3 = 10 := ifEqualThenWhat 4 11 h₄
  let h₂ : 2 = 9 := ifEqualThenWhat 3 10 h₃
  let h₁ : 1 = 8 := ifEqualThenWhat 2 9 h₂
  let h₀ : 0 = 7 := ifEqualThenWhat 1 8 h₁
  ifEqualThenWhat 0 7 h₀

def zeroNotSucc (k : Nat) : 0 = k + 1 → False :=
  ifEqualThenWhat 0 (k + 1)
def succNotZero (k : Nat) : k + 1 = 0 → False :=
  ifEqualThenWhat (k + 1) 0
def succInjective (n k : Nat) : n + 1 = k + 1 → n = k :=
  ifEqualThenWhat (n + 1) (k + 1)

open Decidable in
def decNatEq₀ : (n j : Nat) → Decidable (n = j) :=
  indNat (fun n => ∀ j, Decidable (n = j))
    (casesNat (fun k => Decidable (0 = k))
      (isTrue (Eq.refl 0))
      (fun j' => isFalse (zeroNotSucc j')))
    (fun n' almost j =>
      casesNat (fun k => Decidable (n' + 1 = k))
      (isFalse (succNotZero n'))
      (fun j' => match almost j' with
        | isFalse neq => isFalse (fun eq =>
          neq (ifEqualThenWhat (n' + 1) (j' + 1) eq))
        | isTrue eq => isTrue (Eq.ndrec
          (motive := fun k => n' + 1 = k + 1)
          (Eq.refl (n' + 1)) eq))
      j)

open Decidable in
def indDecidable
    (p : Prop)
    (motive : Decidable p → Sort u)
    (false : (no : ¬p) -> motive (isFalse no))
    (true : (yes : p) -> motive (isTrue yes))
    (target : Decidable p)
  : motive target :=
  match target with
  | isFalse no => false no
  | isTrue yes => true yes

open Decidable in
def decNatEq : (n k : Nat) → Decidable (n = k) :=
  indNat (fun n => ∀ k, Decidable (n = k))
    (casesNat (fun k => Decidable (0 = k))
      (isTrue rfl)
      (fun k' => isFalse (zeroNotSucc k')))
    (fun n' ih =>
      casesNat (fun k => Decidable (n' + 1 = k))
        (isFalse (succNotZero n'))
        (fun k' => @Decidable.casesOn (n' = k')
          (fun __k => Decidable (n' + 1 = k' + 1))
          (ih k')
          (fun neq => isFalse fun (h : n' + 1 = k' + 1) => neq (succInjective n' k' h))
          (fun eq => isTrue (congrArg (· + 1) eq))))

[y-samuel]

Kevin Buzzard said:

you can post code within triple back-ticks ( ``` ) on this Zulip. It's much better than uploading Lean files (for example I cannot read your messages on mobile).

It is excessively long...

[y-samuel]

y-samuel said:

For all odd n, Even n is False:

I find that proof by pattern matching is simpler.
It automatically replaces variables, such as i = Nat.succ i1, with identity types.
Does the match-patterning algorithm perform the same function as my code (fun k1 => n = k1 -> False and so on) behind the scenes?

def notEvenOdd₀ (n : Nat) : (Even (2 * n + 1)) → False :=
  fun h : Even (2 * n + 1) =>
    Even.ind
      (fun k __ek => ∀ (i : Nat), k = 2 * i + 1 → False)
      (fun i eq => zeroNotSucc (2 * i) eq)
      (fun k __ek almost i eq =>
        match i with
        | Nat.zero => succNotZero k (succInjective (k + 1) 0 eq)
        | Nat.succ i₁ =>
          almost i₁
            (succInjective k (2 * i₁ + 1)
              (succInjective (k + 1) (2 * i₁ + 2) eq)))
      (2 * n + 1) h
      n (Eq.refl (2 * n + 1))

[y-samuel]

Kevin Buzzard said:

you can post code within triple back-ticks ( ``` ) on this Zulip. It's much better than uploading Lean files (for example I cannot read your messages on mobile).

Hi, I am sorry to find you are the author of the post No confusion over no_confusion now!
I read it before reading the little typer! it's very innovative and make me "no confusion" a little, LOL!
Thank you so much!