## Stream: Coq users

### Topic: options

#### zohaze (Dec 30 2021 at 17:52):

``````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?

#### Olivier Laurent (Dec 30 2021 at 18:00):

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)

#### zohaze (Jan 08 2022 at 08:11):

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.

#### Olivier Laurent (Jan 08 2022 at 08:19):

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.

#### Olivier Laurent (Jan 08 2022 at 08:26):

It seems you have changed the definition of `natoption`. Are you using something like:

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

#### Olivier Laurent (Jan 08 2022 at 08:31):

If so, replace `Nothing` by `None` in my previous comment.

#### zohaze (Jan 10 2022 at 17:27):

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?

#### Pierre Castéran (Jan 10 2022 at 20:32):

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 .

#### zohaze (Jan 11 2022 at 17:15):

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

#### Ali Caglayan (Jan 11 2022 at 20:19):

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.

#### Pierre Castéran (Jan 11 2022 at 20:21):

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

#### zohaze (Jan 12 2022 at 07:38):

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

#### Pierre Castéran (Jan 12 2022 at 08:01):

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

#### zohaze (Jan 12 2022 at 08:10):

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

#### Pierre Castéran (Jan 12 2022 at 08:24):

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

#### zohaze (Jan 12 2022 at 14:23):

OK, It works . thanks

#### Pierre Castéran (Jan 12 2022 at 18:10):

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.

#### Gaëtan Gilbert (Jan 12 2022 at 18:26):

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: Jan 27 2023 at 02:04 UTC