The one place for your designs
To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.
"Flattened" introduction patterns for intuitionistic conjunction elimination.
The "flattened" introduction patterns (I don't know the official terminology, but I meant the patterns like (H1 & H2 & H3 &H4)) interact in a weird way with intuitionistic conjunction:
In particular, I would expect to get a P from P ∧ Q ∧ R by iDestruct "H" as "(H&_&_)", but it doesn't work this way.
From iris.proofmode Require Import tactics monpred.
From iris.base_logic Require Import base_logic.
Section base_logic_tests.
Context {M : ucmraT}.
Implicit Types P Q R : uPred M.
Lemma test P Q R : (P ∧ Q ∧ R) -∗ P.
Proof.
iIntros "H".
(* This works fine *)
iDestruct "H" as "(_ & _ & H)".
Undo.
iDestruct "H" as "(_ & H & _)".
Undo.
(* This results in an error *)
Fail iDestruct "H" as "(H & _ & _)".
(* "Proper" way of doing it *)
iDestruct "H" as "(H & _)".
done.
Qed.