## Stream: new members

### Topic: Why doesn't dunfold work here?

#### Chris M (Aug 26 2020 at 06:26):

I have the following:

import algebra
--import data.equiv
import group_theory.group_action
import algebra.group.hom

variables (G:Type*) [h:group G]

open equiv
open function

def cayley (G:Type*) [h:group G] : G →* perm G :=
begin
let f: G → perm G := fun g1:G, by
{
let p: G → G := (fun g, g1 * g),
let pinv: G → G := (fun g, g1⁻¹ * g),
have hleftinv: function.left_inverse pinv p, from by
{
dunfold left_inverse,
intro x,
dunfold p,

},
have hrightinv: function.right_inverse pinv p, from sorry,
exact equiv.mk p pinv hleftinv hrightinv,
},
have h1: f 1 = 1, from sorry,
have h2: ∀ (x y : G), f (x * y) = f x * f y, from sorry,
exact ⟨ f, h1, h2 ⟩
end


Hovering above intro x, gives me the goal state

G: Type ?
h: group G
g1: G
p: G → G := λ (g : G), g1 * g
pinv: G → G := λ (g : G), g1⁻¹ * g
x: G
⊢ pinv (p x) = x


I want to unfold pinv (p x), but dunfold p gives me unknown declaration 'p', even though clearly p is part of the assumptions.
Also, just applying the group tactic doesn't work either, to my surprise. It reduces the goal to pinv (p x) * x ^ -1 = 1.
library_search does work by the way, but I don't understand why the previous things don't.

#### Scott Morrison (Aug 26 2020 at 06:59):

dsimp [p] works fine. I tend not to use dunfold much.

#### Kyle Miller (Aug 26 2020 at 07:17):

I've noticed that dunfold doesn't work with let-bound local definitions. I'm not sure why.

A workaround that might be worth knowing in case dsimp doesn't work is set, which lets you define an equation, too:

set p: G → G := (fun g, g1 * g) with hp,


and then you can do rw hp. Another thing worth knowing is delta to expand definitions, though it doesn't work here for some reason.

#### Chris M (Aug 26 2020 at 08:54):

I'm actually getting another error on this: The phrasehave h1: f 1 = 1, from sorry doesn't give any errors, but I get an error when I write have h1: (f 1).to_fun = 1, from sorry, namely:

failed to synthesize type class instance for
G : Type ?,
_inst_1 : group G,
f : G → perm G :=
λ (g1 : G),
let p : G → G := λ (g : G), g1 * g,
pinv : G → G := λ (g : G), g1⁻¹ * g
in {to_fun := p, inv_fun := pinv, left_inv := _, right_inv := _}
⊢ has_one (G → G)
state:
G : Type ?,
_inst_1 : group G,
f : G → perm G :=
λ (g1 : G),
let p : G → G := λ (g : G), g1 * g,
pinv : G → G := λ (g : G), g1⁻¹ * g
in {to_fun := p, inv_fun := pinv, left_inv := _, right_inv := _}
⊢ G →* perm G


I don't understand this error.

#### Kevin Buzzard (Aug 26 2020 at 09:54):

failed to synthesize type class instance for
G : Type ?,
_inst_1 : group G,
f : G → perm G :=
λ (g1 : G),
let p : G → G := λ (g : G), g1 * g,
pinv : G → G := λ (g : G), g1⁻¹ * g
in {to_fun := p, inv_fun := pinv, left_inv := _, right_inv := _}
⊢ has_one (G → G)


I don't understand this error.

It means that you asked Lean for a term called 1 of type G → G and it doesn't know what you mean.

#### Kevin Buzzard (Aug 26 2020 at 09:55):

Half your problem is that you are making definitions using tactic mode.

def cayley (G:Type*) [h:group G] : G →* perm G :=
begin


this is a bad move. You're constructing a term, not a proof. You should create the structure using the usual { field1 := value1, field2 := value2, ...} structure creation syntax.

#### Scott Morrison (Aug 26 2020 at 10:34):

I'm not sure that "don't use tactic mode to make definitions" is an absolute rule. It is true that some tactics can make gross terms, and in particular it's easy to accidentally make terms that aren't definitionally what you expected them to be. Moreover using simp and rw when making definitions is likely to introduce eq.rec in your definition terms and you'll be sad later.

But still I use tactic mode all the time when "exploring" how to make a definition; nearly always I golf it away afterwards to be sure I've done what I thought I was doing, but it can still be helpful.

#### Chris M (Aug 26 2020 at 13:04):

A guess why tactic mode is bad for constructing non-Prop terms: Prop has propositional extentionality, so we don't care about the proof, and hence the "mess" that a tactic block leaves behind is not something we care about, but for definitions, where we are gonna have to "open it up" later, it's a problem?

