Applying a hypothesis to just one term in tactic mode

Stream: new members

[Julian Gilbey]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

just a slight cleanup of your proof

[Bhavik Mehta]

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]

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]

The golfed proof:

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

[Johan Commelin]

I wouldn't mind having mul_on_left and friends in mathlib

[Mario Carneiro]

why do all theorems have to be tactics too

[Mario Carneiro]

there is already a theorem for this, I used it

[Johan Commelin]

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

[Johan Commelin]

And a name that mimics the informal language

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

or named

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

Wait, why with instead of at?

[Mario Carneiro]

it's not rewriting h

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

congr_hyp h2 : x * h

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

so perhaps using [h]

[Johan Commelin]

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

[Mario Carneiro]

using uses terms

[Johan Commelin]

Ok, then I prefer using

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

Aha... we need better syntax to distinguish those

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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

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

[Kevin Buzzard]

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

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

[Bhavik Mehta]

I'd argue we do a bit of both

[Julian Gilbey]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Because it's writing the function forward