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