Is this a valid way of defining a typeclass?

Stream: Is there code for X?

[Quarrie]

I want to define a parametrized typeclass. However, the axioms that define it rely on some variables that can only be defined dependent on the parameters. If I write this:

variable parameter : Type u
variable another : (some_transformation parameter)
class parametrized parameter :=
  (axiom : some_predicate another)

would it be valid Lean code? If not, how do I render this concept?

[Yaël Dillies]

Yes it's definitely possible :smile:. However, you will have to make another visible from the outside of the class, as Lean can't guess it from parameter alone (however it can guess parameter from another).

[Yury G. Kudryashov]

It would be easier to answer if you provide a complete minimal example

[Yury G. Kudryashov]

Your lean code is incorrect and there is more than one way to interpret it

[Yakov Pechersky]

One important detail is parameter is a reserved keyword, so that probably isn't the right "variable name". You can tell from the syntax highlighting here.

[Reid Barton]

Likewise axiom

[Yakov Pechersky]

Reid, you might like: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235698.20strongly.20regular.20graphs/near/266519557

[Quarrie]

So in my case, assume an inductive type called strict_product_type (E : Type u) (prod : E -> E -> E) and a function called down_convert of type strict_product_type E tprod -> Type u are defined earlier in the code. I want to write something like:

variable E : Type u
variable prod : Type u -> Type u -> Type u
variables α, β, γ : strict_product_type E prod
def α' := down_convert α
def β' := down_convert β
def γ' := down_convert γ
variable prod_t : α' -> β' -> prod α' β'
class tensor_product_family E prod prod_t :=
  (product_spaces_is_associative : (x : (prod (prod α' β') γ')) : (prod α' (prod β' γ')))
  (product_elements_is_associative : ∀ (a : α', b : β', g : γ') ((prod_t (prod_t a b) g) = (prod_t a (prod b g)))

[Adam Topaz]

I think you probably just need to write

class tensor_product_family (E : Type u) (prod : Type u -> Type u -> Type u) (prod_t : α' -> β' -> prod α' β') := ...

[Adam Topaz]

Oh, nevermind, I see now that prod_t depends on prod.

[Adam Topaz]

Can you provide a #mwe that will work if we paste it in a lean file?

[Quarrie]

I wouldn't be asking here if I could, unfortunately

[Quarrie]

If I managed to disentangle the element product from the space product I don't see how I could get "the kronecker product over R^n" to be accepted as an instance for example

[Adam Topaz]

I mean just something that includes strict_product_typeand down_convert (or some approximation of those)

[Quarrie]

They are currently defined thus:

universe u
variables {α β γ : Type u}

inductive strict_product_type (E : Type u) (tprod : Type u -> Type u -> Type u)
| unit : strict_product_type
| left_prod : strict_product_type -> strict_product_type

def down_convert {E : Type u} {tprod : Type u -> Type u -> Type u} : strict_product_type E tprod -> Type u
| unit := E
| left_prod χ := (tprod E (down_convert χ))

[Adam Topaz]

and left_prod?

[Adam Topaz]

I'm just looking for code that works without the problematic class declaration.

[Quarrie]

left_prod is a constructor of one argument, isn't it? (Basically strict_product_type is supposed to be a Peano naturals that I can unroll with down_convert to generate some type tensor'd with itself n times.) Did I define it incorrectly?

[Adam Topaz]

Something is off. The code you just gave does not work. Could you take a quick look at the link #mwe ?

[Quarrie]

Oh right the imports

[Quarrie]

import algebra.module.basic
import analysis.inner_product_space.basic
import linear_algebra.bilinear_form
import linear_algebra.tensor_product

[Adam Topaz]

Even if I add open strict_product_type it still doesn't work.

[Adam Topaz]

It's not just the imports, your definition of down_convert doesn't work for me.

[Quarrie]

That's odd, can you paste the error you're receiving?

[Adam Topaz]

I get a ill-formed match/equation expression.

[Quarrie]

Maybe if we wrap the left_prod case with parentheses?

| (left_prod χ) := (tprod E (down_convert χ))

[Adam Topaz]

With the parens I still get an error, that the equation compiler fails because lean can't automatically prove the recursive function terminates. This would be a lot more efficient if you could give us some code that works, not including the class declaration that you want to ask about. If that's not the only issue, then we can start with the first problem first, but it's hard to diagnose anything if we don't have a place to start.

[Eric Wieser]

Perhaps checking your lean version would help here

[Quarrie]

@Eric Wieser
leanprover-community/lean:3.38.0

[Adam Topaz]

I'm also on 3.38.0 with the freshest of mathlibs.

[Yury G. Kudryashov]

Am I right that strict_product_type does not actually depend on E and tprod and can be replaced by a natural number?

[Quarrie]

Yury G. Kudryashov said:

Am I right that strict_product_type does not actually depend on E and tprod and can be replaced by a natural number?

Yeah, the work is done by the down_convert function. It's only an explicit Peano because it seemed less non-obvious-error-prone, with the plan being to replace it with the naturals from the standard library once I got it working

[Quarrie]

The strict_product_type type does contain E and tprod information, but that can indeed be packed into down_convert

[Yury G. Kudryashov]

Then

def down_convert (E : Type u) (tprod : Type u -> Type u -> Type u) : nat -> Type u
| 0 := E
| (n + 1) := (tprod E (down_convert n))

[Yury G. Kudryashov]

which is equivalent (but not defeq because of they use recursion on different sides) to down_convert E tprod n = (tprod E)^[n] E

[Quarrie]

Alright, looks like I found the root error that's causing all the rest

[Quarrie]

/home/quarrie/Git/mathlib_testing/src/tensor_product.lean:38:18: error: type expected at
  α'
term has type
  Type ? → (Type ? → Type ? → Type ?) → ℕ → Type ?

[Quarrie]

...how do I interpret this? that's a concerning amount of unknown universe.

[Yury G. Kudryashov]

I'm not sure why it depends on a natural number.

[Yaël Dillies]

There's an expected line just below

[Yury G. Kudryashov]

What are the first 38 lines of the file?

[Quarrie]

Yaël Dillies said:

There's an expected line just below

No, oddly. Just below is an identical error regarding β'.

[Yury G. Kudryashov]

Can you just copy+paste them in #backticks?

[Quarrie]

Yury G. Kudryashov said:

What are the first 38 lines of the file?

With the comments removed for conciseness:

/- This was lines 1-5 -/

import algebra.module.basic
import analysis.inner_product_space.basic
import linear_algebra.bilinear_form
import linear_algebra.tensor_product

/-! This was lines 12-22 -/

namespace inner_product_space

universe u

def down_convert (E : Type u) (tprod : Type u -> Type u -> Type u) : nat -> Type u
| 0 := E
| (n + 1) := (tprod E (down_convert n))

variable E : Type u
variable prod : Type u -> Type u -> Type u
variables (α β γ : nat)
def α' := (down_convert E prod) α
def β' := (down_convert E prod) β
def γ' := (down_convert E prod) γ
variable prod_t : α' -> β' -> prod α' β'

[Yury G. Kudryashov]

def α' defines a type that depends on E, prod, and α.

[Yury G. Kudryashov]

Actually, α' is defeq to β'

[Yury G. Kudryashov]

And both are defeq to down_convert.

[Quarrie]

Yury G. Kudryashov said:

def α' defines a type that depends on E, prod, and α.

That's the intended use, since α' is meant to be an arbitrary power of E so that I can reason about its tensor product.

[Yaël Dillies]

So the problem is that Lean doesn't know what the argument to α' is

[Yury G. Kudryashov]

variables α is just a way to say "if I use α in a definition/lemma and don't list it as an argument, then add it as an argument to the definition".

[Yury G. Kudryashov]

Probably you want to use (untested)

local notation `α'` := down_convert E prod α

[Quarrie]

Good idea, let me see how that works

[Yury G. Kudryashov]

The problem with your def is that Lean immediately looses connection between the definition α' and the variable α.

[Quarrie]

That makes sense!

[Quarrie]

Alright, that's solved and now there's a new error

[Quarrie]

/home/quarrie/Git/mathlib_testing/src/tensor_product.lean:39:0: error: infer type failed, sort expected
  ?m_1[E]

[Quarrie]

(line 39 is the typeclass declaration)

[Yury G. Kudryashov]

We need to see the source code, not just the error message.

[Quarrie]

/- Former 1-5 -/

import algebra.module.basic
import analysis.inner_product_space.basic
import linear_algebra.bilinear_form
import linear_algebra.tensor_product

/-! Formerly 12-22 -/

namespace inner_product_space

universe u

def down_convert (E : Type u) (tprod : Type u -> Type u -> Type u) : nat -> Type u
| 0 := E
| (n + 1) := (tprod E (down_convert n))

variable E : Type u
variable prod : Type u -> Type u -> Type u
variables (α β γ : nat)
local notation `α'` := down_convert E prod α
local notation `β'` := down_convert E prod β
local notation `γ'` := down_convert E prod γ
variable prod_t : α' -> β' -> prod α' β'
class tensor_product_family E prod prod_t :=
  (product_spaces_is_associative : (x : (prod (prod α' β') γ')) : (prod α' (prod β' γ')))
  (product_elements_is_associative : ∀ (a : α', b : β', g : γ') ((prod_t (prod_t a b) g) = (prod_t a (prod b g)))

end inner_product_space

[Yaël Dillies]

You only need one of the notations if you make it local notation α ' := down_convert E prod α

[Yury G. Kudryashov]

Let's not optimize before we catch the bug.

[Yury G. Kudryashov]

Also, with your notation Lean will try to use down_convert for a'.

[Yury G. Kudryashov]

product_spaces_is_associative has no ∀/∃ on x.

[Yury G. Kudryashov]

Can you post the mathematical definition you're trying to formalize (e.g., what are prod, prod_t in some important specific case)?

[Quarrie]

Yury G. Kudryashov said:

Can you post the mathematical definition you're trying to formalize (e.g., what are prod, prod_t in some important specific case)?

In one extremely important specific case, prod is $\mathbb{C}^n \rightarrow \mathbb{C}^m \rightarrow \mathbb{C}^{n*m}$ and prod_t is $\sum_{i = 0}^{n} a_ie_i \rightarrow \sum_{j = 0}^{m} b_je_j \rightarrow \sum_{i = 0}^{n} \sum_{j = 0}^{m} a_ib_je_{im+j}$

[Quarrie]

The axiom about type product associativity is then "it makes sense to talk about an n-qubit state" and the axiom about element product associativity is then "if a state is separable, what order you separate it in doesn't change the individual qubits"

[Heather Macbeth]

double $ :)

[Quarrie]

thank you

[Yury G. Kudryashov]

What exactly should the first axiom say (in terms of ∀, ∃ etc)?

[Quarrie]

(deleted)

[Yury G. Kudryashov]

Note that Lean doesn't understand that, e.g., α × (β × γ) and (α × β) × γ are "equal".

[Yury G. Kudryashov]

You need to insert an explicit isomorphism.

[Yury G. Kudryashov]

And probably you should use this isomorphism in the second axiom.

[Yury G. Kudryashov]

/me is away for 1-2 hrs

[Quarrie]

Yury G. Kudryashov said:

What exactly should the first axiom say (in terms of ∀, ∃ etc)?

$\forall a, b, g \in \mathbb{N}, E^{\otimes a} \otimes (E^{\otimes b} \otimes E^{\otimes g}) = (E^{\otimes a} \otimes E^{\otimes b}) \otimes E^{\otimes g}$

[Quarrie]

They should be the same type, so putting an isomorphism there would break it.

[Quarrie]

More clearly, the example I'm using is let $E \coloneqq \mathbb{C}^2, a = 1, b = 1, g = 2$.

[Yury G. Kudryashov]

You shouldn't use equality of types in your axioms.

[Yaël Dillies]

They won't ever be the same type. And even if they were, you shouldn't use this equality.

[Yaël Dillies]

Equality of types is evil.

[Yury G. Kudryashov]

You should either make them defeq (probably, impossible), or introduce explicit isomorphisms.

[Quarrie]

Yaël Dillies said:

They won't ever be the same type. And even if they were, you shouldn't use this equality.

For clarity, this is not a cartesian product. This is a tensor product of which Kronecker is an example

[Yakov Pechersky]

Maybe, one can say, you don't require the full power of "equality of types" as an axiom, even having a weaker "these types are explicitly isomorphic" will likely be powerful enough for what you want to use this structure for.

[Yury G. Kudryashov]

Then you'll need extra axioms about this family of isomorphisms.

[Adam Topaz]

I'm fairly sure @Amelia Livingston ran into similar issues when working on the tensor algebra.

[Quarrie]

Yaël Dillies said:

Equality of types is evil.

How should I handle this, then?

[Quarrie]

I cannot use an isomorphism as that would destroy the power of the axiom.

[Adam Topaz]

What are you trying to do, mathematically?

[Yaël Dillies]

The power of the axiom is that it is usually unprovable? :thinking:

[Quarrie]

Adam Topaz said:

What are you trying to do, mathematically?

Define a family of types endowed with a tensor product, so that I can reason about an n-qubit system.

[Adam Topaz]

Take a look at docs#category_theory.monoidal_category

[Quarrie]

404's out, which one?

[Adam Topaz]

Sorry, I fixed the link

[Adam Topaz]

Note the associator axiom, for example

[Adam Topaz]

I don't know how much category theory you want to use in your work, but using monoidal categories is one possible approach

[Quarrie]

This does look useful, though I'll have to restrict the dependent product to an independent product and the associator to the identity.

[Quarrie]

Thanks!

[Adam Topaz]

But you can't restrict them to the identity!

[Adam Topaz]

The tensor product $A\otimes(B\otimes C)$ is not equal to $(A\otimes B)\otimes C$ (at least for vector spaces).

[Quarrie]

Adam Topaz said:

The tensor product $A\otimes(B\otimes C)$ is not equal to $(A\otimes B)\otimes C$ (at least for vector spaces).

Is Kronecker product not an instance of $\otimes$?

[Quarrie]

I've been under the impression that it makes sense to write $(\mathbb{C}^2 \otimes \mathbb{C}^2) \otimes \mathbb{C}^4 = \mathbb{C}^2 \otimes (\mathbb{C}^2 \otimes \mathbb{C}^4) = \mathbb{C}^{16}$ for instance

[Kevin Buzzard]

The tensor product of two vector spaces is "defined" by a universal property, so it doesn't really even make sense to ask if two tensor products are equal.

[Heather Macbeth]

(Of course, we agree these spaces are "canonically isomorphic".)

[Adam Topaz]

The equality symbol you're using there means "canonical isomorphism"

[Heather Macbeth]

(snap!)

[Quarrie]

Kevin Buzzard said:

The tensor product of two vector spaces is "defined" by a universal property, so it doesn't really even make sense to ask if two tensor products are equal.

Okay, so what's the word for the thing I want (an instance of a product that satisfies that property)?

[Adam Topaz]

And actually the right-hand equality (the one with C^16 on the right) should NOT be written as equality (in my opinion).

[Kevin Buzzard]

What do you mean by $V\otimes W$? You can't mean "any vector space satisfying the universal property" because in formalised mathematics this cannot be used as a definition. So you have to choose some explicit model, perhaps some quotient of some huge group or whatever definition you want to use in your proof that tensor products exist. And the moment you make that choice none of the things you're claiming are equalities, are in fact equalities.

[Kevin Buzzard]

They're canonical isomorphisms, sure. But that's not what the = symbol means in lean.

[Kevin Buzzard]

In fact as Adam says that last iso to C^16 isn't even canonical. We all agree that 2*2*4=16 but when you categorify the equality changes to an isomorphism

[Quarrie]

Kevin Buzzard said:

What do you mean by $V\otimes W$? You can't mean "any vector space satisfying the universal property" because in formalised mathematics this cannot be used as a definition. So you have to choose some explicit model, perhaps some quotient of some huge group or whatever definition you want to use in your proof that tensor products exist. And the moment you make that choice none of the things you're claiming are equalities, are in fact equalities.

My intention was that the meaning of $V \otimes W$ was decided by the programmer at the moment that the programmer endowed the family of types containing $V$ and $W$ with an $\otimes$ operation. In my case, I want to use this for quantum program verification, so I'm working on $\mathbb{C}^n$ and want to let $\otimes$ be the Kronecker product and show that it satisfies insert axioms here.

[Kevin Buzzard]

The axioms you want are those of a monoidal category perhaps

[Adam Topaz]

Note Module \C is a category which should have a monoidal category instance :) docs#Module

[Kevin Buzzard]

When the programmer made the definition they did indeed make an explicit construction and that's exactly why we know that the tensor product can't be proved to be associative on the nose

[Kevin Buzzard]

And as for identifying it with C^16 you'll have to explicitly decide how to order your basis vectors of the tensor product -- the isomorphism here involves a genuine choice which you'll need to keep track of if you're doing mathematics rigourously

[Quarrie]

Kevin Buzzard said:

When the programmer made the definition they did indeed make an explicit construction and that's exactly why we know that the tensor product can't be proved to be associative on the nose

Why wouldn't a user-supplied tensor product instance be provably associative? Would $\mathbb{C}^n \otimes \mathbb{C}^m \coloneqq \mathbb{C}^{nm}$ with $e_i : \mathbb{C}^n, e_j : \mathbb{C}^m, e_i \otimes_t e_j = e_{im + j}$ not function as a tensor product?

[Kevin Buzzard]

It would function as a tensor product in that case but it's not the definition which was made in Lean

[Kevin Buzzard]

Your definition is isomorphic to Lean's, hence the isomorphism we're all going on about

[Quarrie]

The typeclass I'm building forces the user to supply their own tensor product though, by providing it as an argument (e.g. one might say "$\mathbb{C}^2$ forms a family of types endowed with the tensor product kron")

[Quarrie]

Is this non-idiomatic for Lean code?

[Kyle Miller]

Maybe the key words here are that @Quarrie wants a strictification of the monoidal category of vector spaces with tensor products

[Adam Topaz]

You can define a skeleton for the subcategory of Module C of f.d. spaces which has N as the type of objects. But again, associativity of multiplication of naturals is propositional equality, not definitional equality, so you will likely run into issues if you start using equality of objects in this skeletal category.

[Adam Topaz]

(if you also want infinite dimensional vector spaces, you can work with cardinals)

[Kyle Miller]

I'm not sure you can define a strictification like this with prod taking Types. This is what down_convert is presumably tying to solve?

Maybe another way is to have a function that takes List Nat and produces the corresponding vector space? Tensor product is then concatenation of lists, which is strictly associative. But then you still have these canonical isomorphisms for whether you concatenate then take the vector space or take the vector spaces and then tensor product.

[Quarrie]

Kyle Miller said:

I'm not sure you can define a strictification like this with prod taking Types. This is what down_convert is presumably tying to solve?

Maybe another way is to have a function that takes List Nat and produces the corresponding vector space? Tensor product is then concatenation of lists, which is strictly associative. But then you still have these canonical isomorphisms for whether you concatenate then take the vector space or take the vector spaces and then tensor product.

down_convert is meant to define a single canonical order of association so that I can (a) check if associating in a different order produces the same result, and (b) have a convenient way to induct through the powers of E. Re: Type u, I ideally want prod to only have to accept powers of E (after all, doesn't really make sense to take the Kronecker product of objects that don't even have a scalar multiple operation, and I'd rather not deal with such when instantiating the Kronecker product as this typeclass) -- is this conveniently possible in Lean?

[Adam Topaz]

docs#matrix.kronecker

[Kyle Miller]

I don't know how well this will work in practice, but what I was suggesting is trying to leave the tensor product in the list nat representation as long as possible, and then prod only takes powers of E since it's actually only taking these lists

[Kyle Miller]

A problem with Type is that, unlike for terms of inductive types, you can't do any sort of match expression on types. So, a way around this is to manipulate algebraic expressions (here, lists of naturals) that then get turned into types.

[Quarrie]

Kyle Miller said:

I don't know how well this will work in practice, but what I was suggesting is trying to leave the tensor product in the list nat representation as long as possible, and then prod only takes powers of E since it's actually only taking these lists

An issue there would seem to be that this produces the product spaces, but does not offer a way to give the product elements.

[Kyle Miller]

Right, that is an issue. A way around that is to have a wrapper around list nat so that it has a coercion to a Type, so you can pretend it's actually a vector space. I need to check how well this actually works in this case

[Quarrie]

So basically, the user would supply:

• the base type
• what's basically a Peano successor, but for tensor products
• and the element tensor product
  Is this correct?

[Yury G. Kudryashov]

When you write a typeclass, it is useful to define at least one instance of that class.

[Yury G. Kudryashov]

This way you'll see whether your axioms make sense in Lean.

[Yury G. Kudryashov]

So, you can start with an instance.

[Yury G. Kudryashov]

Define some prod etc (note that prod in the root namespace is taken), then prove some lemmas about your definitions, then define a typeclass that takes these lemmas as arguments.

[Quarrie]

:+1:

[Yakov Pechersky]

Regarding a list of types, that design strategy is explored in docs#holor

[Kyle Miller]

I haven't succeeded really with my proposal, other than defining a function that takes lists of natural numbers to specific tensor products of spaces.

Is there a better way to recursively take tensor products of spaces? It was awkward needing to recursively create the space and passing along the necessary typeclasses for each step.

Code

import algebra.module.basic
import analysis.inner_product_space.basic
import linear_algebra.bilinear_form
import linear_algebra.tensor_product

namespace inner_product_space

open_locale tensor_product

universe u

variables (R : Type u) [comm_semiring R] (M : Type u) [add_comm_monoid M] [module R M]

@[reducible]
def pow_space (n : ℕ) : Type* := fin n → M

section
include R M
class space_for_list (ns : list ℕ) := (space : Type u)
end

@[reducible]
def tensor_space' : list ℕ → Σ (α : Type*) [add_comm_monoid α], by exactI module R α
| [] := ⟨R, infer_instance, infer_instance⟩
| [n] := ⟨pow_space M n, infer_instance, infer_instance⟩
| (n::ns) :=
begin
  casesI tensor_space' ns with α' b,
  casesI b,
  exact ⟨pow_space M n ⊗[R] α', infer_instance, infer_instance⟩,
end

def tensor_space (ns : list ℕ) : Type* := (tensor_space' R M ns).1

instance (ns : list ℕ) : add_comm_monoid (tensor_space R M ns) := (tensor_space' R M ns).2.1
instance (ns : list ℕ) : module R (tensor_space R M ns) := (tensor_space' R M ns).2.2

-- examples that defeq works
lemma tensor_space₁ {n1 : ℕ} :
  tensor_space R M [n1] = (fin n1 → M) := rfl
lemma tensor_space₂ {n1 n2 : ℕ} :
  tensor_space R M [n1, n2] = (fin n1 → M) ⊗[R] (fin n2 → M) := rfl
lemma tensor_space₃ {n1 n2 n3 : ℕ} :
  tensor_space R M [n1, n2, n3] = (fin n1 → M) ⊗[R] ((fin n2 → M) ⊗[R] (fin n3 → M)) := rfl
lemma tensor_space₄ {n1 n2 n3 n4 : ℕ} :
  tensor_space R M [n1, n2, n3, n4] = (fin n1 → M) ⊗[R] ((fin n2 → M) ⊗[R] ((fin n3 → M) ⊗[R] (fin n4 → M))) := rfl

end inner_product_space

[Adam Topaz]

@Kyle Miller you could use docs#Module with the monoidal tensor product. The correct instances will be part of the structure.

[Adam Topaz]

(deleted)

[Adam Topaz]

Thats wrong. one sec

[Adam Topaz]

This is better:

import algebra.category.Module.monoidal

universes u

variables (A : Type u) [comm_ring A]

def foo : list ℕ → Module.{u} A
| [] := 𝟙_ (Module.{u} A)
| (x :: xs) := Module.of A (fin x → A) ⊗ foo xs

[Adam Topaz]

Of course you could replace A with any A-module M, as needed.

[Adam Topaz]

Note that this is indeed defeq;

example (M N : Module.{u} A) : tensor_product A M N = (M ⊗ N : Module.{u} A) := rfl

[Adam Topaz]

but there is a clash of notations, since $\otimes$ is used both for the unbundled tensor product (under the tensor_product locale), and for the monoidal one.

[Adam Topaz]

Of course, we could also use list.foldr:

import algebra.category.Module.monoidal

universes u

variables (A : Type u) [comm_ring A]

def foo : list ℕ → Module.{u} A :=
list.foldr (λ n M, Module.of A (fin n → A) ⊗ M) (𝟙_ _)