iris-tutorial/basics.v at master · gonzaloUr/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
132
133
134
135
136
From iris.base_logic Require Import iprop.
From iris.proofmode Require Import proofmode.

Section proofs.
Context {Σ: gFunctors}.

Lemma asm (P : iProp Σ) : P ⊢ P.
Proof.
  iStartProof.
  iIntros "H".
  iApply "H".
Qed.

Definition and_success (P Q : iProp Σ) : iProp Σ := (P ∧ Q)%I.

Lemma sep_comm (P Q : iProp Σ) : P ∗ Q ⊢ Q ∗ P.
Proof.
  iIntros "[HP HQ]".
  iSplitL "HQ".
  - iApply "HQ".
  - iApply "HP".
Qed.

Lemma modus_ponens (P Q : iProp Σ) : P -∗ (P -∗ Q) -∗ Q.
Proof.
  iIntros "HP, HPQ".
  iApply "HPQ".
  iAssumption.
Qed.

Lemma sep_assoc_1 (P Q R : iProp Σ) : P ∗ Q ∗ R ⊢ (P ∗ Q) ∗ R.
Proof.
  iIntros "[HP (HQ & HR)]".
  iSplitR "HR".
  - iSplitL "HP".
    * iAssumption.
    * iAssumption.
  - iAssumption.
Qed.

Lemma sep_comm_v2 (P Q : iProp Σ) : P ∗ Q ⊢ Q ∗ P.
Proof.
  iIntros "[HP HQ]".
  iFrame.
Qed.

Lemma sep_assoc_1_v2 (P Q R : iProp Σ) : P ∗ Q ∗ R ⊢ (P ∗ Q) ∗ R.
Proof.
  iIntros "[HP (HQ & HR)]".
  iFrame.
Qed.

Lemma wand_adj_1 (P Q R : iProp Σ) : (P -∗ Q -∗ R) ∗ P ∗ Q ⊢ R.
Proof.
  iIntros "(H & HP & HQ)".
  (**
    When applying ["H"], we get the subgoals [P] and [Q]. To specify that
    we want to use ["HP"] to prove the first subgoal, and ["HQ"] the second,
    we add ["HP"] in the first square bracket, and ["HQ"] in the second.
  *)
  iApply ("H" with "[HP] [HQ]").
  - iApply "HP".
  - iApply "HQ".
Qed.

Lemma wand_adj (P Q R : iProp Σ) : (P -∗ Q -∗ R) ⊣⊢ (P ∗ Q -∗ R).
Proof.
  iSplit.
  - iIntros "H (HP & HQ)".
    iApply ("H" with "[HP] [HQ]").
    * iAssumption.
    * iAssumption.
  - iIntros "H HP HQ".
    iApply "H".
    iFrame.
Qed.

Lemma or_comm (P Q : iProp Σ) : Q ∨ P ⊢ P ∨ Q.
Proof.
  iIntros "[HQ | HP]".
  - iRight.
    iAssumption.
  - iLeft.
    iAssumption.
Qed.

Lemma or_elim (P Q R : iProp Σ) : (P -∗ R) -∗ (Q -∗ R) -∗ P ∨ Q -∗ R.
Proof.
  iIntros "HPR HQR [HP | HQ]".
  - iApply "HPR".
    iAssumption.
  - iApply "HQR".
    iAssumption.
Qed.

Lemma sep_or_distr (P Q R : iProp Σ) : P ∗ (Q ∨ R) ⊣⊢ P ∗ Q ∨ P ∗ R.
Proof.
  iSplit.
  - iIntros "[HP [HQ | HR]]".
    * iLeft.
      iFrame.
    * iRight.
      iFrame.
  - iIntros "[[HP HQ] | [HP HR]]".
    * iSplitL "HP".
      + iAssumption.
      + iLeft.
        iAssumption.
    * iSplitL "HP".
      + iAssumption.
      + iRight.
        iAssumption.
Qed.

Lemma sep_exp_distr {A} (P : iProp Σ) (Φ : A → iProp Σ) : (P ∗ ∃ x, Φ x) ⊣⊢ ∃ x, P ∗ Φ x.
Proof.
  iSplit.
  - iIntros "(HP & %x & HΦ)".
    iExists x.
    iFrame.
  - iIntros "(%x & HP & HΦ)".
    iSplitL "HP".
    * iAssumption.
    * iExists x.
      iAssumption.
Qed.

Lemma sep_all_distr {A} (P Q : A → iProp Σ) : (∀ x, P x) ∗ (∀ x, Q x) -∗ (∀ x, P x ∗ Q x).
Proof.
  iIntros "[HP HQ] %x".
  iSplitL "HP".
  - iApply ("HP" $! x).
  - iApply ("HQ" $! x).
Qed.

End proofs.