Questions on Fin type and def/abbrev

Stream: lean4

[Paul Chisholm]

Looking at the Fin structure defined in the prelude (Lean 4 version) a couple of questions arise:

• I understand most of the Fin definition, but what is the purpose of the last two lines given Fin has already been shown to be an instance of LE and LT:

instance Fin.decLt {n} (a b : Fin n) : Decidable (LT.lt a b)  := Nat.decLt ..
instance Fin.decLe {n} (a b : Fin n) : Decidable (LE.le a b) := Nat.decLe ..

• What causes the following errors?

def To10 : Type := Fin 10

def zero : To10 := ⟨0, by decide⟩
def one : To10 := ⟨1, by decide⟩

#check (⟨0, by decide⟩:To10) = (⟨1, by decide⟩:To10)
#check (⟨0, by decide⟩:To10) ≤ (⟨1, by decide⟩:To10)
#check (⟨0, by decide⟩:To10) < (⟨1, by decide⟩:To10)
#check zero = one
--#check zero ≤ one  -- error: failed to synthesize instance LE To10
--#check zero < one  -- error: failed to synthesize instance LT To10

I just remembered abbrev being mentioned elsewhere so I tried changing the definition of To10 to abbrev To10 : Type := Fin 10 and the errors disappear. Hence something to do with the difference between def and abbrev, but what, any why does it only affect LT and LE, not equality?

• More generally, what are the guidelines for using def vs abbrev?

[Yaël Dillies]

Fin.decLt doesn't declare that Fin has a <, but that this < is decidable, meaning that ∀ a b, a < b ∨ ¬ a < b. Similarly, Fin.decLe states that ∀ a b, a ≤ b ∨ ¬ a ≤ b.

[Yaël Dillies]

Those are derived from their decidability on ℕ, as you can see from the (very brief) proofs.

[Paul Chisholm]

Ok, so without those two lines you have that Fin is an instance of LT and LE but you need decidability to make headway in proofs, or for computation.

[Yaël Dillies]

Yep

[Paul Chisholm]

Thanks

[Yaël Dillies]

Your error is a reducibility issue. eq is defined for all types, so that's no surprise if you don't get any error. < and ≤ however have to be declared (they come from "syntax" typeclasses). Here, you defined To10 to be a type synonym of Fin 10. By design, hardly anything leaks through type synonyms, because this system allows us to overcharge a type with different instances of the same structure.

[Yaël Dillies]

Eg order_dual is equipped with the reverse order. with_top α, with_bot α, alexandroff α are all type synonyms of option α, used to add a top element, a bottom element, a point at infinity, respectively.

[Notification Bot]

This topic was moved here from #general > Questions on Fin type and def/abbrev by Eric Wieser

[Paul Chisholm]

If I really wanted a type to range over 0..9 should I use def and put on the extra effort, or is abbrev a better approach, or indeed something else.

[Yakov Pechersky]

You should use "Fin 10". If you don't want to write "Fin 10", then you can use the "notation" to give it some shorthand

[Eric Wieser]

abbrev should be just fine here I think?

[Kevin Buzzard]

Every new definition comes with a cost, because, unlike a human, Lean does not know when it's best to keep the definition wrapped up in its box and to proceed using the API for the definition (which someone has to write -- every definition needs an API), and when to open the box and use the underlying "definiens". If you want something which is the same as Fin 10 then this is the argument for using Fin 10 rather than letting it be X or whatever -- Fin already has an API so you don't need to write it.

[Paul Chisholm]

Fin 10 would be ok here, but I think there would be situations where I wouldn't want to repeat the basic form. If I say wanted to model dates and times, then rather than have Fin 24 everywhere, I would want to use a type named Hour, and Minute rather than Fin 60, etc.

Sounds like abbev would be the way to go. As you can probably guess from the example, my interest is in computing rather than maths.

[Yakov Pechersky]

I think what's crucial here is the difference between facilitating _defining_ something or proving something about existing definitions.

[Yakov Pechersky]

The < and <= are defined for all Fin n, so you don't have to worry about specializing those instances to Hour or Minute. Hopefully, the API you are using does not care about 24 or 60.

[Yakov Pechersky]

I can understand that perhaps for Hour you might want to have two representations, 00-23 and 00-12 {am,pm}, while for Minute it'd be solely 00-59.

[Yakov Pechersky]

And yes, there you would then need to have at least separate specialization.

[Paul Chisholm]

So by using abbrev everything is inherited from Fin and all the properties hold.

Yes, 24 and 60 are excluded, and all times are modelled in UTC, so hour is always 0..23 (am/pm is just an output presentation).

[Scott Morrison]

It's also quite easy to make a type synonym and copy across the subset of typeclass instances you actually want. Search for @[derive ] in mathlib3 for many examples.