## Stream: Coq users

### Topic: both possibilities exist?

#### zohaze (Jan 25 2023 at 08:39):

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?

#### Laurent Théry (Jan 25 2023 at 09:10):

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 ).
``````

#### Pierre Castéran (Jan 25 2023 at 10:17):

@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.
``````

#### zohaze (Jan 25 2023 at 17:13):

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*)

#### Pierre Castéran (Jan 26 2023 at 12:18):

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].
``````

#### zohaze (Feb 26 2023 at 05:41):

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.

#### Pierre Castéran (Feb 26 2023 at 07:33):

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].
``````

#### zohaze (Feb 26 2023 at 17:33):

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