Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Rewriting with equivalence relations in Set / Type

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Rewriting with equivalence relations in Set / Type


Chronological Thread 
  • From: Rui Baptista <rpgcbaptista AT gmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: [Coq-Club] Rewriting with equivalence relations in Set / Type
  • Date: Thu, 27 Feb 2014 21:21:06 +0000

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 _ _ _ _).



Archive powered by MHonArc 2.6.18.

Top of Page