Stream: Coq users

Topic: ✔ Turning a recusive function into a lemma


view this post on Zulip 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.
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.

view this post on Zulip 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/

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Notification Bot (Jan 31 2022 at 15:09):

Mathieu Dehouck has marked this topic as resolved.


Last updated: Feb 08 2023 at 23:03 UTC