Merge branch 'msammler/assert_closed' into 'master'

Add is_closed_term tactic

See merge request iris/stdpp!345

CHANGELOG.md

@@ -5,6 +5,8 @@ API-breaking change is listed.
 
 Coq 8.10 is no longer supported by this release.
 
+- Add `is_closed_term` tactic for determining whether a term depends on variables bound
+  in the context. (by Michael Sammler)
 - Add `list.zip_with_take_both` and `list.zip_with_take_both'`
 - Specialize `list.zip_with_take_{l,r}`, add generalized lemmas `list.zip_with_take_{l,r}'`
 - Add `bool_to_Z` that converts true to 1 and false to 0. (by Michael Sammler)

tests/is_closed_term.ref

+"is_closed_term_test"
+     : string
+The command has indeed failed with message:
+Tactic failure: The term x is not closed.
+The command has indeed failed with message:
+Tactic failure: The term (x + 1) is not closed.
+The command has indeed failed with message:
+Tactic failure: The term (x + y) is not closed.
+The command has indeed failed with message:
+Tactic failure: The term section_variable is not closed.
+The command has indeed failed with message:
+Tactic failure: The term (section_variable + 1) is not closed.
+The command has indeed failed with message:
+Tactic failure: The term P is not closed.
+The command has indeed failed with message:
+Tactic failure: The term (P ∧ True) is not closed.

tests/is_closed_term.v

+From stdpp Require Import tactics strings.
+Unset Mangle Names.
+
+Section test.
+  Context (section_variable : nat).
+
+  Axiom axiom : nat.
+
+  Check "is_closed_term_test".
+  Lemma is_closed_term_test :
+    ∀ x y (P : Prop),
+      let a := 10 in
+      a = a →
+      let b := (a + 11) in
+      x + y = y + x.
+  Proof.
+    intros x y P a H b.
+    (* Constructors are closed. *)
+    is_closed_term 1.
+
+    (* Functions on closed terms are closed. *)
+    is_closed_term (1 + 1).
+
+    (* Variables bound in the context are not closed. *)
+    Fail is_closed_term x.
+    Fail is_closed_term (x + 1).
+    Fail is_closed_term (x + y).
+
+    (* Section variables are not closed. *)
+    Fail is_closed_term section_variable.
+    Fail is_closed_term (section_variable + 1).
+
+    (* Axioms are considered closed. (Arguably this is a bug, but
+    there is nothing we can do about it.) *)
+    is_closed_term axiom.
+    is_closed_term (axiom + 1).
+
+    (* Let-bindings are considered closed. *)
+    is_closed_term a.
+    is_closed_term (a + 1).
+    is_closed_term b.
+    is_closed_term (b + 1).
+
+    (* is_closed_term also works for propositions. *)
+    is_closed_term True.
+    is_closed_term (True ∧ True).
+    Fail is_closed_term P.
+    Fail is_closed_term (P ∧ True).
+
+    lia.
+  Qed.
+End test.

theories/tactics.v

@@ -599,6 +599,35 @@ Tactic Notation "revert" "select" open_constr(pat) := select pat (fun H => rever
 Tactic Notation "rename" "select" open_constr(pat) "into" ident(name) :=
   select pat (fun H => rename H into name).
 
+(** The tactic [is_closed_term t] succeeds if [t] is a closed term and fails otherwise.
+By closed we mean that [t] does not depend on any variable bound in the context.
+axioms are considered closed terms by this tactic (but Section
+variables are not). A function application is considered closed if the
+function and the argument are closed, without considering the body of
+the function (or whether it is opaque or not). This tactic is useful
+for example to decide whether to call [vm_compute] on [t].
+
+This trick was originally suggested by Jason Gross:
+https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Check.20that.20a.20term.20is.20closed.20in.20Ltac/near/240885618
+*)
+Ltac is_closed_term t :=
+  first [
+      (** We use the [assert_succeeds] sandbox to be able to freely
+      change the context. *)
+      assert_succeeds (
+          (** Make sure that the goal only contains [t]. (We use
+          [const False t] instead of [let x := t in False] as the
+          let-binding in the latter would be unfolded by the [unfold]
+          later.) *)
+          exfalso; change_no_check (const False t);
+          (** Clear all hypotheses. *)
+          repeat match goal with H : _ |- _ => try unfold H in *; clear H end;
+          (** If there are still hypotheses left, [t] is not closed. *)
+          lazymatch goal with H : _ |- _ => fail | _ => idtac end
+        ) |
+      fail 1 "The term" t "is not closed"
+    ].
+
 (** Coq's [firstorder] tactic fails or loops on rather small goals already. In
 particular, on those generated by the tactic [unfold_elem_ofs] which is used
 to solve propositions on sets. The [naive_solver] tactic implements an