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: Oct 13 2024 at 01:02 UTC