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.

That was bad.

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.

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/

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.

Dunno what's `teq`

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

You'll have to check docs on `Function`

for the appropriate tactic; `Equations`

also has a version.

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.

the general sentiment seems to be that `Function`

is legacy and will be maintained, but Equations is the future...

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.

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.

Mathieu Dehouck has marked this topic as resolved.

Last updated: Feb 08 2023 at 23:03 UTC