Stream: new members

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

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 $x*x=x$. OK, here are two maths proofs for $x*x = x$ implies $x=1$:

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

(2) $x$x=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=1$ implies $x*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!

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

Mario Carneiro (Nov 19 2019 at 10:14):

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

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?

Johan Commelin (Nov 19 2019 at 10:15):

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

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.

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


Mario Carneiro (Nov 19 2019 at 10:18):

just a slight cleanup of your proof

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)

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


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]


Johan Commelin (Nov 19 2019 at 10:23):

I wouldn't mind having mul_on_left and friends in mathlib

Mario Carneiro (Nov 19 2019 at 10:24):

why do all theorems have to be tactics too

Mario Carneiro (Nov 19 2019 at 10:24):

there is already a theorem for this, I used it

Johan Commelin (Nov 19 2019 at 10:24):

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

Johan Commelin (Nov 19 2019 at 10:25):

And a name that mimics the informal language

Mario Carneiro (Nov 19 2019 at 10:25):

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

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 (-;

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

or named

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]

Mario Carneiro (Nov 19 2019 at 10:29):

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

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


Johan Commelin (Nov 19 2019 at 10:34):

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

Johan Commelin (Nov 19 2019 at 10:34):

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

Johan Commelin (Nov 19 2019 at 10:35):

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

Mario Carneiro (Nov 19 2019 at 10:35):

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

Mario Carneiro (Nov 19 2019 at 10:36):

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

Johan Commelin (Nov 19 2019 at 10:37):

Wait, why with instead of at?

Mario Carneiro (Nov 19 2019 at 10:37):

it's not rewriting h

Mario Carneiro (Nov 19 2019 at 10:37):

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

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

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

Mario Carneiro (Nov 19 2019 at 10:38):

congr_hyp h2 : x * h

Mario Carneiro (Nov 19 2019 at 10:39):

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

Johan Commelin (Nov 19 2019 at 10:39):

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

Mario Carneiro (Nov 19 2019 at 10:39):

so perhaps using [h]

Johan Commelin (Nov 19 2019 at 10:39):

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

Mario Carneiro (Nov 19 2019 at 10:40):

using uses terms

Johan Commelin (Nov 19 2019 at 10:40):

Ok, then I prefer using

Mario Carneiro (Nov 19 2019 at 10:40):

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

Mario Carneiro (Nov 19 2019 at 10:41):

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

Johan Commelin (Nov 19 2019 at 10:41):

Aha... we need better syntax to distinguish those

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

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]

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]

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?

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?

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?

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!

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 ;-)

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.

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].

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?

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.

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.

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

Kevin Buzzard (Nov 19 2019 at 19:30):

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

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


Kevin Buzzard (Nov 19 2019 at 19:32):

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

Bhavik Mehta (Nov 19 2019 at 19:33):

I'd argue we do a bit of both

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".

Mario Carneiro (Nov 20 2019 at 17:56):

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

Kevin Buzzard (Nov 20 2019 at 17:56):

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

Kevin Buzzard (Nov 20 2019 at 17:56):

Because it's writing the function forward

Last updated: May 15 2021 at 02:11 UTC