## 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: Aug 03 2023 at 10:10 UTC