Zulip Chat Archive

Stream: new members

Topic: Applying a hypothesis to just one term in tactic mode


view this post on Zulip Julian Gilbey (Nov 19 2019 at 10:10):

Hi!
After a hiatus (paper deadline ;-), I've started trying to get my head around tactic mode (thanks for earlier advice). So I thought I'd start with a really really easy example: prove that in a group G, the identity is the unique element to satisfy xx=xx*x=x. OK, here are two maths proofs for xx=xx*x = x implies x=1x=1:

(1) xx=x    x1xx=x1x    1x=1    x=1x*x=x \implies x^{-1}xx=x^{-1}x \implies 1x=1 \implies x=1 where the steps are "multiply on the left by x1x^{-1}", "use (associativity and) inverse property", "use 1 property".

(2) xx=x    xx=x1    x=1xx=x \implies xx=x*1 \implies x=1, where the steps are "multiply the right hand side on the right by 1" and "use the left cancellation property".

The other implication (x=1x=1 implies xx=1x*x=1) is even simpler: substitute in the hypothesis and use the 1 property.

But I have so struggled to write this nicely in tactic mode :-( For approach (1), I couldn't figure out how to multiply the whole equation on the left by something (though I wonder whether congr_arg is the right way to go?), and for (2) I couldn't figure out how to rewrite just one term in the equation. The reverse implication also turned out to be much harder than it should have been.

Here's my best attempt so far, which is just ugly: any suggestions on how to improve it?

import init.algebra.group
variables {α : Type} [group α]

example [group α] (x : α) : x * x = x  x = 1 :=
begin
  apply iff.intro,
    intro h,
    have h1 : x * x = x * 1, by calc
      x * x = x  : h
        ... = x * 1 : by rw mul_one,
    rw mul_left_cancel h1,
  intro h,
  show x * x = x, by calc
    x * x = x * 1 : by rw h
      ... = x     : by rw mul_one,
end

Many thanks!

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:13):

There is no need to import init.algebra.group, because the zeroth line of a lean file imports all of init

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:14):

if you want to not import anything else, you should start the file with prelude

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:15):

@Julian Gilbey For the reverse direction: after intro h, you could do subst h or rw h. Maybe that helps?

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:15):

Probably you can also close the goal directly with simp [h]

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:16):

For the forward direction. I agree that a step like "multiply both sides with ..." doesn't have a nice tactic-verb yet.

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:18):

example [group α] (x : α) : x * x = x  x = 1 :=
begin
  split,
  { intro h,
    calc x = x * x * x⁻¹ : by rw mul_inv_cancel_right
       ... = x * x⁻¹     : by rw h
       ... = 1           : by rw mul_inv_self },
  { intro h,
    calc x * x = x * 1 : by rw h
           ... = x     : by rw mul_one },
end

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:18):

just a slight cleanup of your proof

view this post on Zulip Bhavik Mehta (Nov 19 2019 at 10:19):

Here's how I'd do it, basically following your (2) for the first part:

example [group α] (x : α) : x * x = x  x = 1 :=
begin
  split,
    intro h,
    apply mul_right_cancel,
    rw [h, one_mul],
  intro h,
  rw [h, mul_one]

(I've also deliberately avoided using simp and such so you can see what's going on)

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:20):

variables {α : Type} [group α]

lemma mul_on_left {y z : α} (x : α) (h : x * y = x * z) : y = z :=
mul_left_cancel h

example [group α] (x : α) : x * x = x  x = 1 :=
begin
  split,
  { intro h,
    apply mul_on_left x,
    rwa mul_one, },
  { rintro rfl, exact mul_one _ },
end

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:22):

The golfed proof:

example [group α] (x : α) : x * x = x  x = 1 :=
by rw [ @mul_left_cancel_iff _ _ x x, mul_one]

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:23):

I wouldn't mind having mul_on_left and friends in mathlib

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:24):

why do all theorems have to be tactics too

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:24):

