# Force application of fixpoint to its argument

Hi everyone,
I know a lot of stackoverflow questions are close to this one, but I could not get any proposed solution to work. If one turned out to actually work, I’m sorry for the potential duplicate.

When I define a fixpoint function `my_function` that does not directly pattern match on its argument `a`, I cannot unfold it and explicitly see the body of the function in my hypothesis.

Here is a minimal example :

``````Fixpoint my_function (a: nat) :=
if PeanoNat.Nat.eqb a 42 then true
else
match a with
| S a' => my_function a'
| 0 => false end.

Lemma my_lemma:
forall x, my_function x = true -> x >= 42.
Proof.
intros. unfold my_function in H.
(*
at this point, I have:

x : nat
H : (fix my_function (a : nat) : bool :=
if PeanoNat.Nat.eqb a 42 then true else match a with
| 0 => false
| S a' => my_function a'
end) x = true
============================
x >= 42
*)
Abort.
``````

After the unfold, my function is not applied to its argument and stays in a strange unapplied form. I would like to have `H` transformed into:

``````(*
H : if PeanoNat.Nat.eqb x 42 then true else match x with
| 0 => false
| S a' => my_function a'
end = true
*)
``````

I don’t want to do this because I not able to prove the result in this case. This is a simplified minimal example of my situation. I know that destructing the argument makes Coq apply the function, but in my real case I cannot afford to do the destruct (2 arguments with ~60 constructors). I would like to be able to deal with the `if then else` cases that are before the pattern matching first, and then destruct the arguments. I can give more details to explain why I would like to do this specific rewrite rather than destructing.

Thank you for your help !
Best,
Clément

PS: I can easily prove a dummy lemma that says that an application of my function is equal to the body, and use it to rewrite. It seems like an ugly solution.

``````Lemma my_function_body:
forall a, my_function a =
if PeanoNat.Nat.eqb a 42 then true
else
match a with
| S a' => my_function a'
| 0 => false end.
Proof.
intros. unfold my_function.
destruct a; reflexivity.
Qed.
``````

There’s no other AFAIK

Do you know if there is some way (like ltac magic) to generate this lemma and its proof directly, rather than copy paste the body ?

I stumbled upon this coq-tricks/DefEquality.v at master · tchajed/coq-tricks · GitHub which might be linked, but couldn’t get it to work for my case either…

If you define your function with the Equations plugin instead of `Fixpoint` you get the unfolding equations generated for free.

I would also say that generating the unfolding lemma should be an easy exercise in a meta-programmin/plugin framework like MetaCoq or Coq-Elpi, but as far as I’m aware such a plugin doesn’t exist yet.

No need for a plugin — it’s very easy to generate the equation with plain Ltac:

``````Fixpoint my_function (a: nat) :=
if Nat.eqb a 42 then true
else
match a with
| S a' => my_function a'
| 0 => false end.

Definition unfolder : { f & forall x, my_function x = f x }.
Proof.
eexists ?[f].
[f]: intros x; destruct x.
destruct x; reflexivity.
Defined.

Definition unfolding_lemma := Eval simpl in projT2 unfolder.
``````

For a slightly cleaner unfolding, use `intros x; case x; unfold my_function at 1; fold my_function` instead of `destruct x` on the last line.

``````About unfolding_lemma.
``````
``````unfolding_lemma : forall x : nat,
my_function x = match x with
| 0 => false
| S x0 => if Nat.eqb x0 41 then true else my_function x0
end
``````

Note that the solution above pushes the `if` under the `match`. If you don’t want this, you can use Ltac 2; it’s a bit more complicated, but still manageable:

``````Fixpoint my_function (a: nat) :=
if Nat.eqb a 42 then true
else
match a with
| S a' => my_function a'
| 0 => false end.

From Ltac2 Require Import Ltac2 Constr.

Ltac2 reveal_fixpoint fn :=
match Unsafe.kind fn with
| Unsafe.Constant cst _ =>
Std.eval_unfold [(Std.ConstRef cst, Std.AllOccurrences)] fn
| _ => Control.throw Not_found
end.

Ltac2 unfold_fixpoint_once fn :=
let fixpoint := reveal_fixpoint fn in
match Unsafe.kind fixpoint with
| Unsafe.Fix _ _ binders bodies =>
let binder := Array.get binders 0 in
let unbound_body := Array.get bodies 0 in
let body := Unsafe.substnl [fn] 0 unbound_body in
match Unsafe.check body with
| Val b => b
| Err error => Control.throw error
end
| _ => Control.throw Not_found
end.

Notation beta x :=
ltac:(let x := (eval cbv beta in x) in exact x) (only parsing).

