Is there a way to make Program unfold a definition before computing a constraint? The following works with a regular `let`

but not with `dlet`

:

```
Definition dlet {A B} x (f: A -> B) := f x.
Program Definition x (f: forall x, x = 1 -> nat) : nat :=
dlet 1 (fun x => f x _). (* obligation is [forall x : Z, x = 1] instead of [1 = 1] *).
```

It would seem that you are asking to not just unfold but also reduce: there is no term you can put in for the underscore in that definition that is well typed (without assuming false).

With dependent types, `let x := y in t`

and `(fun x => t) y`

are not equivalent: there are situations like this one where the first is well typed but the second is not.

Jasper Hugunin said:

It would seem that you are asking to not just unfold but also reduce

You're right, or rather I think I want a third option, which is to automatically insert sigma-types as necessary; something like this:

```
Definition dlet {A B} x (f: A -> B) := f x.
Program Definition x (f: forall x, x = 1 -> nat) : nat :=
dlet (exist (fun x => x = 1) 1 eq_refl) (fun x => f x _).
```

(IIUC `Program`

's is basically to insert constraints like that, but I don't have a good intuition for how to force it to create additional constraints)

That would need Program to understand the difference between `dlet`

and `dlet' := @dlet nat nat`

since it also needs to mess with the type arguments

I'm no Program expert but that sounds hard

Would defining `dlet`

as `Definition dlet {A B} x (f : forall a : A, a = x -> B) := f x eq_refl.`

work for you?

(or `f : {a : A | a = x} -> B`

if you prefer the sigma type)

You can use it like

```
Definition dlet {A B} x (f: {a : A | a = x} -> B) := f (exist _ x eq_refl).
Program Definition x (f: forall x, x = 1 -> nat) : nat :=
dlet 1 (fun x => f x _).
```

To force program to insert an introduction in a sigma type, it needs to see a sigma type indeed

Got it, thanks everyone for the clarification, I learnt something :) I am right to think that this means that there's no way to write a lemma in Coq that unfolds one let-binding? Something like the following won't work for the exact reasons in this thread:

```
Lemma unfold_one_let {A B} {P: forall a: A, Type}
(a: A) (k: forall a, P a) (context: P a -> B) :
context (let x := a in k x) =
context (k a).
```

Is there even a way to unfold a single let-binding in Coq then? I can't `set`

the body of the let since that won't be well-typed, I can't `change`

the let to a dependently-typed dlet for the same reason, `cbv beta`

doesn't support `at 1`

… I guess it would need to be `change`

, but with Ltac 1 I can't think of a way to compute the second argument of the call to `change`

.

I guess you could `replace`

with an evar and use `cbv zeta ; reflexivity`

in the subgoal corresponding to the equality?

I can't set the body of the let since that won't be well-typed

isn't it?

@Théo Winterhalter But `cbv zeta`

would unfold more than one let, right?

Yes, hence my suggestion for using it in combination with `replace`

to focus on a subterm of the goal, but that might not work if itself contains `let`

-bindings.

Do you know how to one beta-reduction then?

I can turn one let into a beta-redex as follows:

```
Lemma foo :
forall n m,
0 + (let x := (let y := n in y + m) in
let y := (let z := m in z + m) in
x + y) = 0.
Proof.
intros n m.
match goal with
| |- context C [ let x := ?u in @?b x ] =>
let g := context C [ b u ] in
change g
end.
```

```
match goal with
| |- context C [ let x := ?u in @?b x ] =>
let g := context C [ b u ] in
let g' := eval cbn beta in g in
change g'
end.
```

seems to work fine, but might not be enough if you already have beta-redexes.

Gaëtan Gilbert said:

I can't set the body of the let since that won't be well-typed

isn't it?

@Gaëtan Gilbert is right, you can always `set`

any term, as that introduce a let-binding that is "transparent", not an abstraction

Théo Winterhalter said:

...

seems to work fine, but might not be enough if you already have beta-redexes.

No, it doesn't work, for the reason that Jasper was pointing earlier: `b`

