blob: c59b92a74102ec0d03a3221440dcb4f96cbe5ed2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
(** * Fixes *)
Require Export Crypto.Util.GlobalSettings.
(** Coq is poorly designed in some ways. We fix some of these issues
in this file. *)
(** [intuition] means [intuition auto with *]. This is very wrong and
fragile and slow. We make [intuition] mean [intuition auto]. *)
Tactic Notation "intuition" tactic3(tactic) := intuition tactic.
Tactic Notation "intuition" := intuition auto.
(** [firstorder] means [firstorder auto with *]. This is very wrong
and fragile and slow. We make [firstorder] mean [firstorder
auto]. *)
Global Set Firstorder Solver auto.
(** A version of [intuition] that allows you to see how the old
[intuition] tactic solves the proof. *)
Ltac debug_intuition := idtac "<infomsg>Warning: debug_intuition should not be used in production code.</infomsg>"; intuition debug auto with *.
(** [Coq.Init.Logic.f_equal2] is opaque. A transparent version would serve us better. *)
Definition f_equal2 {A1 A2 B} (f : A1 -> A2 -> B) {x1 y1 : A1} {x2 y2 : A2} (H : x1 = y1)
:= match H in (_ = y) return (x2 = y2 -> f x1 x2 = f y y2) with
| eq_refl =>
fun H0 : x2 = y2 =>
match H0 in (_ = y) return (f x1 x2 = f x1 y) with
| eq_refl => eq_refl
end
end.
(** Work around BZ#5341, https://coq.inria.fr/bugs/show_bug.cgi?id=5341, [subst] fails with bogus error message about universe polymorphism *)
Local Theorem create_internal_eq_rew_r_dep : forall A (a : A) (x : A) (e : a = x),
e = e -> True.
Proof.
intros ? ? ? H.
match goal with |- ?G => assert G end;
[ rewrite -> H
| rewrite <- H ];
constructor.
Defined.
|
