Stream: Coq users

Topic: equal to In

pianke (Mar 16 2023 at 04:15):

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

Dominique Larchey-Wendling (Mar 16 2023 at 10:34):

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

Pierre Castéran (Mar 16 2023 at 11:40):

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.

pianke (Mar 29 2023 at 17:01):

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

zohaze (Mar 29 2023 at 17:42):

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}".

Pierre Castéran (Mar 29 2023 at 20:44):

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