Help understanding DecidableRel stuck metavariable problem

Stream: general

[Chris Moline]

Hi. When I have

def comp {foo} [inst : LT foo]
         [DecidableRel (·<·)]
         (a:Array foo) (b:Array foo) (idx:Nat) : Ordering :=
  match a[idx]?, b[idx]? with
  | some v, some w => if @LT.lt foo inst v w
                      then comp a b (idx+1)
                      else Ordering.gt
  | some v, none => Ordering.gt
  | none, some v => Ordering.lt
  | none, none => Ordering.eq

instance {foo} [Ord foo] : Ord (Array foo) where
  compare xs ys := comp xs ys 0

I get an error:
error: LeanSitter/Length.lean:43:24: typeclass instance problem is stuck, it is often due to metavariables

When I change '[DecidableRel (·<·)]' to ' [DecidableRel (fun a b : foo => @LT.lt foo inst a b)]' I get

rror: LeanSitter/Length.lean:42:4: fail to show termination for
  LeanSitter.Length.comp
with errors
failed to infer structural recursion:
Not considering parameter foo of LeanSitter.Length.comp:
  it is unchanged in the recursive calls
Not considering parameter inst of LeanSitter.Length.comp:
  it is unchanged in the recursive calls
Not considering parameter #3 of LeanSitter.Length.comp:
  it is unchanged in the recursive calls
Not considering parameter a of LeanSitter.Length.comp:
  it is unchanged in the recursive calls
Not considering parameter b of LeanSitter.Length.comp:
  it is unchanged in the recursive calls
Cannot use parameter idx:
  failed to eliminate recursive application
    comp a b (idx + 1)


failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
idx : Nat
⊢ idx + 1 < idx

I don't understand what's going on. What do I need to do?

[Aaron Liu]

the termination prover couldn't automatically prove that your algorithm doesn't go into an infinite loop

[Malvin Gattinger]

Maybe like this?

def comp {foo} [inst : LT foo]
         [DecidableRel (fun a b : foo => @LT.lt foo inst a b)]
         (a:Array foo) (b:Array foo) (idx:Nat) : Ordering :=
  match ha : a[idx]?, hb : b[idx]? with
  | some v, some w => if @LT.lt foo inst v w
                      then comp a b (idx+1)
                      else Ordering.gt
  | some _, none => Ordering.gt
  | none, some _ => Ordering.lt
  | none, none => Ordering.eq
termination_by
  b.size - idx
decreasing_by
  rcases Array.getElem_of_getElem? ha with ⟨_, _⟩
  rcases Array.getElem_of_getElem? hb with ⟨_, _⟩
  omega

More example how to use termination_by and decreasing_by can be found here in #tpil.

[Robin Arnez]

For your DecidableRel problem: use [DecidableLT foo] instead. For your termination problem: you can use something like termination_by a.size - idx (i.e the difference of size and index should decrease in recursive calls). With some other adjustments:

def comp [LT α] [DecidableLT α] (a b : Array α) (idx : Nat) : Ordering :=
  match h : a[idx]?, b[idx]? with
  | some v, some w =>
    if v < w then comp a b (idx+1) else Ordering.gt
  | some _, none => Ordering.gt
  | none, some _ => Ordering.lt
  | none, none => Ordering.eq
termination_by a.size - idx
decreasing_by grind

Although I will note that there already is an Ord instance for Arrays, docs#Array.instOrd

[Chris Moline]

Thank you very much for the help. I didn't know you could write 'a : a[idx]?' to bind the result of 'a[idx]?'. I also haven't covered much for tactics either so to learn about rcases and grind was good. I've updated my code to use the array Ord instance.

I will strive to do better in the hopes of one day being useful to the lean community.