The Coq mailing list

[Elias Castegren <elias.castegren AT it.uu.se>]

Dear all

While investigating writing custom induction principles
I figured out that an alternative solution is to write your
theorems as Fixpoints (questions below).

For example, take this definition of a Rose tree where
the generated induction principle is unhelpful:

Inductive rose_tree (A: Type) :=
| Node (elem: A) (children: list (rose_tree A)).

Check rose_tree_ind.
(*
rose_tree_ind
     : forall (A : Type) (P : rose_tree A -> Prop),
       (forall (elem : A) (children : list (rose_tree A)),
        P (Node A elem children)) ->
       forall r : rose_tree A, P r
*)

Trying to prove for example that a convoluted identity
function is indeed an identity function fails almost
immediately:

Fixpoint rebuild (A: Type) (t: rose_tree A) :=
  match t with
  | Node _ elem children => Node A elem (map (rebuild A) children)
  end.

Theorem rebuild_id:
  forall A t,
    rebuild A t = t.
Proof.
  intros A t.
  induction t. (* No induction hypothesis generated *)
Abort.

Now, the standard solution to this is to write a custom
induction principle that recurses through the list (or something
using well-founded induction), but you can also prove the
theorem directly by formulating it as a Fixpoint:

Fixpoint rebuild_id (A: Type) (t: rose_tree A):
  rebuild A t = t.
Proof with auto.
  destruct t. simpl.
  f_equal. induction children...
  simpl. rewrite rebuild_id'.
  rewrite IHchildren...
Qed.

I was pleasantly surprised by this since I have always found
writing induction principles quite tedious, especially for larger
data types. An obvious drawback of this is that automation
tends to be very eager to use the theorem recursively too
early, creating a non-terminating proof object.

So, to my questions:

1. Is there a tactic that I can use in the proof of a regular
Theorem that turns it into a fixpoint so that I don’t have to
write the theorem statement differently? Note that writing
"Fixpoint rebuild_id: forall A t, rebuild A t = t” fails with an
uncaught exception at the moment.

2. Is there a version of auto that checks guardedness and
backtracks if it fails? What I want is something like
“try solve[auto; Guarded]”, but it seems like Guarded is a
command rather than a tactic so that they don’t compose
(also I guess solve would stop once auto solved the goal?)

Maybe there are other tricks one can employ to solve the
same problem? My goto solution is using well-founded
induction over some size measure, but it always involves
some boilerplate that would be nice to avoid.

Cheers

/Elias








När du har kontakt med oss på Uppsala universitet med e-post så innebär det 
att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan 
du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. 
For more information on how this is performed, please read here: 
http://www.uu.se/en/about-uu/data-protection-policy