Why doesn't dunfold work here?

Stream: new members

[Chris M]

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]

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

[Kyle Miller]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Chris M]

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]

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

[Kevin Buzzard]

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]

what is by group?

[Kevin Buzzard]

the group tactic that Patrick wrote

[Kevin Buzzard]

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]

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]

hmm, just saw Kevin's definition

[Kevin Buzzard]

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]

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]

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

[Chris M]

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]

What is the error?

[Chris M]

invalid structure instance, ':=' expected

[Kevin Buzzard]

perhaps fixing rightinv and to_inv will help

[Reid Barton]

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]

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

[Chris M]

Kevin Buzzard said:

perhaps fixing rightinv and to_inv will help

Sorry for that, no it doesn't.

[Kevin Buzzard]

then just go for the _ or begin sorry end option

[Chris M]

ok

[Chris M]

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]

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

[Chris M]

Great!

[Chris M]

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]

The ext tactic is much more general than that.

[Kevin Buzzard]

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]

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]

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]

  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]

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]

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

[Chris M]

@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]

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

[Kyle Miller]

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

[Kyle Miller]

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]

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

[Reid Barton]

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

[Chris M]

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

[Kevin Buzzard]

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