general introductory advice around tactics

Stream: new members

[JJ]

Hello! I am working my way through Analysis I as a way to learn the theorem proving side of Lean and had a couple of general questions. These are not specific to Analysis I -- they're just questions I had (being new to tactics) so I figured I'd put them here.

1. If I have a hypotheses ¬A and a goal A, how do I tell Lean this is false? (Encountering this using by_cases.)

2. Is there a nicer way to make a new hypothesis than (for example) constructing x++ = y++ via have hxy : x++ = a := hx; symm at hy; rw [hy] at hxy (for hx : x++ = a, hy : y++ a)? Ideally, I'd like to be able to do something like have hxy : x++ = y++ := (rw [(symm hy)] at hx) (fictitious syntax) in a sorta functional manner, but I don't know if this is possible.
   have hxy : x++ = y++ := hx.trans hy.symm

3. On a similar tactic, can I get abel or some other simple rewriting tactic to rewrite a goal for me overtly? i.e. I have hx : a + c = b + c + x, and I would like to say like. replace hx := c + a = c + (b + x) by abel.

4. Is there a way to see the tactics simp applied to close a goal?
   simp?

5. Is apply And.intro or constructor more idiomatic?

6. How do I apply a theorem taking arguments to a goal? Specifically, I have ⊢ c + a = c + (b + x) as my goal, and I have a theorem add_left_cancel (a b c : Nat) (habc = a + b = a + c) : b = c. I would like to do apply add_left_cancel c a (b + x) <goal>, but this doesn't work.
   forgot about backwards reasoning! normal apply works normally

7. I have a hypothesis h : d ≠ 0 and a theorem isPos_iff (n : Nat) : n.IsPos ↔ n ≠ 0. How do I apply isPos_iff to the hypothesis? I think it is that isPos_iff takes an argument that is messing me up. This might be similar to the previous question, but since this is an ↔ I think that I should be able to do it with rewrite.

Thanks for any help!

[Kenny Lau]

2:

import Mathlib

example : 37 = 51 := by
  transitivity 100
  · show 37 = 100
    sorry
  · show 100 = 51
    sorry

[Aaron Liu]

rw [← hy] and rw [hy.symm] are both things you can do

[Kenny Lau]

3:

import Mathlib

example {a b c x : ℤ} (hx : a + c = b + c + x) : 1 + (c + a) = c + (b + x) + 1 := by
  rw [show c + a = c + (b + x) by abel_nf at hx ⊢; exact hx]
  abel

[Kenny Lau]

4: simp?

[Kenny Lau]

5:

import Mathlib

example : 0 = 1 ∧ 1 = 0 := by
  refine ⟨?_, ?_⟩
  · sorry
  · sorry

[Aaron Liu]

You can also have hxy : x++ = y++ := hx.trans hy.symm

[Kenny Lau]

1:

import Mathlib

example {A : Prop} (ha : A) (hna : ¬ A) : False := by
  exact absurd ha hna

[Aaron Liu]

For number 6, what you are doing doesn't seem logically valid

[Kenny Lau]

6: what you're asking is not mathematically sound.

[Kenny Lau]

but there's rw [add_left_inj] instead

[Kenny Lau]

7 : rw [\l isPos_iff] at h

[Matthew Jasper]

For 6 there's also congr

[JJ]

6: Oh right yes, if I'm applying a theorem to a goal I'm reasoning backwards...

[Michael Rothgang]

Another option for 1:

import Mathlib
example {A : Prop} (ha : A) (hna : ¬ A) : False := by
  apply hna ha

[Michael Rothgang]

This works because ¬ A is defined to be A → False

[JJ]

