According to the coq manual, the unfold tactic performs delta reduction on a definition, followed by several other reductions, including beta-reduction.
It seems that sometimes, to trigger beta-reduction after delta-reduction in unfold, you need to destruct an argument first.
For example, in the Lemma 'unfold_lemma' below, the first 'unfold myFunction' (commented out in the code), doesn't seem to trigger beta-reduction, while beta-reduction is performed after destruction of the argument t.
There is obviously something I don't understand with beta-reduction. Can someone help me clarify this point ?
Inductive tree : Type :=
| tree_cons : list tree -> tree.
Fixpoint andAll (ls: list bool) : bool :=
match ls with
| nil => true
| cons h t => andb h (andAll t)
end.
Definition isLeaf (t: tree) : bool :=
match t with
| tree_cons l => match l with
| nil => true
| x::rest => false
end
end.
Definition isSpecial (t: tree) : bool :=
match t with
| tree_cons l => match l with
| nil => false
| x::rest => andAll (map isLeaf l)
end
end.
Section flat_map_index.
Variables A B : Type.
Variable f : nat -> A -> list B.
Fixpoint flat_map_index (n:nat) (l:list A) : list B :=
match l with
| nil => nil
| cons x t => (f n x)++(flat_map_index (S n) t)
end.
End flat_map_index.
Fixpoint myFunction (l:list nat) (index:nat) (t: tree) : list (list nat) :=
let l' := (l++[index]) in
if (isSpecial t) then
match l' with
| [] => []
| xx::rest => [rest]
end
else
match t with
| tree_cons subtrees => flat_map_index (myFunction l') O subtrees
end.
Lemma unfold_lemma: forall a,
In [0] (myFunction [0] 0 a) -> isSpecial a = true.
Proof.
intro t.
(* unfold myFunction. *)
destruct t as [subtrees].
unfold myFunction.
fold myFunction.
destruct (isSpecial (tree_cons subtrees)) eqn:HCase.
+ easy.
+ ...
Beta-reduction substitutes arguments into lambda abstractions. Lambda abstractions cannot be recursive. myFunction, being a Fixpoint, delta-reduces to a fix expression, which is distinct from a lambda abstraction (fun). fix expressions are evaluated using what Coq calls iota-reduction, not beta-reduction. Iota-reduction reduces the application of a fixpoint only when the decreasing argument of the fixpoint is headed by a constructor.
The distinction between iota- and beta-reduction ensures strong normalization: if fixpoints evaluated via ordinary beta-reduction, so they could expand when the decreasing argument was not a constructor, then you could expand the fixpoint inside itself forever. The system would still have weak normalization: for any term there would always be a reduction sequence that terminates with a value. The strong normalization property, that every reduction sequence terminates with a value, goes up in flames.
Some code demonstrating the above.
Definition plus_two n := S (S n).
Print plus_two. (* plus_two = fun n : nat => S (S n) *)
(* plus_two delta-reduces to a lambda abstraction written with fun. *)
Goal plus_two 2 = 4.
cbv delta[plus_two]. (* (plus_two 2 = 4) delta-converts to ((fun n : nat => S (S n)) 2 = 4) *)
Fail (progress cbv iota). (* iota-reduction does not apply here (cbv iota does nothing) *)
cbv beta. (* but beta-reduction does produce 4 = 4 *)
reflexivity.
Qed.
Goal forall n, plus_two n = S (S n).
intros n.
cbv delta.
cbv beta. (* beta is allowed when the argument is a variable *)
reflexivity.
Qed.
Fixpoint quux_two n := match n with | O => 2 | S n => S (quux_two n) end.
Print quux_two. (* quux_two = fix quux_two (n : nat) : nat := ... *)
(* Coq defines quux_two with a fix expression.
Note how a fix expression names itself so it can be used in its own body.
It is NOT a lambda abstraction! *)
Goal quux_two 2 = 4.
cbv delta. (* now the goal contains an application of a fix expression *)
Fail (progress cbv beta). (* beta reduction does nothing because there is no lambda abstraction *)
cbv iota. (* iota reduction does work and unfolds one turn of the fixpoint, exposing a lambda. *)
cbv beta.
cbv iota. (* iota also handles match; this line actually does 2 iotas *)
cbv beta.
cbv iota. (* two iotas again *)
cbv beta.
cbv iota. (* only one iota (for the match) this time *)
reflexivity.
Qed.
Goal forall n, quux_two n = S (S n).
intros n.
cbv delta.
Fail (progress cbv beta iota).
(* beta fails because there is no lambda.
iota fails because the decreasing argument of the fix is not constructor-headed.
the goal is actually in normal form; no reductions can apply.
if you *could* expand quux_two inside itself... that would be bad, since there would be an infinite sequence of reductions.
must proceed by some kind of case split on n, here induction. *)
induction n as [ | n rec]. (* induction appears to do some simplifying *)
- reflexivity.
- f_equal.
exact rec.
Qed.
In your code, the decreasing argument of myFunction is the third one, t : tree. Therefore myFunction l index t will only reduce (that is, only take an iota-reduction after being delta-reduced) when t is headed by tree_cons.
Note that you can always explicitly prove that a fix expression is equal to its expansion. You just can't get Coq to automatically use such an equality during conversion.
Theorem quux_two_eqn (n : nat)
: quux_two n = match n with | O => 2 | S n => S (quux_two n) end.
Proof.
destruct n; reflexivity.
Qed.
If you think it'd be helpful, you can write such a lemma for myFunction and use it instead of relying on conversion. I also hear the Equations plugin for Coq allows generating such lemmas automatically, though I've never used it.
(According to the documentation, unfold applies the specified delta-reduction and then all of the beta-, iota-, and zeta- (simplifies lets) reductions.)