Zulip Chat Archive

Stream: new members

Topic: Working with add_subgroup.closure


view this post on Zulip Eric Wieser (Jun 29 2020 at 10:33):

I've a type defined as def Gᵣ (r : ℕ) := add_subgroup.closure (Bᵣ r)

I have a function smul (k : G₀) (b : Bᵣ r) : Bᵣ r, and would like to derive from it a function smul (k : G₀) (v : Gᵣ r) : Gᵣ r.
There seems to be an intuitive meaning of "deconstruct v to the elements of Bᵣ it was constructed from, apply smul to those elements, and then pick the result from Gᵣ".

I can't really work out how to deconstruct my closure to implement this.

view this post on Zulip Reid Barton (Jun 29 2020 at 10:39):

It's not meaningful in general.

view this post on Zulip Anne Baanen (Jun 29 2020 at 10:39):

I think docs#add_subgroup.closure_induction is in general what you would be looking for to deconstruct the elements.

view this post on Zulip Eric Wieser (Jun 29 2020 at 10:41):

Is there an example of how to use closure_induction anywhere? Can it be used as a tactic?

view this post on Zulip Reid Barton (Jun 29 2020 at 10:42):

You can't use it to make a definition.

view this post on Zulip Anne Baanen (Jun 29 2020 at 10:42):

Indeed, the return type p has to be a Prop

view this post on Zulip Eric Wieser (Jun 29 2020 at 10:43):

I think I can work with that

view this post on Zulip Reid Barton (Jun 29 2020 at 10:43):

Your intuitive explanation is not precise because there could be more than one way to do the deconstruction.

view this post on Zulip Reid Barton (Jun 29 2020 at 10:43):

Presumably, you know some reason why this is actually not possible or not a problem.

view this post on Zulip Eric Wieser (Jun 29 2020 at 10:44):

In my case all the deconstructions are equivalent

view this post on Zulip Anne Baanen (Jun 29 2020 at 10:44):

Aha, then your p x would be something like x ∈ G\_r

view this post on Zulip Eric Wieser (Jun 29 2020 at 10:45):

Indeed

view this post on Zulip Anne Baanen (Jun 29 2020 at 10:48):

Eric Wieser said:

Is there an example of how to use closure_induction anywhere? Can it be used as a tactic?

To use it in a tactic proof, with an assumption hx : x ∈ G\_r, you can write apply add_subgroup.closure_induction hx, and you would get goals corresponding to the possible destructurings of elements of a closure

view this post on Zulip Eric Wieser (Jun 29 2020 at 10:51):

I think I'm getting lost in stale lean annotations in vs-code... Is there any way to clear all old errors after killing the lean server?

view this post on Zulip Reid Barton (Jun 29 2020 at 10:53):

Oh I think I misunderstood your problem.

view this post on Zulip Reid Barton (Jun 29 2020 at 10:53):

Your naming and syntax is a bit weird. Normally we write r ∈ Gᵣ, etc.

view this post on Zulip Eric Wieser (Jun 29 2020 at 10:54):

You'd write that instead of what?

view this post on Zulip Reid Barton (Jun 29 2020 at 10:54):

Gᵣ r

view this post on Zulip Eric Wieser (Jun 29 2020 at 10:55):

As a type?

view this post on Zulip Reid Barton (Jun 29 2020 at 10:55):

Oh I don't even know. What is add_subgroup.closure? A bundled subgroup?

view this post on Zulip Eric Wieser (Jun 29 2020 at 10:55):

The closure of all elements produced under addition of the set (Br r)

view this post on Zulip Reid Barton (Jun 29 2020 at 10:55):

I mean what is the Lean type.

view this post on Zulip Eric Wieser (Jun 29 2020 at 10:56):

The lean type of what?

view this post on Zulip Anne Baanen (Jun 29 2020 at 10:56):

@Reid Barton yes, it's bundled (is_add_subgroup is the unbundled class)

view this post on Zulip Reid Barton (Jun 29 2020 at 10:56):

What's the missing type annotation on Gᵣ.

view this post on Zulip Eric Wieser (Jun 29 2020 at 10:56):

Gᵣ : ℕ → add_subgroup G

view this post on Zulip Eric Wieser (Jun 29 2020 at 10:56):

The r here is really just a distraction, since it's unchanged through all the types

view this post on Zulip Reid Barton (Jun 29 2020 at 10:57):

Okay, then I still don't understand how you could use closure_induction

view this post on Zulip Eric Wieser (Jun 29 2020 at 10:59):

I think I see the path forward, but I'm getting bitten by aliases for the same thing

view this post on Zulip Anne Baanen (Jun 29 2020 at 10:59):

