Zulip Chat Archive

Stream: new members

Topic: synthesized not defeq inferred


view this post on Zulip Utensil Song (Jun 05 2020 at 15:23):

Hi, I have encountered the following error and I can't figure out why, any help would be greatly appreciated:

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  ring.to_semiring
inferred
  comm_semiring.to_semiring K

#mwe is

import tactic.ring_exp ring_theory.algebra algebra.opposites algebra.commute data.equiv.ring
import linear_algebra.quadratic_form
import data.real.basic
import data.complex.basic

class geometric_algebra (G : Type*) (K : set G) (V : set G)
[field K]
[add_comm_group V] [vector_space K V] -- [Q : quadratic_form K V]
[ring G]
[is_subring K]
[is_subring V]
extends algebra K G
 :=
(inner_product : quadratic_form K V)

The background is that I need K ⊆ G and V ⊆ G and they need to share the same +, * and follow the same basic arithmetic rules.

Reference: https://en.wikipedia.org/wiki/Geometric_algebra

view this post on Zulip Jeremy Avigad (Jun 05 2020 at 16:36):

I get a different error message, but the problem seems to be the [is_subring K]. Lean can infer that K is a ring from [field K]. Below, when I ask Lean to print everything and I give it the instance explicitly, it complains that it is trying to match the two different ring instance for K and failing. Why do you need [is_subring K]? If I comment it out, the definition works for me.

import tactic.ring_exp ring_theory.algebra algebra.opposites algebra.commute data.equiv.ring
import linear_algebra.quadratic_form
import data.real.basic
import data.complex.basic

set_option pp.all true

class geometric_algebra (G : Type*) (K : set G) (V : set G)
[field K]
[add_comm_group V] [h : vector_space K V] -- [Q : quadratic_form K V]
[ring G]
[is_subring K]
[is_subring V]
extends algebra K G
 :=
(inner_product : quadratic_form K V _ _ h)

view this post on Zulip Utensil Song (Jun 05 2020 at 16:43):

I need it because there's another property I need that is \forall v : V, v*v \in K

view this post on Zulip Utensil Song (Jun 05 2020 at 16:45):

I can tell the direct cause from the error massage but don't know if it's a limitation of Lean or I'm puting the assumption at the wrong location

view this post on Zulip Utensil Song (Jun 05 2020 at 16:46):

Three places to choose from: [] before extends, after extends, after :=

view this post on Zulip Utensil Song (Jun 05 2020 at 16:51):

By limitation I mean whether one type can be sub-something and something++ and Lean knows the duplication of specifying something is acceptable

view this post on Zulip Jeremy Avigad (Jun 05 2020 at 16:52):

If I understand correctly, what is happening is that you are giving K two different (and possibly entirely unrelated) ring structures. I don't think the type classes are set up to do exactly what you want. Hmm.....

view this post on Zulip Utensil Song (Jun 05 2020 at 16:54):

Yes, I guess that's the root cause and I need to try doing it in another way.

view this post on Zulip Jeremy Avigad (Jun 05 2020 at 16:55):

I think you need to define a special structure for is_subfield K, write down the axioms that describe that, and then show is_subring K and field K both follow.

view this post on Zulip Utensil Song (Jun 05 2020 at 16:56):

but G is not a field...

view this post on Zulip Jeremy Avigad (Jun 05 2020 at 16:56):

(Where is_subfield K says, roughly, that K is equipped with a division that makes it both a field and a subring of the bigger ring. Maybe there is a better name for that, like is_field_as_subring K.)

view this post on Zulip Utensil Song (Jun 05 2020 at 16:57):

I see, that seems ok

view this post on Zulip Utensil Song (Jun 05 2020 at 16:58):

I'll try that, thanks!

view this post on Zulip Johan Commelin (Jun 05 2020 at 16:59):

@Utensil Song In practice it seems to be better in the long run to work with injective structure preserving functions rather than set G

view this post on Zulip Johan Commelin (Jun 05 2020 at 16:59):

(In the perfectoid project we had the definition of a Huber pair, which is a ring A and a subring A^+...

view this post on Zulip Johan Commelin (Jun 05 2020 at 17:00):

And after a while we realised that we couldn't prove that Z_p, Q_p was an example.

view this post on Zulip Johan Commelin (Jun 05 2020 at 17:00):

Because in lean, Z_p is not a subring of Q_p, even though there is a injective ring homomorphism.

view this post on Zulip Johan Commelin (Jun 05 2020 at 17:01):

So then we changed the definition, to use an injective ring hom (or algebra), and most proofs stayed the same, some became shorter.

view this post on Zulip Johan Commelin (Jun 05 2020 at 17:01):

In general it was just a lot more pleasant to work with.

view this post on Zulip Utensil Song (Jun 05 2020 at 17:01):

That's because I just found out how to write is_subring A B (not Lean) from Zulip chat history

view this post on Zulip Utensil Song (Jun 05 2020 at 17:03):

broken into A : set B and is_subring A...

view this post on Zulip Utensil Song (Jun 05 2020 at 17:06):

strictly speaking, in my case, K is indeed not a subring of G

view this post on Zulip Utensil Song (Jun 05 2020 at 17:06):

the hom approach is more accurate

view this post on Zulip Utensil Song (Jun 07 2020 at 14:40):

Johan Commelin said:

So then we changed the definition, to use an injective ring hom (or algebra), and most proofs stayed the same, some became shorter.

The PR seems to be https://github.com/leanprover-community/lean-perfectoid-spaces/pull/56 and particular this commit.

The related code are:

  1. in docs#ring_theory.algebra
class algebra (R : Type u) (A : Type v) [comm_semiring R] [semiring A]
  extends has_scalar R A, R →+* A :=
(commutes' :  r x, to_fun r * x = x * to_fun r)
(smul_def' :  r x, r  x = to_fun r * x)

/-- Embedding `R →+* A` given by `algebra` structure. -/
def algebra_map (R : Type u) (A : Type v) [comm_semiring R] [semiring A] [algebra R A] : R →+* A :=
algebra.to_ring_hom
  1. in https://github.com/leanprover-community/lean-perfectoid-spaces/blob/master/src/Huber_pair.lean
structure Huber_pair :=
(plus : Type)
(carrier : Type)
[ring : comm_ring plus]
[top : topological_space plus]
[Huber : Huber_ring carrier]
[alg : algebra plus carrier]
(intel : is_ring_of_integral_elements plus carrier)

local postfix `` : 66 := λ A : Huber_pair, A.plus

instance : comm_ring (A) := A.ring
instance : topological_space (A) := A.top
instance : Huber_ring A := A.Huber
instance : algebra (A) A := A.alg

view this post on Zulip Utensil Song (Jun 07 2020 at 14:44):

From this example now I can see clearly why @Kevin Buzzard said that B : subring C and algebra B C are kind of the same in https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/algebra.20is.20not.20scaling.20for.20me/near/191348229 (found during searching for a proper solution for my issue here) .

view this post on Zulip Utensil Song (Jun 07 2020 at 14:49):

BTW, I don't know we can do [] after := too(I always wondered how we can reference the algebraic structure), only that it can be used before extends, and we can do it between extends and := without the [].

view this post on Zulip Utensil Song (Jun 07 2020 at 14:56):

And how do we decide where to put [](the type class arguments)? I'm very confused now. All three places seem to be legal, this seems to be just a mathematical design principle issue.

view this post on Zulip Kevin Buzzard (Jun 07 2020 at 14:59):

If you're talking about defining structures and classes, then [] after := means that you tell it the instance at the same time as you're making the structure. Before the := Lean will try to make the instance before you have even started making the structure

view this post on Zulip Utensil Song (Jun 07 2020 at 15:17):

Thanks, but what it means for the definition, mathematically?

view this post on Zulip Utensil Song (Jun 07 2020 at 15:17):

import tactic.ring_exp ring_theory.algebra algebra.opposites algebra.commute data.equiv.ring
import linear_algebra.quadratic_form
import data.real.basic
import data.complex.basic

class test :=
(K : Type*)
(V : Type*)
[field : field K]
[group : add_comm_group V]
[space : vector_space K V]

#check test.mk   -- test.mk ℝ ℝ : test

noncomputable instance test_rr : test := {
  K := ,
  V := 
}

class test'
(K : Type*)
(V : Type*)
[field : field K]
[group : add_comm_group V]
[space : vector_space K V]

#check test'   -- test' ℝ ℝ : Type

instance test'_rr : test'   := by sorry -- by apply_instance -- tactic.mk_instance failed to generate instance for

class test''
(K : Type*)
(V : Type*)
[field : field K]
[group : add_comm_group V]
extends vector_space K V -- invalid 'structure' extends, 'vector_space' is not a structure

view this post on Zulip Utensil Song (Jun 07 2020 at 16:59):

Finally I got to my x of the #xy , here's a #mwe that's actually working :

import tactic.ring_exp ring_theory.algebra algebra.opposites algebra.commute data.equiv.ring
import linear_algebra.quadratic_form
import data.real.basic
import data.complex.basic

class geometric_algebra (G : Type*) (K : Type*) (V : Type*)
[field K] [has_lift K G]
[add_comm_group V] [vector_space K V] [has_lift V G]
[ring G]
 :=
[assoc :  (a b c : G), (a * b) * c = a * (b * c)]
[left_distrib :  a b c : G, a * (b + c) = (a * b) + (a * c)]
[right_distrib :  a b c : G, (a + b) * c = (a * c) + (b * c)]
(v_sq_in_k :  v : V,  k : K, (v : G) * (v : G) = (k : G))

namespace geometric_algebra

variables (G : Type*) (K : Type*) (V : Type*)
[field K] [has_lift K G]
[add_comm_group V] [vector_space K V] [has_lift V G]
[ring G]

variables (a b c : G) [GA : geometric_algebra G K V]

-- the trivial case: prove ℝ is a GA

instance : has_lift   := { lift := λ x, x }

noncomputable instance : geometric_algebra    := {
    assoc := (λ a b c, semigroup.mul_assoc a b c),
    left_distrib := (λ a b c, distrib.left_distrib a b c),
    right_distrib := (λ a b c, distrib.right_distrib a b c),
    v_sq_in_k := begin
        intro v,
        use (v) * (v),
        refl
    end
}

end geometric_algebra

But I have 3 new questions:

Q1: How can I express that there should exist only one k? (by changing \in to \exist, I avoided the has_mem issues but it seems not completely safe)

Q2: Why do I have to write an instance for has_lift ℝ ℝ? Shouldn't it be automatically inferred?

Q3: Why can't assoc, left_distrib, right_distrib be automatically inferred?

view this post on Zulip Johan Commelin (Jun 07 2020 at 17:25):

@Utensil Song You are requiring [ring G] and afterwards you have axioms assoc, left_distrib, and right_distrib. But those are already part of ring G...
Did you mean something else?

view this post on Zulip Johan Commelin (Jun 07 2020 at 17:26):

Also, you are not asking for any compatibility of the field structure on K and the ring structure on G. Should the has_lift respect multiplication and addition?

view this post on Zulip Utensil Song (Jun 07 2020 at 17:30):

Johan Commelin said:

Utensil Song You are requiring [ring G] and afterwards you have axioms assoc, left_distrib, and right_distrib. But those are already part of ring G...
Did you mean something else?

I think that I might have done something redundant here, but what I was thinking is that G is a ring but geometric_algebra G K V isn't so I added these trivial properties and name them under geometric_algebra. This seems to be exactly why it can't be inferred.

Ignore Q3 then.

view this post on Zulip Utensil Song (Jun 07 2020 at 17:35):

Johan Commelin said:

Also, you are not asking for any compatibility of the field structure on K and the ring structure on G. Should the has_lift respect multiplication and addition?

Yes, you're right, it should, I can add [algebra K G] back, and everything still works.

I removed it for K since I can't do the same for V. [algebra V G] requires V to be [comm_semiring V] but * (geometric product) does not commute for vectors and it's not even a group since the multiplication is not closed, a vector times a vector becomes a bivector, it's in G, but not in V. But actually for K, [algebra V G] is fine and so is the * for K.

view this post on Zulip Patrick Massot (Jun 07 2020 at 17:44):

Kevin Buzzard said:

If you're talking about defining structures and classes, then [] after := means that you tell it the instance at the same time as you're making the structure. Before the := Lean will try to make the instance before you have even started making the structure

Either I don't understand this or Kevin is wrong here.

view this post on Zulip Kevin Buzzard (Jun 07 2020 at 17:49):

I can quite believe I'm wrong. I think Utensil Song knows exactly what they are talking about at this point though.

view this post on Zulip Utensil Song (Jun 07 2020 at 17:57):

~To answer Q1, it seems that I should take a closer look at~

/--An R-algebra A is integrally closed if every element of A that is integral over R is contained in
the image of the canonical map R → A. This algebra_map is required to be injective.-/
structure is_integrally_closed : Prop :=
(inj : injective (algebra_map A : R  A))
(closed :  a : A, (is_integral R a)  a  set.range (algebra_map A : R  A))

~from the Huber_pair PR.~

EDIT: doesn't help. The injection of the lift seems to be covered in [algebra K G] , the uniqueness of k is another question.

view this post on Zulip Utensil Song (Jun 07 2020 at 18:00):

Kevin Buzzard said:

I can quite believe I'm wrong. I think Utensil Song knows exactly what they are talking about at this point though.

From the tests in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/synthesized.20not.20defeq.20inferred/near/200028361 , I do know that they're very different, but still, the applicability of each choice is still an unsolved puzzle.

view this post on Zulip Kevin Buzzard (Jun 07 2020 at 18:01):

Lean is just letting you write what you mean.

view this post on Zulip Utensil Song (Jun 07 2020 at 18:09):

Indeed.

view this post on Zulip Kevin Buzzard (Jun 07 2020 at 18:34):

However sometimes there is more than one way to write what you mean...

view this post on Zulip Utensil Song (Jun 12 2020 at 05:42):

After updating Lean to 3.16.0 and mathlib to mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "593f731dd200fe74c218ff9886eb663d4a860dcd"} using leanproject up, Lean dies frequently for the following #mwe :

import algebra.group.hom
import ring_theory.algebra
import data.real.basic
import data.complex.basic

universes u u₀ u₁

class geometric_algebra (G : Type*)
-- Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀] [char_zero G₀] [has_zero G₀] [has_one G₀]
-- Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
-- Axiom 1: G is a ring with unit.
-- The additive identity is called 0 and the multiplicative identity is called 1.
[ring G] [has_zero G] [has_one G]
-- TODO: find better ways to map G₀ and G₁ to G
[has_coe G₀ G] [has_coe G₁ G]
[G₀ →+* G]
[G₁ →+ G]
[algebra G₀ G]
:=
-- Axiom 4: The square of every vector is a scalar.
(vec_sq_scalar :  v : G₁,  k : G₀, (v * v : G) = (k : G))

namespace geometric_algebra

section

variables (G : Type*)
-- Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀] [char_zero G₀] [has_zero G₀] [has_one G₀]
-- Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
-- Axiom 1: G is a ring with unit.
-- The additive identity is called 0 and the multiplicative identity is called 1.
[ring G] [has_zero G] [has_one G]
-- TODO: find better ways to map G₀ and G₁ to G
[has_coe G₀ G] [has_coe G₁ G]
[G₀ →+* G]
[G₁ →+ G]
[algebra G₀ G]
[GA : geometric_algebra G G₀ G₁]

