Zulip Chat Archive

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.

Johan Commelin (Nov 12 2020 at 10:01):

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

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.

Sorawee Porncharoenwase (Nov 13 2020 at 11:56):

Thanks everyone! This is helpful.

Last updated: Aug 03 2023 at 10:10 UTC