## Stream: Coq users

### Topic: Unfold a constant in `Program` constraints

#### Clément Pit-Claudel (Feb 10 2021 at 05:48):

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] *).
``````

#### Jasper Hugunin (Feb 10 2021 at 06:00):

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).

#### Jasper Hugunin (Feb 10 2021 at 06:01):

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.

#### Clément Pit-Claudel (Feb 10 2021 at 06:10):

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)

#### Gaëtan Gilbert (Feb 10 2021 at 10:54):

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

#### Gaëtan Gilbert (Feb 10 2021 at 10:54):

I'm no Program expert but that sounds hard

#### Jasper Hugunin (Feb 10 2021 at 18:18):

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 _).
``````

#### Matthieu Sozeau (Feb 11 2021 at 19:38):

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

#### Clément Pit-Claudel (Feb 12 2021 at 02:20):

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`.

#### Théo Winterhalter (Feb 12 2021 at 07:13):

I guess you could `replace` with an evar and use `cbv zeta ; reflexivity` in the subgoal corresponding to the equality?

#### Gaëtan Gilbert (Feb 12 2021 at 10:20):

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

isn't it?

#### Clément Pit-Claudel (Feb 12 2021 at 14:03):

@Théo Winterhalter But `cbv zeta` would unfold more than one let, right?

#### Théo Winterhalter (Feb 12 2021 at 14:16):

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.

#### Théo Winterhalter (Feb 12 2021 at 14:24):

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.
``````

#### Théo Winterhalter (Feb 12 2021 at 14:27):

``````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.

#### Matthieu Sozeau (Feb 12 2021 at 18:28):

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

#### Clément Pit-Claudel (Feb 13 2021 at 04:53):

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".
``````

#### Clément Pit-Claudel (Feb 13 2021 at 04:57):

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?

#### Clément Pit-Claudel (Feb 13 2021 at 04:59):

@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?

#### Théo Winterhalter (Feb 13 2021 at 08:50):

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.

#### Gaëtan Gilbert (Feb 13 2021 at 09:07):

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`

#### Guillaume Melquiond (Feb 13 2021 at 14:45):

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.

#### Clément Pit-Claudel (Feb 13 2021 at 17:57):

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.

#### Clément Pit-Claudel (Feb 13 2021 at 18:09):

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.

#### Jason Gross (Feb 16 2021 at 20:14):

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

#### Théo Winterhalter (Feb 16 2021 at 20:26):

I don't think it works, because `let x := ?v in ?f` will not match if `f` mentions `x`.

#### Kenji Maillard (Feb 16 2021 at 20:27):

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

#### Théo Winterhalter (Feb 16 2021 at 20:28):

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.
``````

#### Kenji Maillard (Feb 16 2021 at 20:29):

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*)
``````

#### Guillaume Melquiond (Feb 16 2021 at 20:30):

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.

#### Théo Winterhalter (Feb 16 2021 at 20:31):

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

#### Théo Winterhalter (Feb 16 2021 at 20:32):

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.

#### Théo Winterhalter (Feb 16 2021 at 20:36):

So `match v with x => f` is just a way to write the substitution of `x` by `v` in the term `f`.

#### Jason Gross (Feb 16 2021 at 20:37):

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: Feb 08 2023 at 23:03 UTC