end
end geometric_algebra

view this post on Zulip Utensil Song (Jun 12 2020 at 05:44):

After every restart of Lean, and opening only this #mwe in the editor, the orange bar shows up and does not disappear and then
image.png

view this post on Zulip Utensil Song (Jun 12 2020 at 05:45):

How can I get more trace log to debug this?

view this post on Zulip Mario Carneiro (Jun 12 2020 at 05:46):

I don't have any issues running this, although I get an error on the last line because [G₀ →+* G] [G₁ →+ G] are not classes

view this post on Zulip Mario Carneiro (Jun 12 2020 at 05:47):

Usually, if you get something that kills lean straight away, it requires some C++ debugging

view this post on Zulip Mario Carneiro (Jun 12 2020 at 05:47):

because you don't have the opportunity to ask more info

view this post on Zulip Utensil Song (Jun 12 2020 at 05:52):

[G₀ →+* G] [G₁ →+ G] are not classes

Oh I see, type class algebra extends them but it doesn't mean I can use them as type classes. But I can't extend them either since there would be duplicated to_fun etc.

view this post on Zulip Mario Carneiro (Jun 12 2020 at 05:54):

you don't need to extend them

view this post on Zulip Utensil Song (Jun 12 2020 at 05:54):

I don't have any issues running this

I don't always have issues running this, but when I comment out some type classes and add some back, somehow it triggers Lean to be killed and it stays that way even after restart

view this post on Zulip Mario Carneiro (Jun 12 2020 at 05:54):

just have a field

view this post on Zulip Utensil Song (Jun 12 2020 at 05:54):

G1 is not a field by itself

view this post on Zulip Mario Carneiro (Jun 12 2020 at 05:55):

no, the function

view this post on Zulip Mario Carneiro (Jun 12 2020 at 05:55):

the two functions should be fields of the structure

view this post on Zulip Mario Carneiro (Jun 12 2020 at 05:55):

well probably not [G₀ →+* G] since that one duplicates the function embedded in the algebra

view this post on Zulip Mario Carneiro (Jun 12 2020 at 05:56):

you should not ask for has_coe instances either

view this post on Zulip Utensil Song (Jun 12 2020 at 05:57):

the intention was to comment out the has_coe, algebra lines

view this post on Zulip Utensil Song (Jun 12 2020 at 05:57):

Mario Carneiro: the two functions should be fields of the structure

I'll try that

view this post on Zulip Mario Carneiro (Jun 12 2020 at 06:00):

I think you want something like this:

class geometric_algebra (G : Type*)
-- Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀] [char_zero G₀]
-- Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
-- Axiom 1: G is a ring with unit.
[ring G]
[algebra G₀ G]
:=
(f₁ : G₁ →+ G)
-- Axiom 4: The square of every vector is a scalar.
(vec_sq_scalar :  v : G₁,  k : G₀, f₁ v * f₁ v = algebra_map _ _ k)

view this post on Zulip Utensil Song (Jun 12 2020 at 06:01):

import algebra.group.hom
import ring_theory.algebra
import data.real.basic
import data.complex.basic

universes u u₀ u₁

class geometric_algebra (G : Type*)
-- Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀] [char_zero G₀] [has_zero G₀] [has_one G₀]
-- Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
-- Axiom 1: G is a ring with unit.
-- The additive identity is called 0 and the multiplicative identity is called 1.
[ring G] [has_zero G] [has_one G]
-- TODO: find better ways to map G₀ and G₁ to G
-- [has_coe G₀ G] [has_coe G₁ G]
-- [G₀ →+* G]
-- [algebra G₀ G]
:=
(scalar_hom : G₀ →+* G)
(vec_hom : G₁ →+ G)
-- Axiom 4: The square of every vector is a scalar.
(vec_sq_scalar :  v : G₁,  k : G₀, vec_hom(v) * vec_hom(v) = scalar_hom(k) )

Here's what I came up with

view this post on Zulip Mario Carneiro (Jun 12 2020 at 06:01):

you have a lot of duplicate data in the parameters

view this post on Zulip Utensil Song (Jun 12 2020 at 06:02):

Oh, algebra_map _ _ k is the scalar_hom equivalent

view this post on Zulip Mario Carneiro (Jun 12 2020 at 06:03):

those has_zero and has_one instances are also duplicate

view this post on Zulip Utensil Song (Jun 12 2020 at 06:03):

Mario Carneiro: you have a lot of duplicate data in the parameters

Yes, I'm trying to see the effect of doing so. Was expecting to get warnings about them.

view this post on Zulip Mario Carneiro (Jun 12 2020 at 06:03):

no, you will just get stuck in proofs

view this post on Zulip Mario Carneiro (Jun 12 2020 at 06:03):

I don't think lean knows what a warning is

view this post on Zulip Mario Carneiro (Jun 12 2020 at 06:05):

If you have any duplicate data, you are constructing something like "a field with two independent multiplications" or similar. Any theorem using one operation will not be able to play well with definitions based on the other

view this post on Zulip Utensil Song (Jun 12 2020 at 06:06):

Mario Carneiro: no, you will just get stuck in proofs

Oh, I got stuck somewhere else. Using has_coe made me to prove ↑kab - ↑ka - ↑kb = ↑(kab - ka - kb) which can't be proved unless I have a ->+.

view this post on Zulip Mario Carneiro (Jun 12 2020 at 06:06):

for example, with [field G₀] [has_one G₀] you will not be able to prove 1 * x = x

view this post on Zulip Mario Carneiro (Jun 12 2020 at 06:06):

because nothing says that 1 is a unit

view this post on Zulip Utensil Song (Jun 12 2020 at 06:07):

Oh, I thought it's eliminated in the solution to the diamond problem.

view this post on Zulip Mario Carneiro (Jun 12 2020 at 06:07):

if they were fields it would be a different matter, but you are passing everything as parameters

view this post on Zulip Mario Carneiro (Jun 12 2020 at 06:08):

there is no way for lean to assert a relation on the inputs unless you provide such relation

view this post on Zulip Mario Carneiro (Jun 12 2020 at 06:10):

I notice that Axiom 2 and Axiom 3 make additional claims about closure. These need to be axioms inside the structure

view this post on Zulip Mario Carneiro (Jun 12 2020 at 06:10):

maybe they come for free given the homs

view this post on Zulip Utensil Song (Jun 12 2020 at 06:13):

Mario Carneiro: maybe they come for free given the homs

I believe so

view this post on Zulip Utensil Song (Jun 12 2020 at 14:47):

@Mario Carneiro I can't refer to f1 later though:

import ring_theory.algebra

class geometric_algebra (G : Type*)
-- Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀] [char_zero G₀]
-- Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
-- Axiom 1: G is a ring with unit.
[ring G]
[algebra G₀ G]
:=
(f₁ : G₁ →+ G)
-- Axiom 4: The square of every vector is a scalar.
(vec_sq_scalar :  v : G₁,  k : G₀, f₁ v * f₁ v = algebra_map _ _ k)

namespace geometric_algebra

section

variables (G : Type*)
-- Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀] [char_zero G₀]
-- Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
-- Axiom 1: G is a ring with unit.
[ring G]
[algebra G₀ G]
[GA : geometric_algebra G G₀ G₁]

def square (a : G) := a * a

def sym_prod (a b : G) := a * b + b * a

local infix `*`:75 := sym_prod

local postfix `²`:80 := square

#check f₁

/-
  Symmetrised product of two vectors must be a scalar
-/
lemma vec_sym_prod_scalar_failed :
 (a b : G₁),  k : G₀,
  f₁ a * f₁ b = algebra_map _ _ k := by sorry

-- type mismatch at application
--   f₁ a
-- term
--   a
-- has type
--   G₁ : Type u_3
-- but is expected to have type
--   Type ? : Type (?+1)
-- Additional information:
-- minimal.lean:43:2: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
--   type mismatch, term
--     f₁ ?m_2
--   has type
--     ?m_1 →+ ?m_2 : Type (max ? ?)
--   but is expected to have type
--     Type ? : Type (?+1)

lemma vec_sym_prod_scalar_still_failed :
 (a b : G₁),  k : G₀,
  (f₁ G₀ a) * (f₁ G₀ b) = algebra_map _ _ k := by sorry
