iris-tutorial/exercises/pure.v at master · Rocq-zh/iris-tutorial · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
From iris.base_logic Require Import upred iprop.
From iris.proofmode Require Import proofmode.

Section proofs.
Context {Σ : gFunctors}.

(*
  When stating lemmas that do not depend on generic Iris propositions
  (which mention [Σ]), we have to manually specify the [Σ]. We do this
  locally using notation.
*)
Local Notation "⊢ P" := (⊢@{iPropI Σ} P).
Local Notation "Q ⊢ P" := (Q ⊢@{iPropI Σ} P).

(* ################################################################# *)
(** * Pure Propositions *)

(**
  The implementation of Iris in Rocq has a unique class of propositions
  called `pure'. This class arises from the fact that Rocq propositions
  can be embedded into the logic of Iris. Any Rocq proposition [φ : Prop]
  can be turned into an Iris proposition through the pure embedding
  [⌜φ⌝ : iProp Σ]. This allows us to piggyback on much of the
  functionality and theory developed for the logic of Rocq. The
  proposition [⌜φ⌝] is thus an Iris proposition, and we can use it as we
  would any other Iris proposition.
*)

Lemma asm_pure (φ : Prop) : ⌜φ⌝ ⊢ ⌜φ⌝.
Proof.
  iIntros "H".
  iApply "H".
Qed.

(**
  A pure proposition is then any Iris proposition [P] for which there
  exists a Rocq proposition [φ], such that [P ⊣⊢ ⌜φ⌝].

  Pure propositions can be introduced using [iPureIntro]. This exits the
  Iris Proof Mode, throwing away the spatial context and turns the
  proposition into a Rocq proposition.
*)
Lemma eq_5_5 : ⊢ ⌜5 = 5⌝.
Proof.
  iPureIntro.
  reflexivity.
Qed.

(**
  To eliminate a pure proposition, we can use the specialization pattern
  ["%_"]. This adds the proposition to the non-spatial context as a Rocq
  proposition.
*)
Lemma eq_elm {A} (P : A → iProp Σ) (x y : A) : ⌜x = y⌝ -∗ P x -∗ P y.
Proof.
  iIntros "%Heq HP".
  rewrite -Heq.
  iApply "HP".
Qed.

(**
  It is quite easy to show that the propositions [⌜5 = 5⌝] and [⌜x = y⌝]
  from above are pure. However, it can become quite burdensome for more
  complicated Iris propositions. Fortunately, Iris has two typeclasses
  [IntoPure] and [FromPure] that can identify pure propositions for us.
  These are used by the [iPureIntro] tactic to identify pure
  propositions automatically.
*)

(** [True] is pure. *)
Lemma true_intro : ⊢ True.
Proof.
  iPureIntro.
  constructor.
Qed.

(** Conjunction preserves pureness. *)
Lemma and_pure : ⊢ ⌜5 = 5⌝ ∧ ⌜8 = 8⌝.
Proof.
  iPureIntro.
  split; reflexivity.
Qed.

(** Separating conjunction preserves pureness. *)
Lemma sep_pure : ⊢ ⌜5 = 5⌝ ∗ ⌜8 = 8⌝.
Proof.
  iPureIntro.
  split; reflexivity.
Qed.

(** Wand preserves pureness. *)
Lemma wand_pure {A} (x y : A) : ⊢ ⌜x = y⌝ -∗ ⌜y = x⌝.
Proof.
  iPureIntro.
  intros Heq.
  symmetry.
  assumption.
Qed.

(** Arbitrary Iris propositions are not pure. *)
Lemma abstr_not_pure (P : iProp Σ) : ⊢ P -∗ ⌜8 = 8⌝.
Proof.
  Fail iPureIntro. (* [P] is not pure *)
  iIntros "HP".
  iPureIntro. (* [⌜8 = 8⌝] is pure *)
  reflexivity.
Qed.

(**
  The pure embedding allows us to state an important property, namely
  soundness. Soundness is proved in the [uPred_primitive.pure_soundness]
  lemma stating: [∀ φ, (True ⊢ ⌜φ⌝) → φ]. This means that anything
  proved inside the Iris logic is as true as anything proved in Rocq.
*)

(**
  [⌜_⌝] turns Rocq propositions into Iris propositions, while [⊢ _] turns
  Iris propositions into Rocq propositions. These operations are not
  inverses, but they are related.
*)
Lemma pure_adj1 (φ : Prop) : φ → ⊢ ⌜φ⌝.
Proof.
  (* exercise *)
Admitted.

Lemma pure_adj2 (P : iProp Σ) : ⌜⊢ P⌝ -∗ P.
Proof.
  (* exercise *)
Admitted.

End proofs.