The Coq mailing list

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

> Sorry if I was not clear. Of course, you do not have to perform the proofs
> by yourself, I was only speaking about a problem of computation:
>
> - even if computation is rather good in Coq, it takes some time...

Could you elaborate more on the kind of examples that take so much
time ? In my own experience (using FSets/FMaps in automata
construction), it is possible to go quite far without any troubles.

> - in fact, you even cannot perform this computation, since the proofs that
> the lists are not redundant in FSets are opaque. So if you try something
> like :
>
> remove (add x empty_set)

But it seems unavoidable, because x is a variable here. To perform
this computation, you have to match on x, which is abstract. The
problem here is not the fact that the proofs are opaque. The following
code illustrate this (it works with either AVL or Lists).

Require Import FSetInterface.
Require Import FSetList.
Require Import FSetAVL.
Require Import OrderedTypeEx.

Module M := FSetAVL.Make (Nat_as_OT).
Notation "A == B" := (M.Equal A B) (at level 70, no associativity).
Notation "A === B" := (M.equal A B = true) (at level 70, no associativity).

Goal M.remove 2 (M.add 2 (M.empty)) === M.empty . vm_compute. reflexivity. 
Qed.
Goal forall x, M.remove x  (M.add x (M.empty)) === M.empty.
  intros.
  vm_compute.
Abort.


Before the Abort, the printed term is quite intricate, but you can see
that the matching is stuck because x is abstract. However, it works
well with constants. In order to let coq compute to prove the second
goal, you would need some sort of reification and reflexive
simplification procedure, as far as I can tell. Can you elaborate on
how you are able to prove this kind of things by changing the
definition of remove ?

With best regards,
Thomas