The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

I haven't tried reverse engineering rewriting with type classes yet.

Isn't there a command for deleting theorems from the databases auto uses? I think I remember reading about that in this mailing list.

I think it's possible to get a little bit better performance. Now it's not necessary to make [not] opaque.

Hint Extern 1 (_ <~> _) => simple apply A1 : CompatHints.

Hint Extern 1 (_ <~> _) => simple apply A2 : CompatHints.

Hint Extern 1 (_ <~> _) => simple apply A3 : CompatHints.

Hint Extern 1 (_ <~> _) => simple apply A4 : CompatHints.

Hint Extern 1 (_ <~> _) => simple apply A5 : CompatHints.

Hint Extern 1 (_ <~> _) => simple apply A6 : CompatHints.

Hint Extern 1 (_ <~> _) => simple apply A7 : CompatHints.

Hint Extern 1 (_ <~> _) => apply A8 : CompatHints.

Hint Extern 1 (_ <~> _) => apply A9 : CompatHints.

Hint Extern 1 (_ <~> _) => simple apply A10 : CompatHints.

Hint Extern 1 (_ <~> _) => simple apply A11 : CompatHints.

Ltac rw_f h1 := refine (iff_forwards _ _ _ _); [solve [auto 128 using h1 with CompatHints] | lazy beta].

Ltac rw_b h1 := refine (iff_backwards _ _ _ _); [solve [auto 128 using h1 with CompatHints] | lazy beta].

Axiom A12 : forall n1, double n1 ~ add n1 n1.

Goal ~~ ((False -> ((False + ((False * (forall x1, {x2 : nat & double x1 ~ x2})) * False)) + False)) -> False).

rw_f A12.

rw_b A12.

On Thu, Feb 27, 2014 at 9:28 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

I believe Matthieu Sozeau is working on getting the setoid_rewrite machinery to handle relations in Type, and also (I think?) dependent/heterogeneous relations.  It will hopefully be in Coq 8.5.  Have you looked at how setoid_rewriting is implemented with typeclass resolution?

-Jason

On Thu, Feb 27, 2014 at 4:21 PM, Rui Baptista <rpgcbaptista AT gmail.com> wrote:

It works if I use

Hint Extern 1 => apply A1 : CompatHints.

Hint Extern 1 => apply A2 : CompatHints.

Hint Extern 1 => apply A3 : CompatHints.

Hint Extern 1 => apply A4 : CompatHints.

Hint Extern 1 => apply A5 : CompatHints.

Hint Extern 1 => apply A6 : CompatHints.

Hint Extern 1 => apply A7 : CompatHints.

Hint Extern 1 => apply A8 : CompatHints.

Hint Extern 1 => apply A9 : CompatHints.

Hint Extern 1 => apply A10 : CompatHints.

Hint Extern 1 => apply A11 : CompatHints.

instead of

Hint Resolve A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 A11 : CompatHints.

But it's kind of slow, and I'm forced to use

Global Opaque not.

so it doesn't unfold not. Also, it prefers to use compatibility with universal quantification instead of implication.

I used refine (iff_backwards _ _ _ _) when I should have used refine (iff_forwards _ _ _ _).