The Coq mailing list

[David Pichardie <david.pichardie AT inria.fr>]

Dear David,

Here is a solution using Function.

Note that Function fails to generate the right induction principle if  
you dont put H as a variable in a section before (beware that now S  
and H have been swapped). For your lemma, the fixpoint equation would  
have been enough but the powerfull induction principle generated by  
Function should helps
for more complex properties.

Hope this helps,

(* In a world-of-dream, the functionnality of Function and Program  
would be merged :-) *)

David.


----------------------------------------------------------------

Require Import FSetInterface.
Require Import FSetProperties.
Require Import FSetDecide.
Require Import Recdef.

Module FSetsProgram(X:FSetInterface.WS).

 Import X.

 Module Xp := Properties(X).
 Module Xd := Decide(X).

 Section H.
   Variable H:X.t.

 Function add_to_set_not_in (S:X.t) { measure X.cardinal S} : X.t :=
   match X.choose S with
     | None => X.empty
     | Some x => if Xp.In_dec x H then add_to_set_not_in (X.remove x S)
                 else X.add x (add_to_set_not_in (X.remove x S))
   end.
  (* first obligation *)
   intros S x Heq_anonymous i Hi.
   apply X.choose_1 in Heq_anonymous.
   rewrite <- (Xp.remove_cardinal_1 Heq_anonymous).
   omega.
  (* second obligation *)
   intros S x Heq_anonymous i Hi.
   apply X.choose_1 in Heq_anonymous.
   rewrite <- (Xp.remove_cardinal_1 Heq_anonymous).
   omega.
 Qed.
 End H.

 Import Xd.

 Lemma teste : X.Equal (add_to_set_not_in X.empty X.empty) X.empty.
 Proof.
   assert (Aux:forall H S,
     H [=] X.empty -> S [=] X.empty ->
     X.Equal (add_to_set_not_in H S) X.empty).
   intros H S.
   functional induction (add_to_set_not_in H S); intros.
   (* 3 simple cases are generated. Note we don't need the induction  
hypothesis here *)
     fsetdec.

     apply False_ind.
     fsetdec.

     assert (In x S) by (apply choose_1; auto).
     apply False_ind.
     fsetdec.

   (* At last we use the auxiliary result to conclude *)
   apply Aux; fsetdec.
 Qed.

End FSetsProgram.




Le 8 nov. 10 à 18:19, David Pereira a écrit :

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