## Stream: general

### Topic: trying to understand cc

#### Johan Commelin (Apr 24 2018 at 04:27):

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 (Apr 24 2018 at 04:28):

So which tactic do I need here?

#### Simon Hudon (Apr 24 2018 at 04:29):

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

import tactic -- from mathlib

lemma ... := by solve_by_elim


#### Johan Commelin (Apr 24 2018 at 04:30):

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

#### Johan Commelin (Apr 24 2018 at 04:31):

Instead of unpacking that definition myself...

#### Simon Hudon (Apr 24 2018 at 04:31):

Have you tried it?

#### Johan Commelin (Apr 24 2018 at 04:33):

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 (Apr 24 2018 at 04:33):

squiggles under solve_by_elim

#### Simon Hudon (Apr 24 2018 at 04:33):

What error message does it give you?

#### Johan Commelin (Apr 24 2018 at 04:34):

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 (Apr 24 2018 at 04:34):

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

#### Kenny Lau (Apr 24 2018 at 04:34):

and it needs is_group_hom.one

#### Johan Commelin (Apr 24 2018 at 04:34):

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 (Apr 24 2018 at 04:35):

Ideally there is a diagram_chase tactic

#### Johan Commelin (Apr 24 2018 at 04:35):

And I think cc is very close to that

#### Johan Commelin (Apr 24 2018 at 04:35):

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

#### Kenny Lau (Apr 24 2018 at 04:35):

try mixing is_group_hom.one into the ingredient

#### Johan Commelin (Apr 24 2018 at 04:35):

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

#### Kenny Lau (Apr 24 2018 at 04:36):

have := is_group_hom.one f; solve_by_elim

#### Johan Commelin (Apr 24 2018 at 04:37):

That's not enough

Alas

#### Simon Hudon (Apr 24 2018 at 04:38):

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 (Apr 24 2018 at 04:38):

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

#### Johan Commelin (Apr 24 2018 at 04:39):

@Simon Hudon Nice!

#### Kenny Lau (Apr 24 2018 at 04:40):

@Simon Hudon I don’t get it at all

#### Simon Hudon (Apr 24 2018 at 04:40):

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 (Apr 24 2018 at 04:40):

how does apply hf even succeed

#### Kenny Lau (Apr 24 2018 at 04:41):

oh nvm I thought wrongly

#### Simon Hudon (Apr 24 2018 at 04:42):

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 (Apr 24 2018 at 04:42):

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

#### Simon Hudon (Apr 24 2018 at 04:43):

I think I would keep cc at the very least.

#### Simon Hudon (Apr 24 2018 at 04:44):

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 (Apr 24 2018 at 04:45):

Not yet, Lean doesn't like that expression

#### Simon Hudon (Apr 24 2018 at 04:46):

Error message?

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

#### Johan Commelin (Apr 24 2018 at 04:46):

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

#### Johan Commelin (Apr 24 2018 at 04:47):

invalid expression starting at xx:y

#### Simon Hudon (Apr 24 2018 at 04:47):

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 (Apr 24 2018 at 04:48):

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

#### Johan Commelin (Apr 24 2018 at 04:49):

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 (Apr 24 2018 at 04:50):

Do you have an end keyword after that?

yes

#### Johan Commelin (Apr 24 2018 at 04:51):

several lines lower

#### Simon Hudon (Apr 24 2018 at 04:53):

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

#### Simon Hudon (Apr 24 2018 at 04:53):

Also, do you have imports?

#### Johan Commelin (Apr 24 2018 at 05:02):

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 (Apr 24 2018 at 05:03):

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

#### Kenny Lau (Apr 24 2018 at 05:06):

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

#### Johan Commelin (Apr 24 2018 at 05:09):

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

#### Johan Commelin (Apr 24 2018 at 05:09):

the <coords> are of the \fo

#### Simon Hudon (Apr 24 2018 at 05:11):

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

#### Johan Commelin (Apr 24 2018 at 05:14):

Yay, that did it (-;

#### Simon Hudon (Apr 24 2018 at 05:15):

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

#### Johan Commelin (Apr 24 2018 at 05:21):

Ok, need to go now

Thanks!

#### Patrick Massot (Apr 24 2018 at 08:20):

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

#### Patrick Massot (Apr 24 2018 at 08:20):

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 (Apr 24 2018 at 08:22):

Do you have a reproducible test case?

#### Kenny Lau (Apr 25 2018 at 13:39):

Oh so cc deals with commutativity and associativity also?

#### Simon Hudon (Apr 25 2018 at 13:40):

No. Why do you say that?

#### Kenny Lau (Apr 25 2018 at 13:40):

apparently it did

#### Kenny Lau (Apr 25 2018 at 13:51):

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 (Apr 25 2018 at 13:52):

Oh interesting! I didn't think it would

Last updated: May 15 2021 at 02:11 UTC