Rewrite set equality inside a let expression

Using Rocq
1

Hello! Is it possible to make a rewriting inside a let expression that in turn is inside an Inductive definition? More precisely, I am using the Metalib package where [=] represents set equality. I have an hypothesis of the form H: a [=] b, and I want to replace some occurrences of a for b (rewrite H) inside a let expression that, in turn, is inside an Inductive definition. My current proof context is:

 Hfv : fv_nom u [=] fv_nom u'
  ============================
  (let (z, _) := atom_fresh (union (fv_nom u) (union (fv_nom (n_abs y t1)) (singleton x))) in
   n_abs z (subst_rec_fun (swap y z t1) u x)) =a
  (let (z, _) := atom_fresh (union (fv_nom u') (union (fv_nom (n_abs y t1)) (singleton x))) in
   n_abs z (subst_rec_fun (swap y z t1) u' x))

where =a is an inductive predicate. I want to replace (fv_nom u) for (fv_nom u’) in the goal. When I try to “rewrite Hfv” I get Error: build_signature: no constraint can apply on a dependent argument.

Thank you in advance!

Regards,
Flávio.

2

Hi! As a complement to the previous question: the problem is in fact related to the let expression. The following example shows that even if the inductive =a is not in the context, the problem remain the same:

Parameter a b: atom.
Lemma test: (singleton a) [=] (singleton b) -> let (x,_) := atom_fresh (singleton a) in True.
Proof.
 intro H. Fail rewrite H.

The command has indeed failed with message:
build_signature: no constraint can apply on a dependent argument

Any help is very welcome.

Regards,
Flávio.

3

Hum, For the short example, I’m afraid this is a limitation of “setoid rewriting”. Maybe using a definition LET : forall A B, forall a:A, (forall a:A, B a) -> B a.

Another solution would be to first rewrite atom_fresh (singleton a) into pair (fst (atom_fresh (singleton a)) (snd (atom_fresh (singleton a))) (for whatever constructor pair and projections fst and snd available in your type). The let would then reduce.

4

Sorry to revisit this old question, but I still haven’t found a satisfactory solution. Back in 2023, I was using Coq 8.? and now with Rocq 9.1.1, I’m still unable to use setoid rewriting inside the body of a let expression. The error message is the same.

To clarify: I need to perform the rewrite *before* evaluating the let expression. Concretely, I have a hypothesis

H: t [=] u

(with a user-defined equality [=]) and a goal containing a let expression as follows:

let x := r in s

where r may have occurrencesof t. Before evaluating the let expression, I would like to rewrite H and replace all occurrences of t in r by u, and then evaluate the let expression.

Above, Herbelin suggested this might be a limitation of setoid rewriting. So my question is: should I expect this limitation to be permanent? Is there a logical/theoretical issue that prevents setoid rewriting in the body of a let expression?

Best regards,

Flávio.

5

May be solved by Support generalized rewriting in let bindings by mattam82 · Pull Request #20985 · rocq-prover/rocq · GitHub (not yet merged)

6

Very good news! Thanks!