The Coq mailing list

[Erik Martin-Dorel <e.mdorel AT gmail.com>]

Hello Ian,

A possible solution for your question is to (temporarily) make the instance opaque :

(*...*)
Opaque impl.ClSeq.
(*...*)
dependent destruction commute2.
(*...*)

But if you really want to use modules for this purpose (namely, hide the implementation of a Module Type), you can use the feature of "opaque modules" (see example below).

Best,
Erik

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 Type Sig.
Parameter ClSeq : Cl Sequence.
End Sig.

Module impl : Sig. (* Define an opaque module. Note that this is not "<: Sig" *)
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.
(*...*)

2014/1/14 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.

--

Érik Martin-Dorel

http://erik.martin-dorel.org/