```
Inductive natoption : Type :=
| Some : nat -> natoption
| Nothing : natoption.
```

I have used natoption in a function and get following list

l= [Some 4;Nothing;Some 8;Nothing]

I want to change list

l'= [4 ; 0; 8,0] . Want to remove "some" and"replace Nothing with 0". How I can do it?

Here is a possibility:

```
From Coq Require Import List.
Import ListNotations.
Inductive natoption : Type :=
| Some : nat -> natoption
| Nothing : natoption.
Definition natoption_to_default default o :=
match o with
| Nothing => default
| Some n => n
end.
Eval cbn in (map (natoption_to_default 0) [Some 4;Nothing;Some 8;Nothing]).
```

Note you could use `option nat`

instead of `natoption`

.

(deleted)

I have list of natoption, like this

[Some 4, None , Some 6, Some 3, Some 1]. Want to check x (x:nat) presence in the list natoption. I have problem in list reading

```
Fixpoint find (x:nat)(l:list natoption):bool:=
match l with
|None => false
|cons(Some x') t => if (eq x x' ) then true else find x t
end.
```

While eq is another function which compares nat & Some nat and give true in case if they are equal.

There are 3 different problems here:

- The empty list is
`nil`

not`None`

. - The
`match`

should be exhaustive: either the list is empty, or it starts with a`Some _`

element or it starts with a`Nothing`

element (this last case is missing). - The simplest way of making the
`if`

work here is to give it a`bool`

argument. The function testing equality on`nat`

and returning a`bool`

is`Nat.eqb`

, thus you should use`Nat.eqb`

rather than`eq`

in the`if`

statement.

It seems you have changed the definition of `natoption`

. Are you using something like:

```
Notation natoption := (option nat).
```

If so, replace `Nothing`

by `None`

in my previous comment.

Thank you.But now this is the problem

[Some 4,Some 1,None];[[Some 6,Some 1,Some 8];[None,None,None]...]

I have a list of list options.Want to check the presence of option x ( may be none or Some x) in the above list

1)Is there any need to check x may be none

2)elements within the list should be same?

3)How I can terminate the list?

Does this code correspond to what you wanted ?

```
Require Import Arith List.
Import ListNotations.
(** Is [Some x] a member of [l] *)
Fixpoint mem_opt (x:nat) (l:list (option nat)) : bool:=
match l with
nil => false
| None:: l' => mem_opt x l'
| Some y :: l' =>
match Nat.eq_dec x y with left _ => true | _ => mem_opt x l' end
end.
Compute mem_opt 5 [Some 6; None; Some 5; None].
Definition test_opt (x:nat) (ls : list (list (option nat))) : bool :=
existsb (fun l => mem_opt x l) ls.
Compute test_opt 4 [[Some 5; None]; [None;Some 4;None]].
```

You may easily replace the type `nat`

with any type `A`

where equality is decidable. Have a look at the module `List`

of standard library .

Plz ,explain the function of this line [Nat.eq_dec x y with left _ => true | _ =>]

Perhaps it's better written like this:

```
match Nat.eq_dec x y with
| left _ => true
| _ => mem_opt x l'
end
```

If x = y then the bool is true, if x not equal to y then we call mem_opt on the smaller list.

`Nat.eq_dec x y`

has type `{x=y}+{x<>y}`

(see type `sumbool`

in a tutorial, book or reference manual).

So this term may have two forms : either `left H`

, where `H: x=y`

, or `right H'`

, where `H': x<>y`

.

It corresponds more or less to `if Nat.eqb x y then true else mem_opt x l`

, which works also, but with less information than

the `sumbool`

form.

Thank you. This function reads a list but I have list of list in above.

zohaze said:

Thank you. When I apply this function to another inductive type point instead of nat. Then I have this error message

`Fixpoint mem_opt (x:point) (l:list (option point)) : bool:= match l with nil => false | None:: l' => mem_opt x l' | Some y :: l' => if eq_points x y then true else mem_opt x l' end.`

I have function eq_points, which gives true if x y are equal else false.

Error : Found a constructor of inductive type point while a constructor of list

is expected.

Are you sure? The following code works.