is not typable as a function (you can't always convert a let into a function application):

```
Definition f (x: nat) (pr: x = 1) := true.
Goal (let x := 1 in f x eq_refl) = true.
match goal with
| |- context C [ let x := ?u in @?b x ] =>
let g := context C [ b u ] in
let g' := eval cbn beta in g in
change g'
end.
```

```
Error: Illegal application:
The term "f" of type "forall x : nat, x = 1 -> bool"
cannot be applied to the terms
"x" : "nat"
"eq_refl" : "x = x"
The 2nd term has type "x = x" which should be coercible to "x = 1".
```

Gaëtan Gilbert said:

I can't set the body of the let since that won't be well-typed

isn't it?

It's not; that's what Jasper was pointing out earlier.

```
Definition f (x: nat) (pr: x = 1) := true.
Goal (let x := 1 in let y := 2 in f x eq_refl) = true.
```

I can't `set `

the body of the `let x := ...`

, can I? The idea otherwise was that I would be able to `set`

that, then `cbv zeta`

, then subst the body back; but that would require capturing some function `k`

such that the term would be rewritable as `let x := 1 in k x`

, and I think that's what we concluded wasn't possible?

@Matthieu Sozeau but you can't `set`

a term with holes, so if you want to hide the body of the let to do a single zeta-reduction, you have to capture it as a function somehow, don't you? And you can't do that because the body isn't expressible as a function applied to an argument, unless you introduce extra arguments and casts. Right?

Clément Pit-Claudel said:

No, it doesn't work, for the reason that Jasper was pointing earlier:

`b`

is not typable as a function (you can't always convert a let into a function application):

I know, but I thought that since you were using your `dlet`

which only works in the case the `let`

can be made a function, it was not a problem for you. Sorry.

but that would require capturing some function k such that the term would be rewritable as let x := 1 in k x

that seems like a terminology issue, imo the body of the let is the `1`

For me, "body" was the part after `in`

, but you made me doubt, so I went to check. Common Lisp's specification agrees that the body is the part executed once the bindings have been established.

Ah, fun! Indeed I'm using the Lisp meaning:

```
(let VARLIST BODY...)
Bind variables according to VARLIST then eval BODY.
The value of the last form in BODY is returned.
Each element of VARLIST is a symbol (which is bound to nil)
or a list (SYMBOL VALUEFORM) (which binds SYMBOL to the value of VALUEFORM).
All the VALUEFORMs are evalled before any symbols are bound.
```

I guess it's by analogy with a function? The function body is what gets executed once the arguments are bound, not the value of the arguments that are passed to it.

Théo Winterhalter said:

I know, but I thought that since you were using your

`dlet`

which only works in the case the`let`

can be made a function, it was not a problem for you. Sorry.

Sorry, I should have been more clear. With dlet I can simply run `unfold dlet at 1`

; but I'm not sure that dlet works for my use case any more because of this equality propagation issue; so, I wonder if there's a general way to reduce just one let in Coq.

Is there even a way to unfold a single let-binding in Coq then?

```
Ltac zeta1 term :=
lazymatch term with
| let x := ?v in ?f => constr:(match v with x => f end)
end.
```

will take in a term with a `let`

at the head and return the term resulting from performing a single head zeta reduction

I don't think it works, because `let x := ?v in ?f`

will not match if `f`

mentions `x`

.

Why is there a zeta reduction happening with this code ? Naively I would have expected it to be the identity...

I tried using your tactic with my example and "No matching clauses for match":

```
Lemma foo :
forall n m,
0 + (let x := (let y := n in y + m) in
let y := (let z := m in z + m) in
x + y) = 0.
Proof.
intros n m.
lazymatch goal with
| |- ?t = _ =>
let t' := zeta1 t in
change t with t'
end.
```

Théo Winterhalter said:

I don't think it works, because

`let x := ?v in ?f`

will not match if`f`

mentions`x`

.

This works though...

```
Goal nat -> (nat -> nat -> nat) -> nat.
intros x f.
let t0 := constr:(let y := x in f y x) in
let t := zeta1 t0 in
idtac t. (* f x x*)
```

Yes, Coq happily leaves unbound variables in matched terms. As long as you end up closing them (the `with x => f`

of Jason), Coq will survive.

Ah yeah sorry, the error is different in my case.

I was sure it wouldn't work because `Hint Extern`

matching on `let x := ?v in ?f`

and `let x := _ in _`

behaved differently for me. Sorry for the noise.

So `match v with x => f`

is just a way to write the substitution of `x`

by `v`

in the term `f`

.

Yes. I learnt of this from Jonathan Leivent in 2016 on coqdev: https://sympa.inria.fr/sympa/arc/coqdev/2016-01/msg00060.html The thread there is illuminating

Last updated: Oct 13 2024 at 01:02 UTC