l = [3,5,7,8,9]

Definition value (a b : nat)(l:list nat) : bool :=

match l with

| nil => false

| h::nil => true

| h::h1::t =>

Here h=3,h1=5

Definition b :=7.

Definition value (a b : nat)(l:list nat) : bool :=

match l with

| nil => false

| b::h1::t =>

Could i start from 7 ? Then h1 will be 8?

No, the match is made on the whole list

```
Require Import List.
Definition l := 3 :: 5 :: 7 ::8 :: 9 :: nil.
Compute (match l with 3 :: tl => true | _ => false end ).
Compute (match l with 7 :: tl => true | _ => false end ).
```

@zohaze If you want to match a list starting from a given element, you may use a function like below:

```
Fixpoint remove_before n (l: list nat) :=
match l with
| nil => nil
| p:: tl => if Nat.eq_dec n p then l else remove_before n tl
end.
Compute match remove_before 5 [1;2;3;4;5;6;8]
with (_::h1::_) => Some h1
| _ => None
end.
Compute match remove_before 51 [1;2;3;4;5;6;8]
with (_::h1::_) => Some h1
| _ => None
end.
```

Thanks. List starts from particular no (a) and to reach a number b,which may be next to head of list or end or in between . Should I define another function or recursive call is sufficient?

Fixpoint selected (a b : nat) (l: list nat) : bool :=

match l with

| nil => false

| h::t => match (remove_before a l) with

|[]=>false (*no need of this constructor still have error "no patteren for [] " *)

| h::nil => false (*now h=a and b is missing*)

| h1::h2::t => match (Nat.eq h2 b) with (* now h2 or any element of t could be b*)

|true=> true

|false => selected h2 b t with (* define function which output a list when reached to b*)

Here is a possible solution, but I can't be sure it corresponds with your specification.

If it doesn't, please feel free to improve it, using functions from `List`

Coq library.

The problem with informal or semi-formal specifications is that we can interpret them in a wrong way and post useless answers.

Note that this thread is not really about Coq, but about functional programming (which is a pre-requisite to Coq).

```
Fixpoint remove_before n (l: list nat) :=
match l with
| nil => nil
| p:: tl => if Nat.eq_dec n p then l else remove_before n tl
end.
Fixpoint rev_until n (l:list nat) r :=
match l with
nil => nil
| p::l' => if Nat.eq_dec n p then (p::r) else rev_until n l' (p::r)
end.
Compute rev_until 5 [1;2;3;4;5;6;7] nil.
Definition f a b l :=
match remove_before a l with
nil => None
| l' =>
match rev_until b l' nil
with
nil => None
| l'' => Some (rev l'')
end
end.
Compute f 3 5 [1;2;3;4;10; 5;6;8].
Compute f 3 11 [1;2;3;4;10; 5;6;8].
Compute f 33 11 [1;2;3;4;10; 5;6;8].
```

In order to map the values of (f a b l ) to a list , i have to remove option some & none. Or simply consider l' case with function (rev_until b l' nil). Or simply use rev_until to map the values on the list.

Something like that ?

```
Definition f' a b l :=
match f a b l with
Some l' => l'
| None => nil
end.
Definition f_OK a b l : bool :=
match f a b l
with
Some _ => true
| _ => false
end.
Compute f' 3 5 [1;2;3;4;10; 5;6;8].
Compute f' 3 11 [1;2;3;4;10; 5;6;8].
Compute f_OK 3 5 [1;2;3;4;10; 5;6;8].
Compute f_OK 3 11 [1;2;3;4;10; 5;6;8].
```

This simply removed option. I am asking how i can map result of above function on elements of list like

Definition f' a b l := map (fun x => ...) l.

Last updated: Jun 24 2024 at 12:02 UTC