The Coq mailing list

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

Dear Gert,

Initially, when working on the proof of Kruskal's tree theorem, the idea to use Acc came

to me because I realized that I could strengthen the (rose) tree eliminator to a non-informative

list membership predicate (ie In) at the cost of converting structural recursion on the tree into

structural recursion on the Acc predicate, already implemented by Fix_F in the stdlib.

As you noticed, to show well-foundedness (Rwf), one proceeds by structural recursion on

the tree by *this lives in Prop entirely*.

Below are the two versions compared.

Notice tree_rect_In_t below involves a singleton elimination because of the rewrite

whereas tree_rect_In does not involve singleton elimination.

Using In_t instead of In means you need to duplicate a lot of the stdlib code. This is why

I wanted to remove it. You can try to convert the code of tree_rect_In_t to using In instead

of In_t and see why this direct approach fails...

Best,

Dominique

----------------------------------

Require Import List.
Import ListNotations.

Set Implicit Arguments.

Unset Elimination Schemes.

Inductive tree : Type := T : list tree -> tree.

Set Elimination Schemes.

Fixpoint In_t {X} (x : X) l : Type :=
  match l with
    | []   => False
    | y::l => (x = y) + In_t x l
  end.

Section tree_rect_In_t.

  Variables (P : tree -> Type)
            (IH : forall l, (forall t, In_t t l -> P t) -> P (T l)).

  Fixpoint tree_rect_In_t t : P t.
  Proof.
    destruct t as [ l ].
    apply IH; intros t; revert l.
    refine (fix loop l := _); intros Ht.
    destruct l as [ | x l ].
    + exfalso; destruct Ht.
    + destruct Ht as [ E | Ht ].
      * generalize (tree_rect_In_t x); destruct E; trivial.
      * apply (loop l), Ht.
  Defined.

  Hypothesis IH_ext : forall l f g, (forall p Hp, f p Hp = g p Hp) -> IH l f = IH l g.

  Fact tree_rect_In_t_fix l : tree_rect_In_t (T l) = IH l (fun s _ => tree_rect_In_t s).
  Proof.
    simpl.
    apply IH_ext.
    induction l as [ | x l IHl ].
    + intros ? [].
    + intros ? [ -> | ]; trivial.
  Qed.

End tree_rect_In_t.

Section tree_rect_In.

  Let R (s t : tree) := let (l) := t in In s l.

  Fixpoint Rwf t : Acc R t.
  Proof.
    destruct t as [ l ].
    constructor.
    simpl; intros s Hs; revert l Hs.
    refine (fix loop l := _); intros Hs.
    destruct l as [ | x l ].
    + destruct Hs.
    + destruct Hs as [ E | Hs ].
      * generalize (Rwf x).
        rewrite E; trivial.
      * apply (loop l), Hs.
  Qed.

  Variables (P : tree -> Type)
            (IH : forall l, (forall t, In t l -> P t) -> P (T l)).

  Definition tree_rect_In : forall a, P a.
  Proof.
    apply Fix with (1 := Rwf).
    intros [ l ] H; apply IH, H.
  Defined.

  Hypothesis IH_ext : forall l f g, (forall p Hp, f p Hp = g p Hp) -> IH l f = IH l g.

  Fact tree_rect_In_fix l : tree_rect_In (T l) = IH l (fun s _ => tree_rect_In s).
  Proof.
    unfold tree_rect_In at 1.
    unfold Fix.
    rewrite <- Fix_F_eq.
    apply IH_ext.
    intros; apply Fix_F_inv.
    + exact Rwf.
    + intros []; apply IH_ext.
  Qed.

End tree_rect_In.

---

De: "Gert Smolka" <smolka AT ps.uni-saarland.de>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Lundi 14 Septembre 2020 20:16:01
Objet: Re: [Coq-Club] Program Fixpoint and Nested fix expressions

On 14. Sep 2020, at 18:42, Christian Doczkal <christian.doczkal AT inria.fr> wrote:

Unfortunately, I don't remember the precise rules that make this definition okay. It's something along the lines of "l" being structurally smaller than "a" and "flatten_list" applying flatten only to arguments that are "structurally no greater than y". However, this seems to not be covered by relevant section of the current manual: https://coq.inria.fr/refman/language/core/inductive.html#id10

Maybe someone can chime in and provide the precise rules making this legal.

Smiley!  What you are referring to is the guard condition, which was extended over the years but never documented.
Anyway, nested inductive types (e.g., rose trees) are impossible without the extended guard condition.

BTW, someone should delete the reference to Giménez in the reference Manual:
"Before accepting a fixpoint definition as being correctly typed, we check that the definition is “guarded”. A precise analysis of this notion can be found in [Gimenez94].”
At this point there was only a minimal guard condition.

I’m intrigued by Dominique’s idea to define the eliminator for rose trees with ACC.  Below is a minimal version.  
It shows that the extended guard condition can be quite nice.

Cheers, Gert


Inductive tree := T (A: list tree).
Implicit Type s t: tree.

Definition dst s t := let (A) := t in In s A.

Fixpoint tree_Acc t: Acc dst t.
Proof.
 destruct t as [A].
 constructor.
 induction A as [| t A IH]; cbn.
 - intros t [].
 - intros s [[]|H].
   + apply tree_Acc.
   + apply IH, H.
Defined.

Eval cbv -[dst] in tree_Acc.