both possibilities exist? · Coq users

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

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 ListCoq 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):

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

Stream: Coq users

Topic: both possibilities exist?