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

Declare Reduction pm_cbv := cbv [
  (* base *)
6
  base.beq base.Pos_succ base.ascii_beq base.string_beq base.positive_beq base.ident_beq
7 8 9 10 11 12 13 14
  (* 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
  envs_clear_spatial envs_clear_persistent envs_incr_counter
  envs_split_go envs_split prop_of_env
].
15 16 17 18 19 20
(* Some things should only be unfolded according to cbn rules, when
   certain arguments are constructors. This is because they can appear in
   the user side of proofs as well. *)
Declare Reduction pm_cbn := cbn [
  (* PM option combinators *)
  pm_option_bind pm_from_option pm_option_fun
21 22
  (* telescope combinators *)
  tele_fold tele_bind tele_app
23 24
  (* BI connectives *)
  bi_persistently_if bi_affinely_if bi_intuitionistically_if
25
  bi_wandM bi_tforall bi_texist
26
].
27 28
Ltac pm_eval t :=
  let u := eval pm_cbv in t in
29 30
  let v := eval pm_cbn in u in
  v.
31 32 33
Ltac pm_reduce :=
  match goal with |- ?u => let v := pm_eval u in change v end.
Ltac pm_reflexivity := pm_reduce; exact eq_refl.