add_group, has_neg, and subtypes defined as sums

Stream: new members

[Eric Wieser]

Here's my MVE:

import algebra.group.hom
universe u

section
    -- these sorry's I have, but aren't relevant
    parameters {G : Type u} [add_group G]
    def Bᵣ (r : ℕ) : Type u := {g : G // sorry}
    instance Bᵣ_has_neg (r : ℕ) : has_neg (Bᵣ r) := sorry

    /- an r-vector must be decomposable into r blades-/
    def is_rvector  (r : nat) (v : G) : Prop :=
    ∃ (bs : list (Bᵣ r)),
        v = (bs.map subtype.val).sum

    /- the algebra of a single grade -/
    def Gᵣ (r : ℕ) := {g : G // is_rvector r g}

    -- I don't know how to obtain this without tediously expanding `list.sum` for every case.
    instance g (r : ℕ) : add_group (Gᵣ r) := sorry
end

Is there a trivial way to create an instance add_group (Gᵣ r)? I can prove the properties one by one, but I get the feeling that mathlib already has what I need if I define is_rvector in a clever way.

[Eric Wieser]

To help ward off accidental XY problems here, my actual problem is

given a subtype Br of G where [has_neg Br] and [add_group G], how do I form the subtype Gr which is the smallest subgroup of G which contains all of Br?

[Kenny Lau]

it might be better to work with sets instead of subtypes

[Eric Wieser]

Is there any way to convert back an forth between the two?

[Eric Wieser]

I think you've set me on the right track, thanks

[Jalex Stark]

I think you're looking for this? https://leanprover-community.github.io/mathlib_docs/algebra/pointwise.html

[Jalex Stark]

or maybe this https://leanprover-community.github.io/mathlib_docs/algebra/pi_instances.html

[Eric Wieser]

I ended up trying to use add_subgroup.closure (set_of (Bᵣ r).property)

[Kenny Lau]

@Eric Wieser I'm saying, in the first place don't have B_r be a subtype to begin with

[Eric Wieser]

I think I want it to be a subtype because I want to define functions over the objects in the set

[Kenny Lau]

and having it be a set allows for this flexibility, because you can coerce a set into a subtype but not the other way round

[Kenny Lau]

at least idiomatically

[Eric Wieser]

In that ↥ will be invoked automatically?

[Mario Carneiro]

yes

[Kenny Lau]

and you can have additive closure of a set but not of a subtype

[Kenny Lau]

at least idiomatically

[Kenny Lau]

and you can perform set operations (intersections, unions, insertions, etc) on a set but not on a subtype

[Kenny Lau]

at least idiomatically

[Eric Wieser]

Thanks for the tips
I actually had both Gᵣ_subgroup and Gᵣ (r : ℕ) := ↥(Gᵣ_subgroup r).
Sounds like there is no need for the separate definitions

[Kenny Lau]

and you don't need the second one

[Kenny Lau]

aliases are not idiomatic because rw and simp and etc cannot see through it

[Eric Wieser]

A follow-up question - if I have P := set_of p, and can prove ∀ x : α, p x, can I show P = \alpha?

[Kenny Lau]

which I sometimes find annoying as well -- why can't I just make aliases that everything can see through?

[Kenny Lau]

set_of is also not idiomatic: use { x | P x } instead

[Kenny Lau]

\alpha is not a set; you mean set.univ

[Kenny Lau]

and you can prove that using lemmas about set.univ

[Eric Wieser]

I think I was hoping to show type equality

[Mario Carneiro]

set equality is what you want

[Mario Carneiro]

type equality is not meaningful

[Eric Wieser]

Perhaps I was misdirected by the codewars kata asking me to prove bool != nat into thinking that such a proof was common :)

[Mario Carneiro]

heh

[Kenny Lau]

aha

[Kenny Lau]

yeah we don't use type equalities

[Kenny Lau]

we don't ask whether two types are equal

[Kenny Lau]

just like in ZFC you don't ask whether 37 is an element of the real number pi

[Eric Wieser]

Alright, so lets's say I use ∀ x : α, p x to prove set_of p = set.univ. Can I get a free coe from \alpha to P?

[Mario Carneiro]

Not a coe but I believe there is an equiv for this

[Eric Wieser]

equiv is a bijective coe?

[Mario Carneiro]

It's a bijection with computable inverse

[Mario Carneiro]

it is a function you have to apply

[Mario Carneiro]

The relevant function is usually called cod_restrict

[Kenny Lau]

it might be more helpful if you un #xy this further

[Mario Carneiro]

ah yes, src#set.cod_restrict in data.set.function

[Eric Wieser]

@Kenny Lau: Not sure how to un-XY further without giving my full file... If you're willing to skim ~200 lines, then I'll give you a github link. If not, I'll keep exploring myself :)

[Eric Wieser]

The line that feels awkward to me is: https://github.com/eric-wieser/lean-ga/blob/sets-of-blades/src/geometric_algebra/nursery/chisolm.lean#L209 (edit: fixed sorry, I must have just had a typo or something)

[Jalex Stark]

I won't speak for kenny, but if I'm following a conversation and there's a link to a github file, I usually follow the link rather than unfollow the conversation

[Eric Wieser]

Simplified my issue a little bit - its really just a case of working out what's idiomatic and gets me the most for free - I was able to complete my proof

[Jalex Stark]

i find the file kind of hard to read. is there a reason you don't write something more like

lemma vec_sym_prod_scalar:
∀ (a b : G₁), ∃ k : G₀, a *₊ᵥ b = fₛ k :=
begin
  intros a b,
  have h1 : (a + b)²ᵥ = a²ᵥ + b²ᵥ + a *₊ᵥ b,
  { unfold square_vec sym_prod_vec prod_vec,
    rw add_monoid_hom.map_add fᵥ a b,
    rw left_distrib,
    repeat {rw right_distrib},
    abel },
  have vec_sq_scalar : ∀ v : G₁, ∃ k : G₀, v²ᵥ = fₛ k,
  apply geometric_algebra.vec_sq_scalar,
  use vec_sq_scalar (a + b),
  ..
end

[Jalex Stark]

in my local copy of the master branch, typeclass inference can't find has_add G₁

[Eric Wieser]

master branch of mathlib? Of that repo?

[Jalex Stark]

of that repo

[Jalex Stark]

you linked to a branch called sets-of-blades, maybe it's fixed there. for some reason git checkout origin/sets-of-blades doesn't work for me

[Eric Wieser]

Master branch is not super relevant to my question, since all the stuff I added is on another branch

[Eric Wieser]

I think has_add G₁ is implied by [vector_space G₀ G₁]?

[Jalex Stark]

even earlier, by [add_comm_group G₁]

[Eric Wieser]

I didn't write that lemma (@Utensil Song did), so don't want to think too much about its style right now.

[Jalex Stark]

ok i figured out my branch issues (i just nuked my local copy and did leanproject get eric-wieser/lean-ga:sets-of-blades)

[Eric Wieser]

Thanks for (offering to start) helping out!

[Jalex Stark]

well i haven't offered anything useful yet :P

[Jalex Stark]

there's something I don't understand about the difference between tactic mode and term mode. The first lemma throws an error and the second one doesn't

lemma vec_sym_prod_scalar2 (a b : G₁) : is_scalar (a *₊ᵥ b) :=
begin
  have h1 : (a + b)²ᵥ = a²ᵥ + b²ᵥ + a *₊ᵥ b,
  sorry
end

lemma vec_sym_prod_scalar (a b : G₁) : is_scalar (a *₊ᵥ b) :=
have h1 : (a + b)²ᵥ = a²ᵥ + b²ᵥ + a *₊ᵥ b, from begin
  sorry
end, sorry

[Eric Wieser]

I ran into this too - it can't seem to infer the operators

[Eric Wieser]

Putting ( ... : G) around their use seemed to fix it for me

[Kenny Lau]

  def neg (b : Bᵣ r) : Bᵣ r := ⟨-b.val, begin
    cases b with b' hb,
    exact exists.elim hb begin
      intros a ha,
      use -a,
      simp [ha],
    end
  end⟩

  instance has_neg (r : ℕ) : has_neg (Bᵣ r) := { neg := neg}

[Kenny Lau]

this isn't idiomatic: you should instead show that is_rblade r b implies is_rblade r (-b)

[Eric Wieser]

And then derive neg from that proof?

[Jalex Stark]

do you know where the floating end on line 216 of https://github.com/eric-wieser/lean-ga/blob/sets-of-blades/src/geometric_algebra/nursery/chisolm.lean#L209 comes from?

[Eric Wieser]

section

[Jalex Stark]

thanks (anonymous sections seem obviously bad to me, but I guess you're trying not to think about that sort of thing right now)

[Kenny Lau]

also, your file has a lot of aliases, and I mean a whole lot. It is a shame that Lean cannot deal with aliases optimally, so the idiomatic thing to do is to stick with one way to write a certain thing and prove 37 lemmas about that way

[Kenny Lau]

for example, we have 3700 lemmas about multiplication and 0 about your sym_prod so maybe you shouldn't use sym_prod

[Eric Wieser]

Regarding neg, is this closer to idiomatic?

  lemma neg_is_rblade {b : G} (hb : is_rblade r b) : (is_rblade r (-b)) := begin
    exact exists.elim hb begin
      intros a ha,
      use -a,
      simp [ha],
    end
  end
  def neg (b : Bᵣ r) : Bᵣ r := ⟨-b.val, neg_is_rblade b.property⟩

[Kenny Lau]

yeah

[Jalex Stark]

I'm confused, what do you suggest they do instead of use sym_prod?

[Kenny Lau]

@[simp] def sym_prod (a b : G) := a * b + b * a

[Kenny Lau]

I suggest they forget about this definition

[Kenny Lau]

oops I added @[simp] in my local version

[Jalex Stark]

what do you mean by "forget about"?

[Jalex Stark]

do you mean add @[simp]?

[Kenny Lau]

I actually mean delete this definition, but maybe we could ask @Mario Carneiro about how that file could become more idiomatic

[Kenny Lau]

that file = https://github.com/eric-wieser/lean-ga/blob/sets-of-blades/src/geometric_algebra/nursery/chisolm.lean

[Jalex Stark]

is giving it @[reducible] similar to deleting it? or making it a notation?
I imagine the point is just that it's a pain to type out a * b + b * a when a and b are many characters long

[Kenny Lau]

hence "it's a shame Lean can't handle aliases optimally"

[Kenny Lau]

in my ideal world I would be able to write sym_prod in theorems and have it automatically convert to the long version when they store the theorem

[Kenny Lau]

so people won't complain about my LHS not being in "simp-normal" form

[Eric Wieser]

My suspicion is that we will not need sym_prod in its current form, only sym_prod_vec. The true symmetric product over G is much more complex, I think

[Eric Wieser]

Another question about that file - I have:

-- r-vectors
def Gᵣ (r : ℕ) := add_subgroup.closure (Bᵣ r)
namespace Gᵣ
  variables {r : ℕ}
  instance addgroup : add_comm_group (Gᵣ r) := (Gᵣ r).to_add_comm_group
end Gᵣ

Is the add_comm_group instance actually needed, or does lean already provide it? If the latter, can I write an assertion that I satisfy the type class?

[Kenny Lau]

if you tag the definition with @[reducible] then you will automatically have the instance

[Kenny Lau]

@Jalex Stark @Mario Carneiro in my ideal world, writing sym_prod a b would be the same as writing a * b + b * a in all circumstances

[Eric Wieser]

@Kenny Lau, for the second part of the question, how can I check if I have the instance?

[Kenny Lau]

#check \la r, (by instance : add_comm_group G\_r r) (be sure not to put this after a line that starts with by)

[Eric Wieser]

Is it idiomatic to leave checks in files as proof that the instances you intend to satisfy are satified?

[Jalex Stark]

no

[Kenny Lau]

it isn't a proof

[Kenny Lau]

you don't need that line there to use the file

[Eric Wieser]

Right, but it acts as a unit test for the file

[Jalex Stark]

if you "intend to satisfy the instance" then there should be theorems that make use of it

[Kenny Lau]

we don't do unit tests

[Eric Wieser]

@Jalex Stark: what about situations where I don't need it to satisfy any of my theorems, but users building upon my theorems do?

[Kenny Lau]

you don't need the #check line to have the instance

[Kenny Lau]

it's just there literally for you to check that the instance is there

[Eric Wieser]

No, but if I remove the instance by accident, how would I know?

[Kenny Lau]

then the theorems depending on that instance will complain to you

[Eric Wieser]

But they won't, they'd complain at someone else who wrote those theorems on a different machine. Who would then complain to me

[Kenny Lau]

"All repo not PR'd into mathlib is lost" -- Ancient Chinese Proverb

[Jalex Stark]

you can declare the instance by instance : add_comm_group G\0 := by apply_instance, is that what you want?

[Mario Carneiro]

If you want sym_prod a b to be turned into a * b + b * a immediately, you can use a notation

[Eric Wieser]

Yes, I think that's a nice compromise @Jalex Stark , thanks. @Kenny Lau, thanks for the advice.

[Bryan Gin-ge Chen]

Jalex Stark said:

you can declare the instance by instance : add_comm_group G\0 := by apply_instance, is that what you want?

Won't this result in two add_comm_group instances? If so, maybe for a test you should use example here instead.

[Eric Wieser]

@Jalex Stark , that doesn't work, it seems to declare it with a name of add_comm_group.

[Eric Wieser]

example (r : ℕ) : add_comm_group (Gᵣ r) := by apply_instance is what I was after!

[Eric Wieser]

It seems I don't need @[reducible]?

[Jalex Stark]

you don't need reducible where?

[Eric Wieser]

Kenny Lau said:

if you tag the definition with @[reducible] then you will automatically have the instance

On G\_r

[Mario Carneiro]

If the instance gets a bad name, you should give it a name manually

[Mario Carneiro]

instance G0.add_comm_group : add_comm_group G\0 := by apply_instance

[Eric Wieser]

My hope was that instance without a name would result in no name at all. But it sounds like if you need no name at all, example is the right keyword.

[Bryan Gin-ge Chen]

Including this instance explicitly can speed up type class search, right?

[Mario Carneiro]

no name just means it uses an automatic naming scheme which is wrong surprisingly often

[Bryan Gin-ge Chen]

example just throws away the declaration once it's been checked.

[Jalex Stark]

(deleted)

[Jalex Stark]

one example of bad aliasing in this file is left_distrib. everywhere it's used it can (and should) be replaced with the general mul_add

[Eric Wieser]

Yeah, I noticed that too, just didn't want to do too much cleanup to start with.

[Jalex Stark]

( @Utensil Song should probably look at this thread at some point )

[Kenny Lau]

Mario Carneiro said:

If you want sym_prod a b to be turned into a * b + b * a immediately, you can use a notation

@Kevin Buzzard and I are trying out this new approach and it's working fine

[Kenny Lau]

and I'm left here wondering why don't we use this all over mathlib

[Kenny Lau]

-- make all the tactics work
import tactic
import algebra.pi_instances

-- Let's just use Lean's definition of the naturals and not worry
-- about what they are or how to make them.

import data.nat.basic

-- Let's now experiment
namespace experiment

/-
An experiment where we try different definitions of the integers.
-/

namespace int3

notation `ℕ²` := ℕ × ℕ

namespace natsquared

notation `first` := prod.fst
notation `second` := prod.snd

def r (a b : ℕ²) := first a + second b = second a + first b

instance : has_equiv ℕ² := ⟨r⟩

namespace r
theorem refl (a : ℕ²) : a ≈ a :=
begin
  -- unfold it in your head
  change first a + second a = second a + first a,
  -- if you delete the line above, the line below still works
  apply add_comm,
end

theorem symm (a b : ℕ²) : a ≈ b → b ≈ a :=
begin
  intro hab,
  unfold has_equiv.equiv at *,
  rw [r] at *,
  omega,
end

theorem trans (a b c : ℕ²) : a ≈ b → b ≈ c → a ≈ c :=
begin
  intro hab,
  intro hbc,
  unfold has_equiv.equiv at *,
  rw [r] at *,
  omega,
end

theorem equiv : equivalence r :=
⟨refl, symm, trans⟩

end r

instance : setoid ℕ² :=
{ r := r,
  iseqv := r.equiv }

end natsquared

-- definition of int as quotient type
notation `ℤ3` := quotient natsquared.setoid

-- theorem! It's a ring!

def zero : ℤ3 := ⟦0⟧
def one : ℤ3 := ⟦1⟧

open natsquared

@[simp] lemma thing (a b : ℕ²) : a ≈ b ↔ first a + second b = second a + first b := iff.rfl

def add (a b : ℤ3) : ℤ3 := quotient.lift_on₂ a b (λ z w, ⟦(z+w)⟧) begin
  intros,
  simp at *,
  omega,
end

end int3

end experiment

[Kenny Lau]

here, no definition, only notation, and everything works fine

[Kenny Lau]

@Mario Carneiro we should use this all over mathlib

[Kenny Lau]

oh except for one thing: zero and one and add are all definitions

[Mario Carneiro]

I don't think we want int3 to be a notation

[Mario Carneiro]

or rather, ℤ3 should be a notation for def int3 := quotient natsquared.setoid

[Mario Carneiro]

I don't see any problems with ℕ² being a (local) notation though

[Mario Carneiro]

actually these should all probably be local notations

[Mario Carneiro]

But notations are not a substitute for defs. They are like macros, they expand on the spot

[Mario Carneiro]

that's usually not what you want

[Kenny Lau]

but that's what I'm complaining about

[Kenny Lau]

I want them to behave completely the same

[Kenny Lau]

I guess I'm being unreasonable

[Kenny Lau]

if everything were expanded every term would be huge right

[Kenny Lau]

like internally, even though pp gives a short term

[Mario Carneiro]

even pp won't be able to provide small terms in most cases, I think

[Mario Carneiro]

But you've got the idea there - the whole point of definitions is so that term sizes don't grow exponentially as you move up in abstraction

[Mario Carneiro]

if you intend to give something an "API" then it should probably be a definition

[Utensil Song]

Just discovered this topic through @. Thanks for the code review and suggestions!

The file is mostly a messy battlefield when I was fighting with how to proceed to the next line. There're many cleanups in order, and not cleaning them up is simply because of some historical reasons and random feelings about them:

1. The proof would become much more readable if it's rewritten into what @Jalex Stark suggested here, I was just piecing the scalars together so I used elim to give the scalars names from the exists prop;
2. anonymous sections are indeed bad, but if I have a lemma c in namespace a and section b, I can't help to think it as a.b.c so I left b empty ;
3. the abuse of alias is partly an experiment to see how can I see through these noises when I prove things;
4. partly because I need them in the process of writing some deleted code, take sym_prod for an example, initially, there was no sym_prod_vec and only sym_prod since I used coe instead of homes, and I can't just use notation because I need to specify the types to give Lean the hint to automatically add coes for me, see https://github.com/pygae/lean-ga/blob/cf736df9e327ba6822f3b95e996406ec2e87f470/src/geometric_algebra/nursery/basic.lean#L89
5. the existence of left_distrib etc. is because I need to prove this trivial thing locally to verify the local environment, like parameters/variables are working, and I left them there because I wanted to present them locally, the same place they appear in the literature(showing that they are already included in the definition, without explicit appearances in the definition) and felt annoying to have to remember from which algebraic structure left_distrib came from.

[Jalex Stark]

You don't need to remember the name of an algebraic structure to use rw mul_add