The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

Hi all,

As part of a larger proof, I needed to show that adding A then B to a
set is the same as adding B then A to the set (with some extra
equalities floating round). This feels like there should be a 1-line
solution, but I couldn't find one. I've extracted what I did as a
standalone proof below, and I was wondering if anyone could tell me how
I can do it more simply, please?


Require Import FSetWeakList.

Parameter Name : Set.
Axiom eq_Name_dec : forall (n : Name) (o : Name), {n = o} + {n <> o}.

Module DecidableName.
Definition t := Name.
Definition eq := @eq Name.
Definition eq_refl := @refl_equal Name.
Definition eq_sym := @sym_eq Name.
Definition eq_trans := @trans_eq Name.
Definition eq_dec := eq_Name_dec.
End DecidableName.

Module NameSet := Make(DecidableName).

Lemma Foo :
      forall (o oa oab : NameSet.t) (a b : Name),
      NameSet.Equal oa (NameSet.add a o) ->
      NameSet.Equal oab (NameSet.add b oa) ->
      NameSet.Equal oab (NameSet.add a (NameSet.add b o)).
Proof with auto.
intros o oa oab a b oaDef oabDef.
unfold NameSet.Equal.
intro n.
split.
    destruct (eq_Name_dec a n).
        (* n = a *)
        subst.
        intro a_in_oab.
        apply NameSet.add_1...
    destruct (eq_Name_dec b n).
        (* n = b *)
        subst.
        intro b_in_oab.
        apply NameSet.add_2.
        apply NameSet.add_1...
    (* n <> a /\ n <> b *)
    intro H.
    apply (proj1 (oabDef n)) in H.
    apply NameSet.add_3 in H...
    apply (proj1 (oaDef n)) in H.
    apply NameSet.add_3 in H...
    apply NameSet.add_2.
    apply NameSet.add_2...
intro H.
destruct (eq_Name_dec a n).
    (* n = a *)
    subst.
    apply (proj2 (oabDef n)).
    apply NameSet.add_2.
    apply (proj2 (oaDef n)).
    apply NameSet.add_1...
destruct (eq_Name_dec b n).
    (* n = b *)
    subst.
    apply (proj2 (oabDef n)).
    apply NameSet.add_1...
(* n <> a /\ n <> b *)
apply NameSet.add_3 in H...
apply NameSet.add_3 in H...
apply (proj2 (oabDef n)).
apply NameSet.add_2.
apply (proj2 (oaDef n)).
apply NameSet.add_2...
Qed.