Stream: Coq users

Topic: app function in list

sara lee (Jan 04 2022 at 17:01):

I have two lists l1 & l2 (with options)
l1=[some 4,nil,some 3,nil], l2=[some 5,some 3,nil,nil], want to add them so that nil is not present in the list (append l1 l2).
I have used skipn function from library (to skip nil). But have problem(termination)

Pierre Castéran (Jan 04 2022 at 17:41):

Are you sure you don't mistake nilwith None?
A typical list of type option A contains elements of the form Some aor None.
The function which removes the Nones from a list is an application of filterand not skipn.

Definition remove_none {A} :=
      filter  (fun (x:option A) => match  x with   None => false   | _ => true    end).

Compute remove_none (Some 33 :: None :: Some 45 :: None :: nil).

Moreover, filter commutes with app:

Search filter app.
(*
filter_app:
  forall [A : Type] (f : A -> bool) (l l' : list A),
  filter f (l ++ l') = filter f l ++ filter f l'  *)

sara lee (Jan 04 2022 at 18:12):

By mistake wrote nil instead of none. Without removing none, can I add two lists and bool at output in case of some x present in the list?

sara lee (Jan 05 2022 at 17:54):

Definition f1(t:radius):list options:=
match t with
|r1 =>(Some 33 :: None :: Some 45 :: None :: nil)
|r2 =>(Some 3 :: None :: Some 5 :: Some 5 :: nil)
end.

I want to check that some d how many times exist in the list options (in case of r1 & r2 ) .I don't know how to write. Check the existence of some d in the list option?

Last updated: Sep 30 2023 at 06:01 UTC