Canonical inductive types with 0,1,2,3,4 terms

Stream: general

[Johan Commelin]

We have empty and unit, which seem quite unquestionable. For an inductive type with two elements, we have bool, although it might be considered abuse to treat it as an "arbitrary" type with two elements. How about types with 3 or 4 elements?
Should we have inductive three | a | b | c and inductive four | a | b | c | d ?

[Kenny Lau]

why not an inductive type with n elements?

[Kenny Lau]

(fin2, egō tē videō)

[Kenny Lau]

/-- An alternate definition of `fin n` defined as an inductive type
  instead of a subtype of `nat`. This is useful for its induction
  principle and different definitional equalities. -/
inductive fin2 : ℕ → Type
| fz {n} : fin2 (succ n)
| fs {n} : fin2 n → fin2 (succ n)

[Kenny Lau]

https://github.com/leanprover-community/mathlib/blob/2ae7ad811f7bacb636698705064c82551faddbf8/src/data/fin2.lean

[Kenny Lau]

or, even better, just use the recursor for fin

[Kenny Lau]

who cares if it's inductive by definition

[Kevin Buzzard]

fin and fin2 both satisfy the spec for fin so speaking as a mathematician I would say I'd be happy with either of them, but to make my life easy can we just fix upon one?

[Kevin Buzzard]

This is another notation question. Will we be able to tell the equation compiler in Lean 4 "and let me use those cool bars, here's your recursor"?

[Kevin Buzzard]

I think the canonical type with no terms should be 37

[Kevin Buzzard]

there is a problem here right? All those pesky computer scientists think that the canonical type with 0 terms is pempty, but with our new system it's also fin3 0 right?

[Bryan Gin-ge Chen]

I thought only mathematicians knew what "canonical" meant...

[Johan Commelin]

Kenny Lau said:

or, even better, just use the recursor for fin

As far as I know that means you will get a really ugly match expression, if you want the map fin 4 → polynomial nat
that sends
0 to 0,
1 to X^2 + 3,
2 to X + 5, and
3 to X^37 + 57 * X + 1

[Johan Commelin]

Maybe I can abuse that nat is inductive by definition...

[Kenny Lau]

then make it more beautiful

[Johan Commelin]

Sure, but it requires writing dedicated code for fin 2, fin 3, fin 4, right? There's not a generic thing I can do, I guess.

[Reid Barton]

data.matrix.notation?

[Kenny Lau]

import data.fin

@[elab_as_eliminator]
def const_n_ary {C : Sort*} (x : C) (n : ℕ) : (nat.rec_on n C (λ n ih, C → ih) : Sort*) :=
nat.rec_on n x $ λ n ih _, ih

@[elab_as_eliminator]
def fin.magic (n : ℕ) {C : Sort*} : fin n → (nat.rec_on n C (λ n ih, C → ih) : Sort*) :=
nat.rec_on n fin.elim0 $ λ n ih i x, fin.cases (const_n_ary x n) ih i

#eval (fin.magic 4 0 (-1729) (-314) (2718) (37) : ℤ) -- -1729
#eval (fin.magic 4 1 (-1729) (-314) (2718) (37) : ℤ) -- -314
#eval (fin.magic 4 2 (-1729) (-314) (2718) (37) : ℤ) -- 2718
#eval (fin.magic 4 3 (-1729) (-314) (2718) (37) : ℤ) -- 37

[Johan Commelin]

Ooh, that's a nice idea!

[Kenny Lau]

oh did I just wait 30 minutes rewriting what is already in mathlib

[Eric Wieser]

I think my question relates to this thread, since it's about matching against fin N...

Aside from the fact this construction is very contrived, is there any way I can golf out the repeated apply_instance?

def blade : fin 4 → Type
| ⟨0, _⟩ := ℝ  -- scalar
| ⟨1, _⟩ := ℝ × ℝ × ℝ
| ⟨2, _⟩ := ℝ × ℝ × ℝ
| ⟨3, _⟩ := ℝ  -- psuedo-scalar
| ⟨n + 4, _⟩ := by {exfalso, linarith}

instance : Π i, add_comm_group (blade i)
| ⟨0, _⟩ := by {unfold blade, apply_instance}
| ⟨1, _⟩ := by {unfold blade, apply_instance}
| ⟨2, _⟩ := by {unfold blade, apply_instance}
| ⟨3, _⟩ := by {unfold blade, apply_instance}
| ⟨n + 4, h⟩ := by {exfalso, linarith}

[Kevin Buzzard]

What happens if you try to derive add_comm_group in the definition of blade?

[Eric Wieser]

How do you mean?

[Alex J. Best]

I don't think it works in this case but you can do

@[derive add_comm_group]
def myint := int

to automate later doing

instance : add_comm_group myint := by unfold myint; apply_instance

[Utensil Song]

Kevin Buzzard said:

What happens if you try to derive add_comm_group in the definition of blade?

To literally answer the question, what happens is:

tactic.mk_instance failed to generate instance for
  add_comm_group
    (a.cases_on
       (λ (a_val : ℕ) (a_is_lt : a_val < 4),
          a_val.cases_on (λ (a_is_lt : 0 < 4), id_rhs Type ℝ)
            (λ (a_val : ℕ) (a_is_lt : a_val.succ < 4),
               a_val.cases_on (λ (a_is_lt : 1 < 4), id_rhs Type ℝ³)
                 (λ (a_val : ℕ) (a_is_lt : a_val.succ.succ < 4),
                    a_val.cases_on (λ (a_is_lt : 2 < 4), id_rhs Type ℝ³)
                      (λ (a_val : ℕ) (a_is_lt : a_val.succ.succ.succ < 4),
                         a_val.cases_on (λ (a_is_lt : 3 < 4), id_rhs Type ℝ)
                           (λ (a_val : ℕ) (a_is_lt : a_val.succ.succ.succ.succ < 4), id_rhs Type (false.rec Type _))
                           a_is_lt)
                      a_is_lt)
                 a_is_lt)
            a_is_lt))

[Utensil Song]

Sorry I used

notation `ℝ³` := ℝ × ℝ × ℝ`

hence the difference of error message