Can every property proved using Theorem in Coq by induction on one of the premises be refactored to a proof using Fixpoint where we destruct on the same premise? What is the point of having separate commands for Theorem and Fixpoint?
1
votes
1 Answers
4
votes
Yes. When you call the induction tactic, it's equivalent to applying an induction principle lemma (called something like nat_ind or DatatypeName_ind), and that induction principle was proved automatically by Coq using a fixpoint and a match. So if you "inline" the proof of the induction principle, you get a proof that could have been constructed by Fixpoint and destruct.
However, writing proofs manually using Fixpoint is a bit error prone, because it always adds a hypothesis into the context that corresponds to recursive calls, and the proof is only valid if you use the hypothesis on an argument that came out of a destruct. That condition is only checked at the time of the final Qed (you can check this using the Guarded command but this needs to know the recursive argument correctly in advance potentially using the {struct x} declaration). So if you write the proof using Fixpoint, and then call a tactic like eauto, the tactic may "accidentally" use the recursive argument in a non-wellfounded way. If you use induction, you only get inductive hypotheses for the direct subterms, so proofs constructed by tactics are always valid.
