Stream: Coq users

Topic: options


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip zohaze (Dec 31 2021 at 07:42):

(deleted)

view this post on Zulip 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.

view this post on Zulip Olivier Laurent (Jan 08 2022 at 08:19):

There are 3 different problems here:

view this post on Zulip 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).

view this post on Zulip Olivier Laurent (Jan 08 2022 at 08:31):

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

view this post on Zulip 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?

view this post on Zulip 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 natwith any type Awhere equality is decidable. Have a look at the module Listof standard library .

view this post on Zulip zohaze (Jan 11 2022 at 17:15):

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

view this post on Zulip 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.

view this post on Zulip 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 sumboolform.

view this post on Zulip zohaze (Jan 12 2022 at 07:38):

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

view this post on Zulip 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 sumboolinstead 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.

view this post on Zulip 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)

view this post on Zulip 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
*)

view this post on Zulip zohaze (Jan 12 2022 at 14:23):

OK, It works . thanks

view this post on Zulip 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.

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.

view this post on Zulip 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