Zulip Chat Archive

Stream: new members

Topic: Theorem Formalization


Alex Zhang (May 27 2021 at 07:33):

In Lean, how to state/formalize a theorem involving a1,..., an for an arbitrary pos integer n, taking the following trivial theorem as an example: for any pos integer n, for any real numbers a1,..., an, a1^2+...+an^2>=0.

Johan Commelin (May 27 2021 at 07:36):

@Alex Zhang There are two ways to approach this:
(1) Pick a function from fin n to the real numbers. fin n is the type of numbers {0, 1, ..., n-1}.

Johan Commelin (May 27 2021 at 07:37):

(2) Pick an infinite sequence (a0,a1,,an,)(a_0, a_1, \dots, a_n, \dots) and only talk about the first nn elements.

Johan Commelin (May 27 2021 at 07:38):

What I would actually do is to drop the n completely, and prove this for arbitrary finite sums, indexed by any finite set.

Johan Commelin (May 27 2021 at 07:40):

import data.real.basic

open_locale big_operators

lemma sum_of_squares_nonneg {ι : Type*} (s : finset ι) (a : ι  ) :
  0  ( i in s, (a i)^2) :=
begin
  sorry
end

Johan Commelin (May 27 2021 at 07:42):

The next thing I would do, is try to generalize real away. Because the theorem also holds for Z\Z and Q\mathbb Q.

Johan Commelin (May 27 2021 at 07:42):

So then I wonder if it's true in any linear_ordered_comm_semiring.

Johan Commelin (May 27 2021 at 07:43):

And that might actually not be true. I frankly don't know.

Alex Zhang (May 27 2021 at 07:49):

Many thanks, Johan!
To prove the first trivial theorem, I think the next thing I will do is to do induction on the cardinal of s. I am still quite new to Lean.. I know how to do induction, but the achieve the next step, how do I know what files do I need to import to use "cardinal" and where to find a manual illustrating the use of "cardinal"?

Johan Commelin (May 27 2021 at 07:50):

@Alex Zhang in fact, you can do induction on s itself.
Try

begin
  classical,
  apply finset.induction_on s,
end

Johan Commelin (May 27 2021 at 07:51):

That will give you to goals: (i) prove it for empty s, and (ii) prove it for s \union {x} assuming you know the theorem for s

Alex Zhang (May 27 2021 at 07:55):

Thanks, Johan! Could you please explain, if I do want to use something like "cardinal" in the future, how should I figure out the above questions?

Johan Commelin (May 27 2021 at 07:56):

In VScode you can click the :magnifying_glass: button in the bar on the left, and search for cardinal. If that doesn't give you what you want, asking here should usually give you a fast answer as well.

Alex Zhang (May 27 2021 at 08:15):

import data.real.basic
import set_theory.cardinal

#eval cardinal.mk 

This gives me the error message result type does not have an instance of type class 'has_repr', dumping internal representation.

Kevin Buzzard (May 27 2021 at 08:15):

What are you expecting the answer to be?

Kevin Buzzard (May 27 2021 at 08:15):

It says "this is some random equivalence class which doesn't have a string attached to it so I don't know what string to print"

Kevin Buzzard (May 27 2021 at 08:16):

#eval means "turn the internal representation of this object into a string, by "evaluating" it in some way, and print the string"

Kevin Buzzard (May 27 2021 at 08:18):

#eval list.cons 4 list.nil -- [4]

