tactics.v 431 Bytes
Newer Older
Dan Frumin's avatar
Dan Frumin committed
1
From iris.proofmode Require Import tactics.
Dan Frumin's avatar
Dan Frumin committed
2 3 4 5 6 7 8 9 10 11
From iris_logrel.F_mu_ref_conc Require Export tactics notation.

Lemma wp_rec1 `{heapG Σ} Φ :
   Φ #4
   WP (λ: "y", (λ: "x", "x" + #3) "y") #1 {{ Φ }}.
Proof.
  iIntros "Z".
  wp_rec.
  wp_rec.
  wp_op.
Dan Frumin's avatar
Dan Frumin committed
12
  by wp_value.
Dan Frumin's avatar
Dan Frumin committed
13 14 15 16 17 18 19 20 21
Qed.

Lemma wp_proj2 `{heapG Σ} Φ :
   Φ #1
   WP Fst (Fst (#1,#2,#4)) {{ Φ }}.
Proof.
  iIntros "HΦ".
  wp_proj.
  wp_proj.
Dan Frumin's avatar
Dan Frumin committed
22
  by wp_value.
Dan Frumin's avatar
Dan Frumin committed
23
Qed.