constraints on pattern matching

Stream: new members

[Shi Zhengyu]

Hi all,

Is there a way to apply additional propositional constraints on pattern matching? e.g.

def Id (n: ℕ): finMat n n
| ⟨x, _⟩ ⟨x2, _⟩ := if (x == x2) then 1 else 0

How should I replace the if ... then .. else part with actual Lean code?

Thanks!

[Kevin Buzzard]

I think Lean has if...then...else?

[Yaël Dillies]

Maybe you'll consider docs#ite or docs#dite actual Lean code?

[Shi Zhengyu]

Kevin Buzzard said:

I think Lean has if...then...else?

Lol thanks :joy: that was unexpected

[Shi Zhengyu]

By the way, the below definition fail with polyId is noncomputable, may I ask what exactly does noncomputable mean? I vaguely think it's connected with axiom of choice ...

import data.fin.basic
import data.complex.basic
import data.matrix.basic
import data.matrix.notation
import data.polynomial.basic
def finPolyMat (u: ℕ) (v: ℕ) := matrix (fin u) (fin v) (polynomial ℂ)

def polyId (n: ℕ): finPolyMat n n := λ u v: fin n, if u = v then 1 else 0
 ```

[Yaël Dillies]

It means Lean can't generate bytecode (aka computation instructions) for it. So you can't run the code but you can still prove stuff about it.

[Yaël Dillies]

Given that Lean can generate bytecode for all axioms except the axiom of choice (and sorry but you won't use it in final code), noncomputability is indeed linked to using the axiom of choice.