there is already a theorem for this, I used it

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:24):

It's not a tactic. It's a an existing theorem but with different binders

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:25):

And a name that mimics the informal language

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:25):

Actually, core is violating mathlib conventions in this case. The variable being cancelled should be explicit

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:26):

Luckily core doesn't depend on mathlib. So it doesn't have to give a thing for mathlib conventions (-;

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:26):

it is sometimes problematic when people get the wrong idea from the way a theorem from core is stated

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:27):

or named

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:29):

But core doesn't depend on those people's ideas either. So again, it doesn't really care [/sarcasm]

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:29):

We should have a tactic for applying congr_arg though. The term is finicky

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:32):

That is, the replace line here:

example [group α] (x : α) : x * x = x  x = 1 :=
begin
  split,
  { sorry },
  { intro h,
    replace h := congr_arg (λ a, x * a) h, dsimp at h,
    rw [h, mul_one] },
end

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:34):

That's getting close to Kevin's modified apply that also works on hyps

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:34):

Maybe this should be congr (*) x at h?

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:35):

Or congr', if the other is locked into ...

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:35):

I'm thinking something like congr_hyp x * _ with h

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:36):

You should be able to provide more than one placeholder, and more than one hypothesis

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:37):

Wait, why with instead of at?

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:37):

it's not rewriting h

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:37):

my example rewrote h but that's probably not always desirable, since this move loses information

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:38):

A crazier idea is congr_hyp x * h but I don't know if we can typecheck that enough to figure out what's happening

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:38):

If you don't replace h you need the user to supply a new name as well

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:38):

congr_hyp h2 : x * h

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:39):

the equalities might also be terms, they aren't necessarily from the context

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:39):

Hmm.. I think I prefer congr_hyp h2 : x * _ with h

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:39):

so perhaps using [h]

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:39):

or maybe using h... I don't know the difference between with and using

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:40):

using uses terms

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:40):

Ok, then I prefer using

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:40):

with is always names (usually new names generated by the tactic)

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:41):

Downside of using placeholders is then you can't actually use literal placeholders

view this post on Zulip Johan Commelin (Nov 19 2019 at 10:41):

Aha... we need better syntax to distinguish those

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:42):

something like x * ‹h› might work, but we need to be able to capture the notation and control elaboration

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:46):

Eh, too much work. How about using placeholders for simple situations and another keyword for when you still need placeholders, i.e. congr_hyp : x * a with a using [h]

view this post on Zulip Mario Carneiro (Nov 19 2019 at 10:47):

I don't really like that everything is separated here but I'm not sure if parsing will work with other setups, e.g. congr_hyp : x * a using [a : h]

view this post on Zulip Reid Barton (Nov 19 2019 at 16:40):

I think you want to replace the hypothesis more often than not. If you don't want to, you could just copy the hypothesis with have first, right?

view this post on Zulip Reid Barton (Nov 19 2019 at 16:49):

You should be able to provide more than one placeholder, and more than one hypothesis

Could you give an example of how this would look?

view this post on Zulip Reid Barton (Nov 19 2019 at 16:50):

Oh, like if h1 : a = b and h2 : c = d, then you write something like congr_hyp _ + _ using h1 h2 and you get a proof of a + c = b + d?

view this post on Zulip Julian Gilbey (Nov 19 2019 at 18:33):

if you want to not import anything else, you should start the file with prelude

Ah, thanks @Mario Carneiro - I didn't know that!

view this post on Zulip Julian Gilbey (Nov 19 2019 at 18:36):

Probably you can also close the goal directly with simp [h]

Ooh, subst h followed by exact mul_one 1 works, and so does rw [h, mul_one], and so does simp [h]. Thanks! So much nicer than what I did ;-)

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 18:37):

For the forward direction. I agree that a step like "multiply both sides with ..." doesn't have a nice tactic-verb yet.

