circulant matrix

Stream: Is there code for X?

[Alex Zhang]

Is any version of the notion "circulant matrix" defined in mathlib?

[Johan Commelin]

I've never heard of it. I don't think it's in mathlib.

[Eric Wieser]

I assume the definition you're looking for is

def circulant {α : Type*} {n : ℕ} (c : fin n → α) : matrix (fin n) (fin n) α
| i j := c (i - j)

[Eric Wieser]

Or ((∘) c) ∘ has_sub.sub if you're feeling masochistic / point-free

[Yaël Dillies]

Is "point-free" a euphemism of "pointless"?

[Johan Commelin]

@Eric Wieser what is the benefit of using the equation compiler over a lambda expression?

[Eric Rodriguez]

Yaël Dillies said:

Is "point-free" a euphemism of "pointless"?

c.f. with "pointless topology", "Pointless Celebrities" and "abstract nonsense" ;b I think some FP purists really like not using λs when unnecessary

[Mario Carneiro]

@Eric Wieser Doesn't that definition hit against the issue with fin n saturating subtraction?

[Yakov Pechersky]

We use pointfree implicitly when we consider addition of terms of "C_infty", for example. With the right abstractions, it's easier to prove things about things without having to use extensionality.

[Eric Wieser]

Mario Carneiro said:

Eric Wieser Doesn't that definition hit against the issue with fin n saturating subtraction?

The issue with fin n saturating subtraction is that everyone thinks that fin n has saturating subtraction. It does not : src#fin.sub.

[Mario Carneiro]

Ah, that's probably just me and other old hands then

[Eric Wieser]

Johan Commelin said:

Eric Wieser what is the benefit of using the equation compiler over a lambda expression?

It seems to be the pattern in the matrix library. It means that simp [circulant] refuses to make progress on a goal of X = circulant c, and will only unfold circulant if the goal state is X i j = circulant c i j. I don't know if that's a good thing, but it's certainly a measurable difference.

[Johan Commelin]

I don't know if it's a good thing either, but it is certainly a very reasonable thing.
Thanks for explaining! I'll probably make use of this in the future.

[Mario Carneiro]

You normally get the same behavior by moving the arguments left of the colon, but here that would be undesirable because it would prevent you from using the matrix abbreviation

[Alex Zhang]

How can I prolong the time for #eval

def test2 := circulant (![ 1,  1, -1, -1, -1,  1, -1, -1, -1,  1, -1,  1,  1, -1,  1, -1, -1,  -1, 1, -1] : _ → ℚ)
#eval test2

fin 19 may be fine, but fin 20 will time out for a nontrivial example.

[Alex J. Best]

You can try changing the setting lean.timeLimit in the vscode settings (once you open settings you should be able to search for this).
Why would you want to eval that though?

[Alex Zhang]

I am just exploring things here.

[Kevin Buzzard]

You can't use #eval in proofs, and if you just want to do computations you might be better off using a computer algebra package.

[Alex Zhang]

Is norm_num kind of equivalent to #eval?

[Kevin Buzzard]

no, not at all! norm_num is checked by the kernel!

[Kevin Buzzard]

You can certainly use norm_num in proofs.

[Mario Carneiro]

you could say that norm_num aspires to be #eval

[Mario Carneiro]

but with proofs

[Kevin Buzzard]

Mario Carneiro said:

you could say that norm_num aspires to be #eval

I would say vice versa

[Yakov Pechersky]

What do you hope to get when you evaluate a matrix? A 19x19 table representing the coefficients given the standard basis?

[Mario Carneiro]

seems reasonable

[Mario Carneiro]

i.e. ![![1, 2], ![3, 4]]

[Yakov Pechersky]

Probably not the best representation for sparse matrices though.

[Yakov Pechersky]

But yeah makes sense for a matrix of arbitrary small size

[Alex Zhang]

I haven't gone into a proof. I am just exploring things here.
Yakov Pechersky said:

What do you hope to get when you evaluate a matrix? A 19x19 table representing the coefficients given the standard basis?

[Alex Zhang]

Kevin Buzzard said:

no, not at all! norm_num is checked by the kernel!

Could anyone say a bit more about the difference between norm_num and #eval when applied to an expression?

[Mario Carneiro]

#eval compiles your lean expression into VM bytecode and then runs it in the interpreter. As long as the interpreter is correct this should work, but there are no associated proofs, it's just running code

[Yakov Pechersky]

#eval takes a term for a particular type, and attempts to evaluate the term. If it is normal form already, it will display it using its representation, given by the has_repr instance. If it is not in normal form, for example, a function applied to a term, it will try to evaluate the applied function, then do the thing described above to the resulting term.

[Mario Carneiro]

norm_num pattern matches on the expression to produce a proof that the expression is equal to the normalized value, using lemmas for each step. As a result everything is proven correct, and it uses #eval under the hood as an oracle in places (for example, when proving that something is prime or not, it first checks whether the number is actually prime or composite in order to determine how the proof is going to go)

[Mario Carneiro]

In principle, anything that can be #eval'd can also be evaluated in a proof producing way, but the key tactic for this is missing (it is called the cbv tactic in coq). Maybe we can finally have this in lean 4

[Alex Zhang]

Mario Carneiro said:

In principle, anything that can be #eval'd can also be evaluated in a proof producing way, but the key tactic for this is missing (it is called the cbv tactic in coq). Maybe we can finally have this in lean 4

Why isn't norm_num the key tactic for this purpose? @Mario Carneiro

[Mario Carneiro]

It doesn't handle general CIC reduction, it only knows about integer functions for the most part, and every function has to have a manual implementation, it does not look at the definition at all

[Mario Carneiro]

it calls simp, which can sometimes make it over little hurdles, but it's not enough to evaluate arbitrary functions on lists and such

[Mario Carneiro]

The fact that functions are all reimplemented is more of a strength than a weakness, because following lean's actual implementation of nat.add et al would lead to exponential time performance

[Mario Carneiro]

but it's not what #eval would do