Zulip Chat Archive

Stream: general

Topic: trying to understand cc


view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 24 2018 at 04:28):

So which tactic do I need here?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 24 2018 at 04:30):

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

view this post on Zulip Johan Commelin (Apr 24 2018 at 04:31):

Instead of unpacking that definition myself...

view this post on Zulip Simon Hudon (Apr 24 2018 at 04:31):

Have you tried it?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 24 2018 at 04:33):

squiggles under solve_by_elim

view this post on Zulip Simon Hudon (Apr 24 2018 at 04:33):

What error message does it give you?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 24 2018 at 04:34):

and it needs is_group_hom.one

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 24 2018 at 04:35):

Ideally there is a diagram_chase tactic

view this post on Zulip Johan Commelin (Apr 24 2018 at 04:35):

And I think cc is very close to that

view this post on Zulip Johan Commelin (Apr 24 2018 at 04:35):

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

view this post on Zulip Kenny Lau (Apr 24 2018 at 04:35):

try mixing is_group_hom.one into the ingredient

view this post on Zulip Johan Commelin (Apr 24 2018 at 04:35):

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

view this post on Zulip Kenny Lau (Apr 24 2018 at 04:36):

have := is_group_hom.one f; solve_by_elim

view this post on Zulip Johan Commelin (Apr 24 2018 at 04:37):

That's not enough

view this post on Zulip Johan Commelin (Apr 24 2018 at 04:37):

Alas

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Apr 24 2018 at 04:39):

@Simon Hudon Nice!

view this post on Zulip Kenny Lau (Apr 24 2018 at 04:40):

@Simon Hudon I don’t get it at all

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 24 2018 at 04:40):

how does apply hf even succeed

view this post on Zulip Kenny Lau (Apr 24 2018 at 04:41):

oh nvm I thought wrongly

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 24 2018 at 04:42):

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

view this post on Zulip Simon Hudon (Apr 24 2018 at 04:43):

I think I would keep cc at the very least.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Apr 24 2018 at 04:45):

Not yet, Lean doesn't like that expression

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 24 2018 at 04:46):

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

view this post on Zulip Johan Commelin (Apr 24 2018 at 04:47):

invalid expression starting at xx:y

view this post on Zulip 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

view this post on Zulip Simon Hudon (Apr 24 2018 at 04:48):

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

view this post on Zulip 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)),

view this post on Zulip Simon Hudon (Apr 24 2018 at 04:50):

Do you have an end keyword after that?

view this post on Zulip Johan Commelin (Apr 24 2018 at 04:50):

yes

view this post on Zulip Johan Commelin (Apr 24 2018 at 04:51):

several lines lower

view this post on Zulip Simon Hudon (Apr 24 2018 at 04:53):

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

view this post on Zulip Simon Hudon (Apr 24 2018 at 04:53):

Also, do you have imports?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 24 2018 at 05:03):

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

view this post on Zulip Kenny Lau (Apr 24 2018 at 05:06):

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

view this post on Zulip Johan Commelin (Apr 24 2018 at 05:09):

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

view this post on Zulip Johan Commelin (Apr 24 2018 at 05:09):

the <coords> are of the \fo

view this post on Zulip Simon Hudon (Apr 24 2018 at 05:11):

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

view this post on Zulip Johan Commelin (Apr 24 2018 at 05:14):

Yay, that did it (-;

view this post on Zulip Simon Hudon (Apr 24 2018 at 05:15):

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

view this post on Zulip Johan Commelin (Apr 24 2018 at 05:21):

Ok, need to go now

view this post on Zulip Johan Commelin (Apr 24 2018 at 05:21):

Thanks!

view this post on Zulip Patrick Massot (Apr 24 2018 at 08:20):

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

view this post on Zulip 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

view this post on Zulip Gabriel Ebner (Apr 24 2018 at 08:22):

Do you have a reproducible test case?

view this post on Zulip Kenny Lau (Apr 25 2018 at 13:39):

Oh so cc deals with commutativity and associativity also?

view this post on Zulip Simon Hudon (Apr 25 2018 at 13:40):

No. Why do you say that?

view this post on Zulip Kenny Lau (Apr 25 2018 at 13:40):

apparently it did

view this post on Zulip 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)))))
-/

view this post on Zulip 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