IUIC, v : Gr r is interpreted as v : coe_sort (Gr r), i.e. v : {v : G // v ∈ Gr r}. So we're using syntax sugar for subtype

view this post on Zulip Eric Wieser (Jun 29 2020 at 10:59):

If I have def Bᵣ (r : ℕ) := set_of (is_rblade r), is it better to write lemmas in terms of is_rblade r b or b \in Bᵣ r?

view this post on Zulip Eric Wieser (Jun 29 2020 at 11:00):

Because lean doesn't seem to be very helpful when it comes to accepting the former where it expects the latter

view this post on Zulip Anne Baanen (Jun 29 2020 at 11:01):

I expect is_rblade, unless you want to do set operations with them

view this post on Zulip Anne Baanen (Jun 29 2020 at 11:02):

If you hide it behind definition Br, many tactics will not recognize that it's defined in terms of is_rblade until you unfold Br

view this post on Zulip Anne Baanen (Jun 29 2020 at 11:06):

If you really want to write Bᵣ and not have to unfold it, you can also use a notation instead of a def:

notation `B` r := set_of (is_rblade r)

Notations are processed before tactics, so they don't confuse the tactics.

view this post on Zulip Eric Wieser (Jun 29 2020 at 11:06):

Would it be better to eliminate is_rblade, and inline the defintion into B_r?

view this post on Zulip Reid Barton (Jun 29 2020 at 11:07):

With regards to the original question, I'm guessing the formalization is not optimal.

view this post on Zulip Reid Barton (Jun 29 2020 at 11:08):

There is a mathematical issue here, namely you have to check that whatever relations the elements of B_r satisfy as a subgroup of (something??) are preserved by smul. Since smul takes values again in B_r I'm guessing this is not so trivial to check.

view this post on Zulip Eric Wieser (Jun 29 2020 at 11:10):

I'm stuck on the trivial goal:

h1 : is_rblade r (fₛ k * x)
 fₛ k * x  geometric_algebra.is_rblade r

view this post on Zulip Reid Barton (Jun 29 2020 at 11:11):

if it's trivial, then exact h1

view this post on Zulip Eric Wieser (Jun 29 2020 at 11:11):

It can't convert between the types

view this post on Zulip Eric Wieser (Jun 29 2020 at 11:12):

Can I unfold somehow?

view this post on Zulip Reid Barton (Jun 29 2020 at 11:12):

I'm suspicious about the fact that one is displayed with geometric_algebra. and the other is not.

view this post on Zulip Eric Wieser (Jun 29 2020 at 11:12):

I am too

view this post on Zulip Reid Barton (Jun 29 2020 at 11:12):

This is not your issue.

view this post on Zulip Reid Barton (Jun 29 2020 at 11:12):

Well, I guess it could be your issue (maybe the type is something else?) but it seems unlikely

view this post on Zulip Eric Wieser (Jun 29 2020 at 11:13):

apply set.mem_def.mpr does the trick, according to suggest (before the expected exact h1)

view this post on Zulip Eric Wieser (Jun 29 2020 at 11:13):

But I have no idea what that means

view this post on Zulip Reid Barton (Jun 29 2020 at 11:13):

Also, what is the error message!

view this post on Zulip Reid Barton (Jun 29 2020 at 11:13):

Those are helpful.

view this post on Zulip Eric Wieser (Jun 29 2020 at 11:14):

invalid type ascription, term has type
  is_rblade r (fₛ k * x)
but is expected to have type
  fₛ k * x  geometric_algebra.is_rblade r

if I skip the mem_def thing

view this post on Zulip Eric Wieser (Jun 29 2020 at 11:15):

Ah, rw set.mem_def seems more idiomatic

view this post on Zulip Reid Barton (Jun 29 2020 at 11:15):

set.mem_def is basically by rfl, so none of this makes sense

view this post on Zulip Eric Wieser (Jun 29 2020 at 11:17):

Well, I can tell you that without it, I get that error. The snippet causing the trouble is:

      have h1 : is_rblade r ((fₛ k : G) * x) := sorry,
      have h2 : ((fₛ k : G) * x)  B r := begin
        rw set.mem_def,
        exact h1,
      end,

view this post on Zulip Reid Barton (Jun 29 2020 at 11:17):

Hmm, this seems impossible.

view this post on Zulip Eric Wieser (Jun 29 2020 at 11:17):

Except, now that I try again I don't...

view this post on Zulip Eric Wieser (Jun 29 2020 at 11:17):

(deleted)

view this post on Zulip Eric Wieser (Jun 29 2020 at 11:19):

Jumped to conclusions, my lean server is running quite slowly

view this post on Zulip Eric Wieser (Jun 29 2020 at 11:19):

I can confirm that removing rw set.mem_def _does_ cause it to give the type error above

view this post on Zulip Reid Barton (Jun 29 2020 at 11:24):

I guess this is barely possible if the type of h1 secretly contains some metavariables, and Lean somehow fails to hit upon the obvious idea of unfolding the definition of , but it still seems implausible.

view this post on Zulip Reid Barton (Jun 29 2020 at 11:27):

Maybe this is more likely with this "forward reasoning" style. (Whatever you put as a proof of h1, you could just put for h2 directly.)

view this post on Zulip Eric Wieser (Jun 29 2020 at 11:28):

Yeah, I was able to simplify it all by doing basically that, and then set.mem_def wasn't needed


Last updated: May 11 2021 at 14:11 UTC