synthesized not defeq inferred

Stream: new members

[Utensil Song]

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

[Jeremy Avigad]

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)

[Utensil Song]

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

[Utensil Song]

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

[Utensil Song]

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

[Utensil Song]

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

[Jeremy Avigad]

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

[Utensil Song]

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

[Jeremy Avigad]

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.

[Utensil Song]

but G is not a field...

[Jeremy Avigad]

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

[Utensil Song]

I see, that seems ok

[Utensil Song]

I'll try that, thanks!

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Utensil Song]

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

[Utensil Song]

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

[Utensil Song]

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

[Utensil Song]

the hom approach is more accurate

[Utensil Song]

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

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

[Utensil Song]

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

[Utensil Song]

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 [].

[Utensil Song]

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.

[Kevin Buzzard]

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

[Utensil Song]

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

[Utensil Song]

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

[Utensil Song]

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?

[Johan Commelin]

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

[Johan Commelin]

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?

[Utensil Song]

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.

[Utensil Song]

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.

[Patrick Massot]

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.

[Kevin Buzzard]

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

[Utensil Song]

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

[Utensil Song]

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.

[Kevin Buzzard]

Lean is just letting you write what you mean.

[Utensil Song]

Indeed.

[Kevin Buzzard]

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

[Utensil Song]

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

[Utensil Song]

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

[Utensil Song]

How can I get more trace log to debug this?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Utensil Song]

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

[Mario Carneiro]

you don't need to extend them

[Utensil Song]

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

[Mario Carneiro]

just have a field

[Utensil Song]

G1 is not a field by itself

[Mario Carneiro]

no, the function

[Mario Carneiro]

the two functions should be fields of the structure

[Mario Carneiro]

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

[Mario Carneiro]

you should not ask for has_coe instances either

[Utensil Song]

the intention was to comment out the has_coe, algebra lines

[Utensil Song]

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

I'll try that

[Mario Carneiro]

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)

[Utensil Song]

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

[Mario Carneiro]

you have a lot of duplicate data in the parameters

[Utensil Song]

Oh, algebra_map _ _ k is the scalar_hom equivalent

[Mario Carneiro]

those has_zero and has_one instances are also duplicate

[Utensil Song]

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.

[Mario Carneiro]

no, you will just get stuck in proofs

[Mario Carneiro]

I don't think lean knows what a warning is

[Mario Carneiro]

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

[Utensil Song]

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

[Mario Carneiro]

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

[Mario Carneiro]

because nothing says that 1 is a unit

[Utensil Song]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

maybe they come for free given the homs

[Utensil Song]

Mario Carneiro: maybe they come for free given the homs

I believe so

[Utensil Song]

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

[Kevin Buzzard]

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₁

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Utensil Song]

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

[Utensil Song]

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

[Utensil Song]

Is there a way to force so, just locally?

[Utensil Song]

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

[Alex J. Best]

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.

[Utensil Song]

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

[Utensil Song]

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.

[Alex J. Best]

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

[Utensil Song]

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!

[Utensil Song]

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 )

[Kevin Buzzard]

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,

[Eric Wieser]

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?

[Alex J. Best]

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.

[Reid Barton]

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

[Eric Wieser]

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

[Alex J. Best]

Can you give an example of what you mean?

[Eric Wieser]

I'm trying to

[Eric Wieser]

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

[Eric Wieser]

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

[Utensil Song]

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

[Utensil Song]

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

[Utensil Song]

As demonstrated in the #mwe above

[Johan Commelin]

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

[Johan Commelin]

But I'm not a mathlib dictator!

[Johan Commelin]

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

[Utensil Song]

then how to use variables to achieve similar purpose?

[Eric Wieser]

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

[Utensil Song]

I wish to avoid relying on something not recommended by mathlib

[Bryan Gin-ge Chen]

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.

[Eric Wieser]

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

[Utensil Song]

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

[Utensil Song]

since they're not in the original math

[Utensil Song]

the arithmetic just works across "types"

[Eric Wieser]

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

[Utensil Song]

yeah

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Eric Wieser]

What do you mean by bundling in this case?

[Bryan Gin-ge Chen]

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

[Eric Wieser]

That was what I was about to ask

[Eric Wieser]

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

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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

[Eric Wieser]

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

[Eric Wieser]

geometric_algebra.mk_from_instances or something?

[Johan Commelin]

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.

[Bryan Gin-ge Chen]

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)

[Johan Commelin]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Eric Wieser]