```
Require Import Arith List Bool.
Import ListNotations.
Record point : Set :=
{x: nat; y: nat}.
Definition point_eqb (A B: point) :=
Nat.eqb (x A) (x B) && Nat.eqb (y A) (y B).
Fixpoint mem_opt (x:point) (l:list (option point)) : bool:=
match l with
nil => false
| None:: l' => mem_opt x l'
| Some y :: l' =>
if point_eqb x y then true else mem_opt x l'
end.
```

Just for information, a version with `sumbool`

instead of `bool`

.

```
Definition point_eq_dec (A B: point): {A=B}+{A<> B}.
repeat decide equality.
Defined.
Definition point_opt_eq_dec (x y: option point): {x=y}+{x <> y}.
Proof.
decide equality.
apply point_eq_dec.
Defined.
Definition mem_opt_dec (x:point) (l:list (option point)) :
{In (Some x) l} + {~In (Some x) l}.
Proof.
induction l.
- right; tauto.
- destruct IHl as [Hin | HnotIn].
+ left; cbn; auto.
+ destruct (point_opt_eq_dec (Some x) a) as [e | n].
* rewrite e; left; now constructor.
* right; red; destruct 1; congruence.
Defined.
```

This is ok but still it reads list of nat or list of points not list (natoption list ) or list(pointoption list)

Perhaps I didn't understand what you want to compute. If I adapt to `point`

a function I already sent ( with `nat`

),

I get:

```
Definition f (x: point) (ls: list (list (option point))) :=
existsb (fun l => mem_opt x l) ls.
Check f.
(* f : point -> list (list (option point)) -> bool
*)
```

OK, It works . thanks

zohaze said:

OK, It works . thanks

Just for the record, there exists another style for solving the problem you submitted.

- generalize the type
`point`

or`nat`

to any type`A`

where equality is decidable (polymorphism) - replacing booleans whith
`sumbools`

this way, the type of`mem_opt_list_dec`

is indeed its specification, and this function is correct by construction (while you still have to prove the correctness of the version with booleans).

Don't worry if it looks too complex at first sight :thinking:

```
Require Import Arith List Bool.
Import ListNotations.
Definition decide (P:Prop) := {P}+{~P}.
Section MemOpt.
Variable (A:Type).
Variable A_eq_dec : forall a b:A, decide (a = b).
Definition A_opt_eq_dec : forall x y : option A, decide (x=y).
Proof.
red; decide equality; apply A_eq_dec.
Defined.
Definition mem_opt_dec (x:A) (l:list (option A)) :
decide (In (Some x) l).
Proof.
induction l.
- right; tauto.
- destruct IHl as [Hin | HnotIn].
+ left; cbn; auto.
+ destruct (A_opt_eq_dec (Some x) a) as [e | n].
* rewrite e; left; now constructor.
* right; red; destruct 1; congruence.
Defined.
(** [Some x] belongs to some list [l] which belongs to [ls] *)
Definition mem_deep x (ls:list (list (option A))) :=
Exists (fun l => In (Some x) l) ls.
Definition mem_opt_list_dec (x:A) (ls: list (list (option A))) :
decide (mem_deep x ls).
Proof.
unfold mem_deep; induction ls.
- right; rewrite Exists_nil; auto.
- destruct IHls as [e | n].
+ left; destruct e.
* right; left; assumption.
* right; right; assumption.
+ destruct (mem_opt_dec x a).
* left; now left.
* right;red; inversion_clear 1; tauto.
Defined.
End MemOpt.
Check mem_opt_list_dec.
Check mem_opt_list_dec nat Nat.eq_dec.
Record point : Set :=
{x: nat; y: nat}.
Definition point_eq_dec (A B: point) : decide (A=B).
Proof.
red; repeat decide equality.
Defined.
Check mem_opt_list_dec _ point_eq_dec.
```

One may also use type classes, but that's another story.

you don't need to hand-make those deciders, you can just do

```
Definition mem_opt_dec (x:A) (l:list (option A)) :
decide (In (Some x) l)
:= in_dec A_opt_eq_dec _ l.
Definition mem_opt_list_dec (x:A) (ls: list (list (option A))) :
decide (mem_deep x ls)
:= Exists_dec _ _ (mem_opt_dec _).
```

Last updated: Jun 18 2024 at 22:01 UTC