# Zulip Chat Archive

## Stream: general

### Topic: equation compiler match on variable

#### Kevin Buzzard (Jun 02 2022 at 17:36):

I don't know how to do this:

```
def f : ℕ → ℕ := λ x, x + 37
def foo (n : ℕ) : ℕ → bool
| (f n) := tt
| _ := ff
```

The equation compiler complains :-( I can use `if then else`

in my situation but I was hoping for better definitional equalities.

#### Kevin Buzzard (Jun 02 2022 at 17:37):

Note that

```
def foo (n : ℕ) : ℕ → bool
| n := tt
| _ := ff
```

doesn't work because the equation compiler assumes `n`

is a fresh variable, and thus always matches the first branch.

#### Alex J. Best (Jun 02 2022 at 17:37):

```
@[pattern]
def f : ℕ → ℕ := λ x, x + 37
def foo (n : ℕ) : ℕ → bool
| (f n) := tt
| _ := ff
```

hope it works in a non-minimal example :wink:

#### Adam Topaz (Jun 02 2022 at 17:38):

Is this even possible?

#### Adam Topaz (Jun 02 2022 at 17:38):

(And I know why you need it Kevin, and I really do wish it actually is possible)

#### Kevin Buzzard (Jun 02 2022 at 17:40):

In my actual example, `f n`

is just `n - 1`

.

#### Alex J. Best (Jun 02 2022 at 17:42):

Kevin Buzzard said:

In my actual example,

`f n`

is just`n - 1`

.

:frown: so looks like the solution doesn't work, do you need the truncating property of `-`

exactly in this way?

#### Kevin Buzzard (Jun 02 2022 at 17:43):

Scott uses `if then else`

in the definition of `homological_complex.single`

in `algebra/homology/single.lean`

:

```
{ obj := λ A,
{ X := λ i, if i = j then A else 0,
d := λ i j, 0, },
```

and then later on defines `single₀`

"with better definitional equalities" in the special case j = 0, when he can use the equation compiler.

#### Adam Topaz (Jun 02 2022 at 17:44):

Yeah the benefit of `single_0`

is that `(single_0.obj B).X 0`

is defeq to `B`

#### Adam Topaz (Jun 02 2022 at 17:45):

Maybe we can try something approximately like this?

```
def foo : ℕ → ℕ → ℤ
| 0 := λ k, match k with
| 0 := 1
| (i+1) := 0
end
| (n+1) := λ k, match k with
| 0 := 0
| (i+1) := foo n i
end
```

#### Adam Topaz (Jun 02 2022 at 17:49):

With that we get

```
example : ∀ (n : ℕ), foo n n = 1 :=
begin
intros n,
induction n,
refl,
assumption
end
```

#### Adam Topaz (Jun 02 2022 at 17:56):

```
import algebra.homology.homological_complex
import category_theory.abelian.basic
open category_theory
variables {A : Type*} [category A] [abelian A]
open_locale zero_object
noncomputable
def single_X (B : A) : ℕ → ℕ → A
| 0 0 := B
| 0 (k+1) := 0
| (n+1) 0 := 0
| (n+1) (k+1) := single_X n k
noncomputable
def single (B : A) (n : ℕ) : chain_complex A ℕ :=
{ X := single_X B n,
d := λ i j, 0,
shape' := sorry,
d_comp_d' := sorry }
```

#### Adam Topaz (Jun 02 2022 at 18:11):

In the following code, why is the `dsimp`

needed in the last branch of `of_hom_d`

?

```
import algebra.homology.homological_complex
import category_theory.abelian.basic
open category_theory
variables {A : Type*} [category A] [abelian A]
open_locale zero_object
noncomputable
def of_hom_X {X Y : A} (f : X ⟶ Y) : ℕ → ℕ → A
| 0 0 := X
| 0 1 := Y
| 0 (k+2) := 0
| (n+1) 0 := 0
| (n+1) (k+1) := of_hom_X n k
noncomputable
def of_hom_d {X Y : A} (f : X ⟶ Y) : Π (n i j : ℕ), of_hom_X f n i ⟶ of_hom_X f n j
| 0 0 0 := 0
| 0 0 1 := f
| 0 0 (k+2) := 0
| 0 (i+1) 0 := 0
| 0 (i+1) (j+1) := 0
| (n+1) 0 _ := 0
| (n+1) (i+1) 0 := 0
| (n+1) (i+1) (j+1) := by { dsimp [of_hom_X], exact of_hom_d n i j }
noncomputable
def of_hom {X Y : A} (f : X ⟶ Y) (n : ℕ) : chain_complex A ℕ :=
{ X := of_hom_X f n,
d := of_hom_d f n,
shape' := sorry,
d_comp_d' := sorry }
```

#### Adam Topaz (Jun 02 2022 at 18:13):

Is this just a quirk of the equation compiler?

#### Adam Topaz (Jun 02 2022 at 19:04):

(For those in the know, those `d`

's define a cochain complex, not a chain complex as indicated, but the issue is of course unrelated)

#### Kevin Buzzard (Jun 02 2022 at 19:55):

Even if you do it like this, `single_X B n n = B`

won't be `rfl`

, the proof term will have a `nat.rec`

in it.

#### Adam Topaz (Jun 02 2022 at 19:57):

Yeah, you can make it `rfl`

using the equation compiler.

#### Adam Topaz (Jun 02 2022 at 19:57):

Well, no, you're right, not `rfl`

because you need induction.

#### Kevin Buzzard (Jun 02 2022 at 19:57):

For an explicit value of n you can, but not in general right?

#### Adam Topaz (Jun 02 2022 at 19:58):

Yeah you're right.

#### Kevin Buzzard (Jun 02 2022 at 19:58):

I am now using the `eq_to_iso`

trick

#### Kevin Buzzard (Jun 02 2022 at 19:59):

Unless you know how to prove that `cast (f >> g) = cast f >> cast g`

and `cast 0 = 0`

...

#### Adam Topaz (Jun 02 2022 at 20:00):

No, I think that would be worse!

#### Adam Topaz (Jun 02 2022 at 20:01):

At least `eq_to_iso`

is an iso which you can move around

#### Eric Wieser (Jun 02 2022 at 22:23):

This feels like a bug in the equation compiler to me:

```
def foo (n : ℕ) : ℕ → bool
| .(n) := tt
```

Lean is happy to accept this, and is clearly not binding a new variable with the `.(n)`

as `.(bar)`

is forbidden; but it doesn't do the right thing.

#### Eric Wieser (Jun 02 2022 at 22:26):

Maybe I don't understand `.`

notation:

```
def is_37 : ℕ → bool
| .(37) := tt
#eval is_37 1 -- tt
```

#### Kevin Buzzard (Jun 02 2022 at 22:33):

Yeah, Alex' code above doesn't work either, it matches on any `n`

not the one which you want to match on.

Last updated: Dec 20 2023 at 11:08 UTC