Zulip Chat Archive

Stream: new members

Topic: trouble with introv


view this post on Zulip Charlie Conneen (Oct 19 2020 at 21:24):

As I understand it, introv is supposed to automatically introduce variables in a theorem. Looking over examples, it seems it should be able to simplify the forall in my hypothesis in the following example, but it doesn't:

import algebra.group.basic
universe u
variables {G : Type u} [group G]

lemma id_unique : ∃! e : G,  x : G, e * x = x  x * e = x :=
begin
apply exists_unique.intro (1 : G),
intros,
split,
exact one_mul x,
exact mul_one x,
introv h,
sorry
end

any ideas as to what's going on here? I thought applying introv where I did would produce 3 hypotheses, y : G, x : G and h : y * x = x ∧ x * y = x. But that's not quite what happens.

view this post on Zulip Alex J. Best (Oct 19 2020 at 21:26):

Can you include all the imports and defs in your #mwe so we can try it out and see what the goal state is?

view this post on Zulip Charlie Conneen (Oct 19 2020 at 21:26):

only import is algebra.group.basic

view this post on Zulip Alex J. Best (Oct 19 2020 at 21:27):

and variables {G : Type} [ group G] i'm guessing?

view this post on Zulip Charlie Conneen (Oct 19 2020 at 21:27):

naturally

view this post on Zulip Charlie Conneen (Oct 19 2020 at 21:27):

well, {G : Type*}

view this post on Zulip Alex J. Best (Oct 19 2020 at 21:28):

Right but it helps people reading your question if you include those lines so we don't have to guess and type them out to see it in vscode!

view this post on Zulip Bryan Gin-ge Chen (Oct 19 2020 at 21:30):

Including all the imports, variable declarations, etc. also makes it so that your snippet will immediately work in the Lean playground (hover over the snippet and click one of the buttons that appears in the top right).

view this post on Zulip Charlie Conneen (Oct 19 2020 at 21:31):

I'm well aware, thank you, just forgot to include them when pasting in. I've edited the mwe

view this post on Zulip Alex J. Best (Oct 19 2020 at 21:33):

To answer your question anyway, introv is doing what it should, its introducing the hypothesis that ∀ (x : G), y * x = x ∧ x * y = x, there is an important difference between

 (y : G), ( (x : G), y * x = x  x * y = x)  y = 1

and

 (y : G),  (x : G), y * x = x  x * y = x  y = 1

to proceed from where you are you can specialize h 1 to "evaluate the hypothesis" at a useful point.

view this post on Zulip Charlie Conneen (Oct 19 2020 at 21:36):

I see. The examples baked into Lean were a bit misleading at first glance, because this

example :  a b : nat, a = b   c, b = c  a = c :=
begin
  introv h₁ h₂,
  exact h₁.trans h₂
end

initially seemed to be analogous to the context of the above lemma. Thanks for clarifying.


Last updated: May 13 2021 at 05:21 UTC