aboutsummaryrefslogtreecommitdiff
path: root/src/Util/SideConditions/Autosolve.v
blob: 9622ba689f209d4ee83cca9b3405d7f355172c12 (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
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 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 else_tac :=
  CorePackages.preautosolve ();
  lazymatch goal with
  | [ |- True ] => exact I
  | [ |- unit ] => exact tt
  | [ |- IDProp ] => exact idProp
  | [ |- 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)
  | [ |- @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.