Zulip Chat Archive

Stream: new members

Topic: constraints on pattern matching

Shi Zhengyu (Jan 05 2022 at 08:09):

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?


Kevin Buzzard (Jan 05 2022 at 08:15):

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

Yaël Dillies (Jan 05 2022 at 08:16):

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

Shi Zhengyu (Jan 05 2022 at 08:18):

Kevin Buzzard said:

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

Lol thanks :joy: that was unexpected

Shi Zhengyu (Jan 05 2022 at 08:22):

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 (Jan 05 2022 at 08:27):

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 (Jan 05 2022 at 08:28):

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.

Last updated: Dec 20 2023 at 11:08 UTC