BoundedNat.lean

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.add (n1 : BoundedNat min1 max1) (n2 : BoundedNat min2 max2) : BoundedNat (min1 + min2) (max1 + max2) :=
  -- The value of the new BoundedNat is the sum of the values of the two BoundedNats
  BoundedNat.mk (n1.val + n2.val)

  -- The proof that the proposition is true for the new value
  (by
    -- Goal is:
    --    min1 + min2 ≤ n1.val + n2.val ∧ n1.val + n2.val ≤ max1 + max2
    --
    -- I.e.: the new value is between the sum of the lower bounds and the sum of the upper bounds.


    -- The proposition of BoundedNat n1
    have n1Prop := n1.property -- min1 ≤ n1.val ∧ n1.val ≤ max1
    have n1Left := n1Prop.left -- min1 ≤ n1.val
    have n1Right := n1Prop.right -- n1.val ≤ max1

    -- The proposition of BoundedNat n2
    have n2Prop := n2.property -- min2 ≤ n2.val ∧ n2.val ≤ max2
    have n2Left := n2Prop.left -- min2 ≤ n2.val
    have n2Right := n2Prop.right -- n2.val ≤ max2


    -- Nat.add_le_add is a function that says that given Nats `a b c d`, if you
    -- know that `a ≤ b` and `c ≤ d` you also know that `a + c ≤ b + d`.
    -- This lets you rearrange goals or construct new propositions from existing ones.

    -- a : min1, b : n1.val, c : min2, d : n2.val
    have mins := Nat.add_le_add n1Left n2Left -- min1 + min2 ≤ n1.val + n2.val
    -- a : n1.val, b : max1, c : n2.val, d : max2
    have maxs := Nat.add_le_add n1Right n2Right -- n1.val + n2.val ≤ max1 + max2


    -- Combine both propositions into an and
    have and := And.intro mins maxs -- min1 + min2 ≤ n1.val + n2.val ∧ n1.val + n2.val ≤ max1 + max2

    -- The value of and is exactly the goal we set out to prove!
    -- This completes the goal 🎉
    -- Q.E.D. bi
    exact and
  )



def a : BoundedNat 0 10 := BoundedNat.mk 3 (by simp)
def b : BoundedNat 4 63 := BoundedNat.mk 6 (by simp)

def sum := BoundedNat.add a b

#check sum