Johan Commelin said:

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

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

[Kevin Buzzard]

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.

[Eric Wieser]

I think "exactly one" is a perfectly reasonable answer

[Eric Wieser]

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

[Eric Wieser]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Eric Wieser]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Eric Wieser]

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

[Kevin Buzzard]

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.

[Eric Wieser]

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

[Eric Wieser]

So at least G₀ needs to be an argument too

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Eric Wieser]

Or a class taking two arguments?

[Kevin Buzzard]

Eric Wieser said:

So at least G₀ needs to be an argument too

No. Not if you make it a structure

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Eric Wieser]

All makes sense, thanks.

[Eric Wieser]

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

[Johan Commelin]

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

[Kevin Buzzard]

Yes, the definition is completely confusing

[Kevin Buzzard]

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

[Utensil Song]

for a given G, there's only one G0

[Eric Wieser]

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

[Utensil Song]

it's still the same

[Eric Wieser]

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!

[Johan Commelin]

Can you write down the definition in maths?

[Johan Commelin]

Or link to one?

[Kevin Buzzard]

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.

[Eric Wieser]

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

[Kevin Buzzard]

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

[Eric Wieser]

Ah, ok, got it

[Johan Commelin]

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

[Kevin Buzzard]

Just some dumb examples

[Eric Wieser]

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

[Johan Commelin]

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

[Johan Commelin]

However, there is a tonne of structure there.

[Johan Commelin]

There will be some nontrivial design decisions here

[Johan Commelin]

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

[Eric Wieser]

What do you mean by "compatibilities"?

[Johan Commelin]

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

[Kevin Buzzard]

oh this is high-level structure making tips!

[Johan Commelin]

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.

[Johan Commelin]

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

[Utensil Song]

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.

[Kevin Buzzard]

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

[Eric Wieser]

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

[Johan Commelin]

Yes, metric_space is a classical example

[Johan Commelin]

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

[Eric Wieser]

docs#metric_space

[Kevin Buzzard]

It takes a uniform structure now, I think

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Eric Wieser]

What is that constructor?

[Kevin Buzzard]

This is rather advanced structure-making.

[Johan Commelin]

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

[Johan Commelin]

Kevin Buzzard said:

This is rather advanced structure-making.

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

[Kevin Buzzard]

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.

[Eric Wieser]

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

[Kevin Buzzard]

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

[Utensil Song]

IMG_1517.PNG

[Johan Commelin]

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

[Utensil Song]

the current design is that it's a class

[Kevin Buzzard]

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

[Eric Wieser]

Order is specified as G_0 G_1 G

[Kevin Buzzard]

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

[Eric Wieser]

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

[Utensil Song]

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

[Utensil Song]

not R R C

[Kevin Buzzard]

What is G(0,1)?

[Eric Wieser]

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

[Kevin Buzzard]

Unfortunately that definition is circular

[Kevin Buzzard]

Is G determined by G_0 and G_1?

[Eric Wieser]

I think the answer is probably yes.

[Kevin Buzzard]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Johan Commelin]

About how we approached valuations and especially the target type.

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

but it was OK, because we learnt a lot

[Johan Commelin]

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

[Utensil Song]

The answer is no actually

[Johan Commelin]

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.

[Johan Commelin]

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

[Utensil Song]

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

[Johan Commelin]

I will repeat, give me an example.

[Eric Wieser]

The signature pqr is embedded in the G_1 argument

[Johan Commelin]

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

[Utensil Song]

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

[Reid Barton]

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.

[Reid Barton]

If that helps.

[Reid Barton]

And obviously up to isomorphism.

[Utensil Song]

will type examples out tmr

[Johan Commelin]

Reid Barton said:

And obviously up to isomorphism.

That's exactly my point.

[Johan Commelin]

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

[Utensil Song]

IMG_1518.PNG

[Eric Wieser]

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: ℂ ℂ⁰ ℂ

[Johan Commelin]

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

[Eric Wieser]

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

[Johan Commelin]

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

[Eric Wieser]

The (vector) inner product comes from G₁

[Johan Commelin]

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

[Utensil Song]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Utensil Song]

it's actually in G already

[Utensil Song]

the quadratic form and other stuff...

[Utensil Song]

we are talking about two different designs

[Johan Commelin]

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

[Johan Commelin]

Up to isomorphism, everything is fine.

[Utensil Song]

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

[Johan Commelin]

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

[Utensil Song]

