Could not find a decreasing measure.

Stream: new members

[Iocta]

I see what it's complaining about but I don't understand why List.zipWith doesn't have the same problem. How can I fix it?

def zipWithFill (f : α → α → α) (z : α) (as bs : List α) : List α :=
  match (as, bs) with
  | (a::as, b::bs) => (f a b) :: zipWithFill f z as bs
  | (a::as, _) => (f a z) :: zipWithFill f z as []
  | (_, b::bs) => (f z b) :: zipWithFill f z [] bs
  | (_, _) => []
fail to show termination for
  zipWithFill
with errors
argument #4 was not used for structural recursion
  failed to eliminate recursive application
    zipWithFill f✝ z as bs

argument #5 was not used for structural recursion
  failed to eliminate recursive application
    zipWithFill f✝ z as bs

structural recursion cannot be used

Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
             as bs
1) 147:33-54  ?  ?
2) 148:29-50  _  _
3) 149:29-50  _  _
Please use `termination_by` to specify a decreasing measure.

[Damiano Testa]

This seems to work:

def zipWithFill (f : α → α → α) (z : α) (as bs : List α) : List α :=
  match as, bs with
  | a::as, b::bs => (f a b) :: zipWithFill f z as bs
  | a::as, _ => (f a z) :: zipWithFill f z as []
  | [], b::bs => (f z b) :: zipWithFill f z [] bs
  | _, _ => []

There was a question just like this one a few minutes ago, I think.