#### Reid Barton (Aug 26 2020 at 13:05):

That's part of it but this should really be directed not at tactics in general but at specific tactics like rw, simp, linarith etc.

#### Reid Barton (Aug 26 2020 at 13:05):

Another reason is simply that if you make a definition then you will need to know later what the body of the definition actually is, and using tactics might make it harder to understand that

#### Reid Barton (Aug 26 2020 at 13:07):

For example, if you are going to later unfold the definition in the course of some proof, then the actual proof term is going to appear in your proof state anyways

#### Chris M (Aug 26 2020 at 13:13):

Does that apply to my code though? I only used non-trivial tactics in Prop terms.

#### Chris M (Aug 26 2020 at 13:14):

By the way, I've now turned it into a term mode definition, and now I'm getting the weird problem that it doesn't display a tactic goal state at all:

def Cayley (G:Type*) [group G] : G →* perm G :=
let f: G → perm G := (fun g1:G,
let p: G → G := (fun g, g1 * g) in
let pinv: G → G := (fun g, g1⁻¹ * g) in
have hleftinv: function.left_inverse pinv p, from (fun x, inv_mul_cancel_left g1 x),
have hrightinv: function.right_inverse pinv p, from (fun x, (mul_right_inj g1⁻¹).mp (hleftinv (pinv x))),
equiv.mk p pinv hleftinv hrightinv) in
have h1: (f 1) = 1, from by
{
dsimp [f],

},
have h2: ∀ (x y : G), f (x * y) = f x * f y, from fun x y, sorry,

⟨ f, h1, h2 ⟩


When I hover my mouse after dsimp [f], there is no goal state

#### Chris M (Aug 26 2020 at 13:22):

Oh this seems to be because I had the tactic display mode set to "widget". Weird.

#### Kevin Buzzard (Aug 26 2020 at 13:30):

import tactic
import algebra.group.hom

open equiv

universe u

