Stream: Coq users

Topic: A variation of nth_in for lists


view this post on Zulip David R (Nov 21 2020 at 04:00):

Hey guys, have a completely beginner question is anyone is able to help me..

view this post on Zulip Cody Roux (Nov 21 2020 at 05:21):

Many people are probably able to help you (although it is late in the US)! What is your question?

view this post on Zulip Christian Doczkal (Nov 21 2020 at 09:53):

Hmm, looks like a classic case of "Don't ask to ask, just ask!" :shrug:

view this post on Zulip David R (Nov 21 2020 at 11:13):

Haha sorry! I fell asleep pretty quickly was late for me too... I'm trying to solve a variation of nth_in for lists..

Theorem nth_in: forall (n:nat) (l:list), n < length l -> exists a: A, nth l n = Some a.

And was looking for some pointers.

view this post on Zulip David R (Nov 21 2020 at 11:14):

currently I have the following:
https://gist.github.com/dreadn0ught/0ad86cf93a16625ce499be7e03d49c33

view this post on Zulip Kenji Maillard (Nov 21 2020 at 11:17):

It would probably be easier to prove this theorem by induction on the list l (while generalizing the index n)

view this post on Zulip David R (Nov 21 2020 at 11:21):

so I might be being an idiot. I tried that doing the following:
Proof.
unfold lt in |-*.

intros.
induction l.

view this post on Zulip David R (Nov 21 2020 at 11:22):

but find there's no convenient rewrite options

view this post on Zulip David R (Nov 21 2020 at 11:22):

please remember I am very very new to Coq. Last time I dealt with this stuff was doing ML yeaaars ago.

view this post on Zulip Kenji Maillard (Nov 21 2020 at 11:25):

You probably don't want to unfold lt, it does not make your goal progress in any way. what I was thinking is intros n l. revert n. induction l as [| x l' IH].

view this post on Zulip Kenji Maillard (Nov 21 2020 at 11:26):

A first point is that it is good practice to name every hypothesis that you will need to manipulate explicitely in your proof script.

view this post on Zulip Kenji Maillard (Nov 21 2020 at 11:29):

A second point less related to Coq but to formal proof in general is to make sure that you have an intuitive proof in mind/on paper before diving in the proof script. Here the first step I proposed is "Let's prove by induction on a list l that (n:N),n<length la,nth l n =Some a\forall (n : \mathbb{N}), n < \text{length }l \to \exists a, \text{nth }l~n~= \texttt{Some }a. If l=nill = \texttt{nil} then ... . Otherwise if l=cons x ll = \texttt{cons }x~l' then..." and you have to fill in the holes.

view this post on Zulip David R (Nov 21 2020 at 11:36):

Yeah problem I have is I don't seem to be able to deep dive on paper... for example right now I have: "exists a : A, nth nil n = Some a" on paper I stop here but obviously you can't in Coq

view this post on Zulip David R (Nov 21 2020 at 11:36):

I think I'm missing something obvious when approaching this.

view this post on Zulip Kenji Maillard (Nov 21 2020 at 11:36):

David R said:

Yeah problem I have is I don't seem to be able to deep dive on paper... for example right now I have: "exists a : A, nth nil n = Some a" on paper I stop here but obviously you can't in Coq

why do you stop at this point on paper ?

view this post on Zulip Kenji Maillard (Nov 21 2020 at 11:38):

clearly you cannot prove the conclusion "exists a : A, nth nil n = Some a" neither on paper nor in Coq, so what makes it ok on paper ? (and it is actually the same in Coq)

view this post on Zulip David R (Nov 21 2020 at 11:40):

I think you've hit the nail on the head there, I'm just not very good at this stuff at the moment

view this post on Zulip David R (Nov 21 2020 at 11:42):

I've done a load of other exercises this weekend that were fine I think lists are just throwing a curve ball at me

view this post on Zulip David R (Nov 21 2020 at 11:46):

so if I go into a second proof by induction on n after l I get: exists a : A, None = Some a
is there a rewrite I can use on this or again am I missing something obvious?

view this post on Zulip Kenji Maillard (Nov 21 2020 at 11:48):

hint: think about your hypotheses at this point

view this post on Zulip David R (Nov 21 2020 at 12:01):

hmm on paper here I would just add None is a member of A :P

view this post on Zulip David R (Nov 21 2020 at 12:09):

what I have now is..

