zohaze (Jan 28 2023 at 07:22): zohaze (Jan 28 2023 at 07:22):Fixpoint f1 (a b c d: nat) (l: list nat) : bool :=
match (f2 c d l) with
| nil => true
|h::nil => false
|h::h1::t => match (.... ) a' b' c' d' t
end
end.
output of (f2 c d l)= list nat
During execution get message "does not find decreasing argument."
Reason for this error is due to use of same l in f1 input arguments and in f2 ?
Actually i am decreasing the element of list generated by (f2 c d l) on each call.
How i can correct this ?
Michael Soegtrop (Jan 28 2023 at 09:12):f2 could do anything to the list, say c::d::l. Then you would already increase in the outer match. Coq checks the definition of f2 but can't figure out that it f2 does not increase l. To make Coq accept it, you could use Program Fixpoint and add { measure (length l) }. Then Coq asks you to prove that length l is actually decreasing. You can put your knowledge about what f2 does to l in there.
zohaze (Jan 29 2023 at 06:08):Thanks .
1)f2 c d l is a function which generates nat list by using c d l ( like [6;7;8;9;20]) , c d are not the first and second element of list.
2)By each recursive call number of elements of above list are decreashing.
3) According to your reply , i have tried this
i) match (length (f2 c d l)
i ) Found a constructor of inductive type list while a constructor of nat is expected.
ii) { { measure (length f2 c d l )} get message Unknown interpretation for notation "{ _ }".
Michael Soegtrop (Jan 29 2023 at 09:26):You put quite a burden on those who want to help you by not providing minimal examples of your issue. When you have problems with Coq syntax I can't guess what you are doing wrong when you don't give an example. Just saying "measure gives error xyz" is in now way helpful. Please provide a minimal example which gives this error message.
In general when you ask questions here you should really spend a few minutes to strip down your code to a minimal example - replacing functions with stubs and the like - to present something which compiles. Otherwise you ask several people to spend several times the time you would need to do this (because you know your stuff) to help you. In total this is easily more than 10x the time you would need for this. This is not very polite and if you continue to drag unreasonable amounts of time form people, they will stop helping you. In the end this will also be more effective for you, because you get useful answers the first time.
You can find some examples on using measure in this tutorial session: https://fzn.fr/teaching/coq/ecole10/summer/lectures/lec10.pdf.
zohaze (Jan 30 2023 at 14:45):I have simplified the code like this. I am adding two in each element of list ,which is the output of remove one function till it converges to its end. List s contains multiple nat v.
Fixpoint remove_one (v:nat) (s:list nat) : list nat :=
match s with
| [] => []
| h :: t => if beq_nat v h then t else h :: remove_one v t
end.
Fixpoint f2 (d: nat) (l: list nat) : bool :=
match (remove_one d l) with
| nil => true
|h::t2 => f2 (S(S d)) t2
end .
Cannot guess decreasing argument of fix.
Pierre Castéran (Jan 30 2023 at 16:46):With Function (you may also use Equations, or Program Fixpoint).
Fixpoint remove_one (v:nat) (s:list nat) : list nat :=
match s with
| [] => []
| h :: t => if Nat.eqb v h then t else h :: remove_one v t
end.
Lemma remove_one_leq (v:nat) (s: list nat) :
length (remove_one v s) <= length s.
Proof.
induction s; simpl.
- auto with arith.
- case (v =? a); simpl; auto with arith.
Qed.
Require Import Recdef.
Function f2 (d: nat) (l: list nat) {measure length l} : bool :=
match (remove_one d l) with
| nil => true
| h::t2 => f2 (S(S d)) t2
end .
Proof.
intros.
apply Nat.lt_le_trans with (length (h::t2)).
- simpl; auto with arith.
- rewrite <- teq. apply remove_one_leq.
Defined.
Your function f2 always returns true, whichever its arguments. Is this what you wanted to define ?
Last updated: Sep 23 2023 at 07:01 UTC