"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.