equation compiler match on variable

Stream: general

[Kevin Buzzard]

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]

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]

@[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]

Is this even possible?

[Adam Topaz]

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

[Kevin Buzzard]

In my actual example, f n is just n - 1.

[Alex J. Best]

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]

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]

Yeah the benefit of single_0 is that (single_0.obj B).X 0 is defeq to B

[Adam Topaz]

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]

With that we get

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

[Adam Topaz]

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]

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]

Is this just a quirk of the equation compiler?

[Adam Topaz]

(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]

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]

Yeah, you can make it rfl using the equation compiler.

[Adam Topaz]

Well, no, you're right, not rfl because you need induction.

[Kevin Buzzard]

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

[Adam Topaz]

Yeah you're right.

[Kevin Buzzard]

I am now using the eq_to_iso trick

[Kevin Buzzard]

Unless you know how to prove that cast (f >> g) = cast f >> cast g and cast 0 = 0...

[Adam Topaz]

No, I think that would be worse!

[Adam Topaz]

At least eq_to_iso is an iso which you can move around

[Eric Wieser]

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]

Maybe I don't understand . notation:

def is_37 : ℕ → bool
| .(37) := tt

#eval is_37 1  -- tt

[Kevin Buzzard]

Yeah, Alex' code above doesn't work either, it matches on any n not the one which you want to match on.