The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi list,

This is not a FSet specific questions, more a design question for a
library. Any comment would be appreciated.

Using FSets, consider the following (simplified) goal:
<---
Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1 else 2)= 1.
-->

It can be solved, using by doing a case elimination on the result of
mem ...But relying on case_eq can become tedious, if there are several
such destruction to do. Moreover, you need fruther work if you want to
transform this information (mem x s= true) into something more
"useful" (like In x s).

Moreover, you really want the result of mem to be a boolean, if you
want to build effective functions inside coq, and you can't ask to
have mem of type [ x : elt -> s : t -> {In x s} + {~In x s}, which
would be more informative, I think.

Therefore, I came up with the following scheme of specifications,
<---
Lemma mem_spec : forall x s, {In x s} + {~ In x s}. (* Proofs omitted
*) Admitted.
Lemma mem_proj : forall x s, mem x s = proj_sumbool (mem_dec x s). (*
Proofs omitted *) Admitted.
-->
and I ended up with automation tactics trying to rewrite this kind of
lemma wherever they could, and destroying the resulting *_spec lemmas
(which can be arbitrarily informative, like one would write when
defining strongly specified functions)

I was then told that I could use inductives, to do the same job.
<--
Inductive mem_spec_ind : elt -> t -> bool -> Type :=
    | mem_spec_1 : forall x s, In x s -> mem_spec_ind x s true
    | mem_spec_2 : forall x s, ~In x s -> mem_spec_ind x s false.
Lemma mem_eq : forall x s, mem_spec_ind x s (mem x s). Admitted.
-->

Unfortunately, "destruct"-ing mem_eq in a Goal can lead to the
forgetting of useful informations. I have to remember some pieces of
information by hand, while everything is smoother using the
rewrite-destruct scheme.

The goal here would be to be able to automatize such destructions, in
order to be able to reason more easily on more complicated programs. I
wonder if any function should have such a specification (like add,
below).
Inductive add_spec : elt -> t -> t -> Type :=
| add_spec_1 : forall x s s', (forall y, In y s' <-> (E.eq x y \/ In y
s)) -> add_spec x s s'.
Lemma add_eq : forall x s, add_spec x s (add x s).

Any comment would be appreciated.
Best regards,
Thomas Braibant




<-------------------------------- Complete script
--------------------------------------->
Module Test (X : FSetInterface.S).
  Module OrdProps := FSetProperties.OrdProperties X.
  Module EqProps := FSetEqProperties.EqProperties X.
  Module Props := EqProps.MP.
  Module Facts  := Props.FM.
  Module Dec := Props.Dec.

  Include Facts.
  Include OrdProps.
  Import  X.
  Ltac setdec := Dec.fsetdec.

  Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1
else 2)= 1.
    intros.
    case_eq (mem z (add x (add y (singleton z)))); intro H.
      reflexivity.
      apply False_ind. revert H. rewrite <- not_mem_iff. set_iff. intuition.
  Qed.
  Lemma mem_dec : forall x s, {In x s} + {~ In x s}. Admitted.
  Lemma mem_proj : forall x s, mem x s = proj_sumbool (mem_dec x s).  
Admitted.

  Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1
else 2)= 1.
    intros.
    rewrite mem_proj. destruct mem_dec. reflexivity.
    apply False_ind. apply n. set_iff. intuition.
  Qed.

  Inductive mem_spec_ind : elt -> t -> bool -> Type :=
    | mem_spec_1 : forall x s, In x s -> mem_spec_ind x s true
    | mem_spec_2 : forall x s, ~In x s -> mem_spec_ind x s false.
  Lemma mem_eq : forall x s, mem_spec_ind x s (mem x s). Admitted.

  Goal forall x y z , (if mem z (add x (add y (singleton z))) then 1
else 2)= 1.
    intros.
    remember (add x (add y (singleton z))). (* remember is needed here *)
    destruct (mem_eq z t0). reflexivity. subst. apply False_ind. apply
n. setdec.
  Qed.

  Inductive add_spec : elt -> t -> t -> Type :=
  | add_spec_1 : forall x s s', (forall y, In y s' <-> (E.eq x y \/ In
y s)) -> add_spec x s s'.

  Lemma add_eq : forall x s, add_spec x s (add x s).
  Proof.
    intros.
    constructor.  intros. set_iff. reflexivity.
  Qed.

End Test.

thomas braibant