def Cayley (G : Type u) [group G] : G →* perm G :=
{ to_fun := λ g,
{ to_fun := λ h, g * h,
inv_fun := λ h, g⁻¹ * h,
left_inv := λ h, by group,
right_inv := λ h, by group },
map_one' := by {ext, simp},
map_mul' := λ x y, by { ext z, exact mul_assoc x y z } }


#### Kenny Lau (Aug 26 2020 at 13:30):

what is by group?

#### Kevin Buzzard (Aug 26 2020 at 13:31):

the group tactic that Patrick wrote

#### Kevin Buzzard (Aug 26 2020 at 13:32):

def Cayley (G : Type u) [group G] : G →* perm G :=
{ to_fun := λ g,
{ to_fun := λ h, g * h,
inv_fun := λ h, g⁻¹ * h,
left_inv := λ h, by group,
right_inv := λ h, by group },
map_one' := by {ext, simp},
map_mul' := λ x y, by { ext, simp, group } }


#### Chris M (Aug 26 2020 at 13:33):

Now I'm trying to figure out how perm G is an instance of has_one, i.e. where this is defined. How do I figure this out?

#### Chris M (Aug 26 2020 at 13:33):

hmm, just saw Kevin's definition

#### Kevin Buzzard (Aug 26 2020 at 13:34):

variable (G : Type u)
#check (by apply_instance : has_one (perm G)) -- monoid.to_has_one (perm G) : has_one (perm G)


The one is coming from monoid.to_has_one and the monoid structure on perm G

#### Reid Barton (Aug 26 2020 at 13:39):

Yes, since you're defining a structure, unless you intend to do it by applying another definition, it's generally convenient if the first character of your definition is {

#### Chris M (Aug 26 2020 at 13:40):

although perhaps for my learning experience it would have been better not to give the whole definition? not sure.

#### Chris M (Aug 26 2020 at 13:43):

Is there a way to show the types of the elements of a structure as you're defining it? If I write a typing statement in

{ to_fun := λ h, g * h,
inv_fun := λ h, g⁻¹ * h,
left_inv := λ h, by group,
rightinv : function.right_inverse to_inv to_fun := fun h, by group },


Then it gives an error. It'd be helpful to see this so I don't have to rely on memory. Is the only way just to copy the definition into a comment?

#### Kevin Buzzard (Aug 26 2020 at 13:45):

What is the error?

#### Chris M (Aug 26 2020 at 13:46):

invalid structure instance, ':=' expected

#### Kevin Buzzard (Aug 26 2020 at 13:47):

perhaps fixing rightinv and to_inv will help

#### Reid Barton (Aug 26 2020 at 13:47):

Put a _ as the definition and hover over it or however you do it in VS Code. Or is that the memory you want to avoid?

#### Kevin Buzzard (Aug 26 2020 at 13:47):

but just putting begin sorry end after the := will do it

#### Chris M (Aug 26 2020 at 13:52):

Kevin Buzzard said:

perhaps fixing rightinv and to_inv will help

Sorry for that, no it doesn't.

#### Kevin Buzzard (Aug 26 2020 at 13:56):

then just go for the _ or begin sorry end option

ok

#### Chris M (Aug 26 2020 at 14:10):

After the ext tactic, it generates the goal state:

1 goal
G : Type ?,
_inst_1 : group G,
x : G
⊢ ⇑{to_fun := λ (h : G), 1 * h, inv_fun := λ (h : G), 1⁻¹ * h, left_inv := _, right_inv := _} x = ⇑1 x


Is this goal simply equivalent to ( λ(h : G), 1 * h) x = ( λ(h:G), h) x, because of the coercion arrow ⇑? I guess this is true because it says in the tutorial doc: Finally, ⇑f and ↥S are notations for coe_fn f and coe_sort S

#### Kevin Buzzard (Aug 26 2020 at 14:51):

You can use unfold_coes to unfold the coercions and dsimp to simplify afterwards

Great!

#### Chris M (Aug 26 2020 at 15:15):

Actually, I don't understand why this map_one' := by {ext, simp}, proof works, in particular the ext part: The ext tactic seems to (apart from applying the principle of functional extentionality) turn the goal of showing that the entire structure is the same, to just showing that to_fun is the same. Don't we also need to prove that inv_fun is the same? I guess I can accept that we don't need to prove the two properties are the same, because of propositional extentionality (though we're not actually invoking that, so I'm still not sure why that works).

#### Kevin Buzzard (Aug 26 2020 at 15:19):

The ext tactic is much more general than that.

#### Kevin Buzzard (Aug 26 2020 at 15:20):

The goal I'm proving with by {ext, simp} is some statement that f(1)=1, it's an equality of functions, so ext uses functional extensionality.

#### Chris M (Aug 26 2020 at 15:30):

But strictly speaking, it's an equality of "functions with additional structure", right? In particular, there are two functions that we need to show equality of, namely to_fun and inv_inv. We can deduce inv_inv from to_fun, but how does ext know this? did we have to teach this to ext explicitly and specifically for the typeclass equiv?

#### Kevin Buzzard (Aug 26 2020 at 15:32):

Chris M said:

But strictly speaking, it's an equality of "functions with additional structure", right?

Yes, but the ext tactic knows that it suffices to prove the two functions are equal. ext is doing a lot.

#### Kevin Buzzard (Aug 26 2020 at 15:35):

  map_one' := by {show_term {ext}, simp},


shows that ext is using perm.ext, and perm.ext is the statement that if the "to_fun" functions coincide on all inputs, then the equivs are equal. ext is using this because docs#equiv.perm.ext is tagged with ext in data.equiv.basic.

#### Chris M (Aug 26 2020 at 18:30):

As a side-note: The weird thing is that this gives me map_one' := by { refine perm.ext (λ (x : G), _[x]), simp},, which gives me the error placeholders '_' cannot be used where a function is expected

#### Kyle Miller (Aug 26 2020 at 18:31):

What are you expecting with _[x]? I'm not familiar with that notation. What happens if you replace it with just _?

#### Chris M (Aug 26 2020 at 18:33):

@Kyle Miller , to be clear, this is what show_term {ext} gives me, I didn't adjust anything about it and I am not familiar with the notation either. You're right, replacing it with _ makes it work.

#### Chris M (Aug 26 2020 at 18:34):

@Kevin Buzzard , Regarding the ext tactic though. Thanks, this clarifies a lot :).

#### Kyle Miller (Aug 26 2020 at 18:34):

An unfortunate property of the pretty printer is that what it prints is not always what Lean accepts as source code.

#### Kyle Miller (Aug 26 2020 at 18:35):

I'm curious, what if you do set_option pp.proofs true at the top level? Does it still print as _[x]? I think it might be hiding a "proof" with an underscore, but that proof is a metavariable.

#### Chris M (Aug 26 2020 at 18:37):

Doesn't change anything. (I placed it directly above the definition of cayley).

#### Reid Barton (Aug 26 2020 at 18:40):

You should just put _ there instead of _[x]

#### Chris M (Aug 26 2020 at 18:41):

Yes I did that after Kyle Miller's suggestion and it worked

#### Kevin Buzzard (Aug 26 2020 at 19:13):

I just used show_term to see which function Lean had applied. show_term {ext} is a great way to start moving from a tactic proof to a term proof

Last updated: May 10 2021 at 23:11 UTC