I have the following simple structure:
CoInductive super_nat := S : super_nat -> super_nat.
Fact unfold_super_nat : forall (n : super_nat), n = match n with S x => S x end.
CoFixpoint more x := S x.
My goal is to show that forall x, more x = S x, precisely as the definition of more goes. How do I do it?
Unfolding more just leaves me with
(cofix more (x0 : super_nat) : super_nat := S x0) x = S x
I tried running various reductions such as cbv cofix etc, but it seems untouchable. I know that in general equality is undecidable, but come on, this is restate of the definition — the goal should reduce to S x = S x after one step.
It was actually simpler than I thought. Inspiration came from this reply:
Coq has a rule: cofix may only be unfolded if an eliminator (for instance a match) is applied to it, because the eliminator will immediately consume whatever cofix produces, thereby guaranteeing progress.
What I need to do, is to pattern match on the cofix. This is done through the auxilary function I defined in the question post:
Goal forall x, more x = S x.
intros.
rewrite (unfold_super_nat (more x)).
simpl.
reflexivity.
Qed.
It is important to rewrite in the correct subexpression. I guess this is the mistake I did.