HAdd instance use value of operand in outParam type

Stream: new members

[aron]

Hi :wave: I have a BoundedNat type that's effectively a range

def BoundedNat (min max : Nat) : Type :=
  {n : Nat // min ≤ n ∧ n ≤ max}

def BoundedNat.mk {min max : Nat} (n : Nat) (h : min ≤ n ∧ n ≤ max) : BoundedNat min max :=
  ⟨n, h⟩

def BoundedNat.val {min max : Nat} (n : BoundedNat min max) : Nat :=
  n.1

def BoundedNat.addNat {min max : Nat} (m : Nat) (n : BoundedNat min max) : BoundedNat (min + m) (max + m) :=
  ⟨ n.val + m, by
    simp
    exact n.property
  ⟩

I want to be able to use addNat with the + operator, so I'm trying to create a HAdd instance for adding BoundedNats and Nats together. I can't work out how to use the value of the Nat in the outParam type though. Is this possible?

Here's a few things I tried but none of them work

instance {n : Nat} : HAdd n (BoundedNat min1 max1) (BoundedNat (min1 + n) (max1 + n)) where
  hAdd := fun n bn => bn.addNat n

instance : HAdd (n : Nat) (BoundedNat min1 max1) (BoundedNat (min1 + n) (max1 + n)) where
  hAdd := fun n bn => bn.addNat n

instance : HAdd Nat (BoundedNat min1 max1) (BoundedNat min1 max1) where
  hAdd := fun n bn => bn.addNat n

instance : HAdd Nat (BoundedNat min1 max1) _ where
  hAdd := fun n bn => bn.addNat n

[Ruben Van de Velde]

You mean the type of the outparam should depend on the value you're adding? I don't think that's possible

[aron]

Yeah exactly. That's what BoundedNat.addNat does so I'm hoping it's possible with the + operator too

[aron]

Actually I just realised I can't create an Add instance for this type either :thinking:

def BoundedNat.add (n1 : BoundedNat min1 max1) (n2 : BoundedNat min2 max2) : BoundedNat (min1 + min2) (max1 + max2) :=
  BoundedNat.mk (n1.val + n2.val) (by ...)


instance : Add (BoundedNat n x) where
  add := fun a b => BoundedNat.add a b
-- type mismatch
--   a.add b
-- has type
--   BoundedNat (n + n) (x + x) : Type
-- but is expected to have type
--   BoundedNat n x : Type

instance : Add (BoundedNat (.succ k) 0) where
  add := fun a b => BoundedNat.add a b
-- type mismatch
--   a.add b
-- has type
--   BoundedNat (k.succ + k.succ) (0 + 0) : Type
-- but is expected to have type
--   BoundedNat k.succ 0 : Type

-- Only in the single case where both addends and the result have the same type does this work
instance : Add (BoundedNat 0 0) where
  add := fun a b => BoundedNat.add a b

[Eric Wieser]

You would need a new HAddDep notation typeclass for this, along the lines of

class HAddDep (X Y : Type*) (Z : outParam (Π (x : X) (y : Y), Type*) where
  hAddDep : Π (x : X) (y : Y), Z x y

[aron]

@Eric Wieser can you elaborate? if I make my own typeclass will that let me add BNs or BNs and Nats together with the + operator?

[Eric Wieser]

You'll have to define your own + notation to replace the built-in one too

[Ruben Van de Velde]

Adding two BoundedNats is fine, though:

def BoundedNat (min max : Nat) : Type :=
  {n : Nat // min ≤ n ∧ n ≤ max}

def BoundedNat.mk {min max : Nat} (n : Nat) (h : min ≤ n ∧ n ≤ max) : BoundedNat min max :=
  ⟨n, h⟩

def BoundedNat.val {min max : Nat} (n : BoundedNat min max) : Nat :=
  n.1

def BoundedNat.addNat {min max : Nat} (m : Nat) (n : BoundedNat min max) : BoundedNat (min + m) (max + m) :=
  ⟨ n.val + m, by
    simp
    exact n.property
  ⟩

instance (min1 max1 min2 max2) : HAdd (BoundedNat min1 max1) (BoundedNat min2 max2) (BoundedNat (min1+min2) (max1+max2)) where
  hAdd a b := ⟨a.1 + b.1, by have ha := a.property; have hb := b.property; omega⟩

[aron]

@Ruben Van de Velde oh of course! good point, I didn't realise that BoundedNats with different bounds would count as different types, but of course they are because that's the only reason Add doesn't work for it lol

[Kevin Buzzard]

Just to note that we BoundedNat already in mathlib:

import Mathlib

open Set Pointwise

-- `Set.Icc` is "interval, closed at both ends"
example : 4 +ᵥ Icc 5 8 =  Icc 9 12 := by
  ext
  simp

example : Icc 1 3 + Icc 2 5 = Icc 3 8 := by
  ext x
  rw [mem_add]
  sorry -- exercise

[Eric Wieser]

This isn't the addition that @aron; is asking for; that would correspond to example (x : Icc a b) (y : Icc c d) : Icc (a + b) (c + d) := x + y, which doesn't work in mathlib today