Fixpoint myfunction ( l: list nat) : list nat :=
match l with
| nil => nil
|h::t => match (here code requires h and next of h) with
|false => []
|true => h1:: myfunction t
end
end.
Want to keep list of h1 in true (case). e.g l=[2,33,41,5,66,7] require list [33,41,5,66,7] .
If i write h::h1::t then i have to add third constructor h::nil . This case gives wrong results when there are
odd elements in input list.
You need to define what happens in the case the list has exactly 1 element, because if the list length is odd, you will end up in this case. So you need a match structure like:
match l with
| nil => nil
| h::nil => what do we do here?
| h1::h2::t => the usual case
end
Fixpoint myfunction ( l l2: list nat) : list nat :=
match l with
| nil => nil
||h::nil => [h]
|h1::h2::t => match (leb h2 ( count h1 l2) ) with
|false => []
|true => h2:: myfunction t l2
end
end.
I need first &next element of complete list for comaparison (list may contain even or odd elements).
1) h1::h2::t ->during recursive call there is jump/skip of two elements.
e.g l=[2,33,41,5,66,7,8] output list = [33 ] t=[41,5,66,7,8].
During next recursion h1=41 & h2= 5 output list = [33,5 ]
But i need [33,41, 5 ]
2) How i should append element of constructor 2 with list of constructor 3, or correct the above?
You can pass (h2::t) as argument to the recursive call (or (h1::t) since you prepend h2 in the recursive call). You need to give a measure then (as explained before). Coq won't be able to figure out automatically that the list is decreasing, but the proof will be trivial.
You may use the as
keyword like in
Fixpoint f (l: list nat) :list nat :=
match l with
| nil => nil
| [x] => [x]
| h1::((h2::t) as tl) => if p h1 h2
then h1 :: f tl (* skips 1 element *)
else h2 :: h1 :: f t (* skips 2 elements *)
end.
Lot of thanks.
I want to adjust function (fun a b l) in above . Output
of this function is list which gives nil in case of one element in the list and in empty case). I am replacing l with (fun a b l) then second constructor [x]=> [x] gives problem. May i address it? error msg: cannot find decreasing value.
Fixpoint f (a b:nat) (l: list nat) :list nat :=
match (fun a b l) with
| nil => nil
| [x] => [x] (* according to modification it should be nil in case of one element *)
| h1::((h2::t) as tl) => if p h1 h2
then h1 :: f a b tl (* skips 1 element *)
else h2 :: h1 :: f a b t (* skips 2 elements *)
end.
This looks ok :
Require Import List.
Import ListNotations.
Parameter p : nat -> nat -> bool.
Fixpoint f (a b:nat) (l: list nat) : list nat :=
match l with
| nil => nil
| [x] => [x] (* according to modification it should be nil in case of one element *)
| h1::((h2::t) as tl) => if p h1 h2
then h1 :: f a b tl (* skips 1 element *)
else h2 :: h1 :: f a b t (* skips 2 elements *)
end.
output list of (fun a b l) is different list than input argument list l.Secondly, output of (fun a b l) is empty when it contains one element and or when it is empty. But input argument list l is empty only when this list is empty.Third,in recursive call tl should be assign to input argument list l which causes conflict with output of (fun a b l). Introduction of two lists , one for fun ab l and second for recursive call . (could be solution?0
Fixpoint f (a b:nat) (l l2: list nat) :list nat :=
match (F a b l) with
| nil => nil
| [x] => [x] (* problem here, according to modification it should be nil in case of one element in new definition *)
| h1::((h2::t) as tl) => if eq h1 h2
then h1 :: f a b l tl (* skips 1 element *)
else h2 :: h1 :: f a b l t
May be you should assume (or prove with your example) that length (F a b l) <= length l
. (I renamed fun
into F
because fun
is a Coq keyword). Here's a simple example (you may have to change the definitions of F
and p
).
Note that your definitions present some problems (in addition to the recursion):
The arguments a
, b
and l
keep the same value during all the computation, and l2
is unused.
So, it's extremely difficult to understand and comment what you wanted to compute.
Require Import Arith Lia List Recdef .
Import ListNotations.
Definition F a b l := map (fun x => x + a + b) l.
Remark Fdecr : forall a b l, length (F a b l) <= length l.
Proof.
intros; unfold F; now rewrite map_length.
Qed.
Definition p : nat -> nat -> bool := Nat.ltb.
Function f (a b: nat) (l: list nat) {measure length l} : list nat :=
match (F a b l) with
nil | [_] => nil
| x:: ( (y:: t) as tl) => if p x y then x :: f a b tl
else y :: x :: f a b t
end.
Proof.
intros.
generalize (Fdecr a b l) ;rewrite teq; simpl; lia.
intros.
generalize (Fdecr a b l); rewrite teq; simpl; lia.
Defined.
(* Example *)
Compute f 10 20 [4;6;3;7].
(deleted)
Last updated: Oct 13 2024 at 01:02 UTC