Showing decreasing on custom nat like type

Stream: general

[Ben]

I have the following non standard library definition of nat as well as some alternatives for subtraction and inequalities. I am struggling to use Modulo without the unsafe decorator.

Here is the small example. In the full one I have proved the goal (by showing all my operations are equivalent to nat operations). But it still gives me an cannot show decreasing error. Is there a simple fix?

inductive MyNat : Type
| zero
| successor (n: MyNat)
deriving DecidableEq


def MyNat.from.nat : Nat -> MyNat
| Nat.zero => zero
| Nat.succ n => successor (MyNat.from.nat n)

def MyNat.to.nat : MyNat -> Nat
| MyNat.zero => .zero
| MyNat.successor n => Nat.succ (MyNat.to.nat n)

instance (n: Nat) : OfNat MyNat n := ⟨MyNat.from.nat n⟩

instance : Repr MyNat := ⟨fun item => Repr.reprPrec (MyNat.to.nat item)⟩

def MyNat.sub : MyNat → MyNat → MyNat
  | MyNat.zero, MyNat.zero => MyNat.zero
  | MyNat.zero, MyNat.successor _ => MyNat.zero
  | n@ (MyNat.successor _), MyNat.zero => n
  | MyNat.successor n, MyNat.successor m => MyNat.sub n m

def MyNat.le (a b: MyNat) := MyNat.sub a b = MyNat.zero
def MyNat.lt (a b: MyNat) := MyNat.sub a.successor b = MyNat.zero

instance : LE MyNat := ⟨MyNat.le⟩
instance : LT MyNat := ⟨MyNat.lt⟩

instance (a b : MyNat) : Decidable (a <= b) := decidable_of_iff (MyNat.sub a b = 0) (by rfl)
instance (a b : MyNat) : Decidable (a < b) := decidable_of_iff (MyNat.sub a.successor b = 0) (by rfl)

def MyNat.mod (a n: MyNat) (h1: n > 1): MyNat := if
  a < n
then
  a
else MyNat.mod (MyNat.sub a n) n h1
decreasing_by {
  sorry
}

-- Does this help?
instance : SizeOf MyNat := ⟨MyNat.to.nat⟩

[Ben]

This is the error message I get in the full example? Is it because of the axioms?
image.png

[Aaron Liu]

Maybe you need to specify a decreasing measure with termination_by

[Ben]

I believe I am already doing that via decreasing_by

[Ben]

If anyone has anyone has any good minimal examples of using termination_by on a non-inbuilt type (that perhaps looks like Nat), that would be most appreciated

[Eric Paul]

One approach would be to prove

theorem lt_sizeOf (a b : MyNat) (a_lt_b : a < b) : sizeOf a < sizeOf b := sorry

and then combined with showing that a.sub n < a, you would be done. I think you'll have to prove some more facts about how < works for your natural numbers (like irreflexivity, for example).

[Aaron Liu]

Ben said:

I believe I am already doing that via decreasing_by

I think you should still have a termination_by, since the default could be unstable.