-- failed to synthesize type class instance for
-- G₀ : Type u_2,
-- _inst_1 : field G₀,
-- _inst_2 : char_zero G₀,
-- G₁ : Type u_3,
-- _inst_3 : add_comm_group G₁,
-- _inst_4 : vector_space G₀ G₁,
-- a b : G₁,
-- k : G₀
-- ⊢ ring (Type ?)

end

end geometric_algebra

And Lean dies randomly again...

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 17:58):

I'm not able to reproduce this random dying thing. If you hover over the first error, namely f₁, you see that it has this type:

geometric_algebra.f₁ : Π {G : Type u_1} (G₀ : Type u_2) [_inst_1 : field G₀] [_inst_2 : char_zero G₀] {G₁ : Type u_3} [_inst_3 : add_comm_group G₁] [_inst_4 : vector_space G₀ G₁] [_inst_5 : ring G] [_inst_6 : algebra G₀ G] [c : geometric_algebra G G₀ G₁], G₁ →+ G

In particular f₁ a will not work because a is supposed to be G₀, the first () input to f₁

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 18:00):

If you would like G₀ to be inferred by unification, then change (G₀ : Type*) to {G₀ : Type*} when you're setting up your variables.

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 18:03):

Your second error is because when Lean sees f₁ G₀ a it has to now guess all of the {} variables for f₁ by unification, and it doesn't know how to guess G, so it just uses a metavariable, and then it has to prove that this metavariable is a ring because of [ring G], so it gets stuck.

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 18:07):

Next problem: sym_prod expects an explicit G (look at the type) so the *₊ notation won't work.

include GA -- you named it, so it doesn't get included automatically
-- and Lean cannot solve the problem you have left it regarding implicit variables so I
-- told it the solution explicitly
lemma vec_sym_prod_scalar_typechecks :
 (a b : G₁),  k : G₀,
  sym_prod G (@f₁ G G₀ _ _ G₁ _ _ _ _ _ a) (@f₁ G G₀ _ _ G₁ _ _ _ _ _ b) = algebra_map _ _ k := by sorry

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 18:09):

The problem is that if you're just telling f\_1 that it's going to eat a, then it can figure out G\_1, but it can't figure out G or G\_0 because even though we have geometric_algebra G G₀ G₁ Lean thinks that maybe there could be some other instances geometric_algebra H H₀ G₁ so it will refuse to guess G and G_0 from what you told it.

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 18:10):

One easy fix is to let f_1 also eat G and G_0. This sort of thing happens with algebras in Lean -- if A is an R-algebra then Lean never quite knows if A is an algebra for any other ring too, so many definitions and lemmas about R-algebras ask for R explicitly.

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 18:20):

You probably want to make G implicit in sym_prod and to make G and G_0 explicit in f_1. Maybe this?

import ring_theory.algebra

class geometric_algebra (G : Type*)
-- Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀] [char_zero G₀]
-- Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
-- Axiom 1: G is a ring with unit.
[ring G]
[algebra G₀ G]
:=
(f₁' : G₁ →+ G) -- I added a prime because the binders are wrong
-- Axiom 4: The square of every vector is a scalar.
(vec_sq_scalar :  v : G₁,  k : G₀, f₁' v * f₁' v = algebra_map _ _ k)

namespace geometric_algebra

#check @f₁' -- G is implicit
-- let's fix those binders
def f₁ (G : Type*) -- explicit G
  (G₀ : Type*) [field G₀] [char_zero G₀] {G₁ : Type*}
  [add_comm_group G₁] [vector_space G₀ G₁] [ring G] [algebra G₀ G]
  [geometric_algebra G G₀ G₁] : G₁ →+ G := @f₁' G G₀ _ _ G₁ _ _ _ _ _

section

variables {G : Type*} -- make it implicit
-- Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀] [char_zero G₀]
-- Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
-- Axiom 1: G is a ring with unit.
[ring G]
[algebra G₀ G]
[geometric_algebra G G₀ G₁] -- removing the name

def square (a : G) := a * a

-- implicit G for sym_prod
def sym_prod (a b : G) := a * b + b * a

local infix `*`:75 := sym_prod

local postfix `²`:80 := square

-- now back to explicit G
variable (G)
/-
  Symmetrised product of two vectors must be a scalar
-/
lemma vec_sym_prod_scalar_typechecks :
 (a b : G₁),  k : G₀,
  (f₁ G G₀ a) * (f₁ G G₀ b) = algebra_map _ _ k := by sorry

end

end geometric_algebra

view this post on Zulip Utensil Song (Jun 13 2020 at 03:54):

Thanks for your detailed explanations on how Lean works , here's the further #mwe to demonstrate what I need partially following your hints with many comments describing my motivation and goal here:

import algebra.group.hom
import ring_theory.algebra
import data.real.basic
import data.complex.basic

universes u u₀ u₁

class geometric_algebra
-- Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀]
-- Axiom 3: G contains a subset G1 closed under addition, and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
-- Axiom 1: G is a ring with unit.
-- The additive identity is called 0 and the multiplicative identity is called 1.
(G : Type*) [ring G] [algebra G₀ G]
:=
(f₁ : G₁ →+ G)
-- Axiom 4: The square of every vector is a scalar.
(vec_sq_scalar :  v : G₁,  k : G₀, f₁ v * f₁ v = algebra_map _ _ k )

namespace geometric_algebra

section

variables
{G₀ : Type*} [field G₀]
{G₁ : Type*} [add_comm_group G₁] [vector_space G₀ G₁]
{G : Type*} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G]

def square (a : G) := a * a

def sym_prod (a b : G) := a * b + b * a

local infix `*`:75 := sym_prod

local postfix `²`:80 := square

#check @f₁

-- implicit G₀
def f₁' : G₁ →+ G := f₁ G₀

#check @f₁'
/-
f₁' :
  Π {G₀ : Type u_4} [_inst_1 : field G₀]
  {G₁ : Type u_5} [_inst_2 : add_comm_group G₁] [_inst_3 : vector_space G₀ G₁]
  {G : Type u_6} [_inst_4 : ring G] [_inst_5 : algebra G₀ G]
  [_inst_6 : geometric_algebra G₀ G₁ G],
  G₁ →+ G
-/

/-
  Symmetrised product of two vectors must be a scalar
-/
lemma vec_sym_prod_scalar_works_but_not_ideal :
 (a b : G₁),  k : G₀,
  f₁ G₀ a * f₁ G₀ b = algebra_map G₀ G k := by sorry
/-
OK, it seems Lean knows G₁ from a and b,
but requires explicit G₀ to know to which G f₁ belongs
-/

lemma vec_sym_prod_scalar_works_inferred_as_much_as_possible :
 (a b : G₁),  k : G₀,
  f₁ G₀ a * f₁ G₀ b = algebra_map _ G k := by sorry
/-
The only thing can be inferred is the type of k from k
-/

lemma vec_sym_prod_scalar_better_but_failed:
 (a b : G₁),  k : G₀,
  f₁' a * f₁' b = algebra_map G₀ G k := by sorry
/-
Here's why I "think" this should work:
- rhs fixed G₀ and G, a and b fixed G₁, Lean should know everything about f₁'
- plus *₊ fixed G too

Note that now I've made all parameters in f₁' implicit
-/

lemma vec_sym_prod_scalar_ideal_but_seems_impossble_in_lean:
 (a b : G₁),  k : G₀,
  a * b = k := by sorry
/-
Here's why I further "think" this should work:
- a and b fixed G₁
- *₊ fixed G
- G₀ can be inferred from [geometric_algebra G₀ G₁ G]

Here's why I want it:

It's closer to how it's stated in literature, without the hassle of homs
and I have to state more complicated theoerem that involves more +-*/exp
as in https://github.com/pygae/GAlgebra.jl/blob/master/test/runtests.jl#L321

Here's how I'm so close to it:

If I relax →+ and demand [has_coe G₀ G], then I get to state it like:

lemma vec_sym_prod_scalar [geometric_algebra G K V] :
∀ (a b : V), ∃ k : K, a *₊ b = (k : G) := by sorry

as in https://github.com/pygae/lean-ga/blob/master/src/geometric_algebra/nursery/basic.lean#L98
-/

end

end geometric_algebra

view this post on Zulip Utensil Song (Jun 13 2020 at 04:14):

The crucial thing here is "even though we have geometric_algebra G G₀ G₁ Lean thinks that maybe there could be some other instances geometric_algebra H H₀ G₁ so it will refuse to guess G and G_0 from what you told it."

view this post on Zulip Utensil Song (Jun 13 2020 at 04:15):

Is there a way to force so, just locally?

view this post on Zulip Utensil Song (Jun 13 2020 at 04:16):

(sorry I change the order of G₀ G₁ G to make it in an ascendant order like in algebra)

view this post on Zulip Alex J. Best (Jun 13 2020 at 04:46):

The @ character can be used to tell lean you want to explicitly fill some implicit types in

lemma vec_sym_prod_scalar_better_but_failed:
 (a b : G₁),  k : G₀,
  (@f₁' G₀ _ _ _ _ _ _ _ _) a * (@f₁' G₀ _ _ _ _ _ _ _ _) b = algebra_map G₀ G k := by sorry

I think your logic that the right hand side of this fixes G₀ doesn't really follow, the type of the RHS is G and just because you used a particular G₀ doesn't mean the LHS has to use the same one.
P.s. the extra brackets I added aren't needed really.

view this post on Zulip Utensil Song (Jun 13 2020 at 04:47):

It seems that to achieve what I want, I have to redesign the whole thing from ground up.

Starting by giving G₁ a (not has_mul) multiplication that always return G but it's actually just G₀ or G₂, which in turn needs a grade projection operator first, and make G₁ not special and not in the parameters but generated from a projection. But in this case I'll have to use G -> set G as the type of the grade projection, which I have been trying to avoid, because I want G₀ and G₁ to be a real type and not a type to Prop. And then from there I'll need to redefine eq as well, because eventually I'll need all 0 in G₀, G₁, G₂, ..., G etc. to equal and a G with only G₁ or G₂ components to equal to G₁ or G₂. I'll also need to state that G can be written as the infinite sum of G₀, G₁, G₂, ..., which might involve some cardinality stuff......

(This formalism is used in GA to GC by Hestenes and Sobczyk, I thought I could try something simpler first, but the simpler formalism seems to be making it more difficult in Lean)

