How to work with nth_le?

Stream: general

[Sorawee Porncharoenwase]

I feel very frustrated when dealing with nth_le due to the error rewrite tactic failed, motive is not type correct. I get why the error occurs. What I don't know is how to workaround the problem.

I can rewrite the list part, but it requires me to constantly use list.nth_le_of_eq, which doesn't seem ideal. On the other hand, there doesn't seem to be a good way to rewrite the index part.

How do you reason with nth_le? Thanks!

[Johan Commelin]

I don't really have an answer to your question. Most of the time, we don't really use lists...
Would you mind explaining what your bigger goal is?

[Sorawee Porncharoenwase]

I'm working on program verification. We use lists to represent some kind of values, program states, etc.

[Johan Commelin]

Hmm, I'm afraid I can't help you with that.

[Jasmin Blanchette]

This is deep dependent type territory, of the wrong kind. I can vaguely imagine what goes wrong (the term and the type that depends on the term get out of sync), but I'd avoid the issue entirely by avoiding nth_le.

[Jasmin Blanchette]

See p. 64 of The Hitchhiker's Guide to Logical Verification for a discussion of alternatives.

[Jannis Limperg]

In general, you may be able to work around the rewrite error by constructing the motive yourself. rewrite ultimately generates an application of the recursion principle for equality, eq.rec:

eq.rec : Π {α : Sort u_2} {a : α} {C : α → Sort u_1},
  C a → Π {ᾰ : α}, a = ᾰ → C ᾰ

C is called the motive of the recursor and it determines where in your term the substitution is performed. rewrite, like similar mechanisms in other systems, uses a fairly simplistic method to infer these motives. If this fails, you get the 'motive is not type correct' error. To work around this, you can apply eq.rec directly and give a motive yourself.

These proofs won't be pretty, though, and it may be better to refactor your code so that it involves less dependencies.

[Yakov Pechersky]

You can also try using simp_rw, that usually will be able to hit all of the hidden terms as well. But simp_rw [<-...] will probably not work, due to a loop.

[Yakov Pechersky]

That's what I've done to reason about nth_le. You might also want to structure your proofs to induct on the head and tail, which will avoid having to index.

[Logan Murphy]

I don't know if this is helpful at all, but I almost always use fin when I use list.nth_le, for instance

def all_zero (l : list ℕ): Prop :=
    ∀ i : fin (l.length), l.nth_le i.1 i.2 = 0

and I have not had problems with it, but this isnt for all use cases

[Mario Carneiro]

@Sorawee Porncharoenwase A nice trick to avoid using nth_le all the time is to instead quantify over \forall i a, l.nth i = some a -> ... which avoids the "bad" kind of dependent types in favor of a simple predicate. I used this a lot when I wrote the C semantics, so I can attest to its effectiveness in program verification contexts. If you have an example of where you are running into trouble I can show how it goes.

[Sorawee Porncharoenwase]

Thanks everyone! This is helpful.