Skip to content
Snippets Groups Projects
Commit 40ab3fea authored by Ralf Jung's avatar Ralf Jung
Browse files

normalize 'subgoal' to 'goal' to account for Coq output change

parent bbaf3eaf
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 178 additions and 176 deletions
test-normalizer.sed
+ 2
− 0
View file @ 40ab3fea
# adjust for https://github.com/coq/coq/pull/10239
s/(simple_intropattern)/(intropattern)/g
# adjust for https://github.com/coq/coq/pull/13656
s/subgoal/goal/g
tests/atomic.ref
+ 30
− 30
View file @ 40ab3fea
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -20,14 +20,14 @@ The command has indeed failed with message:
Tactic failure: iAuIntro: not all spatial assumptions are laterable.
"printing"
: string
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
============================
⊢ <<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -38,7 +38,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -52,14 +52,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
⊢ <<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -70,7 +70,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -83,14 +83,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
⊢ <<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -101,7 +101,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -115,14 +115,14 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
l : loc
============================
⊢ <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -133,7 +133,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -148,7 +148,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
"Now come the long pre/post tests"
: string
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -157,7 +157,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -169,7 +169,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -178,7 +178,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -190,7 +190,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -200,7 +200,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
code @ ⊤
<<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
RET #() >>>
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -214,7 +214,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -223,7 +223,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< l ↦ x, RET #() >>>
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -235,7 +235,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -245,7 +245,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< ∃ y : val, l ↦ y, RET #() >>>
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -258,7 +258,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -268,7 +268,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
code @ ⊤
<<< l ↦ #(), RET #() >>>
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -281,7 +281,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -291,7 +291,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
code @ ⊤
<<< l ↦ yyyy, RET #() >>>
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -304,7 +304,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
--------------------------------------∗
WP code {{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -315,7 +315,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
code @ ⊤
<<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
RET #() >>>
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -331,7 +331,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
"Prettification"
: string
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......
tests/heap_lang.ref
+ 27
− 27
View file @ 40ab3fea
"heap_e_spec"
: string
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -9,7 +9,7 @@
--------------------------------------∗
WP let: "x" := ref #1 in "x" <- ! "x" + #1;; ! "x" @ E {{ v, ⌜v = #2⌝ }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -22,7 +22,7 @@
"heap_e2_spec"
: string
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -34,7 +34,7 @@
WP let: "x" := #l in let: "y" := ref #1 in "x" <- ! "x" + #1;; ! "x"
@ E [{ v, ⌜v = #2⌝ }]
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -48,7 +48,7 @@
"heap_e7_spec"
: string
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -58,7 +58,7 @@
--------------------------------------∗
WP CmpXchg #l #0 #1 {{ _, l ↦ #1 }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -68,7 +68,7 @@
--------------------------------------∗
|={⊤}=> l ↦ #1
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -79,7 +79,7 @@
--------------------------------------∗
|={⊤}=> True
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -93,7 +93,7 @@
The command has indeed failed with message:
Tactic failure: wp_pure: cannot find ?y in (Var "x") or
?y is not a redex.
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -101,7 +101,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
--------------------------------------∗
WP "x" {{ _, True }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -117,7 +117,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
"test_array_fraction_destruct"
: string
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -131,7 +131,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
"test_wp_finish_fupd"
: string
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -142,7 +142,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
"test_twp_finish_fupd"
: string
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -151,7 +151,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
--------------------------------------∗
|={⊤}=> True
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -165,7 +165,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
--------------------------------------∗
WP ! #l {{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -179,7 +179,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
--------------------------------------∗
WP ! #l [{ v, Φ v }]
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -190,7 +190,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
⊢ l ↦_(λ _ : val, I #true) □
"wp_iMod_fupd_atomic"
: string
2 subgoals
2 goals
Σ : gFunctors
heapG0 : heapG Σ
......@@ -199,14 +199,14 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
============================
Atomic (stuckness_to_atomicity NotStuck) (#() #())
subgoal 2 is:
goal 2 is:
"H" : P
--------------------------------------∗
WP #() #() @ E2 {{ _, |={E2,E1}=> True }}
"wp_iInv_atomic"
: string
2 subgoals
2 goals
Σ : gFunctors
heapG0 : heapG Σ
......@@ -217,7 +217,7 @@ WP #() #() @ E2 {{ _, |={E2,E1}=> True }}
============================
Atomic (stuckness_to_atomicity NotStuck) (#() #())
subgoal 2 is:
goal 2 is:
"H" : ▷ P
"Hclose" : ▷ P ={E ∖ ↑N,E}=∗ emp
--------------------------------------∗
......@@ -225,7 +225,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N,E}=> True }}
"wp_iInv_atomic_acc"
: string
2 subgoals
2 goals
Σ : gFunctors
heapG0 : heapG Σ
......@@ -236,12 +236,12 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N,E}=> True }}
============================
Atomic (stuckness_to_atomicity NotStuck) (#() #())
subgoal 2 is:
goal 2 is:
"H" : ▷ P
--------------------------------------∗
WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -249,7 +249,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
--------------------------------------∗
WP let: "f" := λ: "x", "x" in ref ("f" #10) {{ _, True }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -261,7 +261,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
{{ _, True }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -274,7 +274,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
{{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -288,7 +288,7 @@ WP #() #() @ E ∖ ↑N {{ _, |={E ∖ ↑N}=> ▷ P ∗ True }}
let: "v" := fun3 "v" in if: "v" = "v" then "v" else "v"
@ E {{ v, Φ v }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......
tests/heap_lang2.ref
+ 3
− 3
View file @ 40ab3fea
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
P, Q : iProp Σ
============================
P ={⊤}=∗ Q
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -17,7 +17,7 @@
let: "val3" := fun3 "val2" in if: "val1" = "val2" then "val" else "val3"
{{ _, True }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......
tests/ipm_paper.ref
+ 7
− 7
View file @ 40ab3fea
"sep_exist"
: string
1 subgoal
1 goal
M : ucmraT
A : Type
......@@ -14,7 +14,7 @@
--------------------------------------∗
Ψ x ∗ P
2 subgoals
2 goals
M : ucmraT
A : Type
......@@ -27,13 +27,13 @@
Ψ x
subgoal 2 is:
goal 2 is:
"HP" : P
"HR" : R
--------------------------------------∗
P
1 subgoal
1 goal
M : ucmraT
A : Type
......@@ -48,7 +48,7 @@ P
"sep_exist_short"
: string
1 subgoal
1 goal
M : ucmraT
A : Type
......@@ -63,7 +63,7 @@ P
"read_spec"
: string
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -79,7 +79,7 @@ P
--------------------------------------∗
WP ! #l {{ v, ∃ m : nat, ⌜v = #m ∧ n ≤ m⌝ ∧ C l m }}
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......
tests/list_reverse.ref
+ 2
− 2
View file @ 40ab3fea
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -12,7 +12,7 @@
--------------------------------------∗
WP rev hd acc [{ v, Φ v }]
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......
tests/mosel_paper.ref
+ 14
− 14
View file @ 40ab3fea
1 subgoal
1 goal
PROP : bi
A : Type
......@@ -10,7 +10,7 @@
--------------------------------------∗
∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
1 subgoal
1 goal
PROP : bi
A : Type
......@@ -23,7 +23,7 @@
--------------------------------------∗
∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
1 subgoal
1 goal
PROP : bi
A : Type
......@@ -36,7 +36,7 @@
--------------------------------------∗
∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
1 subgoal
1 goal
PROP : bi
A : Type
......@@ -48,7 +48,7 @@
--------------------------------------∗
∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
1 subgoal
1 goal
PROP : bi
A : Type
......@@ -59,7 +59,7 @@
--------------------------------------∗
∃ x : A, Φ x ∨ Ψ x
1 subgoal
1 goal
PROP : bi
A : Type
......@@ -72,7 +72,7 @@
--------------------------------------∗
Φ x
1 subgoal
1 goal
PROP : bi
A : Type
......@@ -85,7 +85,7 @@
--------------------------------------∗
P ∗ Ψ x
1 subgoal
1 goal
PROP : bi
A : Type
......@@ -98,7 +98,7 @@
--------------------------------------∗
∃ a : A, Φ a ∨ P ∗ P ∗ Ψ a
1 subgoal
1 goal
PROP : bi
A : Type
......@@ -112,7 +112,7 @@
--------------------------------------∗
P ∗ P ∗ Ψ x
1 subgoal
1 goal
PROP : bi
A : Type
......@@ -123,7 +123,7 @@
--------------------------------------□
□ (P ∗ Q)
1 subgoal
1 goal
I : biIndex
PROP : bi
......@@ -134,7 +134,7 @@
--------------------------------------∗
Ψ
1 subgoal
1 goal
I : biIndex
PROP : bi
......@@ -143,7 +143,7 @@
--------------------------------------∗
∀ i : I, Φ i ∗ (Φ -∗ Ψ) i -∗ Ψ i
1 subgoal
1 goal
I : biIndex
PROP : bi
......@@ -157,7 +157,7 @@
--------------------------------------∗
⎡ P ∗ Q ⎤
1 subgoal
1 goal
I : biIndex
PROP : bi
......
tests/one_shot.ref
+ 2
− 2
View file @ 40ab3fea
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -17,7 +17,7 @@
∗ (⌜InjLV #() = InjLV #()⌝
∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......
tests/one_shot_once.ref
+ 2
− 2
View file @ 40ab3fea
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......@@ -17,7 +17,7 @@
∗ (⌜InjLV #() = InjLV #()⌝
∨ (∃ n : Z, ⌜InjLV #() = InjRV #n⌝ ∗ own γ (Shot n)))
1 subgoal
1 goal
Σ : gFunctors
heapG0 : heapG Σ
......
tests/proofmode.ref
+ 41
− 41
View file @ 40ab3fea
"demo_0"
: string
1 subgoal
1 goal
PROP : bi
P, Q : PROP
......@@ -11,7 +11,7 @@
--------------------------------------∗
Q ∨ P
1 subgoal
1 goal
PROP : bi
P, Q : PROP
......@@ -23,7 +23,7 @@
"test_iStopProof"
: string
1 subgoal
1 goal
PROP : bi
Q : PROP
......@@ -34,7 +34,7 @@
--------------------------------------∗
Q
1 subgoal
1 goal
PROP : bi
Q : PROP
......@@ -42,7 +42,7 @@
□ emp ∗ Q -∗ Q
"test_iDestruct_and_emp"
: string
1 subgoal
1 goal
PROP : bi
P, Q : PROP
......@@ -56,7 +56,7 @@
"test_iDestruct_spatial"
: string
1 subgoal
1 goal
PROP : bi
Q : PROP
......@@ -67,7 +67,7 @@
"test_iDestruct_spatial_affine"
: string
1 subgoal
1 goal
PROP : bi
Q : PROP
......@@ -83,7 +83,7 @@ The command has indeed failed with message:
Tactic failure: iExistDestruct: cannot destruct P.
"test_iDestruct_exists_intuitionistic"
: string
1 subgoal
1 goal
PROP : bi
P : PROP
......@@ -96,7 +96,7 @@ Tactic failure: iExistDestruct: cannot destruct P.
"test_iDestruct_exists_anonymous"
: string
1 subgoal
1 goal
PROP : bi
P : PROP
......@@ -109,7 +109,7 @@ Tactic failure: iExistDestruct: cannot destruct P.
"test_iIntros_forall_pure"
: string
1 subgoal
1 goal
PROP : bi
Ψ : nat → PROP
......@@ -120,7 +120,7 @@ Tactic failure: iExistDestruct: cannot destruct P.
"test_iIntros_pure_names"
: string
1 subgoal
1 goal
PROP : bi
H : True
......@@ -162,7 +162,7 @@ The command has indeed failed with message:
Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I with P.
"test_iNext_plus_3"
: string
1 subgoal
1 goal
PROP : bi
P, Q : PROP
......@@ -173,7 +173,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
"test_specialize_nested_intuitionistic"
: string
1 subgoal
1 goal
PROP : bi
φ : Prop
......@@ -189,7 +189,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
"test_iSimpl_in"
: string
1 subgoal
1 goal
PROP : bi
x, y : nat
......@@ -198,7 +198,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
--------------------------------------∗
⌜S (S (S x)) = y⌝
1 subgoal
1 goal
PROP : bi
x, y, z : nat
......@@ -208,7 +208,7 @@ Tactic failure: iSpecialize: cannot instantiate (⌜φ⌝ → P -∗ False)%I wi
--------------------------------------∗
⌜S (S (S x)) = y⌝
1 subgoal
1 goal
PROP : bi
x, y, z : nat
......@@ -225,7 +225,7 @@ The command has indeed failed with message:
Tactic failure: iEval: %: unsupported selection pattern.
"test_iFrame_later_1"
: string
1 subgoal
1 goal
PROP : bi
P, Q : PROP
......@@ -235,7 +235,7 @@ Tactic failure: iEval: %: unsupported selection pattern.
"test_iFrame_later_2"
: string
1 subgoal
1 goal
PROP : bi
P, Q : PROP
......@@ -247,7 +247,7 @@ The command has indeed failed with message:
Tactic failure: iFrame: cannot frame Q.
"test_and_sep_affine_bi"
: string
1 subgoal
1 goal
PROP : bi
BiAffine0 : BiAffine PROP
......@@ -260,7 +260,7 @@ Tactic failure: iFrame: cannot frame Q.
"test_big_sepL_simpl"
: string
1 subgoal
1 goal
PROP : bi
x : nat
......@@ -273,7 +273,7 @@ Tactic failure: iFrame: cannot frame Q.
--------------------------------------∗
P
1 subgoal
1 goal
PROP : bi
x : nat
......@@ -288,7 +288,7 @@ Tactic failure: iFrame: cannot frame Q.
"test_big_sepL2_simpl"
: string
1 subgoal
1 goal
PROP : bi
x1, x2 : nat
......@@ -301,7 +301,7 @@ Tactic failure: iFrame: cannot frame Q.
--------------------------------------∗
P ∨ ([∗ list] _;_ ∈ (x1 :: l1);(x2 :: l2), True)
1 subgoal
1 goal
PROP : bi
x1, x2 : nat
......@@ -317,7 +317,7 @@ Tactic failure: iFrame: cannot frame Q.
"test_big_sepL2_iDestruct"
: string
1 subgoal
1 goal
PROP : bi
Φ : nat → nat → PROP
......@@ -331,7 +331,7 @@ Tactic failure: iFrame: cannot frame Q.
"test_reducing_after_iDestruct"
: string
1 subgoal
1 goal
PROP : bi
============================
......@@ -341,7 +341,7 @@ Tactic failure: iFrame: cannot frame Q.
"test_reducing_after_iApply"
: string
1 subgoal
1 goal
PROP : bi
============================
......@@ -351,7 +351,7 @@ Tactic failure: iFrame: cannot frame Q.
"test_reducing_after_iApply_late_evar"
: string
1 subgoal
1 goal
PROP : bi
============================
......@@ -361,7 +361,7 @@ Tactic failure: iFrame: cannot frame Q.
"test_wandM"
: string
1 subgoal
1 goal
PROP : bi
mP : option PROP
......@@ -373,7 +373,7 @@ Tactic failure: iFrame: cannot frame Q.
--------------------------------------∗
R
1 subgoal
1 goal
PROP : bi
mP : option PROP
......@@ -385,7 +385,7 @@ Tactic failure: iFrame: cannot frame Q.
"elim_mod_accessor"
: string
1 subgoal
1 goal
PROP : bi
BiFUpd0 : BiFUpd PROP
......@@ -400,7 +400,7 @@ Tactic failure: iFrame: cannot frame Q.
"print_long_line_1"
: string
1 subgoal
1 goal
PROP : bi
BiFUpd0 : BiFUpd PROP
......@@ -411,7 +411,7 @@ Tactic failure: iFrame: cannot frame Q.
--------------------------------------∗
True
1 subgoal
1 goal
PROP : bi
BiFUpd0 : BiFUpd PROP
......@@ -424,7 +424,7 @@ Tactic failure: iFrame: cannot frame Q.
"print_long_line_2"
: string
1 subgoal
1 goal
PROP : bi
BiFUpd0 : BiFUpd PROP
......@@ -435,7 +435,7 @@ Tactic failure: iFrame: cannot frame Q.
--------------------------------------∗
True
1 subgoal
1 goal
PROP : bi
BiFUpd0 : BiFUpd PROP
......@@ -448,7 +448,7 @@ Tactic failure: iFrame: cannot frame Q.
"long_impl"
: string
1 subgoal
1 goal
PROP : bi
BiFUpd0 : BiFUpd PROP
......@@ -460,7 +460,7 @@ Tactic failure: iFrame: cannot frame Q.
"long_impl_nested"
: string
1 subgoal
1 goal
PROP : bi
BiFUpd0 : BiFUpd PROP
......@@ -473,7 +473,7 @@ Tactic failure: iFrame: cannot frame Q.
"long_wand"
: string
1 subgoal
1 goal
PROP : bi
BiFUpd0 : BiFUpd PROP
......@@ -485,7 +485,7 @@ Tactic failure: iFrame: cannot frame Q.
"long_wand_nested"
: string
1 subgoal
1 goal
PROP : bi
BiFUpd0 : BiFUpd PROP
......@@ -498,7 +498,7 @@ Tactic failure: iFrame: cannot frame Q.
"long_fupd"
: string
1 subgoal
1 goal
PROP : bi
BiFUpd0 : BiFUpd PROP
......@@ -511,7 +511,7 @@ Tactic failure: iFrame: cannot frame Q.
"long_fupd_nested"
: string
1 subgoal
1 goal
PROP : bi
BiFUpd0 : BiFUpd PROP
......@@ -709,7 +709,7 @@ The command has indeed failed with message:
Tactic failure: iLöb: no 'BiLöb' instance found.
"test_pure_name"
: string
1 subgoal
1 goal
PROP : bi
P : PROP
......
tests/proofmode_ascii.ref
+ 17
− 17
View file @ 40ab3fea
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -12,7 +12,7 @@
--------------------------------------□
|={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -28,7 +28,7 @@
--------------------------------------∗
|={⊤ ∖ ↑N,⊤}=> ▷ P
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -46,7 +46,7 @@
--------------------------------------∗
|={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> cinv_own γ p ∗ ▷ P)
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -65,7 +65,7 @@
--------------------------------------∗
|={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -86,7 +86,7 @@
|={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N))
∗ (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -117,7 +117,7 @@ The command has indeed failed with message:
Tactic failure: iInv: invariant "H2" not found.
"test_iInv"
: string
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -133,7 +133,7 @@ Tactic failure: iInv: invariant "H2" not found.
"test_iInv_with_close"
: string
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -150,42 +150,42 @@ Tactic failure: iInv: invariant "H2" not found.
"p1"
: string
1 subgoal
1 goal
PROP : bi
============================
forall P (_ : True), bi_entails P P
"p2"
: string
1 subgoal
1 goal
PROP : bi
============================
forall P, and True (bi_entails P P)
"p3"
: string
1 subgoal
1 goal
PROP : bi
============================
ex (fun P => bi_entails P P)
"p4"
: string
1 subgoal
1 goal
PROP : bi
============================
bi_emp_valid (bi_exist (fun x : nat => bi_pure (eq x O)))
"p5"
: string
1 subgoal
1 goal
PROP : bi
============================
bi_emp_valid (bi_exist (fun _ : nat => bi_pure (forall y : nat, eq y y)))
"p6"
: string
1 subgoal
1 goal
PROP : bi
============================
......@@ -198,7 +198,7 @@ Tactic failure: iInv: invariant "H2" not found.
bi_sep (bi_pure (forall y : nat, eq y y)) (bi_pure (eq z O))))))
"p7"
: string
1 subgoal
1 goal
PROP : bi
============================
......@@ -206,14 +206,14 @@ Tactic failure: iInv: invariant "H2" not found.
bi_entails (bi_pure True) (bi_pure (ge y O))
"p8"
: string
1 subgoal
1 goal
PROP : bi
============================
forall (a : nat) (_ : eq a O) (y : nat), bi_emp_valid (bi_pure (ge y O))
"p9"
: string
1 subgoal
1 goal
PROP : bi
============================
......
tests/proofmode_iris.ref
+ 12
− 12
View file @ 40ab3fea
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -12,7 +12,7 @@
--------------------------------------□
|={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> ▷ P)
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -28,7 +28,7 @@
--------------------------------------∗
|={⊤ ∖ ↑N,⊤}=> ▷ P
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -40,7 +40,7 @@
P : iProp Σ
============================
cinv N γ (<pers> P) ∗ cinv_own γ p ={⊤}=∗ cinv_own γ p ∗ ▷ P
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -58,7 +58,7 @@
--------------------------------------∗
|={⊤ ∖ ↑N}=> ▷ <pers> P ∗ (|={⊤}=> cinv_own γ p ∗ ▷ P)
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -77,7 +77,7 @@
--------------------------------------∗
|={⊤ ∖ ↑N,⊤}=> cinv_own γ p ∗ ▷ P
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -98,7 +98,7 @@
|={⊤}=> (▷ <pers> P ∗ na_own t (E2 ∖ ↑N))
∗ (na_own t E2 ={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P)
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -112,7 +112,7 @@
↑N ⊆ E2
→ na_inv t N (<pers> P) ∗ na_own t E1 ∗ na_own t E2
={⊤}=∗ na_own t E1 ∗ na_own t E2 ∗ ▷ P
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -143,7 +143,7 @@ The command has indeed failed with message:
Tactic failure: iInv: invariant "H2" not found.
"test_frac_split_combine"
: string
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -157,7 +157,7 @@ Tactic failure: iInv: invariant "H2" not found.
--------------------------------------∗
own γ 1%Qp
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -172,7 +172,7 @@ Tactic failure: iInv: invariant "H2" not found.
"test_iInv"
: string
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......@@ -188,7 +188,7 @@ Tactic failure: iInv: invariant "H2" not found.
"test_iInv_with_close"
: string
1 subgoal
1 goal
Σ : gFunctors
invG0 : invG Σ
......
tests/proofmode_monpred.ref
+ 7
− 7
View file @ 40ab3fea
1 subgoal
1 goal
I : biIndex
PROP : bi
......@@ -9,7 +9,7 @@
--------------------------------------∗
(P -∗ Q) i
1 subgoal
1 goal
I : biIndex
PROP : bi
......@@ -21,7 +21,7 @@
--------------------------------------∗
Q j
1 subgoal
1 goal
I : biIndex
PROP : bi
......@@ -35,7 +35,7 @@
--------------------------------------∗
∀ i, 𝓟 ∗ 𝓠 ∗ Q i
1 subgoal
1 goal
I : biIndex
PROP : bi
......@@ -46,7 +46,7 @@
--------------------------------------∗
(Q -∗ emp) i
1 subgoal
1 goal
I : biIndex
PROP : bi
......@@ -59,7 +59,7 @@
The command has indeed failed with message:
Tactic failure: iFrame: cannot frame (P i).
1 subgoal
1 goal
I : biIndex
Σ : gFunctors
......@@ -72,7 +72,7 @@ Tactic failure: iFrame: cannot frame (P i).
--------------------------------------□
|={⊤ ∖ ↑N}=> ⎡ ▷ <pers> 𝓟 ⎤ ∗ (|={⊤}=> ⎡ ▷ 𝓟 ⎤)
1 subgoal
1 goal
I : biIndex
Σ : gFunctors
......
tests/telescopes.ref
+ 12
− 12
View file @ 40ab3fea
1 subgoal
1 goal
PROP : bi
BiFUpd0 : BiFUpd PROP
......@@ -13,7 +13,7 @@
--------------------------------------∗
|={E2}=> ∃.. x : X, α x ∗ (β x ={E2,E1}=∗ γ2 x)
1 subgoal
1 goal
PROP : bi
BiFUpd0 : BiFUpd PROP
......@@ -22,7 +22,7 @@
α, β, γ1, γ2 : X → PROP
============================
accessor E1 E2 α β γ1 -∗ accessor E1 E2 α β (λ.. x : X, γ1 x ∨ γ2 x)
1 subgoal
1 goal
PROP : bi
BiFUpd0 : BiFUpd PROP
......@@ -35,7 +35,7 @@
--------------------------------------∗
(λ.. x0 : X, γ1 x0 ∨ γ2 x0) x
1 subgoal
1 goal
PROP : bi
BiFUpd0 : BiFUpd PROP
......@@ -48,7 +48,7 @@
--------------------------------------∗
γ1 x ∨ γ2 x
1 subgoal
1 goal
PROP : bi
BiFUpd0 : BiFUpd PROP
......@@ -60,7 +60,7 @@
"test1_test"
: string
1 subgoal
1 goal
PROP : bi
x : nat
......@@ -69,7 +69,7 @@
--------------------------------------∗
▷ False
1 subgoal
1 goal
PROP : bi
x : nat
......@@ -80,7 +80,7 @@
"test2_test"
: string
1 subgoal
1 goal
PROP : bi
============================
......@@ -88,7 +88,7 @@
--------------------------------------∗
False
1 subgoal
1 goal
PROP : bi
x : nat
......@@ -97,7 +97,7 @@
--------------------------------------∗
False
1 subgoal
1 goal
PROP : bi
x : nat
......@@ -108,7 +108,7 @@
"test3_test"
: string
1 subgoal
1 goal
PROP : bi
x : nat
......@@ -117,7 +117,7 @@
--------------------------------------∗
▷ False
1 subgoal
1 goal
PROP : bi
x : nat
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment