Add Ltac2 Constr.is_prod_nd

doc/changelog/06-Ltac2-language/22261-ltac2-constr-is-prod-nd-Added.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  Ltac2 function ``Constr.is_prod_nd``
+  (`#22261 <https://github.com/rocq-prover/rocq/pull/22261>`_,
+  by Jason Gross).

test-suite/ltac2/constr_is_prod_nd.v

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 Type exn ::= [ Regression_Test_Failure ].
+Ltac2 check (b : bool) := if b then () else Control.throw Regression_Test_Failure.
+
+Ltac2 Eval check (Constr.is_prod_nd constr:(nat -> nat)).
+Ltac2 Eval check (Constr.is_prod_nd constr:(nat -> nat -> bool)).
+Ltac2 Eval check (Bool.neg (Constr.is_prod_nd constr:(forall n : nat, n = n))).
+Ltac2 Eval check (Constr.is_prod_nd constr:(forall _ : nat, nat)).
+Ltac2 Eval check (Bool.neg (Constr.is_prod_nd constr:(fun n : nat => n))).
+Ltac2 Eval check (Bool.neg (Constr.is_prod_nd constr:(0))).

theories/Ltac2/Constr.v

@@ -648,3 +648,11 @@ Ltac2 is_case(c: constr) :=
   | Unsafe.Case _ _ _ _ _ => true
   | _ => false
   end.
+
+(** [is_prod_nd c] returns [true] iff [c] is a non-dependent product,
+    i.e. a product whose codomain does not use the bound variable. *)
+Ltac2 is_prod_nd(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Prod _ body => Unsafe.noccurn 1 body
+  | _ => false
+  end.