Commit 1945565f authored by Robbert Krebbers's avatar Robbert Krebbers

Alternative take on making proof mode terms more compact.

This is an alternative to !224.
parent ca513824
...@@ -88,15 +88,14 @@ Proof. ...@@ -88,15 +88,14 @@ Proof.
by rewrite wand_elim_r. by rewrite wand_elim_r.
Qed. Qed.
(* TODO: convert to not take Δ' *) Lemma tac_clear Δ i p P Q :
Lemma tac_clear Δ Δ' i p P Q : envs_lookup i Δ = Some (p,P)
envs_lookup_delete true i Δ = Some (p,P,Δ')
(if p then TCTrue else TCOr (Affine P) (Absorbing Q)) (if p then TCTrue else TCOr (Affine P) (Absorbing Q))
envs_entails Δ' Q envs_entails (envs_delete true i p Δ) Q
envs_entails Δ Q. envs_entails Δ Q.
Proof. Proof.
rewrite envs_entails_eq=> ?? HQ. rewrite envs_lookup_delete_sound //. rewrite envs_entails_eq=> ?? HQ. rewrite envs_lookup_sound //. rewrite HQ.
by destruct p; rewrite /= HQ sep_elim_r. by destruct p; rewrite /= sep_elim_r.
Qed. Qed.
(** * False *) (** * False *)
...@@ -124,15 +123,14 @@ Proof. ...@@ -124,15 +123,14 @@ Proof.
- by apply pure_intro. - by apply pure_intro.
Qed. Qed.
(* TODO: convert to not take Δ' *) Lemma tac_pure Δ i p P φ Q :
Lemma tac_pure Δ Δ' i p P φ Q : envs_lookup i Δ = Some (p, P)
envs_lookup_delete true i Δ = Some (p, P, Δ')
IntoPure P φ IntoPure P φ
(if p then TCTrue else TCOr (Affine P) (Absorbing Q)) (if p then TCTrue else TCOr (Affine P) (Absorbing Q))
(φ envs_entails Δ' Q) envs_entails Δ Q. (φ envs_entails (envs_delete true i p Δ) Q) envs_entails Δ Q.
Proof. Proof.
rewrite envs_entails_eq=> ?? HPQ HQ. rewrite envs_entails_eq=> ?? HPQ HQ.
rewrite envs_lookup_delete_sound //; simpl. destruct p; simpl. rewrite envs_lookup_sound //; simpl. destruct p; simpl.
- rewrite (into_pure P) -persistently_and_intuitionistically_sep_l persistently_pure. - rewrite (into_pure P) -persistently_and_intuitionistically_sep_l persistently_pure.
by apply pure_elim_l. by apply pure_elim_l.
- destruct HPQ. - destruct HPQ.
...@@ -273,15 +271,16 @@ Proof. ...@@ -273,15 +271,16 @@ Proof.
- by rewrite HR assoc !wand_elim_r. - by rewrite HR assoc !wand_elim_r.
Qed. Qed.
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q : Lemma tac_specialize_assert Δ Δ1 Δ2' j q neg js R P1 P2 P1' Q :
envs_lookup_delete true j Δ = Some (q, R, Δ') envs_lookup j Δ = Some (q, R)
IntoWand q false R P1 P2 AddModal P1' P1 Q IntoWand q false R P1 P2 AddModal P1' P1 Q
(''(Δ1,Δ2) envs_split (if neg is true then Right else Left) js Δ'; (''(Δ1,Δ2) envs_split (if neg is true then Right else Left)
js (envs_delete true j q Δ);
Δ2' envs_app false (Esnoc Enil j P2) Δ2; Δ2' envs_app false (Esnoc Enil j P2) Δ2;
Some (Δ1,Δ2')) = Some (Δ1,Δ2') (* does not preserve position of [j] *) Some (Δ1,Δ2')) = Some (Δ1,Δ2') (* does not preserve position of [j] *)
envs_entails Δ1 P1' envs_entails Δ2' Q envs_entails Δ Q. envs_entails Δ1 P1' envs_entails Δ2' Q envs_entails Δ Q.
Proof. Proof.
rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ. rewrite envs_entails_eq. intros ???? HP1 HQ.
destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=; destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
destruct (envs_app _ _ _) eqn:?; simplify_eq/=. destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
rewrite envs_lookup_sound // envs_split_sound //. rewrite envs_lookup_sound // envs_split_sound //.
...@@ -297,15 +296,15 @@ Proof. rewrite envs_entails_eq=> ->. by rewrite -lock -True_sep_2. Qed. ...@@ -297,15 +296,15 @@ Proof. rewrite envs_entails_eq=> ->. by rewrite -lock -True_sep_2. Qed.
Lemma tac_unlock Δ Q : envs_entails Δ Q envs_entails Δ (locked Q). Lemma tac_unlock Δ Q : envs_entails Δ Q envs_entails Δ (locked Q).
Proof. by unlock. Qed. Proof. by unlock. Qed.
Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' : Lemma tac_specialize_frame Δ j q R P1 P2 P1' Q Q' :
envs_lookup_delete true j Δ = Some (q, R, Δ') envs_lookup j Δ = Some (q, R)
IntoWand q false R P1 P2 IntoWand q false R P1 P2
AddModal P1' P1 Q AddModal P1' P1 Q
envs_entails Δ' (P1' locked Q') envs_entails (envs_delete true j q Δ) (P1' locked Q')
Q' = (P2 - Q)%I Q' = (P2 - Q)%I
envs_entails Δ Q. envs_entails Δ Q.
Proof. Proof.
rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some ?? HPQ ->. rewrite envs_entails_eq. intros ??? HPQ ->.
rewrite envs_lookup_sound //. rewrite HPQ -lock. rewrite envs_lookup_sound //. rewrite HPQ -lock.
rewrite (into_wand q false) -{2}(add_modal P1' P1 Q). cancel [P1']. rewrite (into_wand q false) -{2}(add_modal P1' P1 Q). cancel [P1'].
apply wand_intro_l. by rewrite assoc !wand_elim_r. apply wand_intro_l. by rewrite assoc !wand_elim_r.
...@@ -330,18 +329,18 @@ Proof. ...@@ -330,18 +329,18 @@ 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 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_entails Δ' P1' envs_entails (envs_delete true j q Δ) P1'
match envs_simple_replace j q (Esnoc Enil j P2) Δ with match envs_simple_replace j q (Esnoc Enil j P2) Δ with
| Some Δ'' => envs_entails Δ'' Q | Some Δ'' => envs_entails Δ'' Q
| None => False | None => False
end envs_entails Δ Q. end envs_entails Δ Q.
Proof. Proof.
rewrite envs_entails_eq => /envs_lookup_delete_Some [? ->] ??? HP1 HQ. rewrite envs_entails_eq => ???? HP1 HQ.
destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:?; last done. destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:?; last done.
rewrite -HQ envs_lookup_sound //. rewrite -HQ envs_lookup_sound //.
rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))). rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))).
...@@ -464,12 +463,12 @@ Proof. ...@@ -464,12 +463,12 @@ Proof.
by rewrite wand_elim_r. by rewrite wand_elim_r.
Qed. Qed.
Lemma tac_apply Δ Δ' i p R P1 P2 : Lemma tac_apply Δ i p R P1 P2 :
envs_lookup_delete true i Δ = Some (p, R, Δ') envs_lookup i Δ = Some (p, R)
IntoWand p false R P1 P2 IntoWand p false R P1 P2
envs_entails Δ' P1 envs_entails Δ P2. envs_entails (envs_delete true i p Δ) P1 envs_entails Δ P2.
Proof. Proof.
rewrite envs_entails_eq => ?? HP1. rewrite envs_lookup_delete_sound //. rewrite envs_entails_eq => ?? HP1. rewrite envs_lookup_sound //.
by rewrite (into_wand p false) /= HP1 wand_elim_l. by rewrite (into_wand p false) /= HP1 wand_elim_l.
Qed. Qed.
...@@ -570,12 +569,12 @@ Proof. ...@@ -570,12 +569,12 @@ Proof.
auto using and_intro, pure_intro. auto using and_intro, pure_intro.
Qed. Qed.
Lemma tac_frame Δ Δ' i p R P Q : Lemma tac_frame Δ i p R P Q :
envs_lookup_delete false i Δ = Some (p, R, Δ') envs_lookup i Δ = Some (p, R)
Frame p R P Q Frame p R P Q
envs_entails Δ' Q envs_entails Δ P. envs_entails (envs_delete false i p Δ) Q envs_entails Δ P.
Proof. Proof.
rewrite envs_entails_eq. intros [? ->]%envs_lookup_delete_Some Hframe HQ. rewrite envs_entails_eq. intros ? Hframe HQ.
rewrite (envs_lookup_sound' _ false) //. by rewrite -Hframe HQ. rewrite (envs_lookup_sound' _ false) //. by rewrite -Hframe HQ.
Qed. Qed.
...@@ -686,9 +685,9 @@ Proof. ...@@ -686,9 +685,9 @@ Proof.
Qed. Qed.
(** * Invariants *) (** * Invariants *)
Lemma tac_inv_elim {X : Type} Δ Δ' i j φ p Pinv Pin Pout (Pclose : option (X PROP)) Lemma tac_inv_elim {X : Type} Δ i j φ p Pinv Pin Pout (Pclose : option (X PROP))
Q (Q' : X PROP) : Q (Q' : X PROP) :
envs_lookup_delete false i Δ = Some (p, Pinv, Δ') envs_lookup i Δ = Some (p, Pinv)
ElimInv φ Pinv Pin Pout Pclose Q Q' ElimInv φ Pinv Pin Pout Pclose Q Q'
φ φ
( R, ( R,
...@@ -696,11 +695,11 @@ Lemma tac_inv_elim {X : Type} Δ Δ' i j φ p Pinv Pin Pout (Pclose : option (X ...@@ -696,11 +695,11 @@ Lemma tac_inv_elim {X : Type} Δ Δ' i j φ p Pinv Pin Pout (Pclose : option (X
(Pin - (Pin -
( x, Pout x - pm_option_fun Pclose x -? Q' x) - ( x, Pout x - pm_option_fun Pclose x -? Q' x) -
R R
)%I) Δ' )%I) (envs_delete false i p Δ)
with Some Δ'' => envs_entails Δ'' R | None => False end) with Some Δ'' => envs_entails Δ'' R | None => False end)
envs_entails Δ Q. envs_entails Δ Q.
Proof. Proof.
rewrite envs_entails_eq=> /envs_lookup_delete_Some [? ->] Hinv ? /(_ Q) Hmatch. rewrite envs_entails_eq=> ? Hinv ? /(_ Q) Hmatch.
destruct (envs_app _ _ _) eqn:?; last done. destruct (envs_app _ _ _) eqn:?; last done.
rewrite -Hmatch (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl. rewrite -Hmatch (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r. apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r.
......
...@@ -172,7 +172,7 @@ Ltac iElaborateSelPat pat := ...@@ -172,7 +172,7 @@ Ltac iElaborateSelPat pat :=
end. end.
Local Ltac iClearHyp H := Local Ltac iClearHyp H :=
eapply tac_clear with _ H _ _; (* (i:=H) *) eapply tac_clear with H _ _; (* (i:=H) *)
[pm_reflexivity || [pm_reflexivity ||
let H := pretty_ident H in let H := pretty_ident H in
fail "iClear:" H "not found" fail "iClear:" H "not found"
...@@ -180,7 +180,7 @@ Local Ltac iClearHyp H := ...@@ -180,7 +180,7 @@ Local Ltac iClearHyp H :=
let H := pretty_ident H in let H := pretty_ident H in
let P := match goal with |- TCOr (Affine ?P) _ => P end in let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail "iClear:" H ":" P "not affine and the goal not absorbing" fail "iClear:" H ":" P "not affine and the goal not absorbing"
|]. |pm_reduce].
Local Ltac iClear_go Hs := Local Ltac iClear_go Hs :=
lazymatch Hs with lazymatch Hs with
...@@ -297,7 +297,7 @@ Local Tactic Notation "iIntuitionistic" constr(H) := ...@@ -297,7 +297,7 @@ Local Tactic Notation "iIntuitionistic" constr(H) :=
|pm_reduce]. |pm_reduce].
Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) := Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
eapply tac_pure with _ H _ _ _; (* (i:=H1) *) eapply tac_pure with H _ _ _; (* (i:=H1) *)
[pm_reflexivity || [pm_reflexivity ||
let H := pretty_ident H in let H := pretty_ident H in
fail "iPure:" H "not found" fail "iPure:" H "not found"
...@@ -307,7 +307,7 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) := ...@@ -307,7 +307,7 @@ Local Tactic Notation "iPure" constr(H) "as" simple_intropattern(pat) :=
|pm_reduce; iSolveTC || |pm_reduce; iSolveTC ||
let P := match goal with |- TCOr (Affine ?P) _ => P end in let P := match goal with |- TCOr (Affine ?P) _ => P end in
fail "iPure:" P "not affine and the goal not absorbing" fail "iPure:" P "not affine and the goal not absorbing"
|intros pat]. |pm_reduce; intros pat].
Tactic Notation "iEmpIntro" := Tactic Notation "iEmpIntro" :=
iStartProof; iStartProof;
...@@ -342,14 +342,14 @@ Local Ltac iFramePure t := ...@@ -342,14 +342,14 @@ Local Ltac iFramePure t :=
Local Ltac iFrameHyp H := Local Ltac iFrameHyp H :=
iStartProof; iStartProof;
eapply tac_frame with _ H _ _ _; eapply tac_frame with H _ _ _;
[pm_reflexivity || [pm_reflexivity ||
let H := pretty_ident H in let H := pretty_ident H in
fail "iFrame:" H "not found" fail "iFrame:" H "not found"
|iSolveTC || |iSolveTC ||
let R := match goal with |- Frame _ ?R _ _ => R end in let R := match goal with |- Frame _ ?R _ _ => R end in
fail "iFrame: cannot frame" R fail "iFrame: cannot frame" R
|iFrameFinish]. |pm_reduce; iFrameFinish].
Local Ltac iFrameAnyPure := Local Ltac iFrameAnyPure :=
repeat match goal with H : _ |- _ => iFramePure H end. repeat match goal with H : _ |- _ => iFramePure H end.
...@@ -836,7 +836,7 @@ Ltac iSpecializePat_go H1 pats := ...@@ -836,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"
...@@ -845,13 +845,13 @@ Ltac iSpecializePat_go H1 pats := ...@@ -845,13 +845,13 @@ 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
|iFrame Hs_frame; solve_done d (*goal*) |pm_reduce; iFrame Hs_frame; solve_done d (*goal*)
|pm_reduce; 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 =>
let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in let Hs' := eval cbv in (if lr then Hs else Hs_frame ++ Hs) in
notypeclasses refine (tac_specialize_assert _ _ _ _ H1 _ lr Hs' _ _ _ _ _ _ _ _ _ _ _); notypeclasses refine (tac_specialize_assert _ _ _ H1 _ lr Hs' _ _ _ _ _ _ _ _ _ _ _);
[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"
...@@ -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,10 +874,10 @@ Ltac iSpecializePat_go H1 pats := ...@@ -874,10 +874,10 @@ 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"
|solve [iFrame "∗ #"] |pm_reduce; solve [iFrame "∗ #"]
|pm_reduce; 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 ||
let H1 := pretty_ident H1 in let H1 := pretty_ident H1 in
fail "iSpecialize:" H1 "not found" fail "iSpecialize:" H1 "not found"
...@@ -886,7 +886,8 @@ Ltac iSpecializePat_go H1 pats := ...@@ -886,7 +886,8 @@ Ltac iSpecializePat_go H1 pats :=
| GSpatial => class_apply add_modal_id | GSpatial => class_apply add_modal_id
| GModal => iSolveTC || fail "iSpecialize: goal not a modality" | GModal => iSolveTC || fail "iSpecialize: goal not a modality"
end end
|first |pm_reduce;
first
[notypeclasses refine (tac_unlock_emp _ _ _) [notypeclasses refine (tac_unlock_emp _ _ _)
|notypeclasses refine (tac_unlock_True _ _ _) |notypeclasses refine (tac_unlock_True _ _ _)
|iFrame "∗ #"; notypeclasses refine (tac_unlock _ _ _) |iFrame "∗ #"; notypeclasses refine (tac_unlock _ _ _)
...@@ -1060,10 +1061,11 @@ Local Ltac iApplyHypExact H := ...@@ -1060,10 +1061,11 @@ Local Ltac iApplyHypExact H :=
end]. end].
Local Ltac iApplyHypLoop H := Local Ltac iApplyHypLoop H :=
first first
[eapply tac_apply with _ H _ _ _; [eapply tac_apply with H _ _ _;
[pm_reflexivity [pm_reflexivity
|iSolveTC |iSolveTC
|pm_prettify (* reduce redexes created by instantiation *)] |pm_reduce;
pm_prettify (* reduce redexes created by instantiation *)]
|iSpecializePat H "[]"; last iApplyHypLoop H]. |iSpecializePat H "[]"; last iApplyHypLoop H].
Tactic Notation "iApplyHyp" constr(H) := Tactic Notation "iApplyHyp" constr(H) :=
...@@ -2299,7 +2301,7 @@ Tactic Notation "iAssumptionInv" constr(N) := ...@@ -2299,7 +2301,7 @@ Tactic Notation "iAssumptionInv" constr(N) :=
first [let H := constr:(_: IntoInv P' N) in unify i j|find Γ i] first [let H := constr:(_: IntoInv P' N) in unify i j|find Γ i]
end in end in
lazymatch goal with lazymatch goal with
| |- envs_lookup_delete _ ?i (Envs ?Γp ?Γs _) = Some _ => | |- envs_lookup ?i (Envs ?Γp ?Γs _) = Some _ =>
first [find Γp i|find Γs i]; pm_reflexivity first [find Γp i|find Γs i]; pm_reflexivity
end. end.
......
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