CODEWITHSUNDEEP
coq
Lisa
Lisa

Reputation: 227

about the order of the elements in a set

I have the following definitions:

Definition n : set string := ("a" :: "b" :: nil).
Definition m : set (set string) := ("b" :: "a" :: nil) :: ("c" :: "d" :: nil) :: nil.

I try to prove the following:

Example n_in_m : set_In n m.
Proof.
  unfold n . unfold m.
  simpl.

after doing 'simpl', the goal becomes:

"b" :: "a" :: nil = "a" :: "b" :: nil \/
"c" :: "d" :: nil = "a" :: "b" :: nil \/ False

then i don't know how to go on the proof! Is it right the order of the element in a set doesn't matter?

Upvotes: 0

Views: 61

Answers (1)

Ptival
Ptival

Reputation: 9437

It seems that you are trying to prove that:

{a, b} ∈ { {b, a}, {c, d} }

but your set membership is defined with regards to propositional equality. The problem is that the two objects:

("a" :: "b" :: nil)

and:

("b" :: "a" :: nil)

are not propositionally equal.

You probably want to use instead a richer definition for set, one that is parameterized by when two elements are to be considered equal.

Upvotes: 1

Related Questions