The Coq mailing list

[Joonwon Choi <jwchoi AT ropas.snu.ac.kr>]

Hello all,
I have a question on automatic definition unfoldment in Ltac.
I will represent this issue with minimal example.

First, my goal was to give Ltac for every module which has "eq" interface, as belows:

    Module Type HasEqSpec (Export E:EqualityType').
      Parameter eq_refl: Reflexive eq.
      Parameter eq_sym: Symmetric eq.
      Parameter eq_trans: Transitive eq.
    End HasEqSpec.

    Module EqSolver (E:EqualityType') (F:HasEqSpec E).
      Ltac solve_eq :=
        repeat
          (match goal with
                 | [ H: E.eq ?a ?b |- E.eq ?b ?a] => apply F.eq_sym
                 ... (omitted for brevity) ...
           end).
    End EqSolver.

And I implemented "Module Interval_raw" which follows the interface EqualityType' and HasEqSpec.
Finally, I created "Module Interval" as belows:

    Module Interval := Interval_raw <+ EqSolver.

However, when I tried to prove the lemma below with "solve_eq", the proof simply failed.

    Lemma eq_sym_real : forall x y:Interval.t, Interval.eq x y -> Interval.eq y x.
    Proof.
      intros.
      Interval.solve_eq. (* Nothing changed *)
    Admitted.

I tried to find the reason why nothing is changed after applying my tactic,
and I found that defition "E.eq" was unfolded; I checked with "Print Ltac Interval.solve_eq".

So the question is:Is there any way not to unfold the definition "E.eq" in Ltac?
I am also wondering that why definitions in Ltac are unfolded.

best regards,
Joonwon Choi.