diff options
author | Jason Gross <jgross@mit.edu> | 2017-11-10 13:45:31 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-11-10 14:14:28 -0500 |
commit | 1c38c74bc059f67ec58fc8026eb8ba8742b4913b (patch) | |
tree | 60ec735ae78c2d23d02bb305d4599d55231ada47 /src/Util/SideConditions/ReductionPackages.v | |
parent | d5ac8bc07824d9cf6c7b4698bf38bde85cc84704 (diff) |
More modularity in autosolve
Diffstat (limited to 'src/Util/SideConditions/ReductionPackages.v')
-rw-r--r-- | src/Util/SideConditions/ReductionPackages.v | 111 |
1 files changed, 111 insertions, 0 deletions
diff --git a/src/Util/SideConditions/ReductionPackages.v b/src/Util/SideConditions/ReductionPackages.v new file mode 100644 index 000000000..3266540ac --- /dev/null +++ b/src/Util/SideConditions/ReductionPackages.v @@ -0,0 +1,111 @@ +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 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 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 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 ?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_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. |