trying to understand cc

Stream: general

[Johan Commelin]

I had hoped this would work:

universes u

variables
{A : Type u} [group A]
{B : Type u} [group B]
{f : A → B} [is_group_hom f]

lemma test (hf : ∀ x, (f x = 1 → x = 1)) (x : A) (hfx : f x = 1) : x = 1 :=
begin
cc
end

[Johan Commelin]

So which tactic do I need here?

[Simon Hudon]

That's not the kind of stuff it does. Try:

import tactic -- from mathlib

lemma ... := by solve_by_elim

[Johan Commelin]

Next goal: just have hf : function.injective f as hypothesis

[Johan Commelin]

Instead of unpacking that definition myself...

[Simon Hudon]

Have you tried it?

[Johan Commelin]

Yes. Then it fails:

universes u

variables
{A : Type u} [group A]
{B : Type u} [group B]
{f : A → B} [is_group_hom f]

lemma test (hf : function.injective f) (x : A) (hfx : f x = 1) : x = 1 :=
begin
solve_by_elim
end

[Johan Commelin]

squiggles under solve_by_elim

[Simon Hudon]

What error message does it give you?

[Johan Commelin]

assumption tactic failed
state:
A : Type u,
_inst_1 : group A,
B : Type u,
_inst_2 : group B,
f : A → B,
_inst_3 : is_group_hom f,
hf : function.injective f,
x : A,
hfx : f x = 1
⊢ x = 1

[Kenny Lau]

to be fair the proof needs to go like f x = f 1 and then x = 1

[Kenny Lau]

and it needs is_group_hom.one

[Johan Commelin]

Yeah, there is a bit more to be done... but I think there should be a tactic that can do that for me

[Johan Commelin]

Ideally there is a diagram_chase tactic

[Johan Commelin]

And I think cc is very close to that

[Johan Commelin]

It only needs to know little facts like this lemma and some similar stuff.

[Kenny Lau]

try mixing is_group_hom.one into the ingredient

[Johan Commelin]

And then it would be able to prove the five lemma on its own

[Kenny Lau]

have := is_group_hom.one f; solve_by_elim

[Johan Commelin]

That's not enough

[Johan Commelin]

Alas

[Simon Hudon]

This one should work:

lemma test (hf : function.injective f) (x : A) (hfx : f x = 1) : x = 1 :=
begin
  have := is_group_hom.one f,
  apply hf, cc,
end

[Johan Commelin]

Ok, so have := \fo x, (fx = 1 \to x = 1). How should I prove that? Is it a one-liner?

[Johan Commelin]

@Simon Hudon Nice!

[Kenny Lau]

@Simon Hudon I don’t get it at all

[Simon Hudon]

If you want to go fully anonymous (not name your assumptions like this and hf) you can do:

begin
  have := is_group_hom.one f,
  apply_assumption, cc
end

[Kenny Lau]

how does apply hf even succeed

[Kenny Lau]

oh nvm I thought wrongly

[Simon Hudon]

You apply it to x = 1 and hf is hf : ∀ x y, f x = f y → x = y. When you apply it, you instantiate it with x := x, y := 1 so the antecedent becomes f x = f 1. Your idea with have gets us this : f 1 = 1

[Kenny Lau]

I mean, I would just write the proof in term mode

[Simon Hudon]

I think I would keep cc at the very least.

[Simon Hudon]

Ok, so have := \fo x, (fx = 1 \to x = 1). How should I prove that? Is it a one-liner?

Did you find an answer for this?

[Johan Commelin]

Not yet, Lean doesn't like that expression

[Simon Hudon]

Error message?

I would expect it to work but I don't think that's what you're looking for

[Johan Commelin]

And the problem is not fx, I changed that to f x

[Johan Commelin]

invalid expression starting at xx:y

[Simon Hudon]

have := expr uses expr as a proof of an unnamed proposition. That proposition is just the type of the expression. If expr is the proposition you want to prove, you write have : expr

[Simon Hudon]

Can you show me the whole proof? Maybe you missed a comma

[Johan Commelin]

universes u

variables
{A : Type u} [group A]
{B : Type u} [group B]
{f : A → B} [is_group_hom f]

lemma test (hf : function.injective f) (x : A) (hx : x ∈ ker f) : x = 1 :=
begin
have := is_group_hom.one f,
have : (∀ x, (f x = 1 → x = 1)),

[Simon Hudon]

Do you have an end keyword after that?

[Johan Commelin]

yes

[Johan Commelin]

several lines lower

[Simon Hudon]

Can you show me what the rest of the proof is?

[Simon Hudon]

Also, do you have imports?

[Johan Commelin]

import tactic
import init.function
import algebra.group
import group_theory.subgroup

universes u

variables
{A : Type u} [group A]
{B : Type u} [group B]
{f : A → B} [is_group_hom f]

lemma test (hf : function.injective f) (x : A) (hx : x ∈ ker f) : x = 1 :=
begin
have := is_group_hom.one f,
have : (∀ x, (f x = 1 → x = 1))
end

[Johan Commelin]

All the other stuff in that file is wrapped withing a section

[Kenny Lau]

hf $ hx.trans $ eq.symm $ is_group_hom.one f

[Johan Commelin]

I first need to get rid of an error message: invalid expression starting at <coords>

[Johan Commelin]

the <coords> are of the \fo

[Simon Hudon]

I don't see a problem there. Try restarting your Lean server

[Johan Commelin]

Yay, that did it (-;

[Simon Hudon]

Unfortunately, that's a common solution to problems :stuck_out_tongue_winking_eye:

[Johan Commelin]

Ok, need to go now

[Johan Commelin]

Thanks!

[Patrick Massot]

I think this happens more frequently since @Gabriel Ebner enabled the new "region of interest" thing

[Patrick Massot]

It's nice to have Lean reacting quicker but I did get quite a lot of those random invalid expression starting at <coords> yesterday

[Gabriel Ebner]

Do you have a reproducible test case?

[Kenny Lau]

Oh so cc deals with commutativity and associativity also?

[Simon Hudon]

No. Why do you say that?

[Kenny Lau]

apparently it did

[Kenny Lau]

theorem test (m n : nat) : m + n = n + m := by cc
#print test
/-
theorem test : ∀ (m n : ℕ), m + n = n + m :=
λ (m n : ℕ),
  of_eq_true (eq_true_intro (eq.symm (eq.trans (eq.refl (n + m)) (eq.symm (is_commutative.comm has_add.add m n)))))
-/

[Simon Hudon]

Oh interesting! I didn't think it would