blob: 61d4ef33aa3081a239650f3b1afb7941676916cc (
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
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
|
Require Import Crypto.Util.Decidable.
Require Import Crypto.Util.SideConditions.CorePackages.
Require Import Crypto.Util.Tactics.HeadUnderBinders.
Definition vm_decide_package (P : Prop) := P.
Definition cbv_minus_then_vm_decide_package {T} (ident : T) (P : Prop) := P.
Definition vm_compute_reflexivity_package (P : Prop) := P.
Inductive cast_bias := LHS | RHS.
Definition vm_compute_evar_package_gen {bias : cast_bias} {T} (v : T) :=
@evar_package T v.
Notation vm_compute_evar_package_vm_small := (@vm_compute_evar_package_gen LHS).
Notation vm_compute_evar_package_vm_large := (@vm_compute_evar_package_gen RHS).
Notation vm_compute_evar_package := vm_compute_evar_package_vm_small.
Definition native_compute_evar_package_gen {bias : cast_bias} {T} (v : T) :=
@evar_package T v.
Notation native_compute_evar_package_native_small := (@native_compute_evar_package_gen LHS).
Notation native_compute_evar_package_native_large := (@native_compute_evar_package_gen RHS).
Notation native_compute_evar_package := native_compute_evar_package_native_small.
Definition vm_compute_cbv_evar_package_gen {bias : cast_bias} {T} (v : T) :=
@evar_package T v.
Notation vm_compute_cbv_evar_package_vm_small := (@vm_compute_cbv_evar_package_gen LHS).
Notation vm_compute_cbv_evar_package_vm_large := (@vm_compute_cbv_evar_package_gen RHS).
Notation vm_compute_cbv_evar_package := vm_compute_cbv_evar_package_vm_small.
Definition vm_cast_evar_package {s} (v : s) d := @evard_package s d v.
Definition cast_evar_package {s} (v : s) d := @evard_package s d v.
Definition vm_compute_cast_evar_package {s} (v : s) d := @evard_package s d v.
Definition optional_evar_Prop_package {T} (P : T -> Prop) (alt_pkg : Type)
:= @evar_Prop_package
(option T)
(fun v => match v with
| Some v => P v
| None => True
end).
Definition None_evar_Prop_package' {alt_pkg T P} : @optional_evar_Prop_package T P alt_pkg
:= {| val := None ; evar_package_pf := I |}.
Notation None_evar_Prop_package := (@None_evar_Prop_package' unit).
Notation optional_evar_package pkg_type
:= (optional_evar_Prop_package
(ltac:(lazymatch eval hnf in pkg_type%type with evar_Prop_package ?P => exact P end))
pkg_type)
(only parsing).
Definition option_evar_rel_package {A} (v : option A) B (R : B -> A -> Prop) (alt_pkg : A -> Type)
:= @evar_Prop_package
(option B)
(fun v' => match v', v with
| Some v', Some v => R v' v
| None, None => True
| Some _, None | None, Some _ => False
end).
Notation optional_evar_rel_package pkg_type x
:= (option_evar_rel_package
x
_
(fun a b
=> ltac:(lazymatch eval hnf in (pkg_type%function b) with
| evar_Prop_package ?P
=> let P := (eval cbv beta in (P a)) in
exact P
end))
pkg_type)
(only parsing).
Definition unoption_evar_rel_package {A v B R alt_pkg}
(f : forall v, alt_pkg v -> @evar_rel_package A v B R)
: forall (pkg : match v with
| Some v => alt_pkg v
| None => True
end),
@option_evar_rel_package A v B R alt_pkg
:= match v
return match v with
| Some v => alt_pkg v
| None => True
end -> @option_evar_rel_package A v B R alt_pkg
with
| Some v => fun pkg => {| val := Some (val (f _ pkg));
evar_package_pf := evar_package_pf (f _ pkg) |}
| None => fun _ => None_evar_Prop_package
end.
Ltac autosolve autosolve_tac else_tac :=
lazymatch goal with
| [ |- match ?x with Some _ => _ | None => _ end ]
=> let x' := (eval hnf in x) in
progress change x with x';
cbv beta iota;
autosolve_tac else_tac
| [ |- vm_decide_package (_ = true) ] => abstract vm_cast_no_check (eq_refl true)
| [ |- vm_decide_package (_ = false) ] => abstract vm_cast_no_check (eq_refl false)
| [ |- vm_decide_package ?P ] => cbv beta delta [vm_decide_package]; vm_decide
| [ |- cbv_minus_then_vm_decide_package ?ident ?P ] => cbv -[ident]; vm_decide
| [ |- vm_compute_reflexivity_package ?P ] => vm_compute; reflexivity
| [ |- vm_compute_evar_package_vm_small ?v ]
=> let v' := (eval vm_compute in v) in
(exists v'); abstract vm_cast_no_check (eq_refl v')
| [ |- vm_compute_evar_package_vm_large ?v ]
=> let v' := (eval vm_compute in v) in
(exists v'); abstract vm_cast_no_check (eq_refl v)
| [ |- vm_compute_cbv_evar_package_vm_small ?v ]
=> let v' := (eval vm_compute in v) in
let v' := (eval cbv in v) in
(exists v'); abstract vm_cast_no_check (eq_refl v')
| [ |- vm_compute_cbv_evar_package_vm_large ?v ]
=> let v' := (eval vm_compute in v) in
let v' := (eval cbv in v) in
(exists v'); abstract vm_cast_no_check (eq_refl v)
| [ |- native_compute_evar_package_native_small ?v ]
=> let v' := (eval native_compute in v) in
(exists v'); abstract native_cast_no_check (eq_refl v')
| [ |- native_compute_evar_package_native_large ?v ]
=> let v' := (eval native_compute in v) in
(exists v'); abstract native_cast_no_check (eq_refl v)
| [ |- vm_cast_evar_package ?v ?d ]
=> unshelve eexists (v <: d);
[ vm_compute; reflexivity
| cbv beta;
let lhs := lazymatch goal with |- ?lhs = _ => lhs end in
abstract exact_no_check (eq_refl lhs) ]
| [ |- cast_evar_package (s:=?s) ?v ?d ]
=> exact (@Build_evard_package
s d v
v eq_refl eq_refl)
| [ |- vm_compute_cast_evar_package (s:=?s) ?v ?d ]
=> let v' := (eval vm_compute in v) in
exact (@Build_evard_package
s d v
v' eq_refl eq_refl)
| [ |- @option_evar_rel_package ?A ?v ?B ?R ?alt_pkg ]
=> refine (@unoption_evar_rel_package A v B R alt_pkg (fun _ x => x) _);
autosolve_tac else_tac
| _ => else_tac ()
end.
|
