Proof by cases on pattern matches

Stream: new members

[Adomas Baliuka]

Is there a tactic (or a nice way) to prove the theorem? This is giving me the feeling that I'm missing some tools for dealing with pattern matches and inductive types...

inductive TS where
    | t1
    | t2
    | t3
    | s1
    | s2
    | s3
open TS

def TS.isT : TS -> Prop
    | t1 | t2 | t3 => true
    | _ => false

-- return  "t_n" with the same suffix number as input
def TS.numToT : TS -> TS
    | s1 => t1
    | s2 => t2
    | s3 => t3
    | t_n => t_n

theorem numToT_isT (ts : TS) : ts.numToT.isT := by
    simp [isT, numToT]
    split
    repeat simp
    next h hh hhh => cases ts <;> simp at h; simp at hh; simp at hhh; simp at hhh; simp at hh; simp at hhh

[Kyle Miller]

Here's how I'd probably do it:

theorem numToT_isT (ts : TS) : ts.numToT.isT := by
  cases ts <;> simp [isT, numToT]

[Kyle Miller]

You can also do cases ts <;> simp! to have simp unfold definitions automatically.

[Adomas Baliuka]

@Kyle Miller Thanks! Is there a list of tactics somewhere? I've never seen simp!despite reading the "tactics" section of "Theorem Proving in Lean" and also the cheatsheet...

[Adomas Baliuka]

Is there some insight behind unrolling definitions after case analysis? My first instinct currently is "first, unroll all my definitions", unless I have theorems about some of those definitions already.

[Kyle Miller]

It seems to have been overlooked in the Lean 4 documentation... I learned it in Lean 3. simp! is short for simp (config := {autoUnfold := true})

[Kyle Miller]

For unfolding definitions, you're going to need to simp afterwards anyway, so you may as well wait. I also figure it is a bit more efficient since then simp doesn't waste any time trying to simplify the match expressions before you actually give it a concrete value for ts.

[Kyle Miller]

Oh, this works too accidentally:

theorem numToT_isT (ts : TS) : ts.numToT.isT := by
  cases ts <;> rfl

[Kyle Miller]

In your definition of isT, make sure to use True and False instead of true and false. The first are Props, and the second are Bools. There's a mechanism to coerce Bools to Props automatically

[Kyle Miller]

With that changed, cases ts <;> trivial would work.

[Adomas Baliuka]

I was actually unsure if I want Propor Bool there. My (actual) use-case might involve using those "isT"-decision as data, so I should use Bool? I also just noticed that it still lets me prove the theorem without coercion, so even more reason.

[Adomas Baliuka]

I gather there's no "list of all common tactics" though?

[Pedro Sánchez Terraf]

ab said:

Kyle Miller Thanks! Is there a list of tactics somewhere? I've never seen simp!despite reading the "tactics" section of "Theorem Proving in Lean" and also the cheatsheet...

I saw this comprehensive list in another thread.

[Mike]

I have a question inspired by Mathematics in Lean. In the chapter on Hierarchies, S01_Basics
we are not asked to prove the lemma at the bottom, but I am still curious about how to
do it.

(sorry for the length of the post, but the example involved a lot of definitions.)

import Mathlib.Algebra.BigOperators.Ring
import Mathlib.Data.Real.Basic

variable {M : Type*}

class AddSemigroup₃ (α : Type) extends Add α where
/-- Addition is associative -/
  add_assoc₃ : ∀ a b c : α, a + b + c = a + (b + c)

@[to_additive AddSemigroup₃]
class Semigroup₃ (α : Type) extends Mul α where
/-- Multiplication is associative -/
  mul_assoc₃ : ∀ a b c : α, a * b * c = a * (b * c)

class AddMonoid₃ (α : Type) extends AddSemigroup₃ α, AddZeroClass α

@[to_additive AddMonoid₃]
class Monoid₃ (α : Type) extends Semigroup₃ α, MulOneClass α

class AddCommSemigroup₃ (α : Type) extends AddSemigroup₃ α where
  add_comm : ∀ a b : α, a + b = b + a

@[to_additive AddCommSemigroup₃]
class CommSemigroup₃ (α : Type) extends Semigroup₃ α where
  mul_comm : ∀ a b : α, a * b = b * a

class AddCommMonoid₃ (α : Type) extends AddMonoid₃ α, AddCommSemigroup₃ α

@[to_additive AddCommMonoid₃]
class CommMonoid₃ (α : Type) extends Monoid₃ α, CommSemigroup₃ α

class AddGroup₃ (G : Type) extends AddMonoid₃ G, Neg G where
  neg_add : ∀ a : G, -a + a = 0

@[to_additive AddGroup₃]
class Group₃ (G : Type) extends Monoid₃ G, Inv G where
  inv_mul : ∀ a : G, a⁻¹ * a = 1

class AddCommGroup₃ (G : Type) extends AddGroup₃ G, AddCommMonoid₃ G

@[to_additive AddCommGroup₃]
class CommGroup₃ (G : Type) extends Group₃ G, CommMonoid₃ G

