The Coq mailing list

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

Dear Benoit,

The problem you are facing is that Coq does not automatically generate

powerful enough induction principles when facing *nested* inductive

types of which Tree is a typical example. So you need to write (or prove)

your own induction principles by hand.

This might be cumbersome because you have to write them in such a

way to convince the type-checker that recursive sub-calls actually happen

on a sub-term.

One way to solve this problem (this is done that way in the CoLoR

library for instance) is to have mutually inductive types for trees

and forest (aka lists of trees) but the disadvantage of such a method

is that a forest in *only isomorphic* to a list of tree, and thus using

the List library to manipulate forests is uneasy. Basically, you need

to duplicate all the results from the List library.

I encountered the problem many times with my Coq developments.

If you want to represent proof systems for instance, basically proofs

are trees. I had never been completely satisfied with what I got regarding

the trees I was using (even though it was sufficient for my needs at that

time). It has been a quite long learning curve for me and this is why I

decided to give you a comprehensive answer.

Also notice that you want to actually compute with trees, not only

prove properties about trees. So you do not only need an induction

principle, but what you need is a recursor, that is an induction principle

together with a fixpoint equation.

When developing the tree library for the proof of the Kruskal tree

theorem, I did finally end up with a nested induction principle that I

find satisfying and which is easy to work with.

tree_rect
     : forall (X : Type) (P : tree X -> Type),
       (forall (a : X) (ll : list (tree X)),
        (forall x : tree X, In_t x ll -> P x) -> P (in_tree a ll)) ->
       forall t : tree X, P t

with a fixpoint equation like

tree_rect f (in_tree a ll) = f a ll (fun t _ => tree_rect t)

(this equation holds when f is extensional)

There is a simpler recursor for non-dependent

recursion

About that definition, just notice that In_t x ll

is an informative version of In x ll, ie, it is

the type of occurences of x in ll.

I did an update on your example.v source code

to integrate the necessary parts of my tree library

so as to be able to prove lengthVals ...

Beware that some of your definitions are
 duplicates of those of the List library, eg

Fact consAll_map X (f : X -> nat) l : consAll f l = map f l.

Fact consListAll_flat_map X Y (f : X -> list Y) l : consListAll f l = flat_map f l.

If you find that implementation of trees useful for your developments,

there is a lot more in the tree library for the Kruskal project

http://www.loria.fr/~larchey/Kruskal/

Good luck with nested types and remember,

*always write the induction principles that are tailored

  for your needs* (easier to say that to do ...).

Dominique Larchey-Wendling

---

De: "Benoît Viguier" <beviguier AT gmail.com>
À: coq-club AT inria.fr
Envoyé: Dimanche 7 Février 2016 18:48:44
Objet: [Coq-Club] How to prove an inductive property on trees.

Good Evening Coq-club,

I'm trying to work on general trees (not binary) with an iterators semantics and therefore to formalize simple properties.

See attached file.

TL;DR (do not copy paste it, better use the .v file):

Inductive Tree : Set :=
| Node : nat -> list Tree -> Tree.

Fixpoint vals (t:Tree) : list nat := match t with
| Node n l => n :: (consListAll Tree nat vals l)
end. 

(* return the list of the values in the tree *) 

Fixpoint NumVal (t:Tree) := match t with
| Node n l => 1 + SumAll Tree NumVal l
end.

(* recursively count the values in the tree *)

I'm trying to reason by induction over the list of the children (hence a :: l). But I'm stuck in the proof.

My induction hypothesis is :

length (vals (Node n l)) = NumVal (Node n l)

But at the point of my reasoning I'm asked to prove :

length (vals a) = NumVal a

Therefore I got a pretty loop in my demonstration...

Any advices to get out of it ?

Kind regards.

------

Benoît

Require Import List.
Require Import Arith.
Require Import ZArith.

Set Implicit Arguments.

Section In_t.

  Variables X : Type.

  Fixpoint In_t (x : X) ll : Set :=
    match ll with
      | nil   => False
      | y::ll => (( x = y ) + In_t x ll)%type
    end.

  Fact In_t_In x ll : In_t x ll -> In x ll.
  Proof.
    induction ll; intros []; [ left | right ]; subst; auto.
  Qed.

  Fact In_t_P (P : Prop) x ll  : (In_t x ll -> P) -> In x ll -> P.
  Proof.
    intros H1; induction ll as [ | y ll IH ].
    intros [].
    intros [ H2 | H2 ].
    subst; apply H1; left; auto.
    revert H2; apply IH; intro; apply H1; right; auto.
  Qed.

  (* beware the following does not hold when P : X -> Type *)

  Fact In_In_t (P : X -> Prop) ll : (forall x, In_t x ll -> P x) <-> forall x, In x ll -> P x.
  Proof.
    split.
    intros H x; specialize (H x); revert H; apply In_t_P.
    intros H x Hx; apply In_t_In in Hx; auto.
  Qed.

