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

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

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

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.

currently I have the following:

https://gist.github.com/dreadn0ught/0ad86cf93a16625ce499be7e03d49c33

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

so I might be being an idiot. I tried that doing the following:

Proof.

unfold lt in |-*.

intros.

induction l.

but find there's no convenient rewrite options

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

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

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

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.

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

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

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 ?

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)

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

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

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?

hint: think about your hypotheses at this point

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

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.

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?

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

functions on lists seems to have completely stumped me

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

no worries! now solved it!

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!

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

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

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

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

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?

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

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

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

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

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.

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

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

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

do you just want to solve it?

`Require Import Lia.`

`nia.`

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

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

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 ?

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

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

Do you have a hypothesis `x = a`

?

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

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`

.

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

is using reflexivity after that the right way to pursue ?

yep

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 ?

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 ?

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

Ok i found it, I think it's solved now

Many thanks for your patience :)

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

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

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

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

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?

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

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

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.

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.

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

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

you probably used `exists a`

too early, leading to an unsolvable goal

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

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.

Is this part of the DragonCTF challenge?

Yeah, that's the one haha

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

Good luck!

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

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

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)

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

oooh, so `problem4`

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

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

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

Top 1: 2000 USD

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

Who knows what that means tho :-P

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!

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 `elim`

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

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

But indeed, there is point to make here. Defining`nth`

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