autoProp on OfNat instance

Stream: new members

[MrQubo]

I've made a structure family Idx n that represent numbers less than n:

structure Idx (n : ℕ) where
  val : ℕ
  property : val < n := by simp_all_arith <;> omega

Now, I wanted to define na instance of OfNat for this type. But, because of how this type is defined, I cannot define an instance of OfNat (Idx n) i for any i, only for i s.t. i < n. However, I don't know how to do that.

I've tried like this:

instance {n i} (_ : i < n := by simp_all_arith <;> omega) : OfNat (Idx n) i where
  ofNat := { val := i }

This instance does compile, but it doesn't seem to work. This code still raises an error:

def x : Idx 3 := 2

failed to synthesize OfNat (Idx 3) 2

Instance of OfNat (Fin n) i avoids this problem by defining instance for every i. Maybe it's currently not possible to do what I want in Lean?

[Ruben Van de Velde]

Oh yeah, you can't write an instance with a hypothesis like that

[Markus Himmel]

There is a trick due to Gabriel Ebner:

structure Idx (n : Nat) where
  val : Nat
  property : val < n := by simp_all_arith <;> omega

class When (p : Prop) [Decidable p] : Prop where
  isTrue : p

instance : @When p (.isTrue h) := @When.mk p (_) h

instance {n i} [h : When (i < n)] : OfNat (Idx n) i where
  ofNat := { val := i, property := h.isTrue }

def x : Idx 3 := 2 -- works
def y : Idx 3 := 3 -- fails

But it's not exactly supported, and you can't have it use simp_all_arith <;> omega, only decide.

[MrQubo]

I think I was able to implement what I want using macro:

import Mathlib

def idxOfNum {n} (i : ℕ) (_ : i < n := by simp_all_arith <;> omega) : Idx n :=
  ⟨i, ‹i < n›⟩

syntax (name := idxn) num : term

macro_rules (kind := idxn)
  | `($i:num) => `(idxOfNum $i)

def x : Idx 3 := 2
def y : ℕ := 2
#check_failure (3 : Idx 3)