## Stream: new members

#### 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.

#### Reid Barton (Jun 29 2020 at 10:39):

It's not meaningful in general.

#### 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.

#### 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?

#### Reid Barton (Jun 29 2020 at 10:42):

You can't use it to make a definition.

#### Anne Baanen (Jun 29 2020 at 10:42):

Indeed, the return type p has to be a Prop

#### Eric Wieser (Jun 29 2020 at 10:43):

I think I can work with that

#### 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.

#### Reid Barton (Jun 29 2020 at 10:43):

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

#### Eric Wieser (Jun 29 2020 at 10:44):

In my case all the deconstructions are equivalent

#### Anne Baanen (Jun 29 2020 at 10:44):

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

Indeed

#### 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

#### 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?

#### Reid Barton (Jun 29 2020 at 10:53):

Oh I think I misunderstood your problem.

#### Reid Barton (Jun 29 2020 at 10:53):

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

#### Eric Wieser (Jun 29 2020 at 10:54):

You'd write that instead of what?

#### Reid Barton (Jun 29 2020 at 10:54):

Gᵣ r

As a type?

#### Reid Barton (Jun 29 2020 at 10:55):

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

#### Eric Wieser (Jun 29 2020 at 10:55):

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

#### Reid Barton (Jun 29 2020 at 10:55):

I mean what is the Lean type.

#### Eric Wieser (Jun 29 2020 at 10:56):

The lean type of what?

#### Anne Baanen (Jun 29 2020 at 10:56):

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

#### Reid Barton (Jun 29 2020 at 10:56):

What's the missing type annotation on Gᵣ.

#### Eric Wieser (Jun 29 2020 at 10:56):

Gᵣ : ℕ → add_subgroup G

#### Eric Wieser (Jun 29 2020 at 10:56):

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

#### Reid Barton (Jun 29 2020 at 10:57):

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

#### 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

#### 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

#### 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?

#### 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

#### Anne Baanen (Jun 29 2020 at 11:01):

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

#### 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

#### 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.

#### Eric Wieser (Jun 29 2020 at 11:06):

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

#### Reid Barton (Jun 29 2020 at 11:07):

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

#### 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.

#### 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


#### Reid Barton (Jun 29 2020 at 11:11):

if it's trivial, then exact h1

#### Eric Wieser (Jun 29 2020 at 11:11):

It can't convert between the types

#### Eric Wieser (Jun 29 2020 at 11:12):

Can I unfold ∈  somehow?

#### 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.

I am too

#### 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

#### Eric Wieser (Jun 29 2020 at 11:13):

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

#### Eric Wieser (Jun 29 2020 at 11:13):

But I have no idea what that means

#### Reid Barton (Jun 29 2020 at 11:13):

Also, what is the error message!

#### 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

#### Eric Wieser (Jun 29 2020 at 11:15):

Ah, rw set.mem_def seems more idiomatic

#### Reid Barton (Jun 29 2020 at 11:15):

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

#### 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,


#### Reid Barton (Jun 29 2020 at 11:17):

Hmm, this seems impossible.

#### Eric Wieser (Jun 29 2020 at 11:17):

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

(deleted)

#### Eric Wieser (Jun 29 2020 at 11:19):

Jumped to conclusions, my lean server is running quite slowly

#### 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

#### 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.

#### 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.)

#### 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