The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Elias,

There are several questions here:

1) custom induction principles
2) Fixpoint for induction principles or theorems
3) don't mess with the guard-checker
4) rose trees and nested inductive types

1) It is IMHO a very good practice to systematically
   write custom induction principles, either derived
   from more general ones, or directly as Fixpoints
   (see below). It allows to better understand your
   inductive data type. It also allows to get rid of
   unnecessary details in proofs and focus on the
   essential aspects.

   For instance, if an inductive proof on rose trees
   only calls the induction hypothesis on direct sub-trees,
   reasoning by induction on eg. the size forces you
   to show that direct sub-trees are smaller (which is always
   the case), and hence forces a redundant argument that
   hinders the readability of the proof.
   If you use a custom induction principle (see below),
   then you don't even need to consider the size.

2) Behind *every* induction principle (in Coq), there 
   is a fixpoint, or another induction principle which
   itself relies on a fixpoint. There is simply *no other
   way to proceed* when the inductive type is recursive.
   Non-recursive inductive types like eq, sum, bool, or,
   and ... do not require fixpoints though.
   Of course, on case always add an axiom, so what I am
   saying here applies to axiom-free Coq.

   Now if you want to hide the Fixpoint and present
   it as a theorem, there is an easy solution:

Require Import List.

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

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.
  refine (fix rebuild_id t := _).
  destruct t as [ e l ]; simpl; f_equal.
  induction l; simpl; f_equal; trivial.
Qed.

3) Whether you write a theorem as a Fixpoint or by using an
   internal (fix loop ...), automation is likely to apply
   the "loop" too early, on cases where the guard-checker 
   will rightfully complain and insult you. 

   A first advice is to use the command "Guarded" in interactive 
   proof script to detect early and spot where bad calls are made.

   A second advice is to specialize "loop" on the wanted
   calls early. Also, when the call is performed and no more
   calls are expected in the branch, one can "clear loop" so
   that further calls are impossible. One can also avoid
   "auto" or "eauto" if "trivial" or "easy" is enough. 
   
4) Question on rose trees seems to pop up everywhere suddenly.

https://proofassistants.stackexchange.com/questions/3953/how-do-i-define-an-induction-principle-for-a-type-with-a-nested-list-of-tuples

https://proofassistants.stackexchange.com/questions/3938/my-inductive-function-over-a-pair-of-lists-gives-cannot-guess-decreasing-argume

The induction principle I find the most convenient for reasoning
with your rose trees look like:

Theorem rose_tree_rect A (P : rose_tree A -> Type) :
     (forall a l, (forall t, In t l -> P t) -> P (Node _ a l))
  -> (forall t, P t).

You can then specialize to Set/Prop to get rose_tree_rec
and rose_tree_ind.

Using this custom induction principle, you obtain the following
modular proof for rebuild_id:

Fact map_id_ext X (f : X -> X) l :
   (forall x, In x l -> f x = x) -> map f l = l.
Proof.
  rewrite <- Forall_forall.
  induction 1; simpl; f_equal; auto.
Qed.

Theorem rebuild_id' A t : rebuild A t = t.
Proof.
  induction t using rose_tree_rect; simpl; f_equal.
  now apply map_id_ext.
Qed.

Some 1.5 years ago, following a request by J. Hughes, I did
publish a separate Coq library specifically for dealing with
recursors for various kinds of roses trees, eg list or vector
based.

https://github.com/DmxLarchey/Kruskal-Trees

The library is on opam but is also designed to be read
and understood. For instance, you will find your rose_tree
implemented there

https://github.com/DmxLarchey/Kruskal-Trees/blob/main/theories/tree/ltree.v

with some tools like finite quantification over the nodes of
a rose_tree, size or weight, decisions. 

In 

https://github.com/DmxLarchey/Kruskal-Finite/blob/main/theories/examples/trees.v

you can find a proof that rose_tree of a given (or below a given) weight
are finitely many, which is an interesting proof.

Best,

Dominique

PS:

This project on rose trees was extracted from a much larger project,
a complete revamp of an inductive proof of Kruskal's tree theorem, 
that is now distributed on opam as well

https://github.com/DmxLarchey/Kruskal-Theorems


----- Mail original -----
> De: "Elias Castegren" <elias.castegren AT it.uu.se>
> À: "coq-club" <coq-club AT inria.fr>
> Envoyé: Vendredi 3 Mai 2024 08:28:34
> Objet: [Coq-Club] Theorems as Fixpoints

> 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