reduction.v 1.82 KB
Newer Older
1
From iris.bi Require Import bi telescopes.
2
3
From iris.proofmode Require Import base environments.

4
5
6
7
(** Called by all tactics to perform computation to lookup items in the
    context.  We avoid reducing anything user-visible here to make sure we
    do not reduce e.g. before unification happens in [iApply].*)
Declare Reduction pm_eval := cbv [
8
  (* base *)
9
10
  base.negb base.beq
  base.Pos_succ base.ascii_beq base.string_beq base.positive_beq base.ident_beq
11
12
13
14
15
  (* environments *)
  env_lookup env_lookup_delete env_delete env_app env_replace
  env_dom env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom
  envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
  envs_simple_replace envs_replace envs_split
16
  envs_clear_spatial envs_clear_intuitionistic envs_incr_counter
Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
  envs_split_go envs_split
  env_to_prop_go env_to_prop env_to_prop_and_go env_to_prop_and
19
20
  (* PM list and option functions *)
  pm_app pm_option_bind pm_from_option pm_option_fun
21
22
].
Ltac pm_eval t :=
23
  eval pm_eval in t.
24
Ltac pm_reduce :=
Ralf Jung's avatar
Ralf Jung committed
25
  (* Use [change_no_check] instead of [change] to avoid performing the
Robbert Krebbers's avatar
Robbert Krebbers committed
26
  conversion check twice. *)
Ralf Jung's avatar
Ralf Jung committed
27
  match goal with |- ?u => let v := pm_eval u in change_no_check v end.
28
Ltac pm_reflexivity := pm_reduce; exact eq_refl.
29

30
31
(** Called by many tactics for redexes that are created by instantiation.
    This cannot create any envs redexes so we just do the cbn part. *)
32
33
34
35
Declare Reduction pm_prettify := cbn [
  (* telescope combinators *)
  tele_fold tele_bind tele_app
  (* BI connectives *)
36
  bi_persistently_if bi_affinely_if bi_absorbingly_if bi_intuitionistically_if
37
  bi_wandM bi_laterN
38
39
  bi_tforall bi_texist
].
40
Ltac pm_prettify :=
Ralf Jung's avatar
Ralf Jung committed
41
  (* Use [change_no_check] instead of [change] to avoid performing the
Robbert Krebbers's avatar
Robbert Krebbers committed
42
  conversion check twice. *)
Ralf Jung's avatar
Ralf Jung committed
43
  match goal with |- ?u => let v := eval pm_prettify in u in change_no_check v end.