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.
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.
About my_function_eqn.
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)
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 ?
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.
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