## Stream: general

### Topic: How to work with nth_le?

#### Sorawee Porncharoenwase (Nov 12 2020 at 09:23):

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 (Nov 12 2020 at 09:29):

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 (Nov 12 2020 at 09:58):

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

#### Jasmin Blanchette (Nov 12 2020 at 10:03):

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 (Nov 12 2020 at 10:04):

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

#### Jannis Limperg (Nov 12 2020 at 10:33):

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 (Nov 12 2020 at 16:02):

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 (Nov 12 2020 at 16:03):

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 (Nov 12 2020 at 17:41):

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 (Nov 12 2020 at 20:50):

@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.