Okay, working through understanding these. I have run into some rw confusion, though. I have an ih : n + b = 0 → n = 0, an h : n++ + b = 0, and a goal ⊢ n++ + b = 0 (for (b n : Nat). I would like to somehow... apply ih to h and obtain n++ = 0.

But I can't apply ih. I think there's something I don't understand going on there: n : Nat and n++ : Nat so I don't see why I can't apply ih.

But there's also something else I don't understand going on: I can rw [ih] at h (giving h : 0++ + b = 0) and I can rw [← ih] at h (giving h : n++ + b = n). What is going on here? I thought rewrite only functioned on equalities or biconditionals? And why is it transforming my hypotheses to false statements?

[Kyle Miller]

Rewrite supports conditional rewrites. It interprets ih as n = 0, and it adds an extra n + b = 0 goal.

[JJ]

Hm! Okay, that's a little unexpected. I see the new case hind now though.

[Aaron Liu]

JJ said:

Okay, working through understanding these. I have run into some rw confusion, though. I have an ih : n + b = 0 → n = 0, an h : n++ + b = 0, and a goal ⊢ n++ + b = 0 (for (b n : Nat). I would like to somehow... apply ih to h and obtain n++ = 0.

have hnsucc := ih h

[JJ]

That doesn't work because ih expects n + b = 0, but h is n++ + b = 0.

[Aaron Liu]

ok so explain again why you think applying ih to h is something you can do here

[JJ]

Because ih expects something of the form (n : Nat) + (b : Nat) = 0 and h is of the form (n++ : Nat) + (b : Nat) = 0.

[Aaron Liu]

yes they don't match because n++ is not the same as n

[JJ]

Right. I'm trying to understand why this is.

[Aaron Liu]

You're trying to understand why n++ is not the same as n?

[JJ]

No, I'm trying to understand why ih cannot take in h.

[Aaron Liu]

ih cannot take in h because ih eats a proof of n + b = 0 and h is a proof of n++ + b = 0 and n + b = 0 is not the same as n++ + b = 0

[JJ]

Right, but n and b are arbitrary. So I don't get why n++ can't be considered n for the purpose of ih.

[Aaron Liu]

no they're not arbitrary

[Aaron Liu]

since you have intro'd them they are fixed now

[JJ]

Hm.

[Aaron Liu]

if it was arbitrary then ih would look like ∀ k l, k + l = 0 → k = 0

[Aaron Liu]

but no it looks like n + b = 0 → n = 0

[Aaron Liu]

you have fixed them here

[JJ]

Like my full tactic state is (b n : Nat); (ih : n + b = 0 → n = 0); (h : n++ + b = 0) and I'm trying to derive n++ = 0. I look at this, I think "hm -- ih tells me that given some arbitrary n and b, if n + b = 0 then n = 0." I look at this again, I think "hm -- h tells me that for some n++ I have n++ + b = 0". So then I think I can apply h to ih but I obviously can't and now I'm confused.

[Aaron Liu]

you are reverting your variables incorrectly

[JJ]

What does that mean?

[Aaron Liu]

I see this as

I have b and n which are Nat
I have ih which tells me that if I give it a proof of n + b = 0 then it will give me a proof of n = 0
I have h which tells me that n++ + b = 0
I need to prove that n++ = 0

[Aaron Liu]

note the lack of arbitrariness here

[JJ]

Mmm, I see.

[JJ]

Ah! Right okay cool. I think I just closed it with induction. Which makes sense now, I think I was implicitly failing to consider the n = 0 case?

[JJ]

Or rather I guess this was by cases? Hrm. When n = 0, h : 0++ + b = 0 is false.

[JJ]

When n > 0... grr, I'm not sure what I actually just did. Is there a nice by_cases tactic that I should be using (over induction) for introductory stuff? by_cases itself is annoying, because it only takes in p and has the two cases be p and ¬p, and so far I don't actually know how to transform ¬a=0 into a ≠ 0. (And into a > 0, for that matter.)

[Aaron Liu]

¬a=0 is defeq to a ≠ 0

[Aaron Liu]

that means when you unfold all the definitions you get the same thing

[Aaron Liu]

so they're usually interchangeable

[Aaron Liu]

making this the same as a > 0 is a theorem

[JJ]

Ah, I found an example of what I was having trouble with. Yeah, it was not knowing how to convert ¬a = 0 to a ≠ 0.

[JJ]

So I've got a h : ¬d = 0 and an isPos_iff : (n : Nat) : n.isPos ↔ n ≠ 0. I couldn't rewrite [← isPos_iff] at h. But if I put replace h : d ≠ 0 := sorry before, rw [← isPos_iff] at h works fine.

[JJ]

It looks now like I can replace that sorry with h itself, but is there a way to avoid replace altogether?

[Aaron Liu]

rewrite with docs#ne_eq

[Matt Diamond]

Did people misread #1 or did JJ miswrite it? It says "If I have a hypotheses ¬A and a goal A, how do I tell Lean this is false?"

If you have a hypothesis ¬A and your goal is A, it's likely that something has gone wrong

[JJ]

Ah, sorry. The context is that's within a by_cases.

[Matt Diamond]

the context doesn't really matter, I'm asking if the goal is A or if the goal is False and you have both A and ¬A

[JJ]

The goal is A. I basically want to use absurd. Let me see if I can find where I was having trouble doing so.

[JJ]

Sorry! I can't find the place I was running into that. I think I rewrote it to not use by_cases.

[JJ]

Though speaking of by_cases: I have a lot of revert x; apply induction (this is equivalent to Mathlib induction I think, but is a theorem in the first chapter of this Analysis I text) scattered throughout, including in some places where I only really need by_cases. But in a lot of those induction places simp works where it doesn't in by_cases. Is by_cases the idiomatic cases tactic to use, or is there something better?

[Aaron Liu]

For doing cases it depends on what I'm casing on

[Aaron Liu]

sometimes I use by_cases but if there's a more convenient form I will use obtain with the lemma

[Aaron Liu]

like for example docs#eq_or_ne, docs#eq_or_lt_of_le, docs#Set.eq_empty_or_nonempty

[Matt Diamond]

oh yeah, or docs#Option.eq_none_or_eq_some ... doing rcases or obtain with those can be useful if you need more than just a simple P ∨ ¬P

[Aaron Liu]

or sometimes I will use match if I have a way of solving it for all n > 8 for example, and the n ≤ 8 is a case bash

[JJ]

Nice thanks! It seems like match is pretty amenable to what I'd been using apply induction for.

[Matt Diamond]

if you're calling revert before induction you might want to read up on the generalizing option

[JJ]

wow yeah match n with | 0 => ... | m++ => ... is really nice

[JJ]

I think this'll go away next chapter! This is using an induction theorem on a definition of Nat that is not the standard one

[JJ]

Wow... I can just. leave off branches of the match that lead to contradictions. That's very cool

[Aaron Liu]

wait until you hear about recursively calling the theorem from inside itself

[JJ]

Is there a nice way to clean this proof up? Specifically, I'm wondering

1. when my goal is 0 = 0 ∨ m = 0 how to tell Lean "look at the left side"?
   tauto

2. if there's a way to combine the two matches into one (just using (n,m) with cases (0,0), (0,_), (_,0), (a++,b++) didn't give me that n or m are zero in the first three cases)
   yes! just n,m. no parentheses around any match pattern.

3. I apply succ_ne at h to get h : False and then follow it by contradiction -- any way to do it shorter?

lemma Nat.mul_eq_zero (n m: Nat) : n * m = 0 ↔ n = 0 ∨ m = 0 := by
  apply Iff.intro
  . intro h
    match n with
    | 0 => simp? -- goal: ⊢ 0 = 0 ∨ m = 0
    | a++ =>
      match m with
      | 0 => simp?
      | b++ =>
        rw [succ_mul, add_succ] at h
        apply succ_ne at h -- after this, h : False
        contradiction
  . intro h
    rcases h with left | right
    . rw [left, zero_mul]
    . rw [right, mul_zero]

[Niels Voss]

For 2., I think you can do something like

match n, m with
| 0, 0 => sorry
| 0, b++ => sorry
| a++, 0 => sorry
| a++, b++ => sorry

[JJ]

Oh! Thanks. For some reason I thought you needed ( ). That works nicely.

[JJ]

lemma Nat.mul_eq_zero (n m: Nat) : n * m = 0 ↔ n = 0 ∨ m = 0 := by
  refine ⟨?_, ?_⟩
  . intro h
    match n, m with
    | 0, _ | _, 0 => tauto
    | a++, b++ =>
      rw [succ_mul, add_succ] at h
      apply succ_ne at h -- after this, h : False
      contradiction
  . intro h
    rcases h with left | right
    . rw [left, zero_mul]
    . rw [right, mul_zero]

[JJ]

cool :)

[Niels Voss]

As for your last question, remember that:

• False.elim takes in an element of False and produces anything
• exfalso turns the current goal into False
• apply succ_ne at h basically does replace h := succ_ne h

So technically, you could replace apply succ_ne at h; contradiction with exact (succ_ne h).elim, although it's debatable whether this is actually "better"

[Niels Voss]

You could also do nomatch succ_ne h. This is because False is an inductive type with no constructor, so when you pattern match on it, you actually don't even have to provide any cases.

[Matt Diamond]

when my goal is 0 = 0 ∨ m = 0 how to tell Lean "look at the left side"?

you listed tauto as the answer (and that will work) but for the more general case of focusing on the left branch of P ∨ Q you can use left