The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

Hi all,

I am having problems with the implementation of class instances leaking
when I destruct things, as shown in the cut-down example below. My
intention was that subsequent code wouldn't be able to see the
implementation, so this makes proving some things impossible.

Is there a way I can stop the implementation leaking please?


Thanks
Ian


Require Import Equality.

Axiom P : Set.
Axiom Sequence : Set.

Class Cl (T : Type) : Type := mkCl {
    invert : T -> T;
    invertInverse : forall (p : T),
                    invert (invert p) = p
}.

Inductive Catch : Type
    := MkCatch : forall (p : P), Catch
     | Conflictor : forall (conflicts : Sequence), Catch.

Module impl.
Definition invertSequence (ps : Sequence)
                        : Sequence.
Admitted.
Definition invertInverseSequence : forall (s : Sequence),
                                   invertSequence (invertSequence s) = s.
Admitted.

Instance ClSeq : Cl Sequence
    := mkCl Sequence invertSequence invertInverseSequence.
End impl.

Inductive CC : Catch -> Catch -> Catch -> Catch -> Prop
     := MkCC : forall (p : P)
                      (x y : Sequence),
               x = invert y
            -> CC (MkCatch p) (Conflictor x) (Conflictor x) (Conflictor x).

Lemma CatchCommuteUnique :
      forall {p   : Catch} {q   : Catch}
             {q'  : Catch} {p'  : Catch}
             {q'' : Catch} {p'' : Catch}
             (commute1 : CC p q q' p')
             (commute2 : CC p q q'' p''),
      True.
Proof with auto.
intros.
dependent destruction commute1.
dependent destruction commute2.
(*
Now the implementation has leaked out: we have "impl.invertSequence"
rather than "invert":
    H : impl.invertSequence y0 = invert y
*)
apply (f_equal invert) in H.
rewrite invertInverse in H.
(*
This therefore fails to rewrite "invert (impl.invertSequence y0)" to y0:
*)
rewrite invertInverse in H.