Proof.
intros n l.
revert n.
induction l as [| x l' IH].
intros.
induction n as [| m n'].
simpl in |- *; auto.

but this feels wrong.

view this post on Zulip Fabian Kunze (Nov 21 2020 at 12:10):

David R said:

hmm on paper here I would just add None is a member of A :P

there is no a such that None = Some a, so you won't be able to prove exists a : A, None = Some a . Or am I misunderstanding what you mean by that comment?

view this post on Zulip David R (Nov 21 2020 at 12:14):

Hi Fabian, that was partly a joke. I'm doing proof by induction on the length of the list, followed by induction on n but I think I'm just ending up in dead ends.
https://gist.github.com/dreadn0ught/0ad86cf93a16625ce499be7e03d49c33

view this post on Zulip David R (Nov 21 2020 at 12:14):

functions on lists seems to have completely stumped me

view this post on Zulip Fabian Kunze (Nov 21 2020 at 12:50):

oh, i read the :P as some typo, not a smiley ^^'

view this post on Zulip David R (Nov 21 2020 at 12:51):

no worries! now solved it!

view this post on Zulip David R (Nov 21 2020 at 12:51):

turns out I was screwing up my rewrites and then going down massive rabbit holes that didn't make sense. Thanks Fabian and Kenji for the help!

view this post on Zulip Fabian Kunze (Nov 21 2020 at 12:52):

great. As a tip, to find lemmas, there is a search command Search (S _ < S _).

view this post on Zulip Fabian Kunze (Nov 21 2020 at 12:52):

or even Search (S ?n < S ?n) (?n < ?n). to find lemmas that talk about those two terms, where ?n is always the same subterm

view this post on Zulip David R (Nov 21 2020 at 12:54):

thanks, that's good to know. Spent ages getting my Search params wrong today!

view this post on Zulip David R (Nov 21 2020 at 12:54):

I'm going to take a break now and let me brain rest. Thanks again!

view this post on Zulip arte (Nov 21 2020 at 20:04):

Hi everyone, I am having a tough time trying to prove this theorem:

Theorem math_problem: forall m n, (n + m) * (n + m) = n * n + 2 * n * m + m * m.

Can anyone give me any pointers?

view this post on Zulip Babar (Nov 21 2020 at 20:10):

Hello here, i got the exact same assignment about nth_in for lists :
Theorem nth_in: forall (n:nat) (l:list), n < length l -> exists a: A, nth l n = Some a.
I'm kinda stuck at the same point; I end up with the unprovable exists a : A, None = Some a and the wrongful Hypothesis n < length nil.
I'm looking for directions :)

view this post on Zulip Kenji Maillard (Nov 21 2020 at 20:20):

Look at your hypothesis: it is enough to conclude :)

view this post on Zulip Babar (Nov 21 2020 at 20:23):

I've try to rewirte on paper like you suggested. but my hypothesis seems wrong in the l = nil case as far as I cant tell ( Length nil =0 therefore n >= len l )
I don't get how i'm suppose to tell COQ to conclude :/

view this post on Zulip Babar (Nov 21 2020 at 20:34):

I know it's kind of a silly question but i'm very new to COQ

view this post on Zulip Kenji Maillard (Nov 21 2020 at 20:44):

As you say length nil = 0, so in your context you have an hypothesis n < 0, but n is a natural number so it cannot be strictly smaller than 0, so by inverting your hypothesis you would be done.

view this post on Zulip Babar (Nov 21 2020 at 20:48):

Thanks for your help.
I tried the inversion H. command ; Now i'm left with the remaining case l = (cons x l'). I'm not sur what you mean by "You would be done " :)

view this post on Zulip Kenji Maillard (Nov 21 2020 at 20:50):

you are done with the first case of course :) Just one more to go ! Well you will probably need to split it again

view this post on Zulip Babar (Nov 21 2020 at 20:51):

Ahhh Yes Done with the first case that makes more sense :D

view this post on Zulip Fabian Kunze (Nov 21 2020 at 21:00):

do you just want to solve it?
Require Import Lia.

nia.

view this post on Zulip Fabian Kunze (Nov 21 2020 at 21:04):

otherwise, use search to find the lemmas on natural numbers you need:

view this post on Zulip Fabian Kunze (Nov 21 2020 at 21:06):

Goal forall m n, (n + m) * (n + m) = n * n + 2 * n * m + m * m.
Proof.
intros.
Search ((_+_)*_).
rewrite PeanoNat.Nat.mul_add_distr_r.

view this post on Zulip Babar (Nov 21 2020 at 21:25):

I think i'm going down the rabbit hole, i've tried to do an induction on n and it leads me to strange cases. How am I supposed to prove that Some x = Some a ?

view this post on Zulip Kenji Maillard (Nov 21 2020 at 21:28):

I guess you provided either x or a at some point in your proof script ?

view this post on Zulip Babar (Nov 21 2020 at 21:29):

yes i provided x when i did the induction on l the first time