(To make the discussion above easier to interpret, think G as another formalism to spell out Clifford Algebra (it seems to be not ready to be defined generally in mathlib yet as I've read on the Zulip, as well as Grassmann Algebra i.e. exterior algebra ).)

view this post on Zulip Utensil Song (Jun 13 2020 at 04:49):

Alex J. Best said:

I think your logic that the right hand side of this fixes G₀ doesn't really follow, the type of the RHS is G and just because you used a particular G₀ doesn't mean the LHS has to use the same one.

Yes, I can see that now, but I'm wondering whether it's possible to specify so somehow.

view this post on Zulip Alex J. Best (Jun 13 2020 at 04:53):

I haven't used it myself, but perhaps using parameters instead of variables in this file does what you want

view this post on Zulip Utensil Song (Jun 13 2020 at 05:05):

Oh silly me, I've confused them before and doing this again...Changing variables to parameters makes vec_sym_prod_scalar_better_but_failed work as expected! Thanks!

view this post on Zulip Utensil Song (Jun 13 2020 at 16:43):

Is there anyway to simply use ccafter rw h1, by making it somehow see through homs? It's painful to move terms around step by step...

      begin
        intros hb ha hab,
        /-
          G₀ : Type u_1,
          _inst_1 : field G₀,
          G₁ : Type u_2,
          _inst_2 : add_comm_group G₁,
          _inst_3 : vector_space G₀ G₁,
          G : Type u_3,
          _inst_4 : ring G,
          _inst_5 : algebra G₀ G,
          _inst_6 : geometric_algebra G₀ G₁ G,
          a b : G₁,
          h1 : (a + b)²ᵥ = a²ᵥ + b²ᵥ + a*₊ᵥ b,
          vec_sq_scalar : ∀ (v : G₁), ∃ (k : G₀), v²ᵥ = ⇑fₛ k,
          kab ka kb : G₀,
          hb : b²ᵥ = ⇑fₛ kb,
          ha : a²ᵥ = ⇑fₛ ka,
          hab : (a + b)²ᵥ = ⇑fₛ kab
          ⊢ ∃ (k : G₀), a*₊ᵥ b = ⇑fₛ k
        -/
        rw [hb, ha, hab] at h1,
        use (-ka) + (-kb) + kab,
        -- a*₊ᵥ b = ⇑fₛ (-ka - kb + kab)
        rw ring_hom.map_add,
        rw h1,
        -- a*₊ᵥ b = ⇑fₛ (-ka + -kb) + (⇑fₛ ka + ⇑fₛ kb + a*₊ᵥ b)
        rw add_assoc,
        -- a*₊ᵥ b = ⇑fₛ (-ka + -kb) + (⇑fₛ ka + ⇑fₛ kb) + a*₊ᵥ b
        rw add_assoc,
        -- a*₊ᵥ b = ⇑fₛ (-ka + -kb) + ⇑fₛ ka + ⇑fₛ kb + a*₊ᵥ b
        rw ring_hom.map_add,
        -- a*₊ᵥ b = ⇑fₛ (-ka + -kb + ka) + ⇑fₛ kb + a*₊ᵥ b
        rw ring_hom.map_add,
        -- a*₊ᵥ b = ⇑fₛ (-ka + -kb + ka + kb) + a*₊ᵥ b
        rw add_comm (-ka) (-kb),
        -- a*₊ᵥ b = ⇑fₛ (-kb + -ka + ka + kb) + a*₊ᵥ b
        rw add_assoc (-kb) (-ka) ka,
        -- a*₊ᵥ b = ⇑fₛ (-kb + (-ka + ka) + kb) + a*₊ᵥ b
        simp only [add_zero, ring_hom.map_zero, add_left_neg, zero_add],
      end

(Full working code is too long to paste in here, it's at https://github.com/pygae/lean-ga/blob/1d589406ffbed0e00bafff18bf1466689ea8b4b8/src/geometric_algebra/nursery/chisolm.lean#L97 )

view this post on Zulip Kevin Buzzard (Jun 13 2020 at 17:51):

After use (-ka) + (-kb) + kab, you can do simp [fₛ.map_add, h1], which immediately reduces your goal to

 a*₊ᵥ b = -fₛ ka + -fₛ kb + (fₛ ka + fₛ kb + a*₊ᵥ b)

and then the abel tactic finishes the job.

        rw [hb, ha, hab] at h1,
        use (-ka) + (-kb) + kab,
        -- a*₊ᵥ b = ⇑fₛ (-ka - kb + kab)
        simp [fₛ.map_add, h1],
        abel,

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

Alex J. Best said:

I haven't used it myself, but perhaps using parameters instead of variables in this file does what you want

But parameters is being removed in lean 4, right? So what should we do here instead?

view this post on Zulip Alex J. Best (Jun 29 2020 at 16:31):

Well if the problem you're trying to solve is, "I have a bunch of variables, and every def/lemma/theorem in the theory I'm writing takes all of them as input and I don't want to write them all the time (i.e. some ambient space / ring you are working in with some properties)" then I think the solution is to bundle everything you need into a structure that holds all these assumptions and use a single variable of type that structure and use that as input to every lemma etc.

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

Or just don't worry about what Lean 4 may or may not do.

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

Well in this case I run into the same problem using variables as I do trying to move my parameters to separate files

view this post on Zulip Alex J. Best (Jun 29 2020 at 16:36):

Can you give an example of what you mean?

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

I'm trying to

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

Here's a fairly minimal example:

import algebra.group.hom
import ring_theory.algebra

class geometric_algebra
(G₀ : Type*) [field G₀]
(G₁ : Type*) [add_comm_group G₁]
(G : Type*) [ring G]
:=
(f₁ : G₁ →+ G)

namespace geometric_algebra
section

/- doesn't work if `variables` instead -/
parameters
{G₀ : Type*} [field G₀]
{G₁ : Type*} [add_comm_group G₁]
{G : Type*} [ring G] [geometric_algebra G₀ G₁ G]

def f : G₁ →+ G := f₁ G₀
def prod_vec (a b : G₁) : G := f a * f b

end

end geometric_algebra

As is, this has no errors.

If I change parameters to variables, then prod_vec doesn't "know how to synthesize placeholder" at fᵥ.

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

But I if leave it with parameters, then I have the same problem attempting to use fᵥ from another file.

view this post on Zulip Utensil Song (Jun 29 2020 at 16:43):

The problem from the beginning is that I put too many things in parameters, which should probably be bundled into the class.

view this post on Zulip Utensil Song (Jun 29 2020 at 16:46):

But still, I'm very confused about the subtle differences between parameters and variables and the idiomatic ways to use them.

view this post on Zulip Utensil Song (Jun 29 2020 at 16:47):

As demonstrated in the #mwe above

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:47):

idiomatic in the sense of mathlib is "don't use parameters"

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:47):

But I'm not a mathlib dictator!

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:47):

So feel free to use them. I've just never used them myself.

view this post on Zulip Utensil Song (Jun 29 2020 at 16:48):

then how to use variables to achieve similar purpose?

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

I'm seeing the argument against using parameters since I've been trying to split a section in two, but I can't work out an alternative spelling of the above without parameters that doesn't need a gazillion _ placeholders

view this post on Zulip Utensil Song (Jun 29 2020 at 16:48):

I wish to avoid relying on something not recommended by mathlib

view this post on Zulip Bryan Gin-ge Chen (Jun 29 2020 at 16:50):

I think making G implicit in fᵥ is a bit strange. The issue is that when you write fᵥ a , Lean can't tell what G should be.

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

Changing to def fᵥ (G : Type*) : G₁ →+ G := f₁ G₀ in the example above results in an error at →+

view this post on Zulip Utensil Song (Jun 29 2020 at 16:51):

The end goal is even to remove the need of fv...

view this post on Zulip Utensil Song (Jun 29 2020 at 16:52):

since they're not in the original math

view this post on Zulip Utensil Song (Jun 29 2020 at 16:53):

the arithmetic just works across "types"

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

I'd still like to understand how to write the #mwe above, even if we don't end up needing it

view this post on Zulip Utensil Song (Jun 29 2020 at 16:54):

yeah

view this post on Zulip Bryan Gin-ge Chen (Jun 29 2020 at 17:08):

Oh, I was wrong. The issue wasn't with G being implicit, but with G₀:

import algebra.group.hom
import ring_theory.algebra

class geometric_algebra
(G₀ : Type*) [field G₀]
(G₁ : Type*) [add_comm_group G₁]
(G : Type*) [ring G]
:=
(f₁ : G₁ →+ G)

namespace geometric_algebra
section

variables
(G₀ : Type*) [field G₀] -- I made G₀ explicit here
{G₁ : Type*} [add_comm_group G₁]
{G : Type*} [ring G] [geometric_algebra G₀ G₁ G]

def f : G₁ →+ G := f₁ G₀
def prod_vec (a b : G₁) : G := (f G₀ a) * (f G₀ b)

end

end geometric_algebra

view this post on Zulip Bryan Gin-ge Chen (Jun 29 2020 at 17:09):

As Alex says, I get the feeling this would be easier with more bundling though.

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

What do you mean by bundling in this case?

view this post on Zulip Bryan Gin-ge Chen (Jun 29 2020 at 17:11):

Instead of:

class geometric_algebra
(G₀ : Type*) [field G₀]
(G₁ : Type*) [add_comm_group G₁]
(G : Type*) [ring G]
:=
(f₁ : G₁ →+ G)

Something more like:

class geometric_algebra
(G : Type*)
:=
(G₀ : Type*) (f : field G₀)
(G₁ : Type*) (acg : add_comm_group G₁)
(r : ring G)
(f₁ : G₁ →+ G)

(I haven't tested the latter.)

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

That was what I was about to ask

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

That means the field and add_comm_group fields have to be provided explicitly though, right?

view this post on Zulip Bryan Gin-ge Chen (Jun 29 2020 at 17:12):

They should only need to be provided once though when you create an instance of geometric_algebra G.

view this post on Zulip Bryan Gin-ge Chen (Jun 29 2020 at 17:13):

There's a little more about bundled vs unbundled stuff in 4.1.1 of the mathlib paper.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:13):

by apply_instance will supply the e.g. field instance if you're making an instance of the bundled structure

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

I suppose we can make a helper def to obtain them automatically anyway?

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

geometric_algebra.mk_from_instances or something?

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:14):

Eric Wieser said:

That means the field and add_comm_group fields have to be provided explicitly though, right?

You can also use [] for fields in a class.

view this post on Zulip Bryan Gin-ge Chen (Jun 29 2020 at 17:15):

Right, so:

class geometric_algebra (G : Type*)
:=
(G₀ : Type*) [f : field G₀]
(G₁ : Type*) [ag : add_comm_group G₁]
[r : ring G]
(f₁ : G₁ →+ G)

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:16):

Something in between would be to make the three types into arguments, but put all the other stuff in fields.

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:17):

Also, don't you need more functions, and injectivity assumptions?

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

This becomes slightly painful because we have as a field that I removed, (vec_sq_scalar : ∀ v : G₁, ∃ k : G₀, f₁ v * f₁ v = algebra_map _ _ k ), where algebra_map needs the [] arguments

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

Johan Commelin said:

Also, don't you need more functions, and injectivity assumptions?

Yes, I stripped them to get a #mwe of parameter woes

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:18):

import tactic data.complex.basic

noncomputable theory

structure geometric_algebra
(G : Type*)
:=
(G₀ : Type*) [f : field G₀]
(G₁ : Type*) [acg : add_comm_group G₁]
[r : ring G]
(f₁ : G₁ →+ G)

example : geometric_algebra  :=
{ G₀ := ,
  G₁ := ,
  f₁ := add_monoid_hom.id  }

It should surely be a structure not a class if it's bundled this much. How many terms of type geometric_algebra ℂ might there be? Surely "more than one" is a reasonable answer. So structure not class.

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

I think "exactly one" is a perfectly reasonable answer

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

is canonically Cl(0, 1), I think - a GA with a one-dimensional vector space, with the sole basis vector squaring to -1

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

Now maybe I misunderstand the question "how many terms of the form ..."

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:24):

I don't know what a geometric algebra is... so I can't really help there. (I know Clifford algebras, and I think they are examples.)

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:25):

The reason [group G] is a class is that if G is a set/type/whatever you want to call it, then it is generally unlikely that you will want to put more than one group structure on G (i.e. two different multiplications).

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

I was under the impression they were synonymous, but I may be mistaken

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:25):

So under normal circumstances, if G is a type then there will be at most one term of type group G

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:25):

Eric Wieser said:

I was under the impression they were synonymous, but I may be mistaken

Maybe! Like I said, I don't know what a geom alg is

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:25):

The type class inference system algorithm assumes that there will be at most one instance per class.

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

Wikipedia says "Real Clifford algebras are also sometimes referred to as geometric algebras."

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:27):

If you decided to make a vector space structure and wrote

class vector_space (k : Type) [field k] :=
(V : Type)
(all the structure of a vector space on V)

then this would be bad, because a term of type vector_space k would be a vector space over K, and because it's a class, each field is allowed to have at most one vector space over it.

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

I think I now see Kevin's point. ℂ can be thought of as either a 0-d clifford algebra over itself, or a 1d clifford algebra over the reals

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

So at least G₀ needs to be an argument too

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:29):

The question with

class geometric_algebra (G : Type*)
:=
(G₀ : Type*) [f : field G₀]
(G₁ : Type*) [ag : add_comm_group G₁]
[r : ring G]
(f₁ : G₁ →+ G)