This works because someone wrote some code which takes a list and turns it into a string starting with a [ and puts commas between the string representations of the elements of the list etc etc

Eric Wieser (May 27 2021 at 08:26):

What does "induction on a docs#cardinal" mean for uncountable cardinalities?

Alex Zhang (May 27 2021 at 08:28):

Kevin Buzzard said:

What are you expecting the answer to be?

I would expect cardinal.mk ℝ can give me c (or what is used to represent this in Lean), and expect cardinal.mk (fin 5) can give me 5, but cardinal.mk does not work as I thought.

Kevin Buzzard (May 27 2021 at 08:29):

It is a theorem that cardinal.mk (fin 5) is 5.

Alex Zhang (May 27 2021 at 08:32):

Is there any function already defined in Lean which outputs the cardinal of S as a natural number when S is finite and given as input?

Johan Commelin (May 27 2021 at 08:33):

fintype.card

Johan Commelin (May 27 2021 at 08:33):

But depending on what you input, it cannot compute the natural number.

Eric Wieser (May 27 2021 at 08:34):

docs#fintype.card

Eric Wieser (May 27 2021 at 08:34):

We also have docs#finset.card, which is better if you started with a finset.

Johan Commelin (May 27 2021 at 08:35):

For example, Lean will probably timeout on fintype.card {p : fin 100 // nat.prime p}

Eric Wieser (May 27 2021 at 08:36):

Will timeout if you use #eval / #reduce, I assume you mean

Alex Zhang (May 27 2021 at 08:39):

any analogical function for infinite sets or countable sets?

Kevin Buzzard (May 27 2021 at 08:40):

There is no function which takes an arbitrary type and, for example, figures out magically whether it is countable or uncountable, no. Such a function cannot exist.

Johan Commelin (May 27 2021 at 08:40):

That's cardinal.mk

Eric Wieser (May 27 2021 at 08:51):

Sure there is, docs#classical.dec is "for any statement p, figure out magically if it's true". Unfortunately you're just not allowed to ask lean what its conclusion was!

Kevin Buzzard (May 27 2021 at 08:54):

I guess we have different mental models of or.

Anne Baanen (May 27 2021 at 10:18):

Johan Commelin said:

For example, Lean will probably timeout on fintype.card {p : fin 100 // nat.prime p}

(For the record, #eval is still quite fast on natural numbers. Only around #eval fintype.card {p : fin 100000 // nat.prime p} does it start to take over a second on my machine.)

Anne Baanen (May 27 2021 at 10:19):

(Meanwhile, #reduce takes longer than I care to wait on #reduce fintype.card {p : fin 4 // nat.prime p}.)

Johan Commelin (May 27 2021 at 11:13):

Ooh, right! But for proofs it is #reduce which is what matters, right?

Eric Wieser (May 27 2021 at 11:35):

Interestingly #reduce fintype.card {p : fin 3 // nat.prime p} is instant

Eric Wieser (May 27 2021 at 11:37):

This makes it faster:

import data.nat.prime
import data.fintype.basic

attribute [instance] nat.decidable_prime_1
example : fintype.card {p : fin 12 // nat.prime p} = 5 := rfl
#reduce fintype.card {p : fin 12 // nat.prime p}

Mario Carneiro (May 27 2021 at 22:49):

Johan Commelin said:

Ooh, right! But for proofs it is #reduce which is what matters, right?

Not exactly. rfl is similar but not quite as "thorough" as #reduce, and so it is usually a lot faster

Alex Zhang (Jun 28 2021 at 11:12):

I defined Kronecker product to be

variables {α : Type*}  {m n p q s t: }

def Kronecker [has_mul α]
(A : matrix (fin m) (fin n) α) (B : matrix (fin p) (fin q) α)
: matrix (fin (p * m)) (fin (q * n)) α := sorry

I omitted the exact definition.
Then I want to formalize the associativity.
But lemma K_assoc : (A ⊗ (B ⊗ C) = (A ⊗ B) ⊗ C :=sorry gives me the error message:

type mismatch at application
  Kronecker (AB)
term
  AB
has type
  matrix (fin (p * m)) (fin (q * n)) α
but is expected to have type
  matrix (fin m) (fin n) α

How can I fix this issue? Could anyone please give me a help?

Kevin Buzzard (Jun 28 2021 at 11:14):

Can you please post a #mwe ?

Kevin Buzzard (Jun 28 2021 at 11:14):

But I know what the problem will be :-)

Kevin Buzzard (Jun 28 2021 at 11:17):

Lean sees your lemma, and figures that it's an equality of two terms of a type, but it doesn't immediately know what the type is. So it looks at the left hand side to figure it out, and realises that the type is matrix (fin (m * (p * s)) (fin (n * (q * t)) or something (this is where having a mwe would help me), and then it tries to make sense of the RHS, and it sees _ otimes C so decides that C should have type matrix (fin (ps)) (fin (qt)) and _ should have type matrix (fin m) (fin n), and then it takes a look at _ and realises that it can figure out the type and that it's not that.

Kevin Buzzard (Jun 28 2021 at 11:19):

The issue is that a * (b * c) is equal, but not definitionally equal, to (a * b) * c, and hence Lean is reluctant to identify fin (a * (b * c)) and fin ((a * b) * c) as equal. It would rather you used eq.subst to get a map from one to the other.

Alex Zhang (Jun 28 2021 at 11:20):

I understand this is a type mismatch problem, but have no idea how to fix it :(
Here is a #mwe. I tried to make is as short as possible.

Alex Zhang (Jun 28 2021 at 11:20):

import tactic
import data.matrix.notation

variables {α : Type*} {β : Type*} [inhabited α]
variables {m n p q s t: }

def Kronecker [has_mul α]
(A : matrix (fin m) (fin n) α) (B : matrix (fin p) (fin q) α)
: matrix (fin (p * m)) (fin (q * n)) α :=
λ i j, default α

localized "infix `⊗`:100 := Kronecker" in Kronecker

variables
(A : matrix (fin m) (fin n) α)
(B : matrix (fin p) (fin q) α)
(C : matrix (fin s) (fin t) α)
variables [semigroup α]

lemma K_assoc :
(A  (B  C) = (A  B)  C :=sorry

Kevin Buzzard (Jun 28 2021 at 11:22):

I could do the unhelpful thing of inserting the eq.rec into the statement of the lemma so that it compiles, but that would not solve the problem of how to prove the lemma, which would probably be a pretty nasty one.

Kevin Buzzard (Jun 28 2021 at 11:24):

Let's take a step back. Your Kronecker product is really two constructions. Firstly there is a much more natural (from the point of view of functional programming at least) multiplication matrix F1 F2 alpha -> matrix F3 F4 alpha -> matrix (F1 x F2) (F3 x F4) alpha. Your Kronecker is this composed with some functorial map coming from matrices and a construction fin m x fin n -> fin (m*n)

Alex Zhang (Jun 28 2021 at 11:25):

I am going to prove the lemma myself (and I gave an incorrect definition in the first place in the #mwe anyway).
The trouble I am facing is just there is an error in the statement.

Kevin Buzzard (Jun 28 2021 at 11:25):

yes, but want to explain how there is something odd about the statement

Kevin Buzzard (Jun 28 2021 at 11:26):

The map fin m x fin n -> fin (m*n) is rather artificial, there are many such maps.

Alex Zhang (Jun 28 2021 at 11:26):

It would also be great if you can help to fix the problem by rewriting the defn.

Kevin Buzzard (Jun 28 2021 at 11:26):

That will in some sense make the problem worse

Kevin Buzzard (Jun 28 2021 at 11:27):

because what I am getting around to suggesting is that you should be proving something more abstract first

Kevin Buzzard (Jun 28 2021 at 11:27):

The multiplication I indicated above, with products of finite sets, is a more low-level object and the problem already arises there, and my instinct is that we should deal with it there before we get into all the mess of the combinatorics of bijections fin m x fin n -> fin (mn).

Kevin Buzzard (Jun 28 2021 at 11:29):

Now an interesting question is how to state associativity of this more fundamental product, and here you see that we still have the problem that it cannot be stated naively in Lean, because one matrix has type matrix ((F1 x F3) x F5) ((F2 x F4) x F6) alpha and the other has type matrix (F1 x (F3 x F5)) (F2 x (F4 x F6)) alpha and these types are not equal, they're just canonically isomorphic

Kevin Buzzard (Jun 28 2021 at 11:31):

so one should define, or perhaps just find in Lean because it's probably already there, the way to move between matrix A B alpha and matrix C D alpha given maps from C to A and D to B (maybe it will be called docs#matrix.comap or something)

Kevin Buzzard (Jun 28 2021 at 11:31):

and then the statement of associativity would say that mapping a matrix along such a map gave you another matrix

Kevin Buzzard (Jun 28 2021 at 11:32):

so then you can solve that knotty problem without all the extra fin noise, and then build the fin stuff on top where you'll have to prove some elementary number theory lemma saying that your two maps fin a -> fin b -> fin c -> fin (abc) coincide (where you do the multiplications in two different orders)

Alex Zhang (Jun 28 2021 at 11:35):

Kevin Buzzard said:

Now an interesting question is how to state associativity of this more fundamental product, and here you see that we still have the problem that it cannot be stated in Lean, because one matrix has type matrix ((F1 x F3) x F5) ((F2 x F4) x F6) alpha and the other has type matrix (F1 x (F3 x F5)) (F2 x (F4 x F6)) alpha and these types are not equal, they're just canonically isomorphic

Yes. Thanks for your explanations! At this step, we still face the same (almost) problem. (By the way, I think it would be more convenient to use fin n for the defn than using n as a fintpye as I do want elements to have orders to define the Kronecker product.)

Kevin Buzzard (Jun 28 2021 at 11:36):

I don't know if it's there already, but you seem to need a map equiv A B -> equiv C D -> equiv (matrix A C alpha) (matrix B D alpha). This construction (for it's a definition, not a theorem) will be needed in your statement of the more foundational product.

Alex Zhang (Jun 28 2021 at 11:37):

Could you please a #mwe illustrating your way of solving this?

Anne Baanen (Jun 28 2021 at 11:38):

The relevant map is either docs#matrix.reindex (if you don't care whether the equivalence is linear) or docs#matrix.reindex_linear_equiv.

Anne Baanen (Jun 28 2021 at 11:38):

(There is also docs#matrix.reindex_alg_equiv if you only want to work with square matrices)

Alex Zhang (Jun 28 2021 at 11:42):

Thank you both! I have to leave for a moment... before going back to solve the problem.

Yakov Pechersky (Jun 28 2021 at 11:45):

Why do you need the elements to have an order to define the Kronecker product? Perhaps proofs about the definition might use the order. But the definition itself need not have it.

Alex Zhang (Jun 28 2021 at 11:52):

I haven't left. Basically, I used this to define the product (omitted many things here)

(A : matrix (fin m) (fin n) α) (B : matrix (fin p) (fin q) α)
λ i j,  A (i / p) (j / q) * B (i % p)(j % q)

What is the way not using indices?

Alex Zhang (Jun 28 2021 at 11:57):

(deleted)

Yakov Pechersky (Jun 28 2021 at 12:07):

I think Kevin's point here holds, about two separate constructions. First you make the "full" product, then you can use matrix.reindex or matrix.minor

Alex Zhang (Jun 28 2021 at 12:23):

In my #mwe code,
(A ⊗ B) ⊗ C has type A⊗B⊗C : matrix (fin (s * (p * m))) (fin (t * (q * n))) α
the other has type A⊗(B⊗C) : matrix (fin (s * p * m)) (fin (t * q * n)) α.
fin (s * (p * m)) is not only isomorphic but also IDENTICAL to fin (s * p * m).
It is trivial to prove this fact

def aux1 : fin (s * (p * m)) = fin (s * p * m) := by ring_nf
def aux2 : fin (t * (q * n)) = fin (t * q * n) := by ring_nf

How can I make Lean to recognise these two identities when parsing the statement of the lemma in #mwe (perhaps by adding attributes to aux?)?

Johan Commelin (Jun 28 2021 at 12:25):

https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/Kronecker.20product/near/244007513 might be relevant. It's also about Kronecker products

Alex Zhang (Jun 28 2021 at 12:30):

Alex Zhang said:

In my #mwe code,
(A ⊗ B) ⊗ C has type A⊗B⊗C : matrix (fin (s * (p * m))) (fin (t * (q * n))) α
the other has type A⊗(B⊗C) : matrix (fin (s * p * m)) (fin (t * q * n)) α.
fin (s * (p * m)) is not only isomorphic but also IDENTICAL to fin (s * p * m).
It is trivial to prove this fact

def aux1 : fin (s * (p * m)) = fin (s * p * m) := by ring_nf
def aux2 : fin (t * (q * n)) = fin (t * q * n) := by ring_nf

How can I make Lean to recognise these two identities when parsing the statement of the lemma in #mwe (perhaps by adding attributes to aux?)?

Right, it's also about the Kronecer product. I didn't find things relevant to this particular question, however.

Johan Commelin (Jun 28 2021 at 12:32):

Agreed that it's not relevant to your question. I should have said "just wanna make sure you are aware of this other effort going on".

Johan Commelin (Jun 28 2021 at 12:34):

In this case, I think Lean is very bad at using the equalities aux1 and aux2. So I would turn them into equivs, and then use reindex mentioned above.

Yakov Pechersky (Jun 28 2021 at 12:35):

Alex, you need to use something like docs#equiv.cast, and compose in your definition. Or use docs#fin.cast. But it'll be easier if you generalize away from actual fin multiplication

Yakov Pechersky (Jun 28 2021 at 12:37):

Your claim that they're identical requires a proof. Just because it's a relatively trivial proof doesn't mean it can be skipped, when doing type manipulations. And I don't know if I would call it "trivial" if you used a pretty heavy-handed tactic like ring_nf to prove it.

Johan Commelin (Jun 28 2021 at 12:40):

I guess congr_arg _ (mul_assoc _ _ _) might also prove it...

Alex Zhang (Jun 28 2021 at 12:41):

Another #mwe. Is there a way to fix the error occurring in the statement of silly?

import tactic

variables m n: Type
variables h: m = n

def f:m  n   := 0
def g:n  m   := 0

lemma silly: f=g := sorry

Yakov Pechersky (Jun 28 2021 at 12:41):

Of course, but there isn't support for inferring what is or isn't simple type proof munging. One could imagine having a "fin (BB(n))".

Alex Zhang (Jun 28 2021 at 12:42):

Johan, thank you for letting me know.

Yakov Pechersky (Jun 28 2021 at 12:43):

First, you are working with different types. It's only a proposition that they're equal. And you haven't included that proposition in your lemma. You might also have a proposition that they're not equal! What should the system infer then about the types?

Alex Zhang (Jun 28 2021 at 12:44):

what if I include it in the lemma lemma silly (h: m=n): f=g := sorry

Johan Commelin (Jun 28 2021 at 12:45):

As a rule of thumb: equality of types is evil, bad-behaved, and should be avoided, unless it is definitional equality.

Johan Commelin (Jun 28 2021 at 12:45):

(Note: a rule of thumb is exactly that: a rule of thumb.)

Yakov Pechersky (Jun 28 2021 at 12:48):

Alex, equality of two terms of different types will always be an error. Do you mean, that for all inputs, the two functions are the same, modulo type modification?

Yakov Pechersky (Jun 28 2021 at 12:49):

That requires an axiom (functional extensionality) to prove, and using equiv.cast or other casts to state.

Alex Zhang (Jun 28 2021 at 12:49):

In the previous one fin (s * (p * m)) = fin (s * p * m) is decidedly equal if I am correct. The trouble is that I don't know how to make Lean recognise this when parsing.

Alex Zhang (Jun 28 2021 at 12:50):

The trouble is not how to prove it. It is that the statement reports an error.

Yakov Pechersky (Jun 28 2021 at 12:50):

One way to make it recognize it is by providing the explicit cast, which is fin.cast (your_proof)

Alex Zhang (Jun 28 2021 at 12:50):

Thanks, Yakov. Could you please give a #mwe?

Sebastien Gouezel (Jun 28 2021 at 12:53):

It might be enlightening for you to read https://xenaproject.wordpress.com/2020/07/03/equality-specifications-and-implementations/

Yakov Pechersky (Jun 28 2021 at 12:53):

What I'm saying is that lean+mathlib doesn't do arbitrary type equality "fixing" like you're trying to do unless you tell it to, using cast or its relatives. And the proof can of course be a tactic, or any strength you like. "cast" and its relatives are exactly the ways to get it to consider types as equal.

Yakov Pechersky (Jun 28 2021 at 12:57):

Here's an example from mathlib:

/-- Given a finset `s` of cardinality `k` in a linear order `α`, the map `order_iso_of_fin s h`
is the increasing bijection between `fin k` and `s` as an `order_iso`. Here, `h` is a proof that
the cardinality of `s` is `k`. We use this instead of an iso `fin s.card ≃o s` to avoid
casting issues in further uses of this function. -/
def order_iso_of_fin (s : finset α) {k : } (h : s.card = k) : fin k o (s : set α) :=
order_iso.trans (fin.cast ((length_sort ()).trans h).symm) $
  (s.sort_sorted_lt.nth_le_iso _).trans $ order_iso.set_congr _ _ $
    set.ext $ λ x, mem_sort _

Johan Commelin (Jun 28 2021 at 12:58):

@Alex Zhang Sorry, I messed up. My rule of thumb should have mentioned "definitional equality" not decidable equality.

Yakov Pechersky (Jun 28 2021 at 12:59):

With the caveat that definitional equality might hide a very expensive computation.

Alex Zhang (Jun 28 2021 at 13:12):

Suppose a = b is a propositional equality and h: a=b. Is there a way to "cheat" Lean such that Lean will recognise a=b as a definitional equality after?

Yakov Pechersky (Jun 28 2021 at 13:14):

What do you mean by cheat? That expressions like

examples {a b : Type*} (h : a = b) (x : a) (y : b) : x = y := sorry

are valid expressions?

Johan Commelin (Jun 28 2021 at 13:14):

Nope. I'm not an expert, but I think you are looking for an extensional type theory, or something like that. Those exist, but have their own set of problems...

Alex Zhang (Jun 28 2021 at 13:18):

Yakov Pechersky said:

What do you mean by cheat? That expressions like

examples {a b : Type*} (h : a = b) (x : a) (y : b) : x = y := sorry

are valid expressions?

Yes, just like this.

Horatiu Cheval (Jun 28 2021 at 13:19):

That shouldn't typecheck, right?

Yakov Pechersky (Jun 28 2021 at 13:19):

Correct, that is not a valid expression. But this is:

example {a b : Type*} (h : a = b) (x : a) (y : b) : x = (cast h.symm y) := sorry

Horatiu Cheval (Jun 28 2021 at 13:19):

Equality needs both arguments to be of the same type. You either need a cast with h or use heq instead

Yakov Pechersky (Jun 28 2021 at 13:21):

You could extend lean (probably easier in lean4) to try to unify types more aggressively. That might approximate what you want. For example (also, don't do this please!)

import tactic.basic

local notation x ` =F ` y := x = cast _ y

example {a b : Type*} (h : b = a) (x : a) (y : b) : x =F y := sorry

Yakov Pechersky (Jun 28 2021 at 13:23):

There are probably some scary type-theory contradictions or undecidability issues with approaches like this, having to do with \omega and \Omega. One could probably write a heuristic based unifier that could avoid such issues and have pretty errors...

Yakov Pechersky (Jun 28 2021 at 13:24):

OR just use cast and its relatives explicitly when you want to do type equality. This is nice because you can get other nice properties, for example, docs#fin.cast is order-preserving. There are many lemmas about docs#equiv.cast and how it operates when used in composition and simplifies.

Yakov Pechersky (Jun 28 2021 at 13:25):

But this topic is some of the friction of formalization. And the ways to formalize a particular statement require using the tools of formalization, rather than trying to cram set-theoretic like operations into the formalization.

Horatiu Cheval (Jun 28 2021 at 13:26):

What are you referring to by omega?

Yakov Pechersky (Jun 28 2021 at 13:26):

Kevin's, Anne's, and others' suggestions regarding generalizing your definitions to arbitrary types, breaking them up into digestable functions, etc -- these came from much experience working with the formalization and internalizing approaches that don't hit the "issue" you're faced with at the moment.

Yakov Pechersky (Jun 28 2021 at 13:29):

@Horatiu Cheval There was a recent paper shared in Zulip about forming expressions that do not terminate when trying to normalize them, that had to do with the Omega combinator. Let me see if I can find it.

Horatiu Cheval (Jun 28 2021 at 13:30):

Oh, I heard about that. No need to search for it

Horatiu Cheval (Jun 28 2021 at 13:31):

I just didn't know if it was that, or some other well established omega terminology I didn't know

Alex Zhang (Jun 28 2021 at 14:36):

Many thanks to all of you!!

Alex Zhang (Jun 28 2021 at 14:52):

Although I can now get around this problem by using cast as Yakov suggested or using coercions, Kevin's suggestion of defining the product in a more general setting seems pretty good, and I may change my defn later and change my current defn to like fin_Kronecker_prodcut.

Alex Zhang (Jun 28 2021 at 14:59):

@Johan Commelin Thank you for letting me know this. As I noticed that the more abstract tensor product has already been in the matlib, I am working with the Kronecker product in a direct and non-abstract way. It seems that that thread is doing a very abstract way as well. If you have any suggestion, please let me know!

Alex Zhang (Jun 30 2021 at 02:48):

@Kevin Buzzard Kevin, in your way of getting around this problem, should the statement of the associativity actually be'' A \ox B \ox C isomorphic to A \ox (B \ox C)''?

Johan Commelin (Jun 30 2021 at 04:43):

@Alex Zhang yes, isomorphisms are the way to go

Alex Zhang (Jun 30 2021 at 06:07):

I have the goal

  (i : J × M), (AB) (a, b) i * (CD) i (c, d) = ((λ (i : I) (k : K),  (i_1 : J), A i i_1 * C i_1 k)⊗λ (i : L) (k : N),  (i_1 : M), B i i_1 * D i_1 k) (a, b) (c, d)

after using simp [dot_product].
But I do want to have i in the goal written as the form ( , ). What can I do?

Johan Commelin (Jun 30 2021 at 06:08):

Wait, in your question above, are A, B, C matrices or rings?

Alex Zhang (Jun 30 2021 at 06:09):

Johan, they are matrices.

Johan Commelin (Jun 30 2021 at 06:12):

Hmm, then I'm confused. What do you mean by matrices being isomorphic?

Alex Zhang (Jun 30 2021 at 06:15):

Oh, sorry for the confusion. I am just asking a question unrelated to the previous one.

Alex Zhang (Jun 30 2021 at 06:17):

The problem is just that I would like to express the first i in the goal after using simp [dot_product] as a pair... but I don't know if there is a way to doing this.

Johan Commelin (Jun 30 2021 at 06:21):

Well, that means you need to show that (i:J×M),foobar\sum (i : J \times M), foobar is the same as (i1:J),(i2:M),foobar\sum (i_1 : J), \sum (i_2 : M), foobar.

Johan Commelin (Jun 30 2021 at 06:22):

There must be some lemmas about sum and product.

Johan Commelin (Jun 30 2021 at 06:23):

rw to the left with finset.univ_product_univ, and then use finset.sum_product

Alex Zhang (Jun 30 2021 at 06:27):

Thanks a lot! I think your answer is one step further from my question. As Lean know that i has type J prod M, my question is simply to represent i as a pair somehow. I am not sure whether Lean supports such a feature. Anyway, I think your solution does help!

Alex Zhang (Jun 30 2021 at 06:29):

If you know a way of just rewriting i without split the sum into two sums, please also let me know!

Alex Zhang (Jun 30 2021 at 06:32):

It seems that lean does not allow me to naively rewrite i to say \<i1, i2> as i is not in the context.

Johan Commelin (Jun 30 2021 at 06:37):

You could try to simp backwards with something like prod.eta or whatever it is called.


Last updated: Dec 20 2023 at 11:08 UTC