zohaze (Dec 30 2021 at 17:52): 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.
zohaze (Dec 31 2021 at 07:42):(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:
nil not None.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).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).
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 natwith any type Awhere equality is decidable. Have a look at the module Listof 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 sumboolform.
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 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.
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
*)
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.
pointor natto any type Awhere equality is decidable (polymorphism)sumboolsmem_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: Sep 30 2023 at 06:01 UTC