Interaction between type classes and auto tactic
Question
Consider this simple development. I have two trivial data types:
Inductive A := | A1 | A2. Inductive B := | B1 : A -> B | B2.
Now I introduce a concept of relation and define ordering on data types A and B expressed as an inductive data type:
Definition relation (X : Type) := X -> X -> Prop. Reserved Notation "a1 '<=A' a2" (at level 70). Inductive AOrd : relation A := | A1_Ord : A1 <=A A1 | A2_Ord : A2 <=A A2 | A1_A2 : A1 <=A A2 where "a1 '<=A' a2" := (AOrd a1 a2). Reserved Notation "b1 '<=B' b2" (at level 70). Inductive BOrd : relation B := | B1_Ord : forall a1 a2, a1 <=A a2 -> B1 a1 <=B B1 a2 | B2_Ord : B2 <=B B2 | B1_B2 : forall a, B1 a <=B B2 where "b1 '<=B' b2" := (BOrd b1 b2).
Finally, I introduce a concept of reflexivity and prove that both of my relations are reflexive:
Definition reflexive {X : Type} (R : relation X) := forall a : X, R a a.reflexive AOrdreflexive AOrdinduction a; auto. Qed.a: Aa <=A areflexive BOrdreflexive BOrdinduction b; auto. Qed.b: Bb <=B b
Both proofs are finished with auto tactic, with the first proof crucially relying on Hint Constructors and the second one additionally on Hint Resolve AOrd_reflexive being added to hint database.
An ugly thing about the code above is having a separate notation for ordering relation for A and B data types. I'd like to be able to uniformly use <= everywhere. This answer provides a solution to the problem: use type classes. So I introduce a type class for ordering and redefine my ordering relations to use this new notation:
Class OrderR (T : Type) := orderR : relation T. Notation "x '<=' y" := (orderR x y) (at level 70). Inductive AOrd : OrderR A := | A1_Ord : A1 <= A1 | A2_Ord : A2 <= A2 | A1_A2 : A1 <= A2. Inductive BOrd `{OrderR A} : OrderR B := | B1_Ord : forall a1 a2, a1 <= a2 -> B1 a1 <= B1 a2 | B2_Ord : B2 <= B2 | B1_B2 : forall a, B1 a <= B2.
But now proof automation breaks! For example:
reflexive AOrdreflexive AOrda: AAOrd a aAOrd A1 A1AOrd A2 A2
leaves me with a goal:
that auto no longer solves despite AOrd constructors being in hint database. I can solve the goal with constructor though:
reflexive AOrdreflexive AOrdinduction a; constructor. Qed.a: AAOrd a a
More problems arise in second proof. After doing:
H: OrderR Areflexive BOrdH: OrderR Areflexive BOrdH: OrderR A
b: BBOrd b bH: OrderR A
a: Aa <= a
I am left with goal:
Again, auto no longer solves this goal. Even apply AOrd_reflexive does not work.
My question is: is it possible to have a uniform notation by relying on type classes and maintain benefits of proof automation? Or is there a different solution to having a uniform notation for various data types.
Answer (eponier)
A solution that does not involve typeclasses is to take advantage of the scope mechanism of Coq.
Inductive A := | A1 | A2. Inductive B := | B1 : A -> B | B2. Definition relation (X : Type) := X -> X -> Prop. Reserved Notation "a1 '<=' a2" (at level 70).Delimit Scope a_scope with a.Delimit Scope b_scope with b. Definition reflexive {X : Type} (R : relation X) := forall a : X, R a a.reflexive AOrdreflexive AOrdinduction a; auto. Qed.a: A(a <= a)%areflexive BOrdreflexive BOrdinduction b; auto. Qed.b: B(b <= b)%b
Answer (Jason Gross)
The issue is that your hints are set to trigger on, e.g., @orderR _ AOrd A1 A2, not AOrd A1 A2. So the automation never sees the pattern it's looking for, and never triggers the hints. Here are two solutions:
You can adjust the type of your constructors when adding them to the hint database, so that they trigger when you want them to:
You can define "folding" lemmas that convert the types, and add those to the database:
Definition fold_AOrd a1 a2 (v : a1 <= a2) : AOrd a1 a2 := v. Definition fold_BOrd `{OrderR A} (a1 a2 : B) (v : a1 <= a2) : BOrd a1 a2 := v.
Q: Thanks Jason. I'm afraid your solution does not work for me. Folding lemmas don't seem to change anything. Adjusting type of constructors works when proving AOrd_reflexive but in the proof of BOrd_reflexive it is still not possible to prove a <= a from AOrd_reflexive.