The Coq mailing list

[David Pereira <dpereira AT liacc.up.pt>]

Dear all,

I am experimenting with Program Fixpoint feature of Coq for building 
functions on finite sets. I have implemented this simpl function 
[add_to_set_not_in], whose termination criteria was very easy to prove. The 
code is the following:

Module FSetsProgram(X:FSetInterface.WS).

  Import X.

  Module Xp := Properties(X).
  Module Xd := Decide(X).
  
  Program Fixpoint add_to_set_not_in (S:X.t)(H:X.t) { measure X.cardinal S} : 
X.t :=
    match X.choose S with
      | None => X.empty
      | Some x => match Xp.In_dec x H with
                    | left  _ => add_to_set_not_in (X.remove x S) H
                    | right _ => X.add x (add_to_set_not_in (X.remove x S) H)
                  end
    end.
  Next Obligation.
    symmetry in Heq_anonymous.
    apply X.choose_1 in Heq_anonymous.
    rewrite <- (Xp.remove_cardinal_1 Heq_anonymous).
    omega.
  Defined.
  Next Obligation.
    symmetry in Heq_anonymous.
    apply X.choose_1 in Heq_anonymous.
    rewrite <- (Xp.remove_cardinal_1 Heq_anonymous).
    omega.
  Defined.

  Lemma teste : X.Equal (add_to_set_not_in X.empty X.empty) X.empty.
  Proof.
        admit. (* struck here *)
  Qed.

End FSetsProgram.

I am currently struck in the lemma [teste], although it is a very simple 
property. Is there any standard tricks for reasoning about terms built using 
the Program Fixpoint construction?

Any help is very appreciated :)

Best reagards,
   David.