Stream: Coq users

Topic: Unfold a constant in `Program` constraints


view this post on Zulip 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] *).

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (Feb 10 2021 at 10:54):

I'm no Program expert but that sounds hard

view this post on Zulip 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 _).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Clément Pit-Claudel (Feb 12 2021 at 14:03):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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".

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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*)

view this post on Zulip 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.

view this post on Zulip Théo Winterhalter (Feb 16 2021 at 20:31):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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