Commit 7ba11ac0 authored by Robbert Krebbers's avatar Robbert Krebbers

More simple changes to make proof mode terms more compact.

This is a follow up of !248.
parent a82dbaf9
...@@ -252,16 +252,19 @@ Qed. ...@@ -252,16 +252,19 @@ Qed.
(* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact], (* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
but it is doing some work to keep the order of hypotheses preserved. *) but it is doing some work to keep the order of hypotheses preserved. *)
(* TODO: convert to not take Δ' or Δ'' *) (* TODO: convert to not take Δ' *)
Lemma tac_specialize remove_intuitionistic Δ Δ' Δ'' i p j q P1 P2 R Q : Lemma tac_specialize remove_intuitionistic Δ Δ' i p j q P1 P2 R Q :
envs_lookup_delete remove_intuitionistic i Δ = Some (p, P1, Δ') envs_lookup_delete remove_intuitionistic i Δ = Some (p, P1, Δ')
envs_lookup j Δ' = Some (q, R) envs_lookup j Δ' = Some (q, R)
IntoWand q p R P1 P2 IntoWand q p R P1 P2
envs_replace j q (p && q) (Esnoc Enil j P2) Δ' = Some Δ'' match envs_replace j q (p && q) (Esnoc Enil j P2) Δ' with
envs_entails Δ'' Q envs_entails Δ Q. | Some Δ'' => envs_entails Δ'' Q
| None => False
end envs_entails Δ Q.
Proof. Proof.
rewrite envs_entails_eq /IntoWand. rewrite envs_entails_eq /IntoWand.
intros [? ->]%envs_lookup_delete_Some ? HR ? <-. intros [? ->]%envs_lookup_delete_Some ? HR ?.
destruct (envs_replace _ _ _ _ _) as [Δ''|] eqn:?; last done.
rewrite (envs_lookup_sound' _ remove_intuitionistic) //. rewrite (envs_lookup_sound' _ remove_intuitionistic) //.
rewrite envs_replace_singleton_sound //. destruct p; simpl in *. rewrite envs_replace_singleton_sound //. destruct p; simpl in *.
- rewrite -{1}intuitionistically_idemp -{1}intuitionistically_if_idemp. - rewrite -{1}intuitionistically_idemp -{1}intuitionistically_if_idemp.
...@@ -327,16 +330,20 @@ Proof. ...@@ -327,16 +330,20 @@ Proof.
by rewrite intuitionistically_emp left_id wand_elim_r. by rewrite intuitionistically_emp left_id wand_elim_r.
Qed. Qed.
Lemma tac_specialize_assert_intuitionistic Δ Δ' Δ'' j q P1 P1' P2 R Q : Lemma tac_specialize_assert_intuitionistic Δ Δ' j q P1 P1' P2 R Q :
envs_lookup_delete true j Δ = Some (q, R, Δ') envs_lookup_delete true j Δ = Some (q, R, Δ')
IntoWand q true R P1 P2 IntoWand q true R P1 P2
Persistent P1 Persistent P1
IntoAbsorbingly P1' P1 IntoAbsorbingly P1' P1
envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' envs_entails Δ' P1'
envs_entails Δ' P1' envs_entails Δ'' Q envs_entails Δ Q. match envs_simple_replace j q (Esnoc Enil j P2) Δ with
| Some Δ'' => envs_entails Δ'' Q
| None => False
end envs_entails Δ Q.
Proof. Proof.
rewrite envs_entails_eq => /envs_lookup_delete_Some [? ->] ???? HP1 <-. rewrite envs_entails_eq => /envs_lookup_delete_Some [? ->] ??? HP1 HQ.
rewrite envs_lookup_sound //. destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:?; last done.
rewrite -HQ envs_lookup_sound //.
rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))). rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))).
rewrite {2}envs_simple_replace_singleton_sound' //; simpl. rewrite {2}envs_simple_replace_singleton_sound' //; simpl.
rewrite {1}HP1 (into_absorbingly P1' P1) (persistent_persistently_2 P1). rewrite {1}HP1 (into_absorbingly P1' P1) (persistent_persistently_2 P1).
...@@ -346,15 +353,19 @@ Proof. ...@@ -346,15 +353,19 @@ Proof.
by rewrite intuitionistically_if_sep_2 (into_wand q true) wand_elim_l wand_elim_r. by rewrite intuitionistically_if_sep_2 (into_wand q true) wand_elim_l wand_elim_r.
Qed. Qed.
Lemma tac_specialize_intuitionistic_helper Δ Δ'' j q P R R' Q : Lemma tac_specialize_intuitionistic_helper Δ j q P R R' Q :
envs_lookup j Δ = Some (q,P) envs_lookup j Δ = Some (q,P)
(if q then TCTrue else BiAffine PROP) (if q then TCTrue else BiAffine PROP)
envs_entails Δ (<absorb> R) envs_entails Δ (<absorb> R)
IntoPersistent false R R' IntoPersistent false R R'
envs_replace j q true (Esnoc Enil j R') Δ = Some Δ'' match envs_replace j q true (Esnoc Enil j R') Δ with
envs_entails Δ'' Q envs_entails Δ Q. | Some Δ'' => envs_entails Δ'' Q
| None => False
end envs_entails Δ Q.
Proof. Proof.
rewrite envs_entails_eq => ?? HR ?? <-. rewrite -(idemp bi_and (of_envs Δ)) {1}HR. rewrite envs_entails_eq => ?? HR ??.
destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:?; last done.
rewrite -(idemp bi_and (of_envs Δ)) {1}HR.
rewrite envs_replace_singleton_sound //; destruct q; simpl. rewrite envs_replace_singleton_sound //; destruct q; simpl.
- by rewrite (_ : R = <pers>?false R)%I // (into_persistent _ R) - by rewrite (_ : R = <pers>?false R)%I // (into_persistent _ R)
absorbingly_elim_persistently sep_elim_r absorbingly_elim_persistently sep_elim_r
...@@ -374,12 +385,16 @@ Proof. ...@@ -374,12 +385,16 @@ Proof.
rewrite intuitionistically_if_elim comm. f_equiv; auto using pure_intro. rewrite intuitionistically_if_elim comm. f_equiv; auto using pure_intro.
Qed. Qed.
Lemma tac_revert Δ Δ' i p P Q : Lemma tac_revert Δ i Q :
envs_lookup_delete true i Δ = Some (p,P,Δ') match envs_lookup_delete true i Δ with
envs_entails Δ' ((if p then P else P)%I - Q) | Some (p,P,Δ') => envs_entails Δ' ((if p then P else P)%I - Q)
| None => False
end
envs_entails Δ Q. envs_entails Δ Q.
Proof. Proof.
rewrite envs_entails_eq => ? HQ. rewrite envs_lookup_delete_sound //=. rewrite envs_entails_eq => HQ.
destruct (envs_lookup_delete _ _ _) as [[[p P] Δ']|] eqn:?; last done.
rewrite envs_lookup_delete_sound //=.
rewrite HQ. destruct p; simpl; auto using wand_elim_r. rewrite HQ. destruct p; simpl; auto using wand_elim_r.
Qed. Qed.
......
...@@ -582,15 +582,16 @@ Local Tactic Notation "iForallRevert" ident(x) := ...@@ -582,15 +582,16 @@ Local Tactic Notation "iForallRevert" ident(x) :=
(** The tactic [iRevertHyp H with tac] reverts the hypothesis [H] and calls (** The tactic [iRevertHyp H with tac] reverts the hypothesis [H] and calls
[tac] with a Boolean that is [true] iff [H] was in the intuitionistic context. *) [tac] with a Boolean that is [true] iff [H] was in the intuitionistic context. *)
Tactic Notation "iRevertHyp" constr(H) "with" tactic1(tac) := Tactic Notation "iRevertHyp" constr(H) "with" tactic1(tac) :=
(* Create a Boolean evar [p] to keep track of whether the hypothesis [H] was eapply tac_revert with H;
in the intuitionistic context. *) [lazymatch goal with
let p := fresh in evar (p : bool); | |- match envs_lookup_delete true ?i ?Δ with _ => _ end =>
let p' := eval unfold p in p in clear p; lazymatch eval pm_eval in (envs_lookup_delete true i Δ) with
eapply tac_revert with _ H p' _; | Some (?p,_,_) => pm_reduce; tac p
[pm_reflexivity || | None =>
let H := pretty_ident H in let H := pretty_ident H in
fail "iRevert:" H "not found" fail "iRevert:" H "not found"
|pm_reduce; tac p']. end
end].
Tactic Notation "iRevertHyp" constr(H) := iRevertHyp H with (fun _ => idtac). Tactic Notation "iRevertHyp" constr(H) := iRevertHyp H with (fun _ => idtac).
...@@ -783,7 +784,7 @@ Ltac iSpecializePat_go H1 pats := ...@@ -783,7 +784,7 @@ Ltac iSpecializePat_go H1 pats :=
| SIdent ?H2 [] :: ?pats => | SIdent ?H2 [] :: ?pats =>
(* If we not need to specialize [H2] we can avoid a lot of unncessary (* If we not need to specialize [H2] we can avoid a lot of unncessary
context manipulation. *) context manipulation. *)
notypeclasses refine (tac_specialize false _ _ _ H2 _ H1 _ _ _ _ _ _ _ _ _ _); notypeclasses refine (tac_specialize false _ _ H2 _ H1 _ _ _ _ _ _ _ _ _);
[pm_reflexivity || [pm_reflexivity ||
let H2 := pretty_ident H2 in let H2 := pretty_ident H2 in
fail "iSpecialize:" H2 "not found" fail "iSpecialize:" H2 "not found"
...@@ -794,7 +795,7 @@ Ltac iSpecializePat_go H1 pats := ...@@ -794,7 +795,7 @@ Ltac iSpecializePat_go H1 pats :=
let P := match goal with |- IntoWand _ _ ?P ?Q _ => P end in let P := match goal with |- IntoWand _ _ ?P ?Q _ => P end in
let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in
fail "iSpecialize: cannot instantiate" P "with" Q fail "iSpecialize: cannot instantiate" P "with" Q
|pm_reflexivity|iSpecializePat_go H1 pats] |pm_reduce; iSpecializePat_go H1 pats]
| SIdent ?H2 ?pats1 :: ?pats => | SIdent ?H2 ?pats1 :: ?pats =>
(* If [H2] is in the intuitionistic context, we copy it into a new (* If [H2] is in the intuitionistic context, we copy it into a new
hypothesis [Htmp], so that it can be used multiple times. *) hypothesis [Htmp], so that it can be used multiple times. *)
...@@ -810,7 +811,7 @@ Ltac iSpecializePat_go H1 pats := ...@@ -810,7 +811,7 @@ Ltac iSpecializePat_go H1 pats :=
Ltac backtraces (which would otherwise include the whole closure). *) Ltac backtraces (which would otherwise include the whole closure). *)
[.. (* side-conditions of [iSpecialize] *) [.. (* side-conditions of [iSpecialize] *)
|(* Use [remove_intuitionistic = true] to remove the copy [Htmp]. *) |(* Use [remove_intuitionistic = true] to remove the copy [Htmp]. *)
notypeclasses refine (tac_specialize true _ _ _ H2tmp _ H1 _ _ _ _ _ _ _ _ _ _); notypeclasses refine (tac_specialize true _ _ H2tmp _ H1 _ _ _ _ _ _ _ _ _);
[pm_reflexivity || [pm_reflexivity ||
let H2tmp := pretty_ident H2tmp in let H2tmp := pretty_ident H2tmp in
fail "iSpecialize:" H2tmp "not found" fail "iSpecialize:" H2tmp "not found"
...@@ -821,7 +822,7 @@ Ltac iSpecializePat_go H1 pats := ...@@ -821,7 +822,7 @@ Ltac iSpecializePat_go H1 pats :=
let P := match goal with |- IntoWand _ _ ?P ?Q _ => P end in let P := match goal with |- IntoWand _ _ ?P ?Q _ => P end in
let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in let Q := match goal with |- IntoWand _ _ ?P ?Q _ => Q end in
fail "iSpecialize: cannot instantiate" P "with" Q fail "iSpecialize: cannot instantiate" P "with" Q
|pm_reflexivity|iSpecializePat_go H1 pats]] |pm_reduce; iSpecializePat_go H1 pats]]
| SPureGoal ?d :: ?pats => | SPureGoal ?d :: ?pats =>
notypeclasses refine (tac_specialize_assert_pure _ H1 _ _ _ _ _ _ _ _ _ _ _ _); notypeclasses refine (tac_specialize_assert_pure _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity || [pm_reflexivity ||
...@@ -835,7 +836,7 @@ Ltac iSpecializePat_go H1 pats := ...@@ -835,7 +836,7 @@ Ltac iSpecializePat_go H1 pats :=
|pm_reduce; |pm_reduce;
iSpecializePat_go H1 pats] iSpecializePat_go H1 pats]
| SGoal (SpecGoal GIntuitionistic false ?Hs_frame [] ?d) :: ?pats => | SGoal (SpecGoal GIntuitionistic false ?Hs_frame [] ?d) :: ?pats =>
notypeclasses refine (tac_specialize_assert_intuitionistic _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _); notypeclasses refine (tac_specialize_assert_intuitionistic _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity || [pm_reflexivity ||
let H1 := pretty_ident H1 in let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found" fail "iSpecialize:" H1 "not found"
...@@ -844,9 +845,8 @@ Ltac iSpecializePat_go H1 pats := ...@@ -844,9 +845,8 @@ Ltac iSpecializePat_go H1 pats :=
let Q := match goal with |- Persistent ?Q => Q end in let Q := match goal with |- Persistent ?Q => Q end in
fail "iSpecialize:" Q "not persistent" fail "iSpecialize:" Q "not persistent"
|iSolveTC |iSolveTC
|pm_reflexivity
|iFrame Hs_frame; solve_done d (*goal*) |iFrame Hs_frame; solve_done d (*goal*)
|iSpecializePat_go H1 pats] |pm_reduce; iSpecializePat_go H1 pats]
| SGoal (SpecGoal GIntuitionistic _ _ _ _) :: ?pats => | SGoal (SpecGoal GIntuitionistic _ _ _ _) :: ?pats =>
fail "iSpecialize: cannot select hypotheses for intuitionistic premise" fail "iSpecialize: cannot select hypotheses for intuitionistic premise"
| SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats => | SGoal (SpecGoal ?m ?lr ?Hs_frame ?Hs ?d) :: ?pats =>
...@@ -866,7 +866,7 @@ Ltac iSpecializePat_go H1 pats := ...@@ -866,7 +866,7 @@ Ltac iSpecializePat_go H1 pats :=
|iFrame Hs_frame; solve_done d (*goal*) |iFrame Hs_frame; solve_done d (*goal*)
|iSpecializePat_go H1 pats] |iSpecializePat_go H1 pats]
| SAutoFrame GIntuitionistic :: ?pats => | SAutoFrame GIntuitionistic :: ?pats =>
notypeclasses refine (tac_specialize_assert_intuitionistic _ _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _ _); notypeclasses refine (tac_specialize_assert_intuitionistic _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity || [pm_reflexivity ||
let H1 := pretty_ident H1 in let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found" fail "iSpecialize:" H1 "not found"
...@@ -874,9 +874,8 @@ Ltac iSpecializePat_go H1 pats := ...@@ -874,9 +874,8 @@ Ltac iSpecializePat_go H1 pats :=
|iSolveTC || |iSolveTC ||
let Q := match goal with |- Persistent ?Q => Q end in let Q := match goal with |- Persistent ?Q => Q end in
fail "iSpecialize:" Q "not persistent" fail "iSpecialize:" Q "not persistent"
|pm_reflexivity
|solve [iFrame "∗ #"] |solve [iFrame "∗ #"]
|iSpecializePat_go H1 pats] |pm_reduce; iSpecializePat_go H1 pats]
| SAutoFrame ?m :: ?pats => | SAutoFrame ?m :: ?pats =>
notypeclasses refine (tac_specialize_frame _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _); notypeclasses refine (tac_specialize_frame _ _ H1 _ _ _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity || [pm_reflexivity ||
...@@ -943,7 +942,7 @@ Tactic Notation "iSpecializeCore" open_constr(H) ...@@ -943,7 +942,7 @@ Tactic Notation "iSpecializeCore" open_constr(H)
let PROP := iBiOfGoal in let PROP := iBiOfGoal in
lazymatch eval compute in (q || tc_to_bool (BiAffine PROP)) with lazymatch eval compute in (q || tc_to_bool (BiAffine PROP)) with
| true => | true =>
notypeclasses refine (tac_specialize_intuitionistic_helper _ _ H _ _ _ _ _ _ _ _ _ _ _); notypeclasses refine (tac_specialize_intuitionistic_helper _ H _ _ _ _ _ _ _ _ _ _);
[pm_reflexivity [pm_reflexivity
(* This premise, [envs_lookup j Δ = Some (q,P)], (* This premise, [envs_lookup j Δ = Some (q,P)],
holds because [iTypeOf] succeeded *) holds because [iTypeOf] succeeded *)
...@@ -957,8 +956,7 @@ Tactic Notation "iSpecializeCore" open_constr(H) ...@@ -957,8 +956,7 @@ Tactic Notation "iSpecializeCore" open_constr(H)
|iSolveTC || |iSolveTC ||
let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in
fail "iSpecialize:" Q "not persistent" fail "iSpecialize:" Q "not persistent"
|pm_reflexivity |pm_reduce (* goal *)]
|(* goal *)]
| false => iSpecializePat H pat | false => iSpecializePat H pat
end end
| None => | None =>
......
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