def nsmul₁ [Zero M] [Add M] : ℕ → M → M
  | 0, _ => 0
  | n + 1, a => a + nsmul₁ n a

def zsmul₁ {M : Type*} [Zero M] [Add M] [Neg M] : ℤ → M → M
  | Int.ofNat n, a => nsmul₁ n a
  | Int.negSucc n, a => -nsmul₁ n.succ a

lemma zsmul_aux (A : Type) [AddCommGroup₃ A] :
  ∀ (a b : ℤ) (m : A), zsmul₁ (a * b) m = zsmul₁ a (zsmul₁ b m) := by
  simp only [zsmul₁]
  sorry

The issue is that we have to prove:

∀ (a b : ℤ) (m : A),
  (match a * b, m with
    | Int.ofNat n, a => nsmul₁ n a
    | Int.negSucc n, a => -nsmul₁ (Nat.succ n) a) =
    match a,
      match b, m with
      | Int.ofNat n, a => nsmul₁ n a
      | Int.negSucc n, a => -nsmul₁ (Nat.succ n) a with
    | Int.ofNat n, a => nsmul₁ n a
    | Int.negSucc n, a => -nsmul₁ (Nat.succ n) a

I can't get anywhere with the
match a * b, m with statement.

I would like to try something like this

lemma zsmul_aux (A : Type) [AddCommGroup₃ A] :
  ∀ (a b : ℤ) (m : A), zsmul₁ (a * b) m = zsmul₁ a (zsmul₁ b m) := by
  simp only [zsmul₁]
  match a*b, m with
  | Int.ofNat n, a =>
    ... somehow handle the positive case here, then
  | Int.negSucc n, a =>
    ... shomehow handle the negative case here.

But this does not work. Does anyone know how to finish this proof?
is using simp only [zsmul₁] a mistake?

[Kevin Buzzard]

Surely you can't just do cases on a * b: if a * b is positive then you still don't know whether $a>0$ or $a<0$ so you can't figure out what the RHS says. You will surely need to case on both a and b, and in each case figure out whether a * b is >=0 or < 0 (or alternatively do cases on all three of a, b, a*b and then use False.elim to delete the cases which can't occur).

Stepping back a bit, perhaps this is a more helpful thing to say. Lean is a cool puzzle game, but it doesn't prove theorems for you. You have to know the proof already. Do you know the maths proof of what you're trying to prove here? The first line you wrote is "let's first deal with the case where ab>=0". What's the next line of your proof? If you don't know it, then your problem is not a Lean problem, your problem is figuring out the maths proof. The Lean comes later.

[Mike]

That's cool that you can print LaTeX here.

The proof isn't that difficult, and the result isn't even interesting. I'm just trying to get the syntax, and more generally the way to "think in Lean4". Like you said, it's just a bunch of cases. However, the Lean Infoview isn't giving useful information here. I'm just trying to learn.

I asked on here, because I can't find the answer quickly from the manual...

[Kevin Buzzard]

Oh you are asking about the syntax? This would work:

lemma zsmul_aux (A : Type) [AddCommGroup₃ A] :
  ∀ (a b : ℤ) (m : A), zsmul₁ (a * b) m = zsmul₁ a (zsmul₁ b m) := by
  intros a b m
  simp only [zsmul₁]
  match a, b with
  | Int.ofNat p, Int.ofNat q =>
    simp
    sorry
  | Int.negSucc p, Int.ofNat q =>
    simp
    sorry
  | Int.ofNat p, Int.negSucc q =>
    simp
    sorry
  | Int.negSucc p, Int.negSucc q =>
    simp
    sorry

[Mike]

Here's what I have started in a "potential" proof:

lemma zsmul_aux (A : Type) [AddCommGroup₃ A] :
  ∀ (a b : ℤ) (m : A), zsmul₁ (a * b) m = zsmul₁ a (zsmul₁ b m) := by
  simp only [zsmul₁]
  intro a b m
  have h0 : (0 ≤ a ∧ 0 ≤ b) ∨ (0 ≤ a ∧ b < 0) ∨ (a < 0 ∧ 0 ≤ b) ∨ (a < 0 ∧ b < 0) := by
    cases lt_or_ge a 0
    case inl h1 =>
      right
      right
      cases lt_or_ge b 0
      case h.h.inl h2 =>
        right
        constructor
        exact h1
        exact h2
      case h.h.inr h2 =>
        left
        constructor
        exact h1
        exact h2
    case inr h1 =>
      cases lt_or_ge b 0
      case inl h2 =>
        right
        left
        constructor
        exact h1
        exact h2
      case inr h2 =>
        left
        constructor
        exact h1
        exact h2
  cases h0
  case inl h1 =>
    rcases h1 with ⟨zero_le_a, zero_le_b⟩
    set n := a*b
    have h2 : 0 ≤ n := by
      apply mul_nonneg
      exact zero_le_a
      exact zero_le_b
    sorry

To finish up the proof of case inl, we have to show:

(match n, m with
  | Int.ofNat n, a => nsmul₁ n a
  | Int.negSucc n, a => -nsmul₁ (Nat.succ n) a) =
  match a,
    match b, m with
    | Int.ofNat n, a => nsmul₁ n a
    | Int.negSucc n, a => -nsmul₁ (Nat.succ n) a with
  | Int.ofNat n, a => nsmul₁ n a
  | Int.negSucc n, a => -nsmul₁ (Nat.succ n) a

with:

A: Type
inst✝: AddCommGroup₃ A
ab: ℤ
m: A
zero_le_a: 0 ≤ a
zero_le_b: 0 ≤ b
n: ℤ := a * b
h2: 0 ≤ n

What should I do here? It would be nice to know how to get Lean4 to recognize that match n, m will match with Int.ofNat n, a (since we showed that h2: 0 ≤ n). Is this on the right track? Am I way off?

Thanks for any help!

[Kevin Buzzard]

If you are asking how I would do this proof, then I would definitely not be launching straight into it. I would plan it first. I would first prove the nsmul version, as warm-up (which presumably needs some induction). I would then make a design decision about whether I was going to prove the three other subcases individually or try and push through some trick with signs and reduce to the nsmul case (i.e. proving that zsmul (-n) is the same as -nsmul (n) etc). I would build up a bunch of useful API. I wouldn't rush in, there is an art to this stuff. Do you want to work with -n or -1-n ? This needs some thought.

As for your goal, I would have put set n := a * b with hn rather than just the bare set, and then I would do rw hn and then exact? to find the name of the lemma which says a>=0 and b>=0 implies ab>=0. It'll be called mul_nonneg or some such thing.

[Patrick Massot]

Let me quote #mil here:

You are not asked to replace those sorries with proofs. If you insist on doing it then you will probably want to state and prove several intermediate lemmas about nsmul₁ and zsmul₁.

[Mike]

Thank @Kevin Buzzard !
Your answers show me why it was left out of the tutorial. It seems like a big part of learning to "think in Lean4" is that you have to think much more strategically than usual. I've spent hours trying to figure out how to do something the wrong way, and then when I read the solutions given in the text, I realize that all I needed to do was perform some mathematical trick. I'm such a noob I usually assume there's some Lean4 magic that will do what I want, but I just don't know it yet...

Also, how did you write in LaTeX on here?

[Patrick Massot]

Use $$ where you would use $.

[Patrick Massot]

And I'm sorry I didn't keep the proofs of those lemmas when I wrote that chapter. I knew I didn't want reader to waste time on that, but I should have known that some people would do it anyway. I remember I wrote those proofs, but then I simply deleted them :sad:.

[Kevin Buzzard]

Mike is volunteering to fill them in though :-)

Mike one very frustrating thing about working with integers at this super-basic level is that it's not much fun, because the second constructor Int.negSucc is mathematically quite pathological, the function from the naturals to the integers sending x to -1-x doesn't have many nice properties. I think that I would first prove that zsmul₁ (Int.negSucc n) m = -nsmul₁ (n + 1) a, apply this everywhere, decide how to deal with the issue that (Int.negSucc n) * (Int.ofNat m) might either be a negSucc or an ofNat depending on whether m = 0 or not so this is more case splits, yuk, this really is a messy business. In fact that fact that I don't even know which case I'm in pushes me over the edge, I'm not doing it this way, I've changed my mind.

I think I would take the more mathematically sensible approach and avoid Int.negSucc completely. I would concoct some lemma saying that every integer a is either Int.ofNat p or -(Int.ofNat p) and I would do a case split on this. I would show that zsmul₁ (-Int.ofNat p) m = -nsmul_1 p m and then I'd split into the four cases a>=0, a<=0 and b>=0, b<=0 (forget negSucc, it's a pain to deal with) and do each case by juggling signs. I'd prove them all as four separate lemmas and then wrap everything together so I get several short proofs instead of one long one.

[Patrick Massot]

Clearly it wasn't that complicated when I wrote it. But I didn't want to have several intermediate lemmas distracting readers.

[Kevin Buzzard]

Another approach is to just look in std or wherever all this will be actually done, to see how they did it.

[Mike]

@Kevin Buzzard and @Patrick Massot The pdf is an excellent intro to Lean4. There's just a ton of material to learn.

I'm kind of obsessed with this problem because I'd like to know how to prove results that rely on pattern matching. For example, with

lemma zsmul_of_neg (A : Type) [AddCommGroup₃ A] :
  ∀ (a : ℤ) (m : A), zsmul₁ (-a) m = -zsmul₁ a m := by
    simp only [zsmul₁]
    intro a m
    ...

Is there a way to use cases lt_or_ge a 0 and then, for example, in the lt case, to have Lean4 know that

zsmul₁ a m = nsmul₁ a m

(because it's matching on -a)
?

[Kevin Buzzard]

That doesn't even typecheck, right?

[Kevin Buzzard]

Why don't you go through some more of the book and come back to this when you're ready for it? You're right, there is a lot to learn!