Fin Nat, can I avoid having to pass a nat all the time?

Stream: new members

[An Qi Zhang]

Hello! When using a Fin (Nat) in a structure or inductive, I have to provide an n each time the structure's type is used. Is it possible to avoid having to specify an n each time?

import Mathlib

variable (n : Nat)

inductive FinNat
| fn : Fin n → FinNat
| none : FinNat

structure UseFinNat where
  haveFn : FinNat n -- Is there a way to say just use a specified `n`, so I don't need to provide an `n` each time?

-- Same as above, can I specify a specific `n`, and avoid having to pass an `n` each time?
def UseFinNatDef : FinNat n → FinNat n → FinNat n
| n₁, n₂ => sorry

[Aaron Liu]

Can you give an example?

[An Qi Zhang]

Just as in the code snippet above, if I define an inductive (for example, FinNat), every time I use FinNat in a def : FinNat n -> FinNat n, I have to specify FinNat n. But instead, if I could just say the inductive FinNat uses a specified n, and then I could avoid having to pass an n in a def like def : FinNat -> FinNat

So if I could write something like this:

import Mathlib

variable (n : Nat)

inductive FinNat
| fn : Fin n → FinNat
| none : FinNat

-- Instead of this:
def : FinNat n -> FinNat n
| n1 => sorry

-- something like this:
def : FinNat -> FinNat
| n1 => sorry

[Aaron Liu]

What do you mean by "specified n"?

[An Qi Zhang]

If I have an n, for example, one defined by variable (n : Nat), can I just use that n with the definition of inductive FinNat?

[Aaron Liu]

import Mathlib

variable (n : Nat)

inductive FinNat'
| fn : Fin n → FinNat'
| none : FinNat'

-- this will capture whatever in the context is called `n`
set_option quotPrecheck false in
notation "FinNat" => FinNat' n

example (n1 : FinNat) : FinNat :=
  sorry

[An Qi Zhang]

I see, so I assume with this approach, every new type def that uses FinNat (FinNat' n) will need a new notation added for it?

for example:

import Mathlib

variable (n : Nat)

inductive FinNat'
| fn : Fin n → FinNat'
| none : FinNat'

set_option quotPrecheck false in
notation "FinNat" => FinNat' n

inductive NewFinNat'
| fnfn : FinNat → NewFinNat'

set_option quotPrecheck false in
notation "NewFinNat" => NewFinNat' n

-- Every type that uses FinNat needs a new notation added.
abbrev FinSetFN' := Finset NewFinNat -- lean accepts this
abbrev FinSetFN'' := Finset NewFinNat' -- lean requires a Nat

[Aaron Liu]

I guess? I heard there was a better way in Lean 3, but it didn't make it into Lean 4.

[An Qi Zhang]

So, when I take the above as a file, and import it like so:

import FinNatMWE

variable (n : Nat)

abbrev UseFinNat := FinNat -- error: unknown constant 'n✝'
def UseFinNat' := FinNat -- error: unknown constant 'n✝'

Any other def that uses the FinNat defined by notationthrows an error, saying n✝` is an unknown constant. Is there a fix for this?

[Kevin Buzzard]

variable (n : Nat) does not mean "let n be a natural", it means "if the user ever mentions n later on in the file then write "for all naturals n," just in front of it". So your errors are expected.