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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
|
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *)
(* Distributed under the terms of CeCILL-B. *)
From Coq Require Export ssreflect.
Global Set SsrOldRewriteGoalsOrder.
Global Set Asymmetric Patterns.
Global Set Bullet Behavior "None".
(******************************************************************************)
(* Local additions: *)
(* nonPropType == an interface for non-Prop Types: a nonPropType coerces *)
(* to a Type, and only types that do _not_ have sort *)
(* Prop are canonical nonPropType instances. This is *)
(* useful for applied views. *)
(* --> This will become standard with the Coq v8.11 SSReflect core library. *)
(* deprecate old new == new, but warning that old is deprecated and new *)
(* should be used instead. *)
(* --> Usage: Notation old := (deprecate old new) (only parsing). *)
(* --> Caveat: deprecate old new only inherits new's maximal implicits; *)
(* on-demand implicits should be added after : (deprecate old new _). *)
(* --> Caveat 2: if premises or conclusions need to be adjusted, of for *)
(* non-prenex implicits, use the idiom: *)
(* Notation old := ((fun a1 a2 ... => deprecate old new a1 a2 ...) *)
(* _ _ ... _) (only printing). *)
(* where all the implicit a_i's occur first, and correspond to the *)
(* trailing _'s, making sure deprecate old new is fully applied and *)
(* there are _no implicits_ inside the (fun .. => ..) expression. This *)
(* is to avoid triggering a bug in SSReflect elaboration that is *)
(* triggered by such evars under binders. *)
(* Import Deprecation.Silent :: turn off deprecation warning messages. *)
(* Import Deprecation.Reject :: raise an error instead of only warning. *)
(* *)
(* Intro pattern ltac views: *)
(* - top of the stack actions: *)
(* => /[apply] := => hyp {}/hyp *)
(* => /[swap] := => x y; move: y x *)
(* (also swap and perserves let bindings) *)
(* => /[dup] := => x; have copy := x; move: copy x *)
(* (also copies and preserves let bindings) *)
(******************************************************************************)
Module NonPropType.
Structure call_of (condition : unit) (result : bool) := Call {callee : Type}.
Definition maybeProp (T : Type) := tt.
Definition call T := Call (maybeProp T) false T.
Structure test_of (result : bool) := Test {condition :> unit}.
Definition test_Prop (P : Prop) := Test true (maybeProp P).
Definition test_negative := Test false tt.
Structure type :=
Check {result : bool; test : test_of result; frame : call_of test result}.
Definition check result test frame := @Check result test frame.
Module Exports.
Canonical call.
Canonical test_Prop.
Canonical test_negative.
Canonical check.
Notation nonPropType := type.
Coercion callee : call_of >-> Sortclass.
Coercion frame : type >-> call_of.
Notation notProp T := (@check false test_negative (call T)).
End Exports.
End NonPropType.
Export NonPropType.Exports.
Module Deprecation.
Definition hidden (T : Type) := T.
Definition exposed (T : Type) & unit -> unit -> unit := T.
Definition hide T u (v : exposed T u) : hidden T := v.
Ltac warn old_id new_id :=
idtac "Warning:" old_id "is deprecated; use" new_id "instead".
Ltac stop old_id new_id :=
fail 1 "Error:" old_id "is deprecated; use" new_id "instead".
Structure hinted := Hint {statement; hint : statement}.
Ltac check cond := let test := constr:(hint _ : cond) in idtac.
Variant reject := Reject.
Definition reject_hint := Hint reject Reject.
Module Reject. Canonical reject_hint. End Reject.
Variant silent := Silent.
Definition silent_hint := Hint silent Silent.
Module Silent. Canonical silent_hint. End Silent.
Ltac flag old_id new_id :=
first [check reject; stop old_id new_id | check silent | warn old_id new_id].
Module Exports.
Arguments hide {T} u v /.
Coercion hide : exposed >-> hidden.
Notation deprecate old_id new_id :=
(hide (fun old_id new_id => ltac:(flag old_id new_id; exact tt)) new_id)
(only parsing).
End Exports.
End Deprecation.
Export Deprecation.Exports.
Module Export ipat.
Notation "'[' 'apply' ']'" := (ltac:(let f := fresh "_top_" in move=> f {}/f))
(at level 0, only parsing) : ssripat_scope.
(* we try to preserve the naming by matching the names from the goal *)
(* we do move to perform a hnf before trying to match *)
Notation "'[' 'swap' ']'" := (ltac:(move;
let x := lazymatch goal with
| |- forall (x : _), _ => fresh x | |- let x := _ in _ => fresh x | _ => fresh "_top_"
end in intro x; move;
let y := lazymatch goal with
| |- forall (y : _), _ => fresh y | |- let y := _ in _ => fresh y | _ => fresh "_top_"
end in intro y; revert x; revert y))
(at level 0, only parsing) : ssripat_scope.
(* we try to preserve the naming by matching the names from the goal *)
(* we do move to perform a hnf before trying to match *)
Notation "'[' 'dup' ']'" := (ltac:(move;
lazymatch goal with
| |- forall (x : _), _ =>
let x := fresh x in intro x;
let copy := fresh x in have copy := x; revert x; revert copy
| |- let x := _ in _ =>
let x := fresh x in intro x;
let copy := fresh x in pose copy := x;
do [unfold x in (value of copy)]; revert x; revert copy
| |- _ =>
let x := fresh "_top_" in move=> x;
let copy := fresh "_top" in have copy := x; revert x; revert copy
end))
(at level 0, only parsing) : ssripat_scope.
End ipat.
|