view this post on Zulip Brandon Moore (Nov 21 2020 at 21:31):

Do you have a hypothesis x = a?

view this post on Zulip Babar (Nov 21 2020 at 21:33):

no i don't
2 subgoals
A : Type
x : A
l' : list
IH : forall n : nat, n < length l' -> exists a : A, nth l' n = Some a
H : 0 < length (cons x l')
______________________________________(1/2)
exists a : A, Some x = Some a
______________________________________(2/2)
exists a : A, nth (cons x l') (S m) = Some a

view this post on Zulip Brandon Moore (Nov 21 2020 at 21:36):

Oh, the exists a:A, around Some x = Some a makes a big difference. You can pick a value for a with the exists tactic - try exists x.

view this post on Zulip Babar (Nov 21 2020 at 21:40):

Ohh i didn't knew i could do that with the exists a:A thanks !

view this post on Zulip Babar (Nov 21 2020 at 21:42):

is using reflexivity after that the right way to pursue ?

view this post on Zulip Kenji Maillard (Nov 21 2020 at 21:46):

yep

view this post on Zulip Babar (Nov 21 2020 at 21:57):

Ok so now i've 1 subgoal left, its "exists a : A, nth l' m = Some a ".
I've got an hypothesis "S m < len ( cons x l' ) " So it's fair to assume that m < len(l'), therefore "nth l' m" is equal to Some a right ?

view this post on Zulip Babar (Nov 21 2020 at 21:59):

if I apply IH my subgoal becomes m < len (l');
this is equivalent to the H hypothesis S m < len (cons x l' ), how can i tell COQ to "use" my hopthesis and finish the proof ?

view this post on Zulip Kenji Maillard (Nov 21 2020 at 22:00):

the second part of your argument is more or less the induction hypothesis IH. For the first part ("it's fair to assume") you should Search (S _ < S _). to find the relevant lemma

view this post on Zulip Babar (Nov 21 2020 at 22:21):

Ok i found it, I think it's solved now
Many thanks for your patience :)

view this post on Zulip Michael Shen (Nov 22 2020 at 18:11):

I have a question along the same lines...

Likewise, I have a subgoal of n' < length (cons a l') with H: S n' < length (cons a l'). It seems like I could use le_Sn_le, but I'm not sure of the syntax. When I try to assign (m:=length (cons a l')) I get Found no subterm matching "length (cons a l')" in the current goal.

view this post on Zulip Michael Shen (Nov 22 2020 at 18:22):

Where as if I just try to assign (m:=length) I get The term "length" has type "list -> nat" while it is expected to have type "nat". Not sure how to just assign the result of the function...

view this post on Zulip Paolo Giarrusso (Nov 22 2020 at 19:19):

What's the actual tactic that you're using? And a lemma stated about lt would be better.

view this post on Zulip Michael Shen (Nov 22 2020 at 19:23):

Sure, my current state is:

2 subgoals

  A : Type
  a : A
  l' : list
  IHl : forall n : nat, n < length l' -> exists a : A, nth l' n = Some a
  n' : nat
  H : S n' < length (cons a l')
  IHn : n' < length (cons a l') -> nth (cons a l') n' = Some a
  ============================
  nth l' n' = nth (cons a l') n'

subgoal 2 is:
 n' < length (cons a l')

and I'm trying things like apply le_Sn_le with (n:=n') (m:=length).

view this post on Zulip Michael Shen (Nov 22 2020 at 19:26):

It's kind of a challenge question (this is my first day with coq) and we've been restricted to only Require Import Le., but my thought was that le just includes lt, I guess I need a step to convert lt to le?

view this post on Zulip Cody Roux (Nov 22 2020 at 19:53):

I'm pretty sure that goal is unprovable. You probably need to back up a couple of steps.

view this post on Zulip Michael Shen (Nov 22 2020 at 19:56):

Thank you, on paper I had realized I misunderstood what coq was representing. What I'm stuck on is it feels like I should be done here, but am not sure how to "finish."

