Commit e2458a73 authored by Robbert Krebbers's avatar Robbert Krebbers

Make reflexivity hints work for evars.

Since Coq 8.4 did not backtrack on eauto premises, we used to ensure
that hints like

  Hint Extern 0 (?x ≡{_}≡ ?y) => reflexivity.

were not used for goals involving evars by writing ?x ≡{_}≡ ?y instead
of _ ≡{_}≡ _.

This seems to be a legacy issue that no longer applies to Coq 8.5, so
I have removed these restrictions making these hints thus more powerful.
parent c78daf89
......@@ -11,7 +11,7 @@ Notation "(⋅)" := op (only parsing) : C_scope.
Definition included `{Equiv A, Op A} (x y : A) := z, y x z.
Infix "≼" := included (at level 70) : C_scope.
Notation "(≼)" := included (only parsing) : C_scope.
Hint Extern 0 (?x ?y) => reflexivity.
Hint Extern 0 (_ _) => reflexivity.
Instance: Params (@included) 3.
Class Minus (A : Type) := minus : A A A.
......@@ -32,7 +32,7 @@ Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x
Notation "x ≼{ n } y" := (includedN n x y)
(at level 70, format "x ≼{ n } y") : C_scope.
Instance: Params (@includedN) 4.
Hint Extern 0 (?x {_} ?y) => reflexivity.
Hint Extern 0 (_ {_} _) => reflexivity.
Record CMRAMixin A `{Dist A, Equiv A, Unit A, Op A, ValidN A, Minus A} := {
(* setoids *)
......
......@@ -5,7 +5,7 @@ Class Dist A := dist : nat → relation A.
Instance: Params (@dist) 3.
Notation "x ≡{ n }≡ y" := (dist n x y)
(at level 70, n at next level, format "x ≡{ n }≡ y").
Hint Extern 0 (?x {_} ?y) => reflexivity.
Hint Extern 0 (_ {_} _) => reflexivity.
Hint Extern 0 (_ {_} _) => symmetry; assumption.
Tactic Notation "cofe_subst" ident(x) :=
......
......@@ -97,7 +97,7 @@ Qed.
(** logical entailement *)
Definition uPred_entails {M} (P Q : uPred M) := x n, {n} x P n x Q n x.
Hint Extern 0 (uPred_entails ?P ?P) => reflexivity.
Hint Extern 0 (uPred_entails _ _) => reflexivity.
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
(** logical connectives *)
......
......@@ -53,7 +53,7 @@ Notation "(≠)" := (λ x y, x ≠ y) (only parsing) : C_scope.
Notation "( x ≠)" := (λ y, x y) (only parsing) : C_scope.
Notation "(≠ x )" := (λ y, y x) (only parsing) : C_scope.
Hint Extern 0 (?x = ?x) => reflexivity.
Hint Extern 0 (_ = _) => reflexivity.
Hint Extern 100 (_ _) => discriminate.
Notation "(→)" := (λ A B, A B) (only parsing) : C_scope.
......@@ -198,7 +198,7 @@ Instance: Params (@equiv) 2.
(for types that have an [Equiv] instance) rather than the standard Leibniz
equality. *)
Instance equiv_default_relation `{Equiv A} : DefaultRelation () | 3.
Hint Extern 0 (?x ?y) => reflexivity.
Hint Extern 0 (_ _) => reflexivity.
Hint Extern 0 (_ _) => symmetry; assumption.
(** ** Operations on collections *)
......
......@@ -220,8 +220,8 @@ Definition suffix_of {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1.
Definition prefix_of {A} : relation (list A) := λ l1 l2, k, l2 = l1 ++ k.
Infix "`suffix_of`" := suffix_of (at level 70) : C_scope.
Infix "`prefix_of`" := prefix_of (at level 70) : C_scope.
Hint Extern 0 (?x `prefix_of` ?y) => reflexivity.
Hint Extern 0 (?x `suffix_of` ?y) => reflexivity.
Hint Extern 0 (_ `prefix_of` _) => reflexivity.
Hint Extern 0 (_ `suffix_of` _) => reflexivity.
Section prefix_suffix_ops.
Context `{ x y : A, Decision (x = y)}.
......@@ -249,7 +249,7 @@ Inductive sublist {A} : relation (list A) :=
| sublist_skip x l1 l2 : sublist l1 l2 sublist (x :: l1) (x :: l2)
| sublist_cons x l1 l2 : sublist l1 l2 sublist l1 (x :: l2).
Infix "`sublist`" := sublist (at level 70) : C_scope.
Hint Extern 0 (?x `sublist` ?y) => reflexivity.
Hint Extern 0 (_ `sublist` _) => reflexivity.
(** A list [l2] contains a list [l1] if [l2] is obtained by removing elements
from [l1] while possiblity changing the order. *)
......@@ -260,7 +260,7 @@ Inductive contains {A} : relation (list A) :=
| contains_cons x l1 l2 : contains l1 l2 contains l1 (x :: l2)
| contains_trans l1 l2 l3 : contains l1 l2 contains l2 l3 contains l1 l3.
Infix "`contains`" := contains (at level 70) : C_scope.
Hint Extern 0 (?x `contains` ?y) => reflexivity.
Hint Extern 0 (_ `contains` _) => reflexivity.
Section contains_dec_help.
Context {A} {dec : x y : A, Decision (x = y)}.
......
......@@ -86,9 +86,6 @@ Qed.
Lemma vs_mask_frame' E Ef P Q : Ef E = (P ={E}=> Q) (P ={E Ef}=> Q).
Proof. intros; apply vs_mask_frame; solve_elem_of. Qed.
(* FIXME: This is needed to make eauto solve [inv N R ⊑ inv N ?c]. *)
Local Hint Extern 100 (_ _) => reflexivity.
Lemma vs_open_close N E P Q R :
nclose N E
(inv N R ( R P ={E nclose N}=> R Q)) (P ={E}=> Q).
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment