Theorem Formalization

Stream: new members

[Alex Zhang]

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]

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

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

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Alex Zhang]

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]

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

begin
  classical,
  apply finset.induction_on s,
end

[Johan Commelin]

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]

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]

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]

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]

What are you expecting the answer to be?

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

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

[Alex Zhang]

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]

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

[Alex Zhang]

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]

fintype.card

[Johan Commelin]

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

[Eric Wieser]

docs#fintype.card

[Eric Wieser]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Alex Zhang]

any analogical function for infinite sets or countable sets?

[Kevin Buzzard]

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]

That's cardinal.mk

[Eric Wieser]

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]

I guess we have different mental models of or.

[Anne Baanen]

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]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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]

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 (A⊗B)
term
  A⊗B
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]

Can you please post a #mwe ?

[Kevin Buzzard]

But I know what the problem will be :-)

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Alex Zhang]

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

[Kevin Buzzard]

That will in some sense make the problem worse

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Anne Baanen]

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]

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

[Alex Zhang]

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

[Yakov Pechersky]

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]

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]

(deleted)

[Yakov Pechersky]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Alex Zhang]

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]

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]

Johan, thank you for letting me know.

[Yakov Pechersky]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Yakov Pechersky]

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]

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

[Alex Zhang]

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]

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

[Yakov Pechersky]

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

[Alex Zhang]

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

[Sebastien Gouezel]

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

[Yakov Pechersky]

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]

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]

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

[Yakov Pechersky]

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

[Alex Zhang]

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]

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]

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]

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]

That shouldn't typecheck, right?

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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]

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]

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]

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]

What are you referring to by omega?

[Yakov Pechersky]

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]

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

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

[Horatiu Cheval]

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

[Alex Zhang]

Many thanks to all of you!!

[Alex Zhang]

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]

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

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

@Alex Zhang yes, isomorphisms are the way to go

[Alex Zhang]

I have the goal

⊢ ∑ (i : J × M), (A⊗B) (a, b) i * (C⊗D) 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]

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

[Alex Zhang]

Johan, they are matrices.

[Johan Commelin]

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

[Alex Zhang]

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

[Alex Zhang]

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]

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

[Johan Commelin]

There must be some lemmas about sum and product.

[Johan Commelin]

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

[Alex Zhang]

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]

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

[Alex Zhang]

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]

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