HAdd (Fin n) Nat (Fin n)?

Stream: lean4

[James Gallicchio]

is there any discussion of an hadd instance between fin and nat? just doing the usual Z/n behavior.

it is one of those things that makes sense on a type for Z/n but not a type for [n], so I'm not sure if it is there.

[Mario Carneiro]

I think it would be preferable to just use coercions here, same as how we don't have a HAdd Int Nat Int instance

[James Gallicchio]

But having a coercion Nat -> Fin n is admittedly deeply confusing (you could get inadvertent % where you don't want them).

[James Gallicchio]

I thought there was a discussion at one point about separating the type with wrapping ring arithmetic from the type with non-wrapping arithmetic where overflow must be accounted for.

[Mario Carneiro]

keep in mind that 4 : Fin 2 already typechecks

[James Gallicchio]

which always peeved me, since 4 : Fin n with a hypothesis in context like n = 2 or n > 0 or anything along those lines does not typecheck :joy:

[Mario Carneiro]

how is the hypothesis supposed to be used?

[Mario Carneiro]

do you want it to by assumption or something?

[Mario Carneiro]

4 : Fin (n+1) does typecheck

[Mario Carneiro]

and mathlib also has a version where 4 : Fin n typechecks given Fact (0 < n)

[James Gallicchio]

I think for a type like Mod n the current mathlib behavior for Fin makes sense, trying to do whatever it can do show n > 0 so that the ring operations just work (in fact, it might even make sense for Mod n to require n > 0 for simplicity's sake, since Z/0 is degenerate...)

[Mario Carneiro]

you mean docs4#ZMod ?

[James Gallicchio]

yes, that is exactly what i'm looking for :)

[James Gallicchio]

now the question is why the wrapping Fin.add exists!

[Mario Carneiro]

what do you expect it to be?

[Mario Carneiro]

whatever you are thinking, it is much worse to work with

[Mario Carneiro]

one pragmatic reason for Fin.add is that it is used to define UInt32.add and UInt64.add

[James Gallicchio]

yeah. but you could see ZMod being moved to core and used as the backing for UIntX

[James Gallicchio]

Idk. I don't really ever want to add Fins (?). Speaking as someone who only interacts with Fin in Array contexts.

[Mario Carneiro]

then maybe don't

[Mario Carneiro]

ZMod is a conditional type, it is defined as Fin n for n > 0 and Int for n = 0

[Mario Carneiro]

array indices don't even really want Fin n, they would be better off with { i : UInt64 // i < n }

[Yaël Dillies]

Your original question sounds more like vadd. I still believe we should never use HAdd because the only heterogeneous cases that matter are covered by vadd.

[Eric Wieser]

I'd make the stronger claim that it's not just that vadd and smul are the only cases that matter, butHAdd and HMul are massive footguns as there is no sane composition strategy to avoid non-propeq diamonds

[Eric Wieser]

Arguably we could add a nvadd field to AddMonoidWithOne which would give the behavior that @Yaël Dillies suggests

[Eric Rodriguez]

i think HAdd is more useful for programmers

[Notification Bot]

Marc Huisinga has marked this topic as resolved.

[Notification Bot]

Marc Huisinga has marked this topic as unresolved.

[Mac Malone]

Mario Carneiro said:

array indices don't even really want Fin n, they would be better off with { i : UInt64 // i < n }

Or, more precisely, USize.

[Eric Wieser]

Eric Wieser said:

I'd make the stronger claim that [...]HAdd and HMul are massive footguns as there is no sane composition strategy to avoid non-propeq diamonds

Just to give a concrete example of this:

import Mathlib.Logic.Nontrivial.Defs
import Mathlib.Data.Pi.Algebra

variable {ι α β γ : Type _}

-- HMul generalizes to families on the right
instance hmulRight [inst : HMul α β γ] : HMul α (ι → β) (ι → γ) where
  hMul a b := fun i => a * b i

-- HMul generalizes to families on the left
instance hmulLeft [inst : HMul α β γ] : HMul (ι → α) β (ι → γ) where
  hMul a b := fun i => a i * b

-- both of these are valid instance searches, lets give them short names
variable (ι)
abbrev lr : HMul (ι → Nat) (ι → Nat) (ι → ι → Nat) := hmulLeft (inst := hmulRight)
abbrev rl : HMul (ι → Nat) (ι → Nat) (ι → ι → Nat) := hmulRight (inst := hmulLeft)

-- holy diamonds batman
example (a b : ι → Nat) (i j : ι) : let _ := lr ι; (a * b) i j = a i * b j := rfl
example (a b : ι → Nat) (i j : ι) : let _ := rl ι; (a * b) i j = a j * b i := rfl

-- propositional diamonds!
example [Nontrivial ι] : lr ι ≠ rl ι := by
  classical
  obtain ⟨i, j, hij⟩ := exists_pair_ne ι
  dsimp [lr, rl, hmulLeft, hmulRight]
  intro h
  injection h with h
  replace h := congr_fun₂ (congr_fun₂ h (Pi.mulSingle i 2) (Pi.mulSingle i 3)) i j
  rw [Pi.mulSingle_eq_same, Pi.mulSingle_eq_same, Pi.mulSingle_eq_of_ne' hij, Pi.mulSingle_eq_of_ne' hij] at h
  cases h