is nothing to do with what happens when G changes. It's precisely to do with what happens if the other stuff changes.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:29):

If you want more than one G_0 for a given G then you must make it a structure not a class.

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

Or a class taking two arguments?

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:29):

Eric Wieser said:

So at least G₀ needs to be an argument too

No. Not if you make it a structure

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:30):

This is a design decision. You can make whatever you like an input or a structure field.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:30):

My only point was simply that class means that you expect at most one instance, and structure means you are allowed as many as you like.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:31):

but which mathematical object corresponds to "instance" depends on what you make as structure fields and what you make as inputs. The answer changes.

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

All makes sense, thanks.

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

I suppose the question now is whether I expect G₀ to uniquely parameterize a geometric algebra G, or if there's a situation I haven't thought of where multiple choices of G₁ are available

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:33):

If you want help with that decision, please write down 3 examples for me.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:34):

Yes, the definition is completely confusing

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:34):

(in its current state, where G_0 plays no role at all)

view this post on Zulip Utensil Song (Jun 29 2020 at 17:34):

for a given G, there's only one G0

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

Not if we generalize to the clifford algebras I think...

view this post on Zulip Utensil Song (Jun 29 2020 at 17:35):

it's still the same

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

Kevin Buzzard said:

Yes, the definition is completely confusing

That's because the one I post above was the minimum definition that showed a language difficulty, not a mathematically meaningful statement!

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:36):

Can you write down the definition in maths?

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:36):

Or link to one?

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:36):

That's because the one I post above was the minimum definition that showed a language difficulty, not a mathematically meaningful statement!

Yes, I know :-) That's why Johan just wants to see some examples. Then we'll get the hang of it.

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

I can give the paper that @Utensil Song started our formalization from: https://arxiv.org/abs/1205.5935

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:37):

I would rather see three examples of G, G_0 and G_1

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

Ah, ok, got it

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:39):

The definition on wiki is vague and incomplete as far as I can tell

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:39):

Just some dumb examples

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

Discussing offline with utensil to try and find some we agree on :)

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:41):

Hmm, from page 10 onwards in that link there is a pretty precise definition.

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:41):

However, there is a tonne of structure there.

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:41):

There will be some nontrivial design decisions here

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:42):

My intuition is: add all the structure into the definition, and ask for lots of compatibilities.

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

What do you mean by "compatibilities"?

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:42):

Then build custom constructors that take less data, and generate the remaining structure (because there will be apparent redundancy in the definition)

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:43):

oh this is high-level structure making tips!

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:43):

Example: the inner product follows from other pieces of data, but you might want to explicitly include it in the definition, and then say that the inner product that you include is the same as the one built from the other pieces.

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:44):

The reason you want this redundancy is that it will give you flexibility in definitional equalities later on.

view this post on Zulip Utensil Song (Jun 29 2020 at 17:44):

https://stackedit.io/viewer#!url=https://raw.githubusercontent.com/pygae/lean-ga/master/docs/misc/many_faces.md is an incomplete work-in-progress math description of the definition problem here.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:45):

Like < can be deduced from <= in a partial order, but there's an axiom saying a < b ↔ a ≤ b ∧ ¬b ≤ a

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

@Johan Commelin, is there an example of that approach I can look at in mathlib?

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:46):

Yes, metric_space is a classical example

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:46):

It takes a topology, even though that's completely redundant. But...

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

docs#metric_space

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:46):

It takes a uniform structure now, I think

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:47):

The product topology on the product of two metric spaces is not definitionally the same as the metric topology on the product.

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:47):

It is a theorem that they are the same. And this theorem is now part of the definition

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:47):

But there is a constructor that will ignore the topology and just generate it from the metric.

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

What is that constructor?

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:48):

This is rather advanced structure-making.

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:48):

But for the product metric/topology, you don't want to use that constructor!

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:48):

Kevin Buzzard said:

This is rather advanced structure-making.

Yup, but the example at hand (geometric algebra) seems quite a complex thing.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:49):

But I suspect that non-defeq diamonds are right now the least of their worries. We still don't even know if it's a structure or a class.

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

Looks like https://leanprover-community.github.io/mathlib_docs/notes.html#forgetful%20inheritance is related to this conversation?

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:50):

But we can't even think about forgetful inheritence issues until we have decided what is an input and what is a structure field.

view this post on Zulip Utensil Song (Jun 29 2020 at 17:51):

IMG_1517.PNG

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:52):

@Eric Wieser https://github.com/leanprover-community/mathlib/blob/eb05a94/src/topology/metric_space/basic.lean#L71
I was wrong, it's not a seperate constructor, but a default argument.

view this post on Zulip Utensil Song (Jun 29 2020 at 17:52):

the current design is that it's a class

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:52):

So for R R^1 C which is G, G_0, G_1?

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

Order is specified as G_0 G_1 G

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:53):

so if R R^1 C and C C C are both Ok, you can't have a class and just make G an input

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

Correct, but we can have a class and make both G_0 and G an input

view this post on Zulip Utensil Song (Jun 29 2020 at 17:54):

The instended design is geometric_algebra R R^1 G(0, 1)

view this post on Zulip Utensil Song (Jun 29 2020 at 17:54):

not R R C

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:55):

What is G(0,1)?

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

The geometric algebra with 0 basis vectors with length 1 and 1 basis vector with length -1

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:55):

Unfortunately that definition is circular

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:55):

Is G determined by G_0 and G_1?

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

I think the answer is probably yes.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:56):

Is there a reason you're asking for it at all?

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:56):

I suggest also reading the story in §6.1 of https://arxiv.org/pdf/1910.12320.pdf

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

Wait, G can be any implementation of that though right?

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:57):

About how we approached valuations and especially the target type.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:57):

We made a lot of design decisions which turned out to be bad

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:57):

@Utensil Song This G(0,1) looks fishy.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 17:57):

but it was OK, because we learnt a lot

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:58):

It's may work very well for the abstract theory, but it looks bad for application to examples.

view this post on Zulip Utensil Song (Jun 29 2020 at 17:58):

The answer is no actually

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:59):

Kevin Buzzard said:

We made a lot of design decisions which turned out to be bad

Another example was that we gave a mathematically correct definition of "Huber pair" (whatever that may be), but the canonical example that every mathematician will give first (p-adic integers, p-adic numbers) could not be made into an instance with our definition.

view this post on Zulip Johan Commelin (Jun 29 2020 at 17:59):

We could prove lots of stuff though! But all abstract.

view this post on Zulip Utensil Song (Jun 29 2020 at 17:59):

it's also determined by the signature p q r and the specific way to implement a geometric algebra

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:00):

I will repeat, give me an example.

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

The signature pqr is embedded in the G_1 argument

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:00):

Is R,R,C\mathbb{R}, \mathbb{R}, \mathbb{C} an example?

view this post on Zulip Utensil Song (Jun 29 2020 at 18:00):

sorry I'm typing on my phone in bed...

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

I think all(?) examples are given by G = the Clifford algebra of a vector space V over a field k equipped with a quadratic form, G_0 = k, G_1 = V.

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

If that helps.

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

And obviously up to isomorphism.

view this post on Zulip Utensil Song (Jun 29 2020 at 18:01):

will type examples out tmr

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:01):

Reid Barton said:

And obviously up to isomorphism.

That's exactly my point.

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:01):

You want a definition that also applies to objects isomorphic to that.

view this post on Zulip Utensil Song (Jun 29 2020 at 18:03):

IMG_1518.PNG

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

some examples (G₀ G₁ G) that utensil may or may not agree with:

Euclidean space: ℝ ℝ³ some_implementation_of_g3_i_wish_to_register
spacetime: ℝ ℝ³,¹ some_implementation_of_sta_i_wish_to_register
an embedding of the builtin complex numbers: ℝ ℝ⁰,¹ ℂ
a different embedding of the builtin complex numbers: ℂ ℂ⁰ ℂ

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:05):

So your third type should not be some construction, but allow for arbitrary types.

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

G you mean - yes, just like the M argument to vector_space currently behaves

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:07):

And maybe G already has some inner product (from a different part of mathlib), so you don't want to construct the inner product, but take it as an argument. (Even though you might want to give a default argument that constructs it from other data.)

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

The (vector) inner product comes from G₁

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:08):

And maybe your G is already naturally graded into pieces G_0, G_1, ... G_r by another piece of mathlib, so you might want to take all the G_r as parameters as well

view this post on Zulip Utensil Song (Jun 29 2020 at 18:08):

@Eric Wieser your examples made it clear to me that we don't need G1 in the parameters

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:08):

Etc... (this is why I said there is so much data flying around in this definition.)

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

That's funny @Utensil Song, because it made clear to me that we do if we want the algebra to know about it's own metric

view this post on Zulip Utensil Song (Jun 29 2020 at 18:10):

it's actually in G already

view this post on Zulip Utensil Song (Jun 29 2020 at 18:10):

the quadratic form and other stuff...

view this post on Zulip Utensil Song (Jun 29 2020 at 18:12):

we are talking about two different designs

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:13):

@Utensil Song Again, I'll claim that's only true in maths, not in lean.

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:13):

Up to isomorphism, everything is fine.

view this post on Zulip Utensil Song (Jun 29 2020 at 18:17):

We won't have C R^n Gsth, right? @Eric Wieser

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:17):

@Utensil Song Is ℂ ℂ⁰ ℂ an example of a geometric algebra? How about ℝ ℝ⁰,¹ ℂ?

view this post on Zulip Utensil Song (Jun 29 2020 at 18:18):

not in the design I'm referring to

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:19):

Then I can't use your theorems in some interesting concrete examples :sad: :cry:

view this post on Zulip Utensil Song (Jun 29 2020 at 18:19):

C will be proven to be isomorphic to the G something later

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

Utensil Song said:

We won't have C R^n Gsth, right? Eric Wieser

No, because there is no instance of vector_space C R^n

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:19):

Utensil Song said:

C will be proven to be isomorphic to the G something later

Lean doesn't like such isomorphisms. They are a royal pita.

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:20):

If you create a more flexible definition, your proofs will probably also benefit.

view this post on Zulip Utensil Song (Jun 29 2020 at 18:20):

That's why G1 should not be special and it's redundant in the parameter and it's just a bundled field

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:23):

Please read §6.1 of the perfectoid paper (linked above). It's not that long.

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:24):

Note that this was not a problem that we hit during our project. We were done, and we tried to get some juicy examples. That's when we hit the problem.

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:24):

We could easily write 1000s of lines of interesting theorems... but they were useless, because we couldn't apply them to concrete examples.

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

So, the case I'm thinking of is one where I want extra constraints on the vector space for a proof, perhaps that the square of a vector is always positive. I suppose that can be written whether G1 is an argument or not though, as [ga G0 G1 G] (h : ∀ g : G1, p g) or [h : ga G0 G] (h : ∀ g : h.G1, p g)

view this post on Zulip Utensil Song (Jun 29 2020 at 18:25):

consider the complex numbers as either:

  • G(0, 1) over R
  • G(0, 0) over C

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:25):

@Utensil Song Lean disagrees. It only knows complex. That's it.

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

I'm working on reading it @Johan Commelin, my math background is pretty weak :)

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:25):

Lean is pretty stubborn. It will not change it's mind.

view this post on Zulip Utensil Song (Jun 29 2020 at 18:25):

we need both

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:25):

I agree that you need both.

view this post on Zulip Utensil Song (Jun 29 2020 at 18:26):

so it seems isomorphism is the way to go

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:26):

And since both are examples of foobar : Type*, you should include a foobar : Type* that abstracts over this.

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:26):

No, abstracting into types with axioms about that type. That's the way to go.

view this post on Zulip Utensil Song (Jun 29 2020 at 18:26):

(deleted)

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:27):

A Huber pair is a pair (R, A) where R is a subring of A. Except that in mathlib Z_p is not a subring of Q_p. There is an injective ring homomorphism.

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:28):