This just happened to me again: I had h : list.of_fn f = [] with f : fin n -> X and I wanted to deduce that n was 0 (this was not the goal). The theorem list.length_of_fn tells me that length(list.of_fn f) = n so I just wanted to "apply list.length to h" and then rw list.length_of_fn. I don't know an easy way to do this in tactic mode without this apply idea.

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 18:38):

Probably you can also close the goal directly with simp [h]

Ooh, subst h followed by exact mul_one 1 works, and so does rw [h, mul_one], and so does simp [h]. Thanks! So much nicer than what I did ;-)

Of course, the reason that simp might help is that someone already proved all or most of what you wanted, probably in term mode, and then tagged it [@simp].

view this post on Zulip Julian Gilbey (Nov 19 2019 at 18:44):

Here's how I'd do it, basically following your (2) for the first part:

example [group α] (x : α) : x * x = x  x = 1 :=
begin
  split,
    intro h,
    apply mul_right_cancel,
    rw [h, one_mul],
  intro h,
  rw [h, mul_one]

(I've also deliberately avoided using simp and such so you can see what's going on)

Thanks @Bhavik Mehta Now this is interesting: apply mul_right_cancel can apply the lemma backwards, which somewhat surprises me. How does it know that it's a two-way implication?

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 18:53):

If you hover over mul_right_cancel you'll see its definition: mul_right_cancel : ∀ {α : Type} [_inst_1 : right_cancel_semigroup α] {a b c : α}, a * b = c * b → a = c. So it's a one way implication. And apply applies a function, so it's all consistent.

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 18:55):

variable (G : Type*)
example [group G] (x : G) : x * x = x  x = 1 :=
begin
  split,
    intro h,
    apply @mul_right_cancel _ _ _ x,
    rw [h, one_mul],
  intro h,
  rw [h, mul_one]
end

This way doesn't have metavariables in.

view this post on Zulip Bhavik Mehta (Nov 19 2019 at 19:29):

@Julian Gilbey Kevin's answered the question well - I'll add that apply works by backwards reasoning using functions, so it essentially only applies lemmas backwards

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 19:30):

proposition world of the natural number game gets people proving theorems backwards.

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 19:32):

-- computer scientist
example (A B C D : Prop) (hAB : A  B) (hBC : B  C) (hCD : C  D) : A  D :=
begin
  intro a,
  apply hCD,
  apply hBC,
  apply hAB,
  assumption
end

-- mathematician
example (A B C D : Prop) (hAB : A  B) (hBC : B  C) (hCD : C  D) : A  D :=
begin
  intro a,
  have b := hAB a,
  have c := hBC b,
  exact hCD c,
end

view this post on Zulip Kevin Buzzard (Nov 19 2019 at 19:32):

We think forwards, but it doesn't half clutter up the tactic state.

view this post on Zulip Bhavik Mehta (Nov 19 2019 at 19:33):

I'd argue we do a bit of both

view this post on Zulip Julian Gilbey (Nov 20 2019 at 17:54):

Ah, thanks @Bhavik Mehta and @Kevin Buzzard - I think I'm getting it! How does this sound: apply says something along the lines of "we're trying to prove B; we have a theorem of the form A => B, and we apply this theorem, then we only need to prove A in order to be done". So in this case, we're trying to prove x=1, and applying mul_right_cancel therefore says "if we can reach x*y=1*y for some y, then we're done, because we can just apply mul_right_cancel at that point". (And that explains why the state after apply mul_right_cancellooks like this.) So when the docs talk about "rewriting the target", it means something like: apply changes our target by saying "if we get to an earlier point, we are effectively done".

view this post on Zulip Mario Carneiro (Nov 20 2019 at 17:56):

you can think of apply T as saying "by T, it suffices to show..."

view this post on Zulip Kevin Buzzard (Nov 20 2019 at 17:56):

It's doing the proof backwards. The CS people like it

view this post on Zulip Kevin Buzzard (Nov 20 2019 at 17:56):

Because it's writing the function forward


Last updated: May 15 2021 at 02:11 UTC