Make iDestruct smarter about when to copy a hypothesis.

It now copies the hypothesis when: 1.) it is persistent 2.) when destructing
it requires a universal quantifier to be instantiated. The new behavior is
implemented using a type class (called CopyDestruct) so that it can easily be
extended.

theories/proofmode/tactics.v

@@ -958,7 +958,27 @@ Tactic Notation "iRevertIntros" "(" ident(x1) ident(x2) ident(x3) ident(x4)
   iRevertIntros (x1 x2 x3 x4 x5 x6 x7 x8) "" with tac.
 
 (** * Destruct tactic *)
+Class CopyDestruct {M} (P : uPred M).
+Hint Mode CopyDestruct + ! : typeclass_instances.
+
+Instance copy_destruct_forall {M A} (Φ : A → uPred M) : CopyDestruct (∀ x, Φ x).
+Instance copy_destruct_impl {M} (P Q : uPred M) :
+  CopyDestruct Q → CopyDestruct (P → Q).
+Instance copy_destruct_wand {M} (P Q : uPred M) :
+  CopyDestruct Q → CopyDestruct (P -∗ Q).
+Instance copy_destruct_always {M} (P : uPred M) :
+  CopyDestruct P → CopyDestruct (□ P).
+
 Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
+  let hyp_name :=
+    lazymatch type of lem with
+    | string => constr:(Some lem)
+    | iTrm =>
+       lazymatch lem with
+       | @iTrm string ?H _ _ => constr:(Some H) | _ => constr:(@None string)
+       end
+    | _ => constr:(@None string)
+    end in
   let intro_destruct n :=
     let rec go n' :=
       lazymatch n' with
@@ -972,14 +992,25 @@ Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
   | Z => (* to make it work in Z_scope. We should just be able to bind
      tactic notation arguments to notation scopes. *)
      let n := eval compute in (Z.to_nat lem) in intro_destruct n
-  | string => tac lem
-  | iTrm =>
-     (* only copy the hypothesis when universal quantifiers are instantiated *)
-     lazymatch lem with
-     | @iTrm string ?H _ hnil ?pat => iSpecializeCore lem as p; last tac
-     | _ => iPoseProofCore lem as p false tac
+  | _ =>
+     (* Only copy the hypothesis in case there is a [CopyDestruct] instance.
+     Also, rule out cases in which it does not make sense to copy, namely when
+     destructing a lemma (instead of a hypothesis) or a spatial hyopthesis
+     (which cannot be kept). *)
+     lazymatch hyp_name with
+     | None => iPoseProofCore lem as p false tac
+     | Some ?H => iTypeOf H (fun q P =>
+        lazymatch q with
+        | true =>
+           (* persistent hypothesis, check for a CopyDestruct instance *)
+           tryif (let dummy := constr:(_ : CopyDestruct P) in idtac)
+           then (iPoseProofCore lem as p false tac)
+           else (iSpecializeCore lem as p; last (tac H))
+        | false =>
+           (* spatial hypothesis, cannot copy *)
+           iSpecializeCore lem as p; last (tac H)
+        end)
      end
-  | _ => iPoseProofCore lem as p false tac
   end.
 
 Tactic Notation "iDestruct" open_constr(lem) "as" constr(pat) :=