IHn : n'  < length (cons a l') → nth (cons a l') n' = Some a
============================
nth l' n' = Some a

view this post on Zulip Paolo Giarrusso (Nov 22 2020 at 20:01):

Next step would be "apply IHn", except that it will fail because the arguments to nth do not match. This seema much too hard for your first day with Coq.

view this post on Zulip Michael Shen (Nov 22 2020 at 20:03):

Yeah haha, well it's an opt-in/for-fun challenge. I presume it's the same Babar and David R solved above. I did try that and I'm glad that's at least the right line of thinking.

view this post on Zulip Michael Shen (Nov 22 2020 at 20:11):

Are there any references/tactics I could look at to work toward matching the arguments of IHn and the subgoal though?

view this post on Zulip Michael Shen (Nov 22 2020 at 20:39):

Well I've been bouncing back and forth between that and this with not much luck...

IHn : n' < length (cons a l') → nth (cons a l') n' = Some a
============================
nth (cons a l') (S n') = Some a

view this post on Zulip Kenji Maillard (Nov 22 2020 at 20:41):

you probably used exists a too early, leading to an unsolvable goal

view this post on Zulip Michael Shen (Nov 22 2020 at 20:51):

Hm, I think I have to use it to solve the base case of my induction over n and I just tried moving it as late as possible, but end up with the same IHn/subgoal

view this post on Zulip Kenji Maillard (Nov 22 2020 at 20:53):

well you don't need the induction on n, case analysis would be enough. And you have a second more general induction hypothesis lying around.

view this post on Zulip Paolo Giarrusso (Nov 22 2020 at 20:55):

Is this part of the DragonCTF challenge?

view this post on Zulip Michael Shen (Nov 22 2020 at 20:55):

Yeah, that's the one haha

view this post on Zulip Michael Shen (Nov 22 2020 at 20:56):

Don't think I'll figure it out in time (5 min left), but curious beyond that to try and figure this out anyway.

view this post on Zulip Paolo Giarrusso (Nov 22 2020 at 20:56):

Good luck!

view this post on Zulip Paolo Giarrusso (Nov 22 2020 at 20:57):

In case others are curious, here's what I was explained on IRC > CTF competitions usually have a bunch of independently-machine-scored challenges (usually cybersecurity-adjacent), one of the challenges is babykok.hackable.software:1337, which gives you a wrapper around a coqtop session

view this post on Zulip Michael Shen (Nov 22 2020 at 20:58):

Yeah, there were 8 "proofs" to prove, and this is the last of the 8.

view this post on Zulip Paolo Giarrusso (Nov 22 2020 at 21:00):

The website is https://ctf.dragonsector.pl, but to outsiders like me it gives 0 information... OTOH it was visible on IRC :-) (numbers were not huge but definitely notable)

view this post on Zulip Michael Shen (Nov 22 2020 at 21:10):

Well if you're curious it started with more trivial proofs to give people like me I guess a foothold to try to learn coq syntax like

view this post on Zulip Paolo Giarrusso (Nov 22 2020 at 21:18):

oooh, so problem4 is the one in https://coq.discourse.group/t/starting-to-learn-coq/1120/8 ! I was starting to suspect

view this post on Zulip Paolo Giarrusso (Nov 22 2020 at 21:21):

I might have been socially engineered into providing an answer, or it might have been an accident :-P

view this post on Zulip Michael Shen (Nov 22 2020 at 21:22):

Haha that's one way to put it. There aren't really any prizes besides bragging rights, so no big deal

view this post on Zulip Paolo Giarrusso (Nov 22 2020 at 22:48):

Top 1: 2000 USD

view this post on Zulip Paolo Giarrusso (Nov 22 2020 at 22:49):

(from https://ctf.dragonsector.pl/)

view this post on Zulip Paolo Giarrusso (Nov 22 2020 at 22:50):

Who knows what that means tho :-P

view this post on Zulip Michael Shen (Nov 23 2020 at 03:19):

Oh, you got me.

However, normally they're just for fun. Personally I'm not close to the level where I can even compete for any top prizes anyway so I just assumed - my mistake!

view this post on Zulip Emilio Jesús Gallego Arias (Nov 23 2020 at 15:23):

Just for reference, this is what a proof using math-comp looks like:

Theorem nth_in A x0 n (l : seq A)
        (n_bound : n < size l) :
        exists a: A, nth x0 l n = a.
Proof. by elim: l n n_bound => // x l ihl; eauto. Qed.

ssreflect elimhas helped me a lot to learn as it features a stricter disclipine w.r.t. hypothesis generalization than regular induction, which helps to realize what the scope of induction should be.

view this post on Zulip Christian Doczkal (Nov 23 2020 at 17:16):

@Emilio Jesús Gallego Arias , the proof of your lemma can be simplified even further: by exists (nth x0 l n). or even by eexists. I assume the statement wasn't what you wanted to prove. :smirk:

view this post on Zulip Christian Doczkal (Nov 23 2020 at 17:22):

But indeed, there is point to make here. Definingnth to return an option type is making ones life harder than necessary in many (almost all) circumstances. It's much simpler to let nth return a default value when the list isn't long enough. The statement most closely corresponding to the OPs problem is probably:

mem_nth : forall (T : eqType) (x0 : T) (s : seq T) (n : nat), n < size s -> nth x0 s n \in s

Last updated: Jan 27 2023 at 00:03 UTC