Working with add_subgroup.closure

Stream: new members

[Eric Wieser]

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]

It's not meaningful in general.

[Anne Baanen]

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

[Eric Wieser]

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

[Reid Barton]

You can't use it to make a definition.

[Anne Baanen]

Indeed, the return type p has to be a Prop

[Eric Wieser]

I think I can work with that

[Reid Barton]

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

[Reid Barton]

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

[Eric Wieser]

In my case all the deconstructions are equivalent

[Anne Baanen]

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

[Eric Wieser]

Indeed

[Anne Baanen]

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]

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]

Oh I think I misunderstood your problem.

[Reid Barton]

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

[Eric Wieser]

You'd write that instead of what?

[Reid Barton]

Gᵣ r

[Eric Wieser]

As a type?

[Reid Barton]

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

[Eric Wieser]

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

[Reid Barton]

I mean what is the Lean type.

[Eric Wieser]

The lean type of what?

[Anne Baanen]

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

[Reid Barton]

What's the missing type annotation on Gᵣ.

[Eric Wieser]

Gᵣ : ℕ → add_subgroup G

[Eric Wieser]

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

[Reid Barton]

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

[Eric Wieser]

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

[Anne Baanen]

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]

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]

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

[Anne Baanen]

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

[Anne Baanen]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

I'm stuck on the trivial goal:

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

[Reid Barton]

if it's trivial, then exact h1

[Eric Wieser]

It can't convert between the types

[Eric Wieser]

Can I unfold ∈ somehow?

[Reid Barton]

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

[Eric Wieser]

I am too

[Reid Barton]

This is not your issue.

[Reid Barton]

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

[Eric Wieser]

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

[Eric Wieser]

But I have no idea what that means

[Reid Barton]

Also, what is the error message!

[Reid Barton]

Those are helpful.

[Eric Wieser]

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]

Ah, rw set.mem_def seems more idiomatic

[Reid Barton]

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

[Eric Wieser]

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]

Hmm, this seems impossible.

[Eric Wieser]

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

[Eric Wieser]

(deleted)

[Eric Wieser]

Jumped to conclusions, my lean server is running quite slowly

[Eric Wieser]

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

[Reid Barton]

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]

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]

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