## Stream: Coq users

### Topic: ✔ Turning a recusive function into a lemma

#### Mathieu Dehouck (Jan 29 2022 at 16:01):

Dear Coq users,
I am making my way through Coq proofs slowly but surely.
I had defined a recursive function on a list that returned a sublist of the list, but since it was not structuraly recursive I resorted to use a dummy counter which I knew would be bigger than the actual list size.
Then I discovered the `Function F x y z {measure length x}` notation, and I could easily prove the function since the recursion criterion was exactly `if length f x < length x then F (f x) else x`, so pretty easy to do.

My problem now, is that I would like to prove that `forall x, length (F x) <= length x`.
In a way it should be straightforward from the definition of F.
But for some reason, it's not as easy.

Do you know how I could do to turn a well defined already proven recursive function into a lemma on the fact that its arguments decrease?

Best.

#### Karl Palmskog (Jan 29 2022 at 16:39):

I'm not aware of a mechanism for obtaining well-foundedness proofs directly from recursive functions. You may want to check out the Equations plugin for more powerful machinery for dealing with recursion and well-foundedness: https://github.com/mattam82/Coq-Equations/

#### Mathieu Dehouck (Jan 29 2022 at 16:49):

I don't necessarily need a direct way, I am ok with proving it myself, but I don't know how to.
Here is my original function to give you a feeling of what I want to do :

``````Function iter_keeps (cells:list t_cell) (edges: list edge) {measure length edges} : list edge :=
let n_edges := keeps cells edges nil in
if Nat.ltb (length n_edges) (length edges)
then iter_keeps cells n_edges
else edges.
Proof.
intros.
apply PeanoNat.Nat.ltb_lt in teq.
assumption.
Qed.
``````

Then I'd like to prove :

``````Lemma iter_keeps_shortens :
forall cells edges, length (iter_keeps cells edges) <= length edges.
``````

In a way it should be the same proof, but in the lemma there is no `teq` term so I need to find another road.

Thank you very much.

#### Paolo Giarrusso (Jan 29 2022 at 16:54):

Dunno what's `teq`, but have you tried using _functional induction_? It's essentially induction on the tree of recursive calls.

#### Paolo Giarrusso (Jan 29 2022 at 16:55):

You'll have to check docs on `Function` for the appropriate tactic; `Equations` also has a version.

#### Paolo Giarrusso (Jan 29 2022 at 16:56):

I vaguely recall `Function` having extra bugs compared to Equations, but I last tried it > 5 years ago, so take it just as a caveat.

#### Karl Palmskog (Jan 29 2022 at 16:56):

the general sentiment seems to be that `Function` is legacy and will be maintained, but Equations is the future...

#### Mathieu Dehouck (Jan 31 2022 at 14:53):

I will have a look at functional induction.
I was using Recdef instead of FunInd so far, and there did not seem to be something like that.
Thank you.

#### Mathieu Dehouck (Jan 31 2022 at 15:08):

Ok, that's exactly what I was looking for.
I may have learned to read the doc a bit better in the future in the mean time.
But to be honest I did not see how it was structured.
So the point is not FunInd or Recdef, it was just using `functional induction`.

And `teq` is the name of a recursion hypothesis introduced by Coq in order to prove that a recursive function defined with `{measure ...}` is indeed well defined.
So when you prove the definition of the function, you have an extra hypothesis that you do not have when proving it as a lemma.

#### Notification Bot (Jan 31 2022 at 15:09):

Mathieu Dehouck has marked this topic as resolved.

Last updated: Oct 03 2023 at 02:34 UTC