# Zulip Chat Archive

## 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 phrase`have 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

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

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

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

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