End In_t.

Section map_t.

  Variable X : Type.
  Variable P : X -> Type.
  Variable f : forall x, P x.
  
  Fixpoint map_t ll : forall x, In_t x ll -> P x.
  Proof. 
    refine(match ll with 
      | nil   => fun x H => _
      | a::ll => fun x H => _
    end).
    elim H.
    destruct H as [ | H ].
    subst; apply f.
    apply (map_t _ _ H).
  Defined.
  
  Fact map_t_prop ll x (Hx : In_t x ll) : map_t ll x Hx = f x.
  Proof.
    induction ll; destruct Hx; simpl; subst; trivial.
  Qed.

End map_t.

Section list_In_t_map.

  Variables (X Y : Type).

  Fixpoint list_In_t_map ll : (forall x : X, In_t x ll -> Y) -> list Y.
  Proof.
    refine (match ll return (forall x : X, In_t x ll -> Y) -> list Y with
      | nil   => fun _ => nil
      | x::mm => fun H => H x _ :: list_In_t_map mm _
    end).
    left; reflexivity.
    intros z ?; apply (H z); right; assumption.
  Defined.

  Fact list_In_t_map_ext ll f g : (forall x (H : In_t x ll), f x H = g x H) -> list_In_t_map ll f = list_In_t_map ll g.
  Proof.
    induction ll; simpl; intros; f_equal; auto.
  Qed.

  Fact list_In_t_map_t f ll : list_In_t_map ll (map_t _ f ll) = map f ll.
  Proof.
    induction ll; simpl; f_equal; assumption.
  Qed.
 
End list_In_t_map.

Section trees.

  Variable (X : Type).

  (* we do not want the too weak Coq generated induction principles *)

  Unset Elimination Schemes.

  Inductive tree : Type := in_tree : X -> list tree -> tree.

  Set Elimination Schemes.

  (* let us define our own induction principles *)

  Section tree_rect.

    Variable P : tree -> Type.
    Hypothesis f : forall a ll, (forall x, In_t x ll -> P x) -> P (in_tree a ll).

    Fixpoint tree_rect t : P t :=
      match t with
        | in_tree a ll => f a _ (map_t _ tree_rect  _) 
      end.

    Hypothesis f_ext : forall a ll f1 f2, (forall x Hx, f1 x Hx = f2 x Hx) -> f a ll f1 = f a ll f2.

    (* Coq recursive type-checking does not allow such a definition 
       but it is possible to prove this identity
    *)

    Fact tree_rect_fix a ll : tree_rect (in_tree a ll) = f a ll (fun t _ => tree_rect t).
    Proof.
      simpl.
      apply f_ext.
      clear a; intros a Ha.
      apply map_t_prop.
    Qed.

  End tree_rect.

  Definition tree_rec (P : tree -> Set) := tree_rect P.

  Section tree_ind.

    Variable P : tree -> Prop.
    Hypothesis HP : forall a ll, (forall x, In x ll -> P x) -> P (in_tree a ll).

    Definition tree_ind : forall t, P t.
    Proof.
      apply tree_rect.
      intros; apply HP.
      rewrite <- In_In_t; auto.
    Qed.

  End tree_ind.

  Section tree_recursion.

    (* the particular case when the output type does not depend on the tree *)

    Variables (Y : Type) (f : X -> list tree -> list Y -> Y).

    Definition tree_recursion : tree -> Y.
    Proof.
      apply tree_rect.
      intros x ll IH.
      apply (f x ll (list_In_t_map _ IH)).
    Defined.

    Fact tree_recursion_fix x ll : tree_recursion (in_tree x ll) = f x ll (map tree_recursion ll).
    Proof.
      unfold tree_recursion at 1.
      rewrite tree_rect_fix.
      f_equal.
      rewrite <- list_In_t_map_t.
      apply list_In_t_map_ext.
      clear x.
      intros x Hx; simpl.
      rewrite map_t_prop; auto.
      clear x ll.
      intros a ll u v Hfg.
      f_equal.
      apply list_In_t_map_ext; auto.
    Qed.
  
  End tree_recursion.

End trees.

Check tree_rect.
Check tree_rect_fix.

