From 1c38c74bc059f67ec58fc8026eb8ba8742b4913b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 10 Nov 2017 13:45:31 -0500 Subject: More modularity in autosolve --- src/Util/SideConditions/Autosolve.v | 120 +++------------------------- src/Util/SideConditions/CorePackages.v | 10 +++ src/Util/SideConditions/ReductionPackages.v | 111 +++++++++++++++++++++++++ src/Util/SideConditions/RingPackage.v | 29 +++++++ 4 files changed, 160 insertions(+), 110 deletions(-) create mode 100644 src/Util/SideConditions/ReductionPackages.v create mode 100644 src/Util/SideConditions/RingPackage.v (limited to 'src/Util/SideConditions') diff --git a/src/Util/SideConditions/Autosolve.v b/src/Util/SideConditions/Autosolve.v index 3428a77e9..51c13647c 100644 --- a/src/Util/SideConditions/Autosolve.v +++ b/src/Util/SideConditions/Autosolve.v @@ -1,115 +1,15 @@ Require Import Crypto.Util.Decidable. Require Import Crypto.Util.SideConditions.CorePackages. -Require Import Crypto.Util.Tactics.HeadUnderBinders. +Require Import Crypto.Util.SideConditions.ReductionPackages. +Require Import Crypto.Util.SideConditions.RingPackage. -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_gen autosolve_tac else_tac := + CorePackages.preautosolve (); + CorePackages.Internal.autosolve ltac:(fun _ => + ReductionPackages.autosolve autosolve_tac ltac:(fun _ => + RingPackage.autosolve ltac:(fun _ => + CorePackages.autosolve else_tac + ))). Ltac autosolve else_tac := - CorePackages.preautosolve (); - lazymatch goal with - | [ |- True ] => exact I - | [ |- unit ] => exact tt - | [ |- IDProp ] => exact idProp - | [ |- match ?x with Some _ => _ | None => _ end ] - => let x' := (eval hnf in x) in - progress change x with x'; - cbv beta iota; - autosolve 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 else_tac - | _ => CorePackages.autosolve else_tac - end. + autosolve_gen autosolve else_tac. diff --git a/src/Util/SideConditions/CorePackages.v b/src/Util/SideConditions/CorePackages.v index 7af4cc133..c4511c93e 100644 --- a/src/Util/SideConditions/CorePackages.v +++ b/src/Util/SideConditions/CorePackages.v @@ -46,4 +46,14 @@ Definition evard_package_pf {s d v} (pkg : @evard_package s d v) Ltac preautosolve _ := repeat autounfold with autosolve in *. +Module Internal. + Ltac autosolve else_tac := + lazymatch goal with + | [ |- True ] => exact I + | [ |- unit ] => exact tt + | [ |- IDProp ] => exact idProp + | _ => else_tac () + end. +End Internal. + Ltac autosolve else_tac := else_tac (). 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. diff --git a/src/Util/SideConditions/RingPackage.v b/src/Util/SideConditions/RingPackage.v new file mode 100644 index 000000000..f979b77ba --- /dev/null +++ b/src/Util/SideConditions/RingPackage.v @@ -0,0 +1,29 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.setoid_ring.Ring_tac. +Require Import Crypto.Util.Prod. +Require Import Crypto.Util.SideConditions.CorePackages. +Require Export Crypto.Util.FixCoqMistakes. + +Definition eq_by_Zring_prod_package (P : Prop) := P. + +Ltac auto_split_prod_step _ := + match goal with + | [ H : prod _ _ |- _ ] => destruct H + | [ |- forall a, _ ] => let a := fresh in intro a; compute in a + | [ |- pair _ _ = pair _ _ ] => apply f_equal2 + | [ |- @eq (prod _ _) _ _ ] => apply path_prod + end. + +Ltac Zring_prod_eq_tac _ := + cbv -[Z.add Z.sub Z.mul Z.div Z.pow Z.opp Z.log2 Z.land Z.lor Z.log2_up Z.abs]; + repeat match goal with + | _ => auto_split_prod_step () + | [ |- @eq Z _ _ ] => ring + end. + +Ltac autosolve else_tac := + lazymatch goal with + | [ |- eq_by_Zring_prod_package _ ] + => solve [ Zring_prod_eq_tac () ] + | _ => else_tac () + end. -- cgit v1.2.3