# Zulip Chat Archive

## 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}$ where the steps are "multiply on the left by $x^{-1}$", "use (associativity and) inverse property", "use 1 property".

(2) $x$, 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

#### Mario Carneiro (Nov 19 2019 at 10:27):

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

notimport 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_cancel`

looks 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