not in the design I'm referring to

[Johan Commelin]

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

[Utensil Song]

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

[Eric Wieser]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Utensil Song]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Eric Wieser]

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)

[Utensil Song]

consider the complex numbers as either:

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

[Johan Commelin]

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

[Eric Wieser]

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

[Johan Commelin]

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

[Utensil Song]

we need both

[Johan Commelin]

I agree that you need both.

[Utensil Song]

so it seems isomorphism is the way to go

[Johan Commelin]

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

[Johan Commelin]

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

[Utensil Song]

(deleted)

[Johan Commelin]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

And guess what! Some proofs became easier!

[Utensil Song]

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

I see, this is it.

[Eric Wieser]

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

[Johan Commelin]

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.

[Utensil Song]

yes

[Johan Commelin]

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

[Eric Wieser]

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

[Johan Commelin]

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

[Eric Wieser]

Did you find it would never have been useful?

[Eric Wieser]

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

[Utensil Song]

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

[Johan Commelin]

I'm confused...

[Eric Wieser]

At me or utensil, @Johan Commelin?

[Johan Commelin]

Utensil

[Johan Commelin]

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

[Kevin Buzzard]

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.

[Johan Commelin]

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.

[Eric Wieser]

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

[Utensil Song]

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.

[Johan Commelin]

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.

[Johan Commelin]

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:

[Bryan Gin-ge Chen]

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.

[Johan Commelin]

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.

[Utensil Song]

thanks!

[Utensil Song]

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.

[Utensil Song]

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.

[Reid Barton]

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) $k$-algebras equipped with a $k$-linear map from $V$ compatible with the quadratic form on $V$ in a certain way.

[Reid Barton]

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

[Reid Barton]

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

[Utensil Song]

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.

[Utensil Song]

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.

[Utensil Song]

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

$\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 $\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 $\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 $\mathbb{R}_{\ge 0} = (\mathbb{R}_{\gt 0})_0$. This tiny lie only requires that we forget that the 0 in $(\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 $\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?

[Johan Commelin]

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.

[Kevin Buzzard]

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

[Utensil Song]

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

[Utensil Song]

The goal state is

v : ℝ
⊢ ↑v * ↑v = ⇑(algebra_map ℝ ℂ) v * ⇑(algebra_map ℝ ℂ) v

[Eric Wieser]

The solution to your sorry is refl

[Utensil Song]

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

[Utensil Song]

I tried everything except refl!

[Reid Barton]

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 $x$, $y$, $z$, we have $(x * y) * z = x * (y * z)$"). Free groups however are not the models of an algebraic theory.

[Utensil Song]

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

[Utensil Song]

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

[Utensil Song]

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.

[Utensil Song]

For example, would the following qualify for universal algebra?

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

Then $\mathcal{A}$ is said to be a Clifford algebra for $(\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.

[Utensil Song]

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

[Reid Barton]

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

[Utensil Song]

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

[Jalex Stark]

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"

[Jalex Stark]

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.

[Eric Wieser]

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

[Kevin Buzzard]

refl will unfold everything. simp won't.

[Kevin Buzzard]

def foo := ℕ

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

[Kevin Buzzard]

def foo := ℕ

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

Of course refl works.

[Kevin Buzzard]

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.

[Jalex Stark]

Yes

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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.

[Utensil Song]

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?

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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)

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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!

[Scott Morrison]

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

[Scott Morrison]

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

[Utensil Song]

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

[Utensil Song]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Utensil Song]

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:

0. only use simp only [xxx] with the help of squeeze_simp;
1. simp involving only the simp lemmas in mathlib is allowed;
2. use no simp inside the theory if it involves simp lemmas in the theory; -- to avoid the circular feeling
3. 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].

[Jalex Stark]

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

[Scott Morrison]

I'm not sure either.

[Scott Morrison]

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

[Utensil Song]

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

[Johan Commelin]

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

[Utensil Song]

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.

[Utensil Song]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Utensil Song]

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

[Johan Commelin]

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

[Bryan Gin-ge Chen]

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

[Scott Morrison]

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

[Utensil Song]

That's basically set_option pp.coercions false?

[Utensil Song]

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

[Utensil Song]

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

[Scott Morrison]

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_. :-)

[Scott Morrison]

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.

[Scott Morrison]

(and get more attention)

[Utensil Song]

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.

[Utensil Song]

Moved to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/unbundled.20v.2Es.2E.20%28semi-%29bundled/near/204049917