Fixpoint proofs with a nested induction on the value of a function

Question

I am trying to proof an induction principle in Coq. Due to the definition of the data structure it is obligatory to show this principle via two nested inductions. The outer induction is done via the Fixpoint construct and the inner induction is done with principle list_ind. The problem occuring is now that the induction argument of the inner induction is the result of a function, namely dfs t.

Inductive SearchTree (A : Type) : Type :=
  | empty : SearchTree A
  | leaf : A -> SearchTree A
  | choice : SearchTree A -> SearchTree A -> SearchTree A.

Fixpoint dfs (A : Type) (t: SearchTree A) : list A :=
  match t with
  | empty => nil
  | leaf x => cons x nil
  | choice t1 t2 => app (dfs t1) (dfs t2)
  end.

In the inner induction step I need to be able to apply the outer induction hypothesis to the first element of dfs t. But: when doing induction on dfs t this is not possible as it leads to an ill-formed recursion.

In my eyes the "normal" approach would be to do induction on t and simplification, but in case t = choice t1 t2 this always leads back to the initial problem as dfs (choice t1 t2) only reduces to dfs t1 ++ dfs t2.

Does somebody have an suggestion how to go on with this proof?

EDIT: Thought it might be a little much to show the code, but here it is:

Require Import Setoid.
Require Import Coq.Lists.List.

Set Implicit Arguments.
Set Contextual Implicit.

Section list.
  Section listEquality.

    Variable A : Type.
    Variable eqA : A -> A -> Prop.

    Inductive EqL : list A -> list A -> Prop :=
    | EqL_nil : EqL nil nil
    | EqL_cons : forall (x y : A) (xs ys : list A),
        eqA x y ->
        EqL xs ys ->
        EqL (cons x xs) (cons y ys).

  End listEquality.
End list.

Section SearchTree.

  Inductive SearchTree (A : Type) : Type :=
  | empty : SearchTree A
  | leaf : A -> SearchTree A
  | choice : SearchTree A -> SearchTree A -> SearchTree A.

  Fixpoint dfs (A : Type) (t: SearchTree A) : list A :=
    match t with
    | empty => nil
    | leaf x => cons x nil
    | choice t1 t2 => app (dfs t1) (dfs t2)
    end.

  Section DFSEquality.

    Variable A : Type.
    Variable eqA : relation A.

    Definition EqDFS (t1 t2: SearchTree A) : Prop :=
      EqL eqA (dfs t1) (dfs t2).

  End DFSEquality.
End SearchTree.

Section List.
  Inductive List A :=
  | Nil : List A
  | Cons : SearchTree A -> SearchTree (List A) -> List A.
End List.

Section EqND.
    Variable A : Type.
    Variable eqA : relation A.
    Inductive EqND : List A -> List A -> Prop :=
    | Eq_Nil : EqND Nil Nil
    | Eq_Cons : forall tx ty txs tys,
        EqDFS eqA tx ty ->
        EqDFS EqND txs tys ->
        EqND (Cons tx txs) (Cons ty tys).
End EqND.

Section EqNDInd.
    Variable A : Type.
    Variable eqA : relation A.
    Variable P : List A -> List A -> Prop.
    Hypothesis BC : P Nil Nil.
    Hypothesis ST: forall mx my mxs mys,
        EqDFS eqA mx my
        -> EqDFS (fun xs ys => EqND eqA xs ys /\ P xs ys) mxs mys
        -> P (Cons mx mxs) (Cons my mys).

    Fixpoint IND (xs ys : List A) { struct xs } : EqND eqA xs ys -> P xs ys.
    Proof.
      intro eq.
      destruct xs,ys.
      + exact BC. 
      + inversion eq.
      + inversion eq.
      + inversion eq. subst. apply ST.
        ++ exact H2.
        ++ unfold EqDFS in *.
           generalize dependent (dfs s2).
           induction (dfs s0).
           +++ intros. inversion H4. constructor.
           +++ intros. inversion H4. subst. constructor.
               ++++ split.
                    * exact H1.
                    * apply IND. exact H1. (* Guarded. *)
               ++++ clear IND. firstorder.
     Admitted.
End EqNDInd.

The problem occurs proving IND, the Guarded. commented out fails.

Answer 1

To use nested recursion you have to resort to the raw fix construct using the "fix 1" tactic for example. The induction principles won't give you the right recursive calls. Beware that inversions might do rewritings that confuse the guard checker.

Actually, if you want the "nested" fixpoint to not be on a subterm of the original list but on [dfs t] then it's no longer a structural recursion and you need to justify the recursion using well-founded recursion. I have a similar example on rose trees where well-founded nested recursion is used.

Answer 2

There are two problems in your attempt:

• The way you wrote IND prevent the recursive argument to be eq: EqND eqA xs ys, while this would be the natural one.

• As remarked by @Matthieu Sozeau, the multiple inversions introduce noise.

Surprisingly, the proof is quite short.

Here is my solution:

Fixpoint IND (xs ys : List A) (eq: EqND eqA xs ys) : P xs ys.
Proof.
  destruct eq.
  - assumption.
  - apply ST.
    + assumption.
    + unfold EqDFS in H0 |- *. induction H0.
      * constructor.
      * constructor.
        -- split.
           ++ assumption.
           ++ apply IND. assumption.
        -- assumption.
Qed.