diff options
author | 2016-07-25 15:00:47 +0200 | |
---|---|---|
committer | 2016-07-26 14:00:27 +0200 | |
commit | 46a866aa5fd63cc577c4a453bcf26ee75c47c433 (patch) | |
tree | 9896794ed3b31663b95ff843b2e3b5164cffd392 /test-suite/bugs/closed/4754.v | |
parent | b36fc3478dc893b05edd2884972622531105d43d (diff) |
Fix bug #4754, allow conversion problems to remain
when checking that the rewrite relation is homogeneous in
setoid_rewrite.
Diffstat (limited to 'test-suite/bugs/closed/4754.v')
-rw-r--r-- | test-suite/bugs/closed/4754.v | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4754.v b/test-suite/bugs/closed/4754.v new file mode 100644 index 000000000..5bb3cd1be --- /dev/null +++ b/test-suite/bugs/closed/4754.v @@ -0,0 +1,35 @@ + +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms. +Definition f (v : option nat) := match v with + | Some k => Some k + | None => None + end. + +Axioms F G : (option nat -> option nat) -> Prop. +Axiom FG : forall f, f None = None -> F f = G f. + +Axiom admit : forall {T}, T. + +Existing Instance eq_Reflexive. + +Global Instance foo (A := nat) + : Proper ((pointwise_relation _ eq) + ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl)) + (@option_rect A (fun _ => Prop)) | 0. +exact admit. +Qed. + +Global Instance bar (A := nat) + : Proper ((pointwise_relation _ eq) + ==> eq ==> eq ==> Basics.flip Basics.impl) + (@option_rect A (fun _ => Prop)) | 0. +exact admit. +Qed. + +Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k. +Proof. + intro. + pose proof (_ : (Proper (_ ==> eq ==> _) and)). + setoid_rewrite (FG _ _); [ | reflexivity.. ]. + Undo. + setoid_rewrite (FG _ eq_refl). (* Error: Tactic failure: setoid rewrite failed: Nothing to rewrite. in 8.5 *) Admitted.
\ No newline at end of file |