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
|
Require Import Coq.Lists.List.
Section with_T.
Context {T : Type}.
Fixpoint length (ls : list T) : nat :=
match ls with
| nil => 0
| _ :: ls => S (length ls)
end.
End with_T.
Definition a_string := "hello...\n \r \\ \
world".
Definition zero_string := "0".
Definition b_string := "b".
Definition escape_string := """ hello world ".
Notation "A /\ B" := (and A B) : type_scope.
Theorem progress : ∀t T,
empty ⊢ t ∈ T →
value t ∨ ∃t', t --> t'.
Proof. Admitted.
Theorem ev_plus4 : ∀n, even n → even (4 + n).
Proof.
intros n H. simpl.
apply ev_SS.
apply ev_SS.
apply H.
Qed.
(*
The iris examples here are used under this license:
> All files in this development, excluding those in docs/ and tex/, are
distributed under the terms of the 3-clause BSD license
(https://opensource.org/licenses/BSD-3-Clause), included below.
> Copyright: Iris developers and contributors
*)
(* Unicode next to braces, mixed ascii/unicode operators. *)
Lemma ghost_var_update γ b' b c :
own γ (●E b) -∗ own γ (◯E c) ==∗ own γ (●E b') ∗ own γ (◯E b').
Proof.
something (a ={n}= b).
- by apply case1.
- apply case2. eauto.
Qed.
(* #[], {Σ}, `{!xxx}, (?)
https://gitlab.mpi-sws.org/iris/iris/-/blob/f1e2242daa0e448135a5074ce99b41e6058ea1c3/iris_heap_lang/adequacy.v *)
Definition heapΣ : gFunctors :=
#[invΣ; gen_heapΣ loc (option val); inv_heapΣ loc (option val); proph_mapΣ proph_id (val * val)].
Global Instance subG_heapGpreS {Σ} : subG heapΣ Σ → heapGpreS Σ.
Proof. solve_inG. Qed.
(* (?), `{!class}, greek lettering *)
Definition heap_adequacy Σ `{!heapGpreS Σ} s e σ φ :
(∀ `{!heapGS Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (? κs) "".
iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
iMod (inv_heap_init loc (option val)) as (?) ">Hi".
iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
(* lambda should highlight as an operator *)
iModIntro. iExists
(λ σ κs, (gen_heap_interp σ.(heap) ∗ proph_map_interp κs σ.(used_proph_id))%I),
(λ _, True%I).
iFrame. iApply (Hwp (HeapGS _ _ _ _ _)). done.
Qed.
(* thorny ops + braces + lettering
https://gitlab.mpi-sws.org/iris/iris/-/blob/f1e2242daa0e448135a5074ce99b41e6058ea1c3/iris_heap_lang/primitive_laws.value
BSD licensed *)
Lemma wp_rec_löb s E f x e Φ Ψ :
□ ( □ (∀ v, Ψ v -∗ WP (rec: f x := e)%V v @ s; E {{ Φ }}) -∗
∀ v, Ψ v -∗ WP (subst' x v (subst' f (rec: f x := e) e)) @ s; E {{ Φ }}) -∗
∀ v, Ψ v -∗ WP (rec: f x := e)%V v @ s; E {{ Φ }}.
Proof.
iIntros "#Hrec". iLöb as "IH". iIntros (v) "HΨ".
(* dotted gives a path *)
iApply lifting.wp_pure_step_later; first done.
iNext. iApply ("Hrec" with "[] HΨ"). iIntros "!>" (w) "HΨ".
iApply ("IH" with "HΨ").
Qed.
(* unicode symbols distinct from braces and idents *)
Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
¬ ✓(dq1 ⋅ dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
Proof. apply mapsto_frac_ne. Qed.
Lemma inv_mapsto_own_acc E l v I:
↑inv_heapN ⊆ E →
inv_heap_inv -∗ l ↦_I v ={E, E ∖ ↑inv_heapN}=∗
(⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ={E ∖ ↑inv_heapN, E}=∗ l ↦_I w)).
Proof. (*snip*) Qed.
Lemma mapsto_persist l dq v : l ↦{dq} v ==∗ l ↦□ v.
Proof.
refine ?[named]. refine ?[named2].
[named]: done.
[named2]: { done. }
(* Bullets are distinct from operators, and are treated as Punctuation *)
- done.
+ done.
-- done.
+ apply (f -888 + 5).
all: nice.
1: { done. }
1,2: { done. }
1,2,3: { done. }
Qed.
Unset Implicit Arguments.
Set Strict Implicit.
Set Printing Notations.
CoInductive Trace (A:automaton) : states A -> LList (actions A) -> Prop :=
| empty_trace : forall q:states A, deadlock A q -> Trace A q LNil
| lcons_trace :
forall (q q':states A) (a:actions A) (l:LList (actions A)),
In q' (transitions A q a) -> Trace A q' l -> Trace A q (LCons a l).
Set Implicit Arguments.
Unset Strict Implicit.
|
