SIGINT as Prolog cut

proof_by_ctrl_c.v

(*
 * Copyright (C) BedRock Systems Inc. 2020-22
 *
 * This software is distributed under the terms of the BedRock Open-Source License.
 * See the LICENSE-BedRock file in the repository root for details.
 *)
Require Export stdpp.fin_sets.
Require Export iris.prelude.prelude.

(** * Small extensions to [stdpp.fin_sets]. *)

Section finset.
  #[local] Set Default Proof Using "Type*".
  Context `{FinSet A C}.
  Implicit Types X Y : C.

  #[global] Instance list_to_set_elements_cancel :
    Cancel (≡@{C}) list_to_set elements | 100 := list_to_set_elements.

  #[global] Instance elements_inj : Inj equiv eq (elements (C := C)) | 100.
  Proof. apply: (cancel_inj (f := list_to_set)). Qed.

  Lemma elements_set_equiv_1 (x y : C) :
    elements x = elements y -> x ≡ y.
  Proof.
    apply: (inj elements). (* Press Ctrl-C here to help the proof succeed. *)
  Succeed Qed. Restart. Proof.
    Timeout 1 apply: (inj elements). (* Automating Ctrl-C *)
  Succeed Qed. Restart. Proof.
  (* A few alternatives that work immediately *)
    move: x y. apply: (inj elements).
  Succeed Qed. Restart. Proof.
    apply (inj elements).
  Succeed Qed. Restart. Proof.
    apply: (inj (elements (C := C))). 
    (* [elements] projects from an arbitrary [Elements] instance, so it can
    unify against too many choices causing diverges; OTOH fixing [C] fixes the
    instance to consider. *)
  Qed.
End finset.

Tested on both Coq 8.15 and on the 8.16 platform:

$ opam list coq coq-stdpp coq-iris
# Packages matching: (name-match(coq) | name-match(coq-stdpp) | name-match(coq-iris)) & (installed | available)
# Name    # Installed # Synopsis
coq       8.16.0      pinned to version 8.16.0
coq-iris  4.0.0       A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs
coq-stdpp 1.8.0       An extended "Standard Library" for Coq