Lemma my_function_eqn : forall x: nat,
my_function x =
beta(ltac2:(let fn := unfold_fixpoint_once constr:(my_function) in exact \$fn) x).
Proof. intros; destruct x; reflexivity. Qed.

``````
``````my_function_eqn :
forall x : nat, my_function x =
(if Nat.eqb x 42 then true
else match x with
| 0 => false
| S a' => my_function a'
end)
``````
2 Likes

Thanks! That was exactly the kind of ltac2 black magic I was hoping someone would master. It works like a charm even in my more complex case (with 4 arguments to the function), but it has a strange side effect:
all my other previously defined ltac tactics are now `Unbound`. Is that some conflict between `Ltac` and `Ltac2` that you might know of ? Should I build a minimal example ?

1 Like

Importing Ltac2 changes the default tactic language to Ltac2, so you need to wrap everything in `ltac1:(…)`. The simplest solution to avoid that is to Import Ltac2 in a module, and expose just one notation (I usually just make a separate file):

``````From Ltac2 Require Ltac2.

Module Ltac2Magic.
Import Ltac2 Constr.

Ltac2 reveal_fixpoint fn :=
match Unsafe.kind fn with
| Unsafe.Constant cst _ =>
Std.eval_unfold [(Std.ConstRef cst, Std.AllOccurrences)] fn
| _ => Control.throw Not_found
end.

Ltac2 unfold_fixpoint_once fn :=
let fixpoint := reveal_fixpoint fn in
match Unsafe.kind fixpoint with
| Unsafe.Fix _ _ binders bodies =>
let binder := Array.get binders 0 in
let unbound_body := Array.get bodies 0 in
let body := Unsafe.substnl [fn] 0 unbound_body in
match Unsafe.check body with
| Val b => b
| Err error => Control.throw error
end
| _ => Control.throw Not_found
end.

Notation unfold_fixpoint_once fn :=
ltac2:(let fn := Constr.pretype fn in
let fn := unfold_fixpoint_once fn in exact \$fn) (only parsing).
End Ltac2Magic.

Notation beta x :=
ltac:(let x := (eval cbv beta in x) in exact x) (only parsing).

Fixpoint my_function (a: nat) :=
if Nat.eqb a 42 then true
else
match a with
| S a' => my_function a'
| 0 => false end.

Lemma my_function_eqn : forall x: nat,
my_function x =
beta((Ltac2Magic.unfold_fixpoint_once my_function) x).
Proof. intros; destruct x; reflexivity. Qed.
``````

I used the qualified name `Ltac2Magic.unfold_fixpoint_once` here, but you can also `Import Ltac2Magic`: that won’t break things because I `Import`-ed Ltac2 in the module, but I didn’t `Export` it.

1 Like

Works perfectly ! Thank you very much !

I tried this version also, but the computation of the unfolding lemma does not go through in a reasonable time (still no result after 5 minutes). Is there a solution ?
My try looks like this:

``````Definition unfolder : { f & forall t1 t2 a b, my_more_complex_function t1 t2 a b = f t1 t2 a b }.
Proof.
eexists ?[f].
[f]: intros t1; destruct t1.
intros t1; case t1; unfold my_more_complex_function at 1; fold my_more_complex_function; reflexivity.
Defined.
``````

Where `t1, t2, a, b` are elements of an inductive type with ~ 60 constructors

the computation of the unfolding lemma does not go through in a reasonable time (still no result after 5 minutes). Is there a solution ?

The `Eval simpl` part, right? Try this then (`simpl` can be extremely slow):

``````Definition unfolding_lemma :=
Eval cbv [projT2 unfolder] in projT2 unfolder.
``````

Or use `Derive`, though you’ll have to `unfold my_function'` after rewriting with the generated lemma:

``````Require Import Coq.derive.Derive.

Derive my_function' SuchThat (forall x, my_function x = my_function' x) As unfolding_lemma'.
Proof.
subst my_function'.
instantiate (1 := ltac:(intros x; destruct x)).
intros x; case x; unfold my_function at 1; fold my_function; reflexivity.
Qed.
``````

You can recover the pre-unfolded lemm this way:

``````Definition unfolding_lemma :
forall x, my_function x =
ltac:(let y := eval unfold my_function' in (my_function' x) in exact y) :=
unfolding_lemma'.
``````

Or like this, which is a gross hack (and it requires `Defined` instead of `Qed` above):

``````Definition unfolding_lemma :=
Eval unfold unfolding_lemma' in unfolding_lemma'.
``````

(But I still expect that you’ll prefer the Ltac2 version, because the Ltac version above flips the `if` and the `match`)