So we changed the definition of Huber pair to: a pair (R, A) with an injective ring homomorphism R →+* A.

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:28):

Mathematically an isomorphic definition, but it makes a big difference in lean.

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:28):

And guess what! Some proofs became easier!

view this post on Zulip Utensil Song (Jun 29 2020 at 18:28):

abstracting into types with axioms about that type. That's the way to go.

I see, this is it.

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

So to be clear, you replace the requirement "is a subring of" with a field providing that homomorphism?

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:30):

And my impression from what I've read so far about geometric algebras, is that there are lot's of things that can be abstracted into types and functions, and there will be many compatibility axioms.

view this post on Zulip Utensil Song (Jun 29 2020 at 18:30):

yes

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:30):

@Eric Wieser Yes, replace (A : Type*) (R : subring A) with (A : Type*) (R : Type*) (f : R →+* A) (hf : injective f).

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

And then presumably provide a constructor that populates f and hf for you if you can show R : subring A?

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:31):

We didn't provide such a constructor, but you could do that.

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

Did you find it would never have been useful?

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

It seems like you're obliged to provide that constructor to prove the statements are mathematically isomorphic ;)

view this post on Zulip Utensil Song (Jun 29 2020 at 18:33):

so now we all agree C cant directly stand at the position of G, but a structure abstracted over it, right?

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:34):

I'm confused...

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

At me or utensil, @Johan Commelin?

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:34):

Utensil

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:35):

I would think that when you create examples, you do want to be able to plug C into some field at some point.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 18:35):

Eric Wieser said:

So to be clear, you replace the requirement "is a subring of" with a field providing that homomorphism?

In type theory there is no such thing as a subring, really. There is some construction called a subring. But if A -> B is an injective ring homomorphism then that does not make A a subring of B, and indeed it would be impossible in general to make A a subring of B. A and B are just different types. The whole "sub" thing is dangerous.

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:35):

Eric Wieser said:

Did you find it would never have been useful?

We just directly plugged in R, subtype.val and subtype.val_injective. It's so short that it didn't merit a new constructor.

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

This has been lots of useful discussion for me, thanks everyone

view this post on Zulip Utensil Song (Jun 29 2020 at 18:42):

sorry since its 2:39am in my timezone, I'll get some sleep first. I'm pretty sure I can come up with a #mwe to demonstrate what's in my mind after the discussion above, with defs and juicy concrete examples.

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:42):

So clearly, if you start with Q : V → K, and you construct the Clifford algebra, then you want Q, V and K to be fields in the structure. Not isomorphic things.

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:43):

Utensil Song said:

sorry since its 2:39am in my timezone, I'll get some sleep first. I'm pretty sure I can come up with a #mwe to demonstrate what's in my mind after the discussion above, with defs and juicy concrete examples.

Sleep well! :sleeping:

view this post on Zulip Bryan Gin-ge Chen (Jun 29 2020 at 18:43):

Kevin Buzzard said:

In type theory there is no such thing as a subring, really. There is some construction called a subring. But if A -> B is an injective ring homomorphism then that does not make A a subring of B, and indeed it would be impossible in general to make A a subring of B. A and B are just different types. The whole "sub" thing is dangerous.

