tests.v 4.73 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
(** This file is essentially a bunch of testcases. *)
2
Require Import program_logic.upred.
Ralf Jung's avatar
Ralf Jung committed
3
Require Import heap_lang.lifting heap_lang.sugar.
4
Import heap_lang.
5
Import uPred.
Ralf Jung's avatar
Ralf Jung committed
6 7

Module LangTests.
8
  Definition add := Plus (LitNat 21) (LitNat 21).
9
  Goal  σ, prim_step add σ (LitNat 42) σ None.
10
  Proof. intros; do_step done. Qed.
11
  Definition rec := Rec (App (Var 0) (Var 1)). (* fix f x => f x *)
12
  Definition rec_app := App rec (LitNat 0).
Ralf Jung's avatar
Ralf Jung committed
13
  Goal  σ, prim_step rec_app σ rec_app σ None.
14
  Proof. intros; do_step done. Qed.
15 16
  Definition lam := Lam (Plus (Var 0) (LitNat 21)).
  Goal  σ, prim_step (App lam (LitNat 21)) σ add σ None.
17
  Proof. intros; do_step done. Qed.
Ralf Jung's avatar
Ralf Jung committed
18 19
End LangTests.

20
Module LiftingTests.
21 22
  Context {Σ : iFunctor}.
  Implicit Types P : iProp heap_lang Σ.
23
  Implicit Types Q : val  iProp heap_lang Σ.
24

25 26
  (* TODO RJ: Some syntactic sugar for language expressions would be nice. *)
  Definition e3 := Load (Var 0).
27
  Definition e2 := Seq (Store (Var 0) (Plus (Load $ Var 0) (LitNat 1))) e3.
28
  Definition e := Let (Alloc (LitNat 1)) e2.
29
  Goal  σ E, (ownP σ : iProp heap_lang Σ)  (wp E e (λ v, (v = LitNatV 2))).
30 31
  Proof.
    move=> σ E. rewrite /e.
32
    rewrite -wp_let. rewrite -wp_alloc_pst; last done.
33 34 35
    apply sep_intro_True_r; first done.
    rewrite -later_intro. apply forall_intro=>l.
    apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_.
36
    rewrite -later_intro. asimpl.
37 38 39
    rewrite -(wp_bindi (SeqCtx (Load (Loc _)))).
    rewrite -(wp_bindi (StoreRCtx (LocV _))).
    rewrite -(wp_bindi (PlusLCtx _)).
40
    rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
41
    { by rewrite lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
42
    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
Ralf Jung's avatar
Ralf Jung committed
43
    rewrite -wp_plus -later_intro.
44
    rewrite -wp_store_pst; first (apply sep_intro_True_r; first done); last first.
45 46
    { by rewrite lookup_insert. }
    { done. }
47
    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
48
    rewrite -wp_lam // -later_intro. asimpl.
49
    rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
50
    { by rewrite lookup_insert. }
51
    rewrite -later_intro. apply wand_intro_l. rewrite right_id.
52 53
    by apply const_intro.
  Qed.
54 55 56 57 58 59

  Definition FindPred' n1 Sn1 n2 f := If (Lt Sn1 n2)
                                      (App f Sn1)
                                      n1.
  Definition FindPred n2 := Rec (Let (Plus (Var 1) (LitNat 1))
                                     (FindPred' (Var 2) (Var 0) n2.[ren(+3)] (Var 1))).
Ralf Jung's avatar
Ralf Jung committed
60 61 62 63 64
  Definition Pred := Lam (If (Le (Var 0) (LitNat 0))
                             (LitNat 0)
                             (App (FindPred (Var 0)) (LitNat 0))
                         ).

65 66
  Lemma FindPred_spec n1 n2 E Q :
    ((n1 < n2)  Q (LitNatV $ pred n2)) 
67
       wp E (App (FindPred (LitNat n2)) (LitNat n1)) Q.
68 69 70 71 72 73 74 75
  Proof.
    revert n1. apply löb_all_1=>n1.
    rewrite -wp_rec //. asimpl.
    (* Get rid of the ▷ in the premise. *)
    etransitivity; first (etransitivity; last eapply equiv_spec, later_and).
    { apply and_mono; first done. by rewrite -later_intro. }
    apply later_mono.
    (* Go on. *)
76
    rewrite -(wp_let _ _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred $ LitNat n2))).
77
    rewrite -wp_plus. asimpl.
78
    rewrite -(wp_bindi (CaseCtx _ _)).
79
    rewrite -!later_intro /=.
80
    apply wp_lt; intros Hn12.
81
    * (* TODO RJ: It would be better if we could use wp_if_true here
82 83 84
         (and below). But we cannot, because the substitutions in there
         got already unfolded. *)
      rewrite -wp_case_inl //.
85
      rewrite -!later_intro. asimpl.
86
      rewrite (forall_elim (S n1)).
87 88 89
      eapply impl_elim; first by eapply and_elim_l. apply and_intro.
      + apply const_intro; omega.
      + by rewrite !and_elim_r.
90
    * rewrite -wp_case_inr //.
91
      rewrite -!later_intro -wp_value' //.
92
      rewrite and_elim_r. apply const_elim_l=>Hle.
Ralf Jung's avatar
Ralf Jung committed
93
      by replace n1 with (pred n2) by omega.
94 95 96
  Qed.

  Lemma Pred_spec n E Q :
97
    Q (LitNatV $ pred n)  wp E (App Pred (LitNat n)) Q.
98 99
  Proof.
    rewrite -wp_lam //. asimpl.
100
    rewrite -(wp_bindi (CaseCtx _ _)).
101
    apply later_mono, wp_le=> Hn.
Ralf Jung's avatar
Ralf Jung committed
102 103
    - rewrite -wp_case_inl //.
      rewrite -!later_intro -wp_value' //.
Ralf Jung's avatar
Ralf Jung committed
104
      by replace n with 0 by omega.
Ralf Jung's avatar
Ralf Jung committed
105
    - rewrite -wp_case_inr //.
106
      rewrite -!later_intro -FindPred_spec.
Ralf Jung's avatar
Ralf Jung committed
107
      auto using and_intro, const_intro with omega.
108
  Qed.
Ralf Jung's avatar
Ralf Jung committed
109

110
  Goal  E,
111 112
    True  wp (Σ:=Σ) E
      (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (λ v, (v = LitNatV 40)).
Ralf Jung's avatar
Ralf Jung committed
113 114 115 116 117
  Proof.
    intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro.
    asimpl. (* TODO RJ: Can we somehow make it so that Pred gets folded again? *)
    rewrite -Pred_spec -later_intro. by apply const_intro.
  Qed.
118
End LiftingTests.