Commit 0618ab9a authored by Ralf Jung's avatar Ralf Jung

make a proofmode copy of from_option to control simplification

parent 351ca6f1
...@@ -84,6 +84,11 @@ Qed. ...@@ -84,6 +84,11 @@ Qed.
Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2). Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
Proof. apply iff_reflect. by rewrite ident_beq_true. Qed. Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
(** Copies of some definitions so we can control their unfolding *)
Definition option_bind {A B} (f : A option B) (mx : option A) : option B := Definition option_bind {A B} (f : A option B) (mx : option A) : option B :=
match mx with Some x => f x | None => None end. match mx with Some x => f x | None => None end.
Arguments option_bind _ _ _ !_ /. Arguments option_bind {_ _} _ !_ / : assert.
Definition from_option {A B} (f : A B) (y : B) (mx : option A) : B :=
match mx with None => y | Some x => f x end.
Arguments from_option {_ _} _ _ !_ / : assert.
...@@ -851,7 +851,7 @@ Proof. ...@@ -851,7 +851,7 @@ Proof.
rewrite /ElimAcc /IntoAcc /ElimInv. rewrite /ElimAcc /IntoAcc /ElimInv.
iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)". iIntros (Hacc Helim Hφ) "(Hinv & Hin & Hcont)".
iApply (Helim with "[Hcont]"). iApply (Helim with "[Hcont]").
- iIntros (x) "Hα". iApply "Hcont". iSplitL; done. - iIntros (x) "Hα". iApply "Hcont". iSplitL; simpl; done.
- iApply (Hacc with "Hinv Hin"). done. - iApply (Hacc with "Hinv Hin"). done.
Qed. Qed.
...@@ -860,7 +860,7 @@ Global Instance elim_inv_acc_with_close {X : Type} ...@@ -860,7 +860,7 @@ Global Instance elim_inv_acc_with_close {X : Type}
M1 M2 α β γ Q Q' : M1 M2 α β γ Q Q' :
IntoAcc Pinv φ Pin M1 M2 α β γ IntoAcc Pinv φ Pin M1 M2 α β γ
( R, ElimModal True false false (M1 R) R Q Q') ( R, ElimModal True false false (M1 R) R Q Q')
ElimInv (X:=X) φ Pinv Pin α (Some (λ x, β x - M2 (default emp (γ x) id)))%I ElimInv (X:=X) φ Pinv Pin α (Some (λ x, β x - M2 (proofmode.base.from_option id emp (γ x))))%I
Q (λ _, Q'). Q (λ _, Q').
Proof. Proof.
rewrite /ElimAcc /IntoAcc /ElimInv. rewrite /ElimAcc /IntoAcc /ElimInv.
......
...@@ -1101,7 +1101,7 @@ Lemma tac_inv_elim {X : Type} Δ Δ' i j φ p Pinv Pin Pout (Pclose : option (X ...@@ -1101,7 +1101,7 @@ Lemma tac_inv_elim {X : Type} Δ Δ' i j φ p Pinv Pin Pout (Pclose : option (X
φ φ
( R, Δ'', ( R, Δ'',
envs_app false (Esnoc Enil j envs_app false (Esnoc Enil j
(Pin - ( x, Pout x - default (Q' x) Pclose (λ Pclose, Pclose x - Q' x)) - R)%I) Δ' (Pin - ( x, Pout x - from_option (λ Pclose, Pclose x - Q' x) (Q' x) Pclose) - R)%I) Δ'
= Some Δ'' = Some Δ''
envs_entails Δ'' R) envs_entails Δ'' R)
envs_entails Δ Q. envs_entails Δ Q.
......
...@@ -7,8 +7,11 @@ From stdpp Require Import hlist pretty. ...@@ -7,8 +7,11 @@ From stdpp Require Import hlist pretty.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Export ident. Export ident.
(** These are all proofmode-internal definitions and hence unfolding them should
not affect the user's goal. *)
(* TODO: Can we option_bind, from_option, maybe_wand reduce only if applied to a constructor? *)
Declare Reduction env_cbv := cbv [ Declare Reduction env_cbv := cbv [
option_bind from_option (* TODO: Can we make these (and maybe_wand) reduce only if applied to a constructor? *) option_bind from_option
beq ascii_beq string_beq positive_beq Pos.succ ident_beq beq ascii_beq string_beq positive_beq Pos.succ ident_beq
env_lookup env_lookup_delete env_delete env_app env_replace env_dom 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 env_intuitionistic env_spatial env_counter env_spatial_is_nil envs_dom
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment