Commit e42aece0 authored by Ralf Jung's avatar Ralf Jung

make some arguments implicit, for nicer proof scripts

parent 0b56a3e3
......@@ -5,7 +5,7 @@ Import uPred.
(* TODO RJ: Figure out a way to to always use our Σ. *)
(** Bind. *)
Lemma wp_bind E e K Q :
Lemma wp_bind {E e} K Q :
wp (Σ:=Σ) E e (λ v, wp (Σ:=Σ) E (fill K (v2e v)) Q) wp (Σ:=Σ) E (fill K e) Q.
Proof.
by apply (wp_bind (Σ:=Σ) (K := fill K)), fill_is_ctx.
......@@ -65,7 +65,7 @@ Proof.
apply wand_intro_l. rewrite -pvs_intro.
rewrite always_and_sep_l' -associative -always_and_sep_l'.
apply const_elim_l. intros [l [-> [-> Hl]]].
rewrite (forall_elim _ l). eapply const_intro_l; first eexact Hl.
rewrite (forall_elim l). eapply const_intro_l; first eexact Hl.
rewrite always_and_sep_l' associative -always_and_sep_l' wand_elim_r.
rewrite -wp_value'; done.
Qed.
......@@ -332,6 +332,6 @@ Qed.
Lemma wp_let e1 e2 E Q :
wp (Σ:=Σ) E e1 (λ v, wp (Σ:=Σ) E (e2.[v2e v/]) Q) wp (Σ:=Σ) E (Let e1 e2) Q.
Proof.
rewrite -(wp_bind _ _ (LetCtx EmptyCtx e2)). apply wp_mono=>v.
rewrite -(wp_bind (LetCtx EmptyCtx e2)). apply wp_mono=>v.
rewrite -wp_lam //. by rewrite v2v.
Qed.
......@@ -42,14 +42,13 @@ Module LiftingTests.
rewrite -later_intro. apply forall_intro=>l.
apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_.
rewrite -later_intro. asimpl.
rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _)
(PlusLCtx EmptyCtx _)) (Load (Loc _)))).
rewrite -(wp_bind (SeqCtx EmptyCtx (Load (Loc _)))).
rewrite -(wp_bind (StoreRCtx (LocV _) EmptyCtx)).
rewrite -(wp_bind (PlusLCtx EmptyCtx _)).
rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
{ apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
rewrite -later_intro. apply wand_intro_l. rewrite right_id.
rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _) EmptyCtx) (Load (Loc _)))).
rewrite -wp_plus -later_intro.
rewrite -(wp_bind _ _ (SeqCtx EmptyCtx (Load (Loc _)))).
rewrite -wp_store_pst; first (apply sep_intro_True_r; first done); last first.
{ apply: lookup_insert. }
{ reflexivity. }
......@@ -82,14 +81,14 @@ Module LiftingTests.
(* Go on. *)
rewrite -(wp_let _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred $ LitNat n2))).
rewrite -wp_plus. asimpl.
rewrite -(wp_bind _ _ (CaseCtx EmptyCtx _ _)).
rewrite -(wp_bind _ _ (LeLCtx EmptyCtx _)).
rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
rewrite -(wp_bind (LeLCtx EmptyCtx _)).
rewrite -wp_plus -!later_intro. simpl.
assert (Decision (S n1 + 1 n2)) as Hn12 by apply _.
destruct Hn12 as [Hle|Hgt].
- rewrite -wp_le_true /= //. rewrite -wp_case_inl //.
rewrite -!later_intro. asimpl.
rewrite (forall_elim _ (S n1)).
rewrite (forall_elim (S n1)).
eapply impl_elim; first by eapply and_elim_l. apply and_intro.
+ apply const_intro; omega.
+ by rewrite !and_elim_r.
......@@ -107,7 +106,7 @@ Module LiftingTests.
Q (LitNatV $ pred n) wp (Σ:=Σ) E (App Pred (LitNat n)) Q.
Proof.
rewrite -wp_lam //. asimpl.
rewrite -(wp_bind _ _ (CaseCtx EmptyCtx _ _)).
rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
assert (Decision (n 0)) as Hn by apply _.
destruct Hn as [Hle|Hgt].
- rewrite -wp_le_true /= //. rewrite -wp_case_inl //.
......
......@@ -44,7 +44,7 @@ Proof.
rewrite (associative _ P) {1}/vs always_elim impl_elim_r.
rewrite (associative _) pvs_impl_r pvs_always_r wp_always_r.
rewrite wp_pvs; apply wp_mono=> v.
by rewrite (forall_elim _ v) pvs_impl_r !pvs_trans'.
by rewrite (forall_elim v) pvs_impl_r !pvs_trans'.
Qed.
Lemma ht_atomic E1 E2 P P' Q Q' e :
E2 E1 atomic e
......@@ -55,7 +55,7 @@ Proof.
rewrite (associative _ P) {1}/vs always_elim impl_elim_r.
rewrite (associative _) pvs_impl_r pvs_always_r wp_always_r.
rewrite -(wp_atomic E1 E2) //; apply pvs_mono, wp_mono=> v.
rewrite (forall_elim _ v) pvs_impl_r -(pvs_intro E1) pvs_trans; solve_elem_of.
rewrite (forall_elim v) pvs_impl_r -(pvs_intro E1) pvs_trans; solve_elem_of.
Qed.
Lemma ht_bind `(HK : is_ctx K) E P Q Q' e :
({{ P }} e @ E {{ Q }} v, {{ Q v }} K (of_val v) @ E {{ Q' }})
......@@ -64,7 +64,7 @@ Proof.
intros; apply (always_intro' _ _), impl_intro_l.
rewrite (associative _ P) {1}/ht always_elim impl_elim_r.
rewrite wp_always_r -wp_bind //; apply wp_mono=> v.
rewrite (forall_elim _ v) pvs_impl_r wp_pvs; apply wp_mono=> v'.
rewrite (forall_elim v) pvs_impl_r wp_pvs; apply wp_mono=> v'.
by rewrite pvs_trans'.
Qed.
Lemma ht_mask_weaken E1 E2 P Q e :
......
......@@ -29,7 +29,7 @@ Proof.
rewrite always_and_sep_r' -associative; apply sep_mono; first done.
rewrite (later_intro ( _, _)) -later_sep; apply later_mono.
apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
rewrite (forall_elim _ e2) (forall_elim _ σ2) (forall_elim _ ef).
rewrite (forall_elim e2) (forall_elim σ2) (forall_elim ef).
apply wand_intro_l; rewrite !always_and_sep_l'.
rewrite (associative _ _ P') -(associative _ _ _ P') associative.
rewrite {1}/vs -always_wand_impl always_elim wand_elim_r.
......@@ -56,8 +56,7 @@ Proof.
(λ e2 σ2 ef, φ e2 σ2 ef P)%I);
try by (rewrite /φ'; eauto using atomic_not_value, atomic_step).
apply and_intro; [by rewrite -vs_reflexive; apply const_intro|].
apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
rewrite (forall_elim _ e2) (forall_elim _ σ2) (forall_elim _ ef).
apply forall_mono=>e2; apply forall_mono=>σ2; apply forall_mono=>ef.
apply and_intro; [|apply and_intro; [|done]].
* rewrite -vs_impl; apply (always_intro' _ _),impl_intro_l;rewrite and_elim_l.
rewrite !associative; apply sep_mono; last done.
......@@ -66,7 +65,7 @@ Proof.
* apply (always_intro' _ _), impl_intro_l; rewrite and_elim_l.
rewrite -always_and_sep_r'; apply const_elim_r=>-[[v Hv] ?].
rewrite -(of_to_val e2 v) // -wp_value -pvs_intro.
rewrite -(exist_intro _ σ2) -(exist_intro _ ef) (of_to_val e2) //.
rewrite -(exist_intro σ2) -(exist_intro ef) (of_to_val e2) //.
by rewrite -always_and_sep_r'; apply and_intro; try apply const_intro.
Qed.
Lemma ht_lift_pure_step E (φ : iexpr Σ option (iexpr Σ) Prop) P P' Q e1 :
......@@ -82,7 +81,7 @@ Proof.
rewrite -(wp_lift_pure_step E φ _ e1) //.
rewrite (later_intro ( _, _)) -later_and; apply later_mono.
apply forall_intro=>e2; apply forall_intro=>ef; apply impl_intro_l.
rewrite (forall_elim _ e2) (forall_elim _ ef).
rewrite (forall_elim e2) (forall_elim ef).
rewrite always_and_sep_l' !always_and_sep_r' {1}(always_sep_dup' ( _)).
rewrite {1}(associative _ (_ _)%I) -(associative _ ( _)%I).
rewrite (associative _ ( _)%I P) -{1}(commutative _ P) -(associative _ P).
......
......@@ -206,7 +206,7 @@ Proof. by setoid_rewrite (always_and_sep_r' _ _); rewrite wp_frame_r. Qed.
Lemma wp_impl_l E e Q1 Q2 : (( v, Q1 v Q2 v) wp E e Q1) wp E e Q2.
Proof.
rewrite wp_always_l; apply wp_mono=> v.
by rewrite always_elim (forall_elim _ v) impl_elim_l.
by rewrite always_elim (forall_elim v) impl_elim_l.
Qed.
Lemma wp_impl_r E e Q1 Q2 : (wp E e Q1 v, Q1 v Q2 v) wp E e Q2.
Proof. by rewrite (commutative _) wp_impl_l. Qed.
......
......@@ -395,9 +395,9 @@ Lemma impl_elim P Q R : P ⊑ (Q → R) → P ⊑ Q → P ⊑ R.
Proof. by intros HP HP' x n ??; apply HP with x n, HP'. Qed.
Lemma forall_intro {A} P (Q : A uPred M): ( a, P Q a) P ( a, Q a).
Proof. by intros HPQ x n ?? a; apply HPQ. Qed.
Lemma forall_elim {A} (P : A uPred M) a : ( a, P a) P a.
Lemma forall_elim {A} {P : A uPred M} a : ( a, P a) P a.
Proof. intros x n ? HP; apply HP. Qed.
Lemma exist_intro {A} (P : A uPred M) a : P a ( a, P a).
Lemma exist_intro {A} {P : A uPred M} a : P a ( a, P a).
Proof. by intros x [|n] ??; [done|exists a]. Qed.
Lemma exist_elim {A} (P : A uPred M) Q : ( a, P a Q) ( a, P a) Q.
Proof. by intros HPQ x [|n] ?; [|intros [a ?]; apply HPQ with a]. Qed.
......@@ -713,7 +713,7 @@ Lemma löb_all_1 {A} (P Q : A → uPred M) :
( a, (( b, P b Q b) P a) Q a) a, P a Q a.
Proof.
intros Hlöb a. apply impl_entails. transitivity ( a, P a Q a)%I; last first.
{ by rewrite (forall_elim _ a). } clear a.
{ by rewrite (forall_elim a). } clear a.
etransitivity; last by eapply löb.
apply impl_intro_l, forall_intro=>a. rewrite right_id. by apply impl_intro_r.
Qed.
......
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