Commit 8fd3233e authored by Ralf Jung's avatar Ralf Jung
Browse files

tests/mosel_paper: show the two goals separately

parent f9435245
...@@ -10,7 +10,7 @@ ...@@ -10,7 +10,7 @@
--------------------------------------∗ --------------------------------------∗
∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
2 subgoals 1 subgoal
PROP : bi PROP : bi
A : Type A : Type
...@@ -23,13 +23,19 @@ ...@@ -23,13 +23,19 @@
--------------------------------------∗ --------------------------------------∗
∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a ∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
1 subgoal
subgoal 2 is:
"HP" : P PROP : bi
"H2" : Ψ x A : Type
--------------------------------------∗ P : PROP
∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a Φ, Ψ : A → PROP
x : A
============================
"HP" : P
"H2" : Ψ x
--------------------------------------∗
∃ a : A, P ∗ Φ a ∨ P ∗ Ψ a
1 subgoal 1 subgoal
PROP : bi PROP : bi
......
...@@ -12,9 +12,9 @@ Lemma example_1 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A → PROP) : ...@@ -12,9 +12,9 @@ Lemma example_1 {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A → PROP) :
P ( a, Φ a Ψ a) - a, (P Φ a) (P Ψ a). P ( a, Φ a Ψ a) - a, (P Φ a) (P Ψ a).
Proof. Proof.
iIntros "[HP H]". Show. iIntros "[HP H]". Show.
iDestruct "H" as (x) "[H1|H2]". Show. iDestruct "H" as (x) "[H1|H2]".
- iExists x. iLeft. iSplitL "HP"; iAssumption. - Show. iExists x. iLeft. iSplitL "HP"; iAssumption.
- iExists x. iRight. iSplitL "HP"; iAssumption. - Show. iExists x. iRight. iSplitL "HP"; iAssumption.
Qed. Qed.
Lemma example {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A PROP) : Lemma example {PROP : bi} {A : Type} (P : PROP) (Φ Ψ : A PROP) :
P ( a, Φ a Ψ a) - a, (P Φ a) (P Ψ a). P ( a, Φ a Ψ a) - a, (P Φ a) (P Ψ a).
......
Supports Markdown
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