Why is it not possible to define a positional expression with an abstract value in Coq?
I need to prove the theorem:
Theorem t : forall x, (fix f (n : nat) : nat := n) x = x.
Informal proof will be as simple as
f is an identity function. So the result is the same as the input.
If I use simpl
after intro x
, nothing changes. Coq does not attempt to evaluate the fix function with an abstract x value. However, if I do an inductive analysis on x, Coq will automatically evaluate the left side of the equation and reduce it to 0
and S x
.
Why is Coq preventing me from evaluating a fix function with an abstract x value?
source to share
simpl
(and all other calculation tactics) transformation rules apply. Since your goal is equality, you can directly use reflexivity
if your terms were convertible. But they are (fix f (n : nat) : nat := n) x
also x
not convertible.
The rule for shortening fix
is the iota transformation. It is described in the manual (chapter 4 "Calculus of inductive constructions", p. 4.5.5 "Endpoint definitions", in the "Reduction rule" section). The reduction rule requires the argument to begin with a constructor. In general, this is necessary to ensure completion. Here's an example in the manual that is similar to yours:
The following is not a conversion, but can be proven after case analysis.
Coq < Goal forall t:tree, sizet t = S (sizef (sont t)). Coq < Coq < 1 subgoal ============================ forall t : tree, sizet t = S (sizef (sont t)) Coq < reflexivity. (** this one fails **) Toplevel input, characters 0-11: > reflexivity. > ^^^^^^^^^^^ Error: Impossible to unify "S (sizef (sont t))" with "sizet t". Coq < destruct t. 1 subgoal f : forest ============================ sizet (node f) = S (sizef (sont (node f))) Coq < reflexivity. No more subgoals.
The equality you want to prove is actually some form of extensionality. Coq does not have expansion as a primitive rule, it can be obtained when the types are explicit. Explicit argument destruction nat
does exactly that: you can prove this redistribution property. It is quite common in Coq developments to prove this continuation lemma.
Theorem t : forall x, (fix f (n : nat) : nat := n) x = x.
Proof.
destruct x; reflexivity.
Qed.
source to share