Stream: Coq users

Topic: A variation of nth_in for lists

David R (Nov 21 2020 at 04:00):

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

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?

Christian Doczkal (Nov 21 2020 at 09:53):

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

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.

David R (Nov 21 2020 at 11:14):

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

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)

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.

David R (Nov 21 2020 at 11:22):

but find there's no convenient rewrite options

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.

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

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.

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 $\forall (n : \mathbb{N}), n < \text{length }l \to \exists a, \text{nth }l~n~= \texttt{Some }a$. If $l = \texttt{nil}$ then ... . Otherwise if $l = \texttt{cons }x~l'$ then..." and you have to fill in the holes.

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

David R (Nov 21 2020 at 11:36):

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

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 ?

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)

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

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

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?

Kenji Maillard (Nov 21 2020 at 11:48):

hint: think about your hypotheses at this point

David R (Nov 21 2020 at 12:01):

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

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.

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?

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

David R (Nov 21 2020 at 12:14):

functions on lists seems to have completely stumped me

Fabian Kunze (Nov 21 2020 at 12:50):

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

David R (Nov 21 2020 at 12:51):

no worries! now solved it!

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!

Fabian Kunze (Nov 21 2020 at 12:52):

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

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

David R (Nov 21 2020 at 12:54):

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

David R (Nov 21 2020 at 12:54):

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

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?

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 :)

Kenji Maillard (Nov 21 2020 at 20:20):

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

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 :/

Babar (Nov 21 2020 at 20:34):

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

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.

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 " :)

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

Babar (Nov 21 2020 at 20:51):

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

Fabian Kunze (Nov 21 2020 at 21:00):

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

nia.

Fabian Kunze (Nov 21 2020 at 21:04):

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

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.

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 ?

Kenji Maillard (Nov 21 2020 at 21:28):

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

Babar (Nov 21 2020 at 21:29):

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

Brandon Moore (Nov 21 2020 at 21:31):

Do you have a hypothesis x = a?

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

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.

Babar (Nov 21 2020 at 21:40):

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

Babar (Nov 21 2020 at 21:42):

is using reflexivity after that the right way to pursue ?

Kenji Maillard (Nov 21 2020 at 21:46):

yep

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 ?

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 ?

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

Babar (Nov 21 2020 at 22:21):

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

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.

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

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.

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

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?

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.

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

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.

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.

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?

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

Kenji Maillard (Nov 22 2020 at 20:41):

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

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

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.

Paolo Giarrusso (Nov 22 2020 at 20:55):

Is this part of the DragonCTF challenge?

Michael Shen (Nov 22 2020 at 20:55):

Yeah, that's the one haha

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.

Paolo Giarrusso (Nov 22 2020 at 20:56):

Good luck!

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

Michael Shen (Nov 22 2020 at 20:58):

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

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)

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

• Theorem problem0: forall A B, A \/ B -> B \/ A.
• Theorem problem1: forall b1 b2, negb (b1 && b2) = orb (negb b1) (negb b2).
• Theorem problem2: forall A B C D: Prop,(A->B)/\(C->D)/\A/\C -> B/\D.
• Theorem problem3: forall (m n: nat), m + n = n + m.
• Theorem problem4: forall A B, ((((A -> B) -> A) -> A) -> B) -> B.
• Theorem problem5: forall (C:Prop) (T:Set) (B: T -> Prop), (exists x : T, C -> B x) -> C -> exists x : T, B x.
  Then the next was Theorem math_problem: forall m n, (n + m) * (n + m) = n * n + 2 * n * m + m * m. which was an adventure for me
  Followed by this nth_in problem for the last proof, which I think is kind of over my head in coq...I feel like a monkey at the typewriter haha

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

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

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

Paolo Giarrusso (Nov 22 2020 at 22:48):

Top 1: 2000 USD

Paolo Giarrusso (Nov 22 2020 at 22:49):

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

Paolo Giarrusso (Nov 22 2020 at 22:50):

Who knows what that means tho :-P

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!

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.

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:

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: Sep 23 2023 at 13:01 UTC