In a l has proposition output data type. How i can find its bool equivalent in library?

You would need a decider for equality on the base type to do that, because `In x [y]`

is equivalent to `x = y`

.

You may use Stdlib's `List.In_dec`

and convert the result into a boolean.

```
Require Import List ListDec.
Import ListNotations.
Definition memb {A}
(Aeq_dec : forall a b: A, {a = b} + {a <> b}) x l :=
match In_dec Aeq_dec x l
with left _ => true | right _ => false end.
Compute memb Nat.eq_dec 4 [3;6;8;4;0].
Compute memb Nat.eq_dec 14 [3;6;8;4;0].
Lemma memb_ok {A} Aeq_dec :
forall (x:A) l, memb Aeq_dec x l = true <-> In x l.
Proof.
unfold memb; intros x l; destruct ( In_dec Aeq_dec x l).
- tauto.
- split; try discriminate; tauto.
Qed.
```

If i use above definition then i will be able to use all lemmas related to In from standard library? When i execute the above code i get this message " The reference Nat.eq_dec was not found in the current environment."

I have another data type (instead of nat) . I have defined function for the equlaity of two values. But i want to use memb function

to prove equality. When i write it as memb a l6, i get this message

" The term "a" has type "value" while it is expected to have type "forall a b : ?value, {a = b} + {a <> b}".

You may do `Require Import Arith`

to get `Nat.eq_dec`

.

```
Compute memb Nat.eq_dec 3 [2;3;4].
```

Please note that `memb`

takes three arguments (as in the example above).

Last updated: Oct 04 2023 at 21:01 UTC