Zulip Chat Archive

Stream: new members

Topic: Why doesn't dunfold work here?


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

view this post on Zulip Scott Morrison (Aug 26 2020 at 06:59):

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Chris M (Aug 26 2020 at 13:13):

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

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

view this post on Zulip Chris M (Aug 26 2020 at 13:22):

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

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

view this post on Zulip Kenny Lau (Aug 26 2020 at 13:30):

what is by group?

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 13:31):

the group tactic that Patrick wrote

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

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

view this post on Zulip Chris M (Aug 26 2020 at 13:33):

hmm, just saw Kevin's definition

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

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

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

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 13:45):

What is the error?

view this post on Zulip Chris M (Aug 26 2020 at 13:46):

invalid structure instance, ':=' expected

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 13:47):

perhaps fixing rightinv and to_inv will help

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 13:47):

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

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 13:56):

then just go for the _ or begin sorry end option

view this post on Zulip Chris M (Aug 26 2020 at 14:00):

ok

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 14:51):

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

view this post on Zulip Chris M (Aug 26 2020 at 15:03):

Great!

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

view this post on Zulip Kevin Buzzard (Aug 26 2020 at 15:19):

The ext tactic is much more general than that.

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

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

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

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

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

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

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

view this post on Zulip Chris M (Aug 26 2020 at 18:34):

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

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

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

view this post on Zulip Chris M (Aug 26 2020 at 18:37):

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

view this post on Zulip Reid Barton (Aug 26 2020 at 18:40):

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

view this post on Zulip Chris M (Aug 26 2020 at 18:41):

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

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