weakestpre_fix.v 4.38 KB
Newer Older
1
From Coq Require Import Wf_nat.
Ralf Jung's avatar
Ralf Jung committed
2
From iris.program_logic Require Import weakestpre wsat.
3
Local Hint Extern 10 (_  _) => omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
Local Hint Extern 10 (_  _) => set_solver.
5 6 7 8
Local Hint Extern 10 ({_} _) =>
  repeat match goal with
  | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
  end; solve_validN.
Ralf Jung's avatar
Ralf Jung committed
9

10 11 12
(** This files provides an alternative definition of wp in terms of a fixpoint
of a contractive function, rather than a CoInductive type. This is how we define
wp on paper.  We show that the two versions are equivalent. *)
Ralf Jung's avatar
Ralf Jung committed
13
Section def.
14 15
Context {Λ : language} {Σ : iFunctor}.
Local Notation iProp := (iProp Λ Σ).
Ralf Jung's avatar
Ralf Jung committed
16

17
Program Definition wp_pre
18 19
    (wp : coPset -c> expr Λ -c> (val Λ -c> iProp) -c> iProp) :
    coPset -c> expr Λ -c> (val Λ -c> iProp) -c> iProp := λ E e1 Φ,
20
  {| uPred_holds n r1 :=  k Ef σ1 rf,
Robbert Krebbers's avatar
Robbert Krebbers committed
21
       0  k < n  E  Ef 
22 23 24 25 26 27 28 29 30 31 32
       wsat (S k) (E  Ef) σ1 (r1  rf) 
       ( v, to_val e1 = Some v 
          r2, Φ v (S k) r2  wsat (S k) (E  Ef) σ1 (r2  rf)) 
       (to_val e1 = None  0 < k 
         reducible e1 σ1 
         ( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef 
            r2 r2',
             wsat k (E  Ef) σ2 (r2  r2'  rf) 
             wp E e2 Φ k r2 
             default True ef (λ ef, wp  ef (cconst True%I) k r2'))) |}.
Next Obligation.
33
  intros wp E e1 Φ n r1 r2 Hwp [r3 Hr2] k Ef σ1 rf ??.
34
  rewrite (dist_le _ _ _ _ Hr2); last lia. intros Hws.
35
  destruct (Hwp k Ef σ1 (r3  rf)) as [Hval Hstep]; rewrite ?assoc; auto.
36
  split.
37 38
  - intros v Hv. destruct (Hval v Hv) as [r4 [??]].
    exists (r4  r3). rewrite -assoc. eauto using uPred_mono, cmra_includedN_l.
39 40
  - intros ??. destruct Hstep as [Hred Hpstep]; auto.
    split; [done|]=> e2 σ2 ef ?.
41 42
    edestruct Hpstep as (r4&r4'&?&?&?); eauto.
    exists r4, (r4'  r3); split_and?; auto.
43
    + by rewrite assoc -assoc.
44
    + destruct ef; simpl in *; eauto using uPred_mono, cmra_includedN_l.
45
Qed.
46
Next Obligation. repeat intro; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
47

48
Local Instance pre_wp_contractive : Contractive wp_pre.
49
Proof.
50 51 52 53 54 55 56 57 58 59 60 61 62 63 64
  assert ( n E e Φ r
    (wp1 wp2 : coPset -c> expr Λ -c> (val Λ -c> iProp) -c> iProp),
    ( i : nat, i < n  wp1 {i} wp2) 
    wp_pre wp1 E e Φ n r  wp_pre wp2 E e Φ n r) as help.
  { intros n E e Φ r wp1 wp2 HI Hwp k Ef σ1 rf ???.
    destruct (Hwp k Ef σ1 rf) as [Hval Hstep]; auto.
    split; first done.
    intros ??. destruct Hstep as [Hred Hpstep]; auto.
    split; [done|]=> e2 σ2 ef ?.
    destruct (Hpstep e2 σ2 ef) as (r2&r2'&?&?&?); [done..|].
    exists r2, r2'; split_and?; auto.
    - apply HI with k; auto.
    - destruct ef as [ef|]; simpl in *; last done.
      apply HI with k; auto. }
  split; split; eapply help; auto using (symmetry (R:=dist _)).
65
Qed.
Ralf Jung's avatar
Ralf Jung committed
66

67 68
Definition wp_fix : coPset  expr Λ  (val Λ  iProp)  iProp := 
  fixpoint wp_pre.
Ralf Jung's avatar
Ralf Jung committed
69

70 71
Lemma wp_fix_unfold E e Φ : wp_fix E e Φ  wp_pre wp_fix E e Φ.
Proof. apply (fixpoint_unfold wp_pre). Qed.
Ralf Jung's avatar
Ralf Jung committed
72

73
Lemma wp_fix_correct E e (Φ : val Λ  iProp) : wp_fix E e Φ  wp E e Φ.
74 75 76 77
Proof.
  split=> n r Hr. rewrite wp_eq /wp_def {2}/uPred_holds.
  split; revert r E e Φ Hr.
  - induction n as [n IH] using lt_wf_ind=> r1 E e Φ ? Hwp.
78
    case EQ: (to_val e)=>[v|].
79
    + rewrite -(of_to_val _ _ EQ) {IH}. constructor. rewrite pvs_eq.
80
      intros [|k] Ef σ rf ???; first omega.
81
      apply wp_fix_unfold in Hwp; last done.
82 83
      destruct (Hwp k Ef σ rf); auto.
    + constructor; [done|]=> k Ef σ1 rf ???.
84
      apply wp_fix_unfold in Hwp; last done.
85
      destruct (Hwp k Ef σ1 rf) as [Hval [Hred Hpstep]]; auto.
86 87 88 89 90
      split; [done|]=> e2 σ2 ef ?.
      destruct (Hpstep e2 σ2 ef) as (r2&r2'&?&?&?); [done..|].
      exists r2, r2'; split_and?; auto.
      intros ? ->. change (weakestpre.wp_pre  (cconst True%I) e' k r2'); eauto.
  - induction n as [n IH] using lt_wf_ind=> r1 E e Φ ? Hwp.
91
    apply wp_fix_unfold; [done|]=> k Ef σ1 rf ???. split.
92 93
    + intros v Hval.
      destruct Hwp as [??? Hpvs|]; rewrite ?to_of_val in Hval; simplify_eq/=.
94
      rewrite pvs_eq in Hpvs.
95
      destruct (Hpvs (S k) Ef σ1 rf) as (r2&?&?); eauto.
96 97
    + intros Hval ?.
      destruct Hwp as [|???? Hwp]; rewrite ?to_of_val in Hval; simplify_eq/=.
98
      edestruct (Hwp k Ef σ1 rf) as [? Hpstep]; auto.
99 100 101 102
      split; [done|]=> e2 σ2 ef ?.
      destruct (Hpstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
      exists r2, r2'. destruct ef; simpl; auto.
Qed.
Ralf Jung's avatar
Ralf Jung committed
103
End def.