Speaking for myself, this has been one of the harder things to wrap my head around in formalization. (I spent a bunch of time trying to figure out how to define and work with submatroids and I'm still stuck...) I hope that MiL has a lot of discussion about this.

view this post on Zulip Johan Commelin (Jun 29 2020 at 18:43):

Johan Commelin said:

So clearly, if you start with Q : V → K, and you construct the Clifford algebra, then you want Q, V and K to be fields in the structure. Not isomorphic things.

Because in the end, you want to deduce facts about Q, V and K.

view this post on Zulip Utensil Song (Jun 29 2020 at 18:43):

thanks!

view this post on Zulip Utensil Song (Jun 30 2020 at 10:37):

I realized that I should first #xy the problem before writing a new #mwe . The following will refer to the definitions in The Many Faces of Geometric Algebra by section titles with <> around them. I'll try to avoid mentioning any specific language structure in Lean such as structure/type class/instance, inheritance, parameters, bundled v.s. unbundled etc. because they're part of the y.

The grand design is somewhat top-down.

  1. Define general Geometric Algebra (GA) with axioms about its properties/behaviors instead of representations, avoid mentioning grades/coordinates/metric, etc., keep it as readable and intuitive as possible;
  2. Define G(p, q, r) over a field which could be ℝ, ℂ or dual numbers 𝔻, hyperbolic numbers ℍ ( note that this is not quaternions ) but without specific metric, where (p, q, r) means p positive, q negative and r zero dimensions, e.g. Minkowski space is ℝ(1, 3, 0), dual number is G(0, 0, 1); Projective GA(PGA) and Conformal GA(CGA) are of specific interest at this abstraction layer with their own theorems and identities unrelated to specific metrics
  3. Define G(p, q, r) over a field a specific metric(or quadratic form)
  4. All of
    a. Formalize data structures and the corresponding algorithms in sense of software libraries, such as using binary trees or prefix trees or whatever to implement GA
    b. formalize GA in other ways so that it's equivalent to the definition in 1 (with certain limited scope), the formalization might be <Lawson 1989>, <Clifford algebra as a quotient of the tensor algebra> or <Clifford 1882>
    c. ℝ, ℂ, dual numbers 𝔻, hyperbolic numbers ℍ, quaternions ℚ are all GAs

  5. Prove general theorems and identities for 1, prove 2 "is" 1, prove dedicated theorems and identities for PGA and CGA, prove 3 "is" 2, prove 4b is 2 or 1, prove 4a and 4c are 3.

Last night, Eric was talking about at most the relationship between 3 and 4, and I was thinking about how to handle all the relationships between all of the above(and they might not be the same!). Maybe I've overcomplicated the problem at an initial stage. That's why I kept saying "not exactly" to Eric's examples.

Now let's come back to the current attempt in https://github.com/pygae/lean-ga/blob/master/src/geometric_algebra/nursery/chisolm.lean . It's trying to directly address 1 and it has at least the following mistakes:

  1. it should not directly try to address 1, instead, it should try something more concrete at the level of 2 or 3 and attack 1 based on what's learned during the process;
  2. it should not choose the axiom sets in <Chisolm 2012>, the axioms treated G₀ and G₁ specially and I believe this is its weakness; on the opposite, something like <Buchholz 2005>, <Definition by generators and relations>, <Lynn> might be better alternatives;
  3. it should not choose using [] parameters to specify most of the axioms, the axioms should be bundled fields
  4. it could reduce the numbers of types in parameters, the possibilities are 2(only G₀ and G), 1(only G) or 0;
  5. it should not stick to type class to implement the "is"s in 5, and might need to use the technique documented in https://leanprover-community.github.io/mathlib_docs/notes.html#forgetful%20inheritance for better definitionally equality; there might be other alternatives;
  6. it should handle the equality across types (i.e. Gr) better, such as the way to deal with the fact that the square of G₁ is G₀, homs are used here, but there're alternatives like coe, set, subtype etc.
  7. it should pick a way to prove that ℂ could "be" G(0, 1, 0) over ℝ or G(0, 0, 0) over ℂ, and find a way to allow plugging ℂ into proven theorems about abstract GA.

view this post on Zulip Utensil Song (Jun 30 2020 at 11:09):

Some concrete examples of GA (but not of the geometric_algebra G₀ G₁ G here) are(note: it's not Lean):

    # Basic
     = G(0)          # Real numbers.
      = G(0,1)      # Complex numbers.
      = G(0,2)      # Quaternions.
     = G(1)           # Hyperbolic numbers.
    𝔻  = G(0,0,1)   # Dual numbers.


    # Clifford
    Cl2       = G(2)     # Clifford algebra for 2D vector space.
    Cl3       = G(3)     # Clifford algebra for 3D vector space.
    Spacetime = G(1,3)   # Clifford algebra for timespace vectors.

    # Geometric
    PGA2D = G(2,0,1)     # Projective Euclidean 2D plane. (dual)
    PGA3D = G(3,0,1)     # Projective Euclidean 3D space. (dual)
    CGA2D = G(3,1)       # Conformal 2D space.
    CGA3D = G(4,1)       # Conformal 3D space.

view this post on Zulip Reid Barton (Jun 30 2020 at 12:55):

One curious thing about this notion of geometric algebra (at least in the Chisolm version) which is clarified by some of the other presentations is that it is not really an algebraic structure at all, in the sense of describing a kind of algebra. Rather, it's attempting to axiomatize the free algebra of some sort: namely (noncommutative) kk-algebras equipped with a kk-linear map from VV compatible with the quadratic form on VV in a certain way.

view this post on Zulip Reid Barton (Jun 30 2020 at 12:57):

So maybe it would be worthwhile to start by formalizing that kind of algebra.

view this post on Zulip Reid Barton (Jun 30 2020 at 12:57):

I think equations which hold in all geometric algebras would also hold in all of these guys.

view this post on Zulip Utensil Song (Jun 30 2020 at 14:23):

Mathematically, it's correct. GA is simply a free algebra with one particular constraint on the quadratic form. But such a statement is of no interest to the community applied GA in mathematical physics, quantum physics, electromagnetism, astrophysics, computer graphics, machine vision, engineering, robotics etc. All rich structures and interesting behaviors arise from that one constraint, and in turn, embeds many concepts in different math areas with different appearances.

view this post on Zulip Utensil Song (Jun 30 2020 at 14:48):

it is not really an algebraic structure at all, in the sense of describing a kind of algebra.

I don't follow what qualifies as an algebra here.

Repeatedly and independently a long list of Clifford's geometric algebras, their subalgebras have been studied and applied historically, often under different names. Some of these algebras are complex numbers (and the complex number plane), hyperbolic numbers (split complex numbers, real tessarines), dual numbers, quaternions, biquaternions (complex quaternions), dual quaternions, Plucker coordinates, bicomplex numbers (commutative quaternions, tessarines, Segre quaternions), Pauli algebra (space algebra), Dirac algebra (space-time algebra, Minkowski algebra), algebra of physical space, para-vector algebra, spinor algebra, Lie algebras, Cartan algebra, versor algebra, rotor algebra, motor algebra, Clifford bracket algebra, conformal algebra, algebra of differential forms, etc.

view this post on Zulip Utensil Song (Jul 01 2020 at 04:03):

Johan Commelin said:

I suggest also reading the story in §6.1 of https://arxiv.org/pdf/1910.12320.pdf

I'm trying to sort out what's going on in that section. The storyline seems to be:

The definition

Γ0:=Γ0\Gamma_0 := \Gamma \cup {0} where the multiplication and order relation are extended by specifying that 0γ = 0 × 0 = 0 and 0 ≤ γ for every γ in Γ.
focuses on the construction of Γ0\Gamma_0, starting from an ordered group and adding an element, rather than the properties of the resulting object.

The latter (directly addressing the properties of the resulting object instead of piecing some construction together and suddenly new behaviors emerge out of no(intuitively)where) is exactly what I'm after. If I have to extend some structure or bundle some field, I'll rather be adding some behaviors rather than gluing some constructions.

We used Lean’s coercion mechanism to automatically insert the “inclusion” map from Γ to Γ0\Gamma_0. In set
theory, this is indeed a true inclusion, but there are no inclusions between types in type theory as a term
can only have one type. The norm_cast tactic, by Paul-Nicolas Madeleine [Mad19], greatly alleviates
the pain of invoking lemmas about such coercions
Set-theoretically, it is almost true that R0=(R>0)0\mathbb{R}_{\ge 0} = (\mathbb{R}_{\gt 0})_0. This tiny lie only requires that we forget that the 0 in (R>0)0 (\mathbb{R}_{\gt 0})_0 is meant to be an extra element coming from nowhere in particular, hence has nothing to do with the neutral element of the additive group R. It gets harder to ignore with type-theoretic foundations. It means that merging the elementary theory with our abstract theory would require non-trivial glue.

Generally I love type-theoretic foundations because it seems more strict and you can't blur things out unintentionally. But it's really problematic when you intentionally need to do something across types, it forces you to be verbosely formal and I'm yet to find the best practice to handle such situations. This story give hints about how to handle it, accompanied by old code presumably here.

We defined the concept of totally ordered commutative monoid with zero as a type equipped with a composition law, a total order, and special elements 0 and 1 with enough properties to guarantee that all instances are isomorphic (as ordered commutative monoids) to some Γ0\Gamma_0. This corresponds to a type class which admits both with_zero Γ and {x : R // 0 ≤ x} as instances. Once again, focusing on properties instead of constructions gives us the needed extra flexibility at no cost.

So here's the solution. Basically I understood the last sentence and worked my way backwards with the help of the corresponding code here, particularly src/valuation/basic.lean(see also linear_ordered_comm_group_with_zero at master branch). The core idea here seems to be we should model the properties in the definitions and prove some construction is an instance of it later and the benefit would be (I guess) better integration with elementary theory which involves more informal treatment?

view this post on Zulip Johan Commelin (Jul 01 2020 at 05:58):

The core idea here seems to be we should model the properties in the definitions and prove some construction is an instance of it later

Yes, exactly.

and the benefit would be (I guess) better integration with elementary theory which involves more informal treatment?

The benefit would be that examples that are not by definition equal to you construction can still be turned into instances, whereas with the approach we took first this is simply impossible.

  • nnreal is not of the form with_zero G. It's only isomorphic to it.
  • Z_p is not a set Q_p and hence is_subring Z_p will never work. But it does have an injective ring homomorphism to Q_p.

view this post on Zulip Kevin Buzzard (Jul 01 2020 at 06:35):

As a mathematician you might say "but what is the problem here? If X and Y are isomorphic then everything which is true for X is true for Y". This is problematic for two reasons. Firstly, the principle is not true in general. For example if P(T) is T=X (which makes sense in type theory) then P(X) is true and P(Y) might not be (in Lean at least -- in a univalent theory this would be true but their = is not proof-irrelevant and this seems to bring other problems).

And secondly, because all the mathematical facts about X, which of course do translate over to Y, actually have to be translated over. There is no "rewrite along an isomorphism" like there is a rewrite along an equality, and until such a tactic exists (and it will be hard to write because it's not always true, it's not true for P above for example) everything has to be transferred manually. Completely dumb proofs like if V and W are isomorphic algebras and V is 10 dimensional over some subalgebra isomorphic to the reals then so is W -- this is mathematically obvious but will not be a one-liner in Lean by any means

view this post on Zulip Utensil Song (Jul 01 2020 at 13:40):

I was trying to have a few examples under the current definition, and have difficulty proving instance rrc_ga : geometric_algebra ℝ ℝ ℂ at the sorry /- here -/ in the following #mwe:

import algebra.group.hom
import ring_theory.algebra
import data.real.basic
import data.complex.basic
import data.complex.module
import tactic

universes u u₀ u₁

class geometric_algebra
-- Axiom 2: G contains a field G0 of characteristic zero which includes 0 and 1.
(G₀ : Type*) [field G₀]
-- Axiom 3: G contains a subset G1 closed under addition,
-- and λ ∈ G0, v ∈ G1 implies λv = vλ ∈ G1.
(G₁ : Type*) [add_comm_group G₁] [vector_space G₀ G₁]
-- Axiom 1: G is a ring with unit.
-- The additive identity is called 0 and the multiplicative identity is called 1.
(G : Type*) [ring G]
[algebra G₀ G]
:=
(f₁ : G₁ →+ G)
-- Axiom 4: The square of every vector is a scalar.
(vec_sq_scalar :  v : G₁,  k : G₀, f₁ v * f₁ v = algebra_map _ _ k )

namespace geometric_algebra

section

parameters
{G₀ : Type*} [field G₀]
{G₁ : Type*} [add_comm_group G₁] [vector_space G₀ G₁]
{G : Type*} [ring G] [algebra G₀ G] [geometric_algebra G₀ G₁ G]

def f : G₁ →+ G := f₁ G₀

def fₛ : G₀ →+* G := algebra_map G₀ G

noncomputable instance rrc_ga : geometric_algebra    := {
  f₁ := {
    to_fun := λx, x,
    map_zero' := rfl,
    map_add' := begin
      intros x y,
      norm_cast,
    end
  },
  vec_sq_scalar := begin
    intro v,
    use v * v,
    simp only [add_monoid_hom.coe_mk, ring_hom.map_mul],
    sorry /- here -/
  end
}

/- For later discussion, the below doesn't matter for this question -/

instance field_ga (K : Type*) [field K] : geometric_algebra K K K := {
  f₁ := {
    to_fun := id,
    map_zero' := rfl,
    map_add' := begin
      simp only [forall_const, id.def, eq_self_iff_true]
    end
  },
  vec_sq_scalar := begin
    intro v,
    use v * v,
    simp only [algebra.id.map_eq_self, add_monoid_hom.coe_mk, id.def],
  end
}

-- noncomputable instance rcc_ga : geometric_algebra ℝ ℂ ℂ := {
--   f₁ := {
--     to_fun := id,
--     map_zero' := rfl,
--     map_add' := by simp,
--   },
--   vec_sq_scalar := /- mathematically false due to the wrong mul equiped with ℂ -/
-- }

end

end geometric_algebra

view this post on Zulip Utensil Song (Jul 01 2020 at 13:40):

The goal state is

v : 
 v * v = (algebra_map  ) v * (algebra_map  ) v

view this post on Zulip Eric Wieser (Jul 01 2020 at 13:46):

The solution to your sorry is refl

view this post on Zulip Utensil Song (Jul 01 2020 at 13:46):

unfold algebra_map only gives

v : 
 v * v = algebra.to_ring_hom v * algebra.to_ring_hom v

and I can't do any rw or apply with algebra.to_ring_hom.xxx

view this post on Zulip Utensil Song (Jul 01 2020 at 13:47):

I tried everything except refl!

view this post on Zulip Reid Barton (Jul 01 2020 at 13:48):

Utensil Song said:

it is not really an algebraic structure at all, in the sense of describing a kind of algebra.

I don't follow what qualifies as an algebra here.

I mean in the sense of universal algebra. For example groups are the models of an algebraic theory in the sense that they are sets equipped with certain functions/constants which satisfy universally quantified equations (like "for all xx, yy, zz, we have (xy)z=x(yz)(x * y) * z = x * (y * z)"). Free groups however are not the models of an algebraic theory.

view this post on Zulip Utensil Song (Jul 01 2020 at 13:48):

It's really weird that simp can't cover this and refl can.

view this post on Zulip Utensil Song (Jul 01 2020 at 14:02):

@Reid Barton After reading the group example in https://en.wikipedia.org/wiki/Universal_algebra , I'm pretty sure GA can be rephrased so that it's also a universal algebra.

view this post on Zulip Utensil Song (Jul 01 2020 at 14:05):

There are many existing substitutions of "Axiom 4: The square of every vector is a scalar" in literature, I always wondered which's the best one.

view this post on Zulip Utensil Song (Jul 01 2020 at 14:10):

For example, would the following qualify for universal algebra?

Let (X,Q)(\mathrm{X}, \mathrm{Q}) be an arbitrary finite dimensional real quadratic space and let A\mathcal{A} be a real associative algebra with identity. Furthermore, let
α:RA\alpha: \mathbb{R} \rightarrow \mathcal{A} and v:XAv: \mathrm{X} \rightarrow \mathcal{A} be linear injections such that
(i) A\mathcal{A} is generated as an algebra by its distinct subspaces {v(v)vX}\{v(v) \mid v \in X\} and {α(a)aR}\{\alpha(a) \mid a \in \mathbb{R}\}
(ii) vX:(v(v))2=α(Q(v))\forall v \in X:(v(v))^{2}=\alpha(Q(v))

Then A\mathcal{A} is said to be a Clifford algebra for (X,Q)(\mathrm{X}, \mathrm{Q}). The elements of a Clifford algebra are
called multivectors. The product of a Clifford algebra is named geometric product. The signature of the quadratic space is also the signature of the algebra.

view this post on Zulip Utensil Song (Jul 01 2020 at 14:16):

I guess not yet. It's still not only about n-ary operations and identities.

view this post on Zulip Reid Barton (Jul 01 2020 at 14:24):

If you remove part (i), then I think so

view this post on Zulip Utensil Song (Jul 01 2020 at 14:55):

I think (i) is not necessary but a natural result of the rest of the definition. Will have to verify that.

view this post on Zulip Jalex Stark (Jul 01 2020 at 16:57):

Utensil Song said:

It's really weird that simp can't cover this and refl can.

A proof of equality by simp is "once we simplify both sides, using simp lemmas we created on purpose, they become syntactically equal".

A proof of equality by refl is "these are definitionally equal, you can check by unfolding the definitions"

view this post on Zulip Jalex Stark (Jul 01 2020 at 17:00):

If simp can't solve something that you expect it to solve, there's implicitly a lemma that you think should be tagged with @[simp] but isn't.

view this post on Zulip Eric Wieser (Jul 01 2020 at 17:13):

@Jalex Stark: So to be clear, if simp fails but refl succeeds, refl is unfolding definitions that simp is not?

view this post on Zulip Kevin Buzzard (Jul 01 2020 at 17:19):

refl will unfold everything. simp won't.

view this post on Zulip Kevin Buzzard (Jul 01 2020 at 17:19):

def foo := 

example : foo =  :=
begin
  simp, -- fails
end

view this post on Zulip Kevin Buzzard (Jul 01 2020 at 17:20):

def foo := 

example : foo =  :=
begin
  simp [foo], -- works
end

Of course refl works.

view this post on Zulip Kevin Buzzard (Jul 01 2020 at 17:21):

simp [foo] looks a bit weird because simp likes to use lemmas of the form A=B or A <-> B -- it is a confluent rewriting system.

view this post on Zulip Jalex Stark (Jul 01 2020 at 17:21):

Yes

view this post on Zulip Kevin Buzzard (Jul 01 2020 at 17:21):

But

def foo := 

#print prefix foo
/-
foo : Type
foo.equations._eqn_1 : foo = ℕ
-/

and what's happening is that simp temporarily is adding foo.equations._eqn_1 to the simp set

view this post on Zulip Kevin Buzzard (Jul 01 2020 at 17:22):

This is how unfold works. unfold X is basically "simp only [X.equations*]" I think.

view this post on Zulip Scott Morrison (Jul 01 2020 at 23:05):

This difference between simp and refl is quite instructive. At first everyone thinks of refl as a "really simply" tactic, that "just checks if things are equal". However it's actually potentially doing a huge amount of work, because it is willing to unfold definitions arbitrarily deeply. This is what people are referring to when they say "a heavy refl".

view this post on Zulip Scott Morrison (Jul 01 2020 at 23:06):

On the other hand simp looks complicated because it potentially makes use of a whole zoo of lemmas, but on the other hand it works at a syntactic level (it will unfold reducible, and this can be tweaked) so is in some sense much more controllable.

view this post on Zulip Scott Morrison (Jul 01 2020 at 23:07):

I would say that is refl is succeeding and simp is failing, it's probably an indication you should try to add some simp lemmas.

view this post on Zulip Utensil Song (Jul 02 2020 at 02:36):

Thanks for the very informative answers!

By "weird", actually there's a whole bunch of questions:

Q1. As @Jalex Stark @Scott Morrison pointed out the potential possibility, is there some simp lemma missing for algebra, ring_hom? Should we and how can we do something about it?

Q2. Are all the understandings below correct or some of them are misleading? Particularly c, d, f, i, j, l. And the questions n through r.

a. Initially I enjoy the atomic apply and rw for -> and =, respectively.
b. simp was merely a tool helping me find out the stuff in simp only [stuff].
c. Using simp only [stuff] instead of rw [stuff] was merely saving me the trouble from handling the order and the repetition of the rewrites.
d. Then I noticed that sometimes seemingly complex goal can be simplified significantly by simp only [] which indicates there must be something other than just rewrites using simp lemmas in simp which I have no idea what's going on.
e. I try to avoid using simp in the middle of a proof and consider it a finishing tactic.
f. but I find myself repeatedly having to using simp only [] or simp only [stuff] to clean up some noise in the goal and proceed. I don't know if it's something wrong with my use of coe/homs/alias etc.
g. then I noticed the differences of syneq, defeq, propeq (and in this order the eq is from close to more far away)
h. and start using unfold for defeq instead of rw since the latter can only apply the defeq rewrite for one pattern repeatedly but unfold can do this for all patterns repeatedly. by pattern I mean, if I have a def of f, than rw works on both f(a) in f(a) + f(b) + f(a) but not f(b) but unfold works on f(*).
i. then I noticed dsimp, which seems to be more powerful than unfold which should help me figure out the stuff in unfold [stuff]
j. and it's more conservative than simp since it only uses defeq
k. but I haven't been able to use dsimp to solve any goal yet
l. and I'm reluctant to use dsimp because I don't know how to squeeze it or trace it
m. with the discussions above, it seems refl is much heavier than just check defeq at a shallow level and applying refl lemmas, and it's "willing" to check defeq at arbitrary depth
n. then why there's the need of manual unfold and dsimp? is the difference only that refl is a finishing tactic and it fails if it can't close the goal?
o. why I can't close the goal with dsimp?
p. do I have some non-finishing tactic to do what's similar to refl did but in the middle of a proof?
q. the most important question is, what defeq did refl check in this example?
r. can I mimic it with other tactics which explicitly mention the defeq it used?

view this post on Zulip Scott Morrison (Jul 02 2020 at 02:43):

Oof, too many questions to be able to answer...

view this post on Zulip Scott Morrison (Jul 02 2020 at 02:44):

o. why I can't close the goal with dsimp?

because it doesn't have anything in it that could close a goal; it always replaces one goal with another. Anytime you think you might "close a goal with dsimp", you want to use refl.

view this post on Zulip Scott Morrison (Jul 02 2020 at 02:45):

re: m. and n. Yes! I never use unfold, only dsimp.

view this post on Zulip Scott Morrison (Jul 02 2020 at 02:46):

d. simp only [] will do beta reduction, and I think also unfold projections(?)

view this post on Zulip Scott Morrison (Jul 02 2020 at 02:47):

dsimp is allowed mid-proof (although often can be removed once the proof is working, unless the following tactic is relying on the syntactic form that dsimp produced)

view this post on Zulip Scott Morrison (Jul 02 2020 at 02:48):

(i.e. in anything of the form dsimp, exact ..., the dsimp is unnecessary. Often however a dsimp may be needed before simp or rw)

view this post on Zulip Scott Morrison (Jul 02 2020 at 02:49):

re "n" again: the need for dsimp is that it unfolds definitions, and many other tactics won't, so you need to do it by hand before calling them

view this post on Zulip Scott Morrison (Jul 02 2020 at 02:50):

Regarding Q1: anytime you think simp should help, but it doesn't, you should try to write the simp lemma that you think should have fired!

view this post on Zulip Scott Morrison (Jul 02 2020 at 02:50):

This is a very important part of developing a new theory --- setting up the (hopefully confluent) rewriting rules that are always "safe" to use.

view this post on Zulip Scott Morrison (Jul 02 2020 at 02:50):

You want as much as possible to be handled by simp, because it makes everything easier for anyone who comes afterwards to your theory.

view this post on Zulip Utensil Song (Jul 02 2020 at 04:15):

Scott Morrison said:

o. why I can't close the goal with dsimp?

because it doesn't have anything in it that could close a goal; it always replaces one goal with another. Anytime you think you might "close a goal with dsimp", you want to use refl.

Ah, I phrased it wrong. The actual question is, now that refl can close the goal, and it's about defeq, why can't dsimp which focuses on defeq achieve the same thing? What can I do to help it to achieve this, like supply defs in dsimp [defs]?

view this post on Zulip Utensil Song (Jul 02 2020 at 04:18):

Scott Morrison said:

Regarding Q1: anytime you think simp should help, but it doesn't, you should try to write the simp lemma that you think should have fired!

Yes, but the defs involved here are in algebra part of mathlib, I was wondering if anyone is aware of the situation that some simp lemma is missing.

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:25):

dsimp will only use lemmas marked with @[simp]. So yes, you need to explicitly make these lemmas.

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:26):

And yes, @[simp] lemmas are missing all across mathlib! As you identify them, please make PRs adding @[simp] to them. :-)

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:27):

