I'm building a recursive function that does a match on a list l. In the cons branch I need to use the information that l = cons a l' in order to prove that the recursive function terminates. However, when I use match l the information gets lost.
How can I use match to keep the information?
Here is the function (drop and drop_lemma_le are given at the end, for readability):
Fixpoint picksome (l:list nat) (H : Acc lt (length l)) {struct H}: list nat.
refine (
match l with
nil => nil
| cons a l' => cons a (picksome (drop a l') _)
end
).
apply H.
assert (l = cons a l') by admit. (* here is where I need the information *)
rewrite H0.
simpl.
apply le_lt_n_Sm.
apply drop_lemma_le.
Defined. (* Can't end definition here because of the 'admit'. *)
I am actually able to define the whole function via refine like below, but it is not really readable. Doing Print picksome. reveals how Coq has handled the problem, but it is also quite long and unreadable with nested functions, etc.
There must be a more readable way to write it, right?
Fixpoint picksome (l:list nat) (H : Acc lt (length l)) {struct H}: list nat.
Proof.
refine ( _ ).
remember l as L.
destruct l as [| a l'].
apply nil.
apply (cons a).
apply (picksome (drop a l')).
apply H.
rewrite HeqL.
simpl.
apply le_lt_n_Sm.
apply drop_lemma_le.
Defined.
My first attempt was to try something like this
Definition list_cons_dec {T} (l:list T) :
{exists a l', l=a::l'} + {~ exists a l', l=a::l'}.
remember l as L.
destruct l as [| a l'].
- right; subst L; intros [a [A B]]; inversion B.
- left; exists a, l'; apply HeqL.
Defined.
Fixpoint picksome (l:list nat) (H : Acc lt (length l)) {struct H}: list nat.
Proof.
refine (
match list_cons_dec l with
| right Hdec => nil
| left Hdec => cons _ (picksome (drop _ _) _)
end
).
destruct l.
inversion Hdec. (* fails *)
I'm unable to get out the actual a and l' that l is made from. Coq complains:
Error: Inversion would require case analysis on sort Set which is not allowed
for inductive definition ex.
What would be the proper (readable) way to do this?
Here are the definitions of drop and drop_lemma_le.
Fixpoint drop {T} n (l:list T) :=
match n with
| O => l
| S n' => match l with
| nil => nil
| cons _ l' => drop n' l'
end
end.
Lemma drop_lemma_le : forall {T} n (l:list T), length (drop n l) <= (length l).
Proof.
intros; generalize n;
induction l; intros; destruct n0; try reflexivity.
apply le_S; apply IHl.
Defined.
To remember what the list you are pattern-matching on looks like, you need to simply change the return type of your match like so.
Fixpoint picksome (l:list nat) (H : Acc lt (length l)) {struct H}: list nat.
refine (
(match l as m return l = m -> list nat with
nil => fun Hyp => nil
| cons a l' => fun Hyp => cons a (picksome (drop a l') _)
end) (eq_refl l)
).
What this match l as m return l = m -> list nat is saying is that you are performing a pattern matching on l, that you'll call the matching form m and that, given a proof that l equals m, you'll build a list of nats.
Now, the type of the match block will be slightly different: instead of just delivering a list nat, it will deliver a function of type l = l -> list nat. Luckily for us, eq_refl l delivers a proof that l is equal to itself so we can apply the match to that and get back our initial list nat.
Looking at the branches of the match, we can see that:
In the nil case, you can ignore the extra Hypothesis which you don't need.
In the cons case, it provides you precisely the much needed hypothesis and you can discharge your proof obligation like so:
apply H.
rewrite Hyp.
simpl.
apply le_lt_n_Sm.
apply drop_lemma_le.
Defined.