(* Iterative tools *)
Section All.
  Variable T : Type.
  Variable P : T -> Prop.
  Variable S: T -> nat.
  Variable A : Type.
  Variable LS: T -> list A.
  Variable V: T -> Prop.

  Fixpoint orAll (ls:list T) : Prop := match ls with
    | nil => False
    | h :: q =>  (V h) \/ (orAll q)
  end.
  Fixpoint andAll (ls:list T) : Prop := match ls with
    | nil => True
    | h :: q => P h /\ andAll q
  end.

  Fixpoint SumAll (ls:list T) : nat := match ls with
    | nil => 0
    | h :: q => S h + SumAll q
  end.
  (*S is not the succ function here !!! *)

  Fixpoint MaxAll (ls:list T) : nat := match ls with
    | nil => 0
    | h :: q => max (S h) (MaxAll q)
  end.
  (*S is not the succ function here !!! *)

  Fixpoint consAll (ls:list T) : list nat := match ls with 
    | nil => nil
    | h :: q => S h :: consAll q
  end.
  (*S is not the succ function here !!! *)

  Fixpoint consListAll (ls:list T) : list A := match ls with 
    | nil => nil
    | h :: q => (LS h) ++ consListAll q
  end.
  
  Inductive orderedList : list nat -> Prop := 
    | NilOrdered         : orderedList nil
    | SingletonOrdered n : orderedList (n::nil)
    | ConOrdered a h q
      (ORDER: a < h)
      (ORDERED: orderedList (h::q))
      : (* ===================== *)
      orderedList (a::h::q).
End All.

Fixpoint vals (t:tree nat) : list nat := match t with
| in_tree n l => n :: (consListAll vals l)
end.

(* An alternate definition using tree_recursion *)

Definition vals' : tree nat -> list nat.
Proof.
  induction 1 as [ n l IH ] using tree_recursion.
  exact (n::flat_map (fun x => x) IH).
Defined.

Fact flat_map_map X Y Z (f : Y -> list Z) (g : X -> Y) l : 
   flat_map f (map g l) = flat_map (fun x => f (g x)) l.
Proof.
  induction l; simpl; f_equal; auto.
Qed.

Fact flat_map_ext X Y (f g : X -> list Y) l :
   (forall x, In x l -> f x = g x) -> flat_map f l = flat_map g l.
Proof.
  induction l; simpl; intro; f_equal; auto.
Qed.

Fact vals'_fix n l : vals' (in_tree n l) = n::flat_map vals' l.
Proof.
  unfold vals' at 1; rewrite tree_recursion_fix.
  f_equal; apply flat_map_map.
Qed.

Fact consAll_map X (f : X -> nat) l : consAll f l = map f l.
Proof.
  induction l; simpl; f_equal; auto.
Qed.

Fact consListAll_flat_map X Y (f : X -> list Y) l : consListAll f l = flat_map f l.
Proof.
  induction l; simpl; f_equal; auto.
Qed.

Fact vals_eq_vals' t : vals t = vals' t.
Proof.
  induction t as [ n l IH ].
  simpl vals.
  rewrite consListAll_flat_map.
  rewrite vals'_fix.
  f_equal.
  apply flat_map_ext, IH.
Qed.

Fixpoint NumVal (t:tree nat) := match t with
| in_tree n l => 1 + SumAll NumVal l
end.

Fixpoint lsum l := 
  match l with
    | nil  => 0
    | n::l => n + lsum l
  end.

Fact SumAll_eq_lsum_map X (f : X -> nat) l : SumAll f l = lsum (map f l).
Proof.
  induction l; simpl; f_equal; auto.
Qed.

Definition NumVal' : tree nat -> nat.
Proof.
  induction 1 as [ x l IH ] using tree_recursion.
  exact (1 + (lsum IH)).
Defined.

Fact NumVal'_fix x l : NumVal' (in_tree x l) = 1 + lsum (map NumVal' l).
Proof.
  apply tree_recursion_fix.
Qed.

Fact map_ext X Y (f g : X -> Y) l :
   (forall x, In x l -> f x = g x) -> map f l = map g l.
Proof.
  induction l; simpl; intro; f_equal; auto.
Qed.

Fact NumVal_eq_NumVal' t : NumVal t = NumVal' t.
Proof.
  induction t as [ x l IH ].
  simpl NumVal.
  rewrite NumVal'_fix; simpl.
  f_equal.
  rewrite SumAll_eq_lsum_map.
  f_equal.
  apply map_ext, IH.
Qed.

Theorem GaussSum: forall a b c, a + c = b + c <-> a = b.
Proof.
  split; omega.
Qed.

Lemma lengthVals : forall t, length (vals t) = NumVal t.
Proof.
  induction t as [ x l IH ].
  induction l as [ | t l IHl ]; intros.
  simpl;reflexivity.
  simpl.
  rewrite app_length.
  do 2 f_equal.
  apply IH; left; auto.
  apply eq_add_S, IHl.
  intros ? ?; apply IH; right; auto.
Qed.