It's nontrivial to decide exactly which lemmas should be simp lemmas, and so it doesn't always get done thoroughly.

view this post on Zulip Utensil Song (Jul 02 2020 at 04:27):

Scott Morrison said:

You want as much as possible to be handled by simp, because it makes everything easier for anyone who comes afterwards to your theory.

I totally agree to do so for the end-users and intend to do so in a later stage. And yet inside the library, I'm a little bit afraid of the lemmas proven by simp, which means I don't have any clue about the dependencies here, it feels circular to me somehow although I know this is unlikely the actual case.

So, what's the best practice here? I might be a little pedantic or overcautious here and was thinking about:

  1. only use simp only [xxx] with the help of squeeze_simp;
  2. simp involving only the simp lemmas in mathlib is allowed;
  3. use no simp inside the theory if it involves simp lemmas in the theory; -- to avoid the circular feeling
  4. to relax 2 a little bit, if I can break the theory into a few layers, then the top layers can invoke the layers under it; -- but I don't know how to prevent simp using simp lemmas from the same layer, except check manually or by a linter examining the [xxx] in simp only [xxx].

view this post on Zulip Jalex Stark (Jul 02 2020 at 04:34):

i don't understand what circularity you are trying to avoid

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:37):

I'm not sure either.

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:39):

How could there be any circularity? simp will only use lemmas proved higher up the page

view this post on Zulip Utensil Song (Jul 02 2020 at 05:25):

The circularity does not exist in Lean. It exists in one's mind because one has read the simp lemmas higher up the page and everywhere else...

view this post on Zulip Johan Commelin (Jul 02 2020 at 06:05):

@Utensil Song

p. do I have some non-finishing tactic to do what's similar to refl did but in the middle of a proof?

How about tactic#change ? Is that what you're looking for?

view this post on Zulip Utensil Song (Jul 02 2020 at 06:08):

I tried change but I fail to provide the new goal to change, copying from the goal and modifying it won't always work, what's printed in goal view is not always legal lean.

view this post on Zulip Utensil Song (Jul 02 2020 at 06:09):

e.g. copying the goal state in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/synthesized.20not.20defeq.20inferred/near/202569857

view this post on Zulip Johan Commelin (Jul 02 2020 at 06:10):

Utensil Song said:

I tried change but I fail to provide the new goal to change, copying from the goal and modifying it won't always work, what's printed in goal view is not always legal lean.

Yup, this is a known issue, and it's hard to solve. Lean 4 will have a delaborator, and then life should be much better.

view this post on Zulip Johan Commelin (Jul 02 2020 at 06:10):

However, usually you can fix this by adding some type annotations and removing some up-arrows.

view this post on Zulip Utensil Song (Jul 02 2020 at 06:10):

or {re := v, im := 0} * {re := v, im := 0} = ⇑(algebra_map ℝ ℂ) (v * v)

view this post on Zulip Johan Commelin (Jul 02 2020 at 06:10):

What's printed in the goal is not always legal lean, but it is almost always almost legal lean.

view this post on Zulip Bryan Gin-ge Chen (Jul 02 2020 at 06:12):

You can try using set_option pp.implicit true or other pp options, sometimes that helps to get something you can use.

view this post on Zulip Scott Morrison (Jul 02 2020 at 06:20):

I find deleting the up arrows fixes 95% of pretty-printed output problems.

view this post on Zulip Utensil Song (Jul 02 2020 at 06:38):

That's basically set_option pp.coercions false?

view this post on Zulip Utensil Song (Jul 02 2020 at 06:38):

What's the quickest way to convert the structure stuff in goal view into legal Lean? like in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/synthesized.20not.20defeq.20inferred/near/202653388

view this post on Zulip Utensil Song (Jul 16 2020 at 04:46):

We got stuck on how to implement the bundled version for a while and here's how far we have got ( #mwe for unbundled, bundling V, and bundling both R&V, demonstrated in 3 different namespaces). The most natural one seems to be bundling only V.

It there any way to make the references to the maps less verbose?

import ring_theory.algebra

universes u₀ u₁ u₂

namespace unbundled

class mwc
(R : Type u₀) [field R]
(V : Type u₁) [add_comm_group V] [vector_space R V]
(G : Type u₂) [ring G]
extends algebra R G
:=
(f : R →+* G := algebra_map R G)
(f : V →+ G)

section lemmas

variables (R : Type u₀) [field R]
variables (V : Type u₁) [add_comm_group V] [vector_space R V]
variables (G : Type u₂) [ring G]

variables (r₀ : R)
variables (v₀ : V)

example [mwc R V G] :  v : V,  r : R,
  ((mwc.f R v) * (mwc.f R v)) = (mwc.f V r : G)
:= sorry

end lemmas

end unbundled

namespace V_bundled

class mwc
(R : Type u₀) [field R]
(G : Type u₂) [ring G]
extends algebra R G
:=
(V : Type u₁)
[V_acg : add_comm_group V]
[V_vs : vector_space R V]
(f : R →+* G := algebra_map R G)
(f : V →+ G)

section lemmas

variables (R : Type u₀) [field R]
variables (G : Type u₂) [ring G] [mwc R G]

variables (r₀ : R)
variables (v₀ : mwc.V R G)

example :  v : mwc.V R G,  r : R,
  (mwc.f v) * (mwc.f v) = mwc.f r
:= sorry

end lemmas

end V_bundled

namespace VR_bundled

class mwc
(G : Type u₂) [ring G]
:=
(R : Type u₀)
[R_f : field R]
(V : Type u₁)
[V_acg : add_comm_group V]
[V_vs : vector_space R V]
(to_algebra : algebra R G)
(f : R →+* G := algebra_map R G)
(f : V →+ G)

section lemmas

variables (G : Type u₂) [ring G] [mwc G]

variables (r₀ : mwc.R G)
variables (v₀ : mwc.V G)

example :  v : mwc.V G,  r : mwc.R G,
  (mwc.f v) * (mwc.f v) = mwc.f r
:= sorry

end lemmas

end VR_bundled

view this post on Zulip Scott Morrison (Jul 16 2020 at 05:25):

Just a random comment --- using abbreviations like mwc is unhelpful. Presumably this is intended to be some standard mathematical object, and perhaps if you'd written out mwc I'd have heard of it, and not have to reverse engineer by _actually reading the code_. :-)

view this post on Zulip Scott Morrison (Jul 16 2020 at 05:26):

Also -- given there's been a two week pause on this thread, and this doesn't seem to be about the original title anymore, perhaps moving this to a new thread would be easier.

view this post on Zulip Scott Morrison (Jul 16 2020 at 05:26):

(and get more attention)

view this post on Zulip Utensil Song (Jul 16 2020 at 06:06):

Thanks, I'll start a new topic. As for the naming, because other mathematical properties are stripped away and only the technical issue (figuring out how bundling v.s. unbundling type classes works in Lean and how to refer to fields in them) is left, I don't have any meaningful name for it anymore...I'll add a description though.

view this post on Zulip Utensil Song (Jul 16 2020 at 07:04):

Moved to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/unbundled.20v.2Es.2E.20%28semi-%29bundled/near/204049917


Last updated: May 08 2021 at 10:12 UTC