Clément Pit-Claudel (Feb 10 2021 at 05:48): 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] *).
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 _).
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.
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".
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:
bis 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
dletwhich only works in the case theletcan 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.
Théo Winterhalter said:
I don't think it works, because
let x := ?v in ?fwill not match iffmentionsx.
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.
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: Oct 01 2023 at 18:01 UTC