The Coq mailing list

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

Notice that it is much simpler to define your function

once you know that F t = t. But I suppose you are

interested in a general approach, not just implementing

the identity function in  a cumbersome way ...

Best,

Dominique

PS: F is now called G below to avoid naming

conficts

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

Section shorter_when_semantics_is_know.

  Let R (t1 t2 : tree) := exists n, t2 = cons n t1.

  Let Rwf : well_founded R.
  Proof.
    intros t.
    induction t as [ n | n t IHt ]; constructor; intros x (m & Hm).
    + discriminate.
    + inversion Hm; subst; trivial.
  Qed.

  Let G_full (t : tree) : { t' | t' = t }.
  Proof.
    generalize (Rwf t); revert t.
    refine (fix G t Ht { struct Ht } :=
      match t as t' return t = t' -> _ with
        | node _    => fun _ => exist _ t _
        | cons n t' => fun E =>
           let (t1,H1) := G t' _ in
           let (t2,H2) := G t1 _
           in exist _ (cons n t2) _
      end eq_refl).
    1,4: subst; trivial.
    all: apply (Acc_inv Ht); exists n; subst; trivial.
  Defined.

  Definition G t := proj1_sig (G_full t).
 
  Fact G_spec t : G t = t.
  Proof. apply (proj2_sig (G_full _)). Qed.

End shorter_when_semantics_is_know.

Extraction G.
 

---

De: "Dominique Larchey-Wendling" <dominique.larchey-wendling AT loria.fr>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Samedi 13 Juillet 2019 10:03:59
Objet: Re: [Coq-Club] Error: "Only structural decreasing is supported for a non-Program Fixpoint"

Hi Morgane,

From our work with JF Monin,

"Simulating Induction-Recursion for Partial Algorithms"

here is what you can do on your particular nested algorithm ...

I let you with the proof that your function is total ...

Best,

Dominique

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

Require Extraction Setoid.

Set Implicit Arguments.

Section nested_on_trees.

  Inductive tree : Type :=
    | node : nat -> tree
    | cons : nat -> tree -> tree.

  Inductive gF : tree -> tree -> Prop :=
    | in_gF0 : forall n, gF (node n) (node n)
    | in_gF1 : forall n t1 t2 t3, gF t1 t2 -> gF t2 t3 -> gF (cons n t1) (cons n t3).

  Fact gF_fun s t1 t2 : gF s t1 -> gF s t2 -> t1 = t2.
  Proof.
    intros H1 H2; revert H1 t2 H2.
    induction 1 as [ n | n t1 t2 t3 H1 IH1 H2 IH2 ].
    + inversion 1; auto.
    + inversion 1; auto.
      apply IH1 in H4; subst.
      apply IH2 in H6; subst; auto.
  Qed.

  Unset Elimination Schemes.

  Inductive dF : tree -> Prop :=
    | in_dF0 : forall n, dF (node n)
    | in_dF1 : forall n t1, dF t1 -> (forall t2, gF t1 t2 -> dF t2) -> dF (cons n t1).

  Set Elimination Schemes.

  Section F.

    Let F_full : forall s, dF s -> sig (gF s).
    Proof.
      refine (fix loop s Hs { struct Hs } :=
        match s as t return s = t -> sig (gF t) with
          | node n   => fun E => exist _ s _
          | cons n t => fun E =>
            let (t1,H1) := loop t _ in
            let (t2,H2) := loop t1 _ in
            exist _ (cons n t2) _
        end eq_refl).
      + subst; constructor.
      + subst; inversion Hs; trivial.
      + subst; inversion Hs; apply H3; trivial.
      + constructor 2 with t1; trivial.
    Qed.

    Definition F s Hs := proj1_sig (@F_full s Hs).
 
    Fact F_spec s Hs : gF s (@F s Hs).
    Proof.  apply (proj2_sig _). Qed.

  End F.

  Arguments F : clear implicits.

  Fact dF0 n : dF (node n).
  Proof. apply in_dF0. Qed.

  Fact dF1 n t (Ht : dF t) : dF (F t Ht) -> dF (cons n t).
  Proof.
    intros H1; constructor 2; auto.
    intros s Hs.
    rewrite (gF_fun Hs (F_spec Ht)); trivial.
  Qed.

  Section dF_ind.

    Variable P : forall t, dF t -> Prop.

    Hypothesis HP0 : forall t H1 H2, @P t H1 -> @P t H2.
    Hypothesis HP1 : forall n, P (dF0 n).
    Hypothesis HP2 : forall n t1 H1 (_ : P H1) H2 (_ : P H2), P (@dF1 n t1 H1 H2).

    Fixpoint dF_ind t Ht { struct Ht } : @P t Ht.
    Proof.
      destruct Ht as [ n | n t1 H1 H2 ].
      + apply HP0 with (1 := HP1 _).
      + apply HP0 with (1 := @HP2 n t1 _ (dF_ind _ H1) _ (dF_ind _ (H2 _ (F_spec H1)))).
    Qed.

  End dF_ind.

  Fact F_fix0 n : F _ (dF0 n) = node n.
  Proof.
    apply gF_fun with (node n).
    + apply F_spec.
    + constructor.
  Qed.

  Fact F_fix1 n t1 H1 H2 : F _ (@dF1 n t1 H1 H2) = cons n (F _ H2).
  Proof.
     apply gF_fun with (cons n t1).
     + apply F_spec.
     + constructor 2 with (F _ H1); apply F_spec.
  Qed.

  Fact F_pirr t H1 H2 : F t H1 = F t H2.
  Proof.
    apply gF_fun with t; apply F_spec.
  Qed.

  (** Now you can study your function and show that it is total *)

  Fact dF_total t : dF t.
  Proof.
  Admitted.

  Definition F' t := F _ (dF_total t).

  Fact F'_fix0 n : F' (node n) = node n.
  Proof.
    rewrite <- (F_fix0 n) at 2.
    apply F_pirr.
  Qed.

  Fact F'_fix1 n t : F' (cons n t) = cons n (F' (F' t)).
  Proof.
    unfold F' at 2 3.
    rewrite <- F_fix1.
    apply F_pirr.
  Qed.

End nested_on_trees.

Extraction F.

---

De: "Morgan Sinclaire" <morgansinclaire AT boisestate.edu>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Jeudi 11 Juillet 2019 23:46:51
Objet: [Coq-Club] Error: "Only structural decreasing is supported for a non-Program Fixpoint"

Summary: I've received the error message "Only structural decreasing is supported for a non-Program Fixpoint", I have little clue what it means, and googling this message turned up no actual results. In particular I don't get what it means exactly by "structural decreasing" and "non-Program".

~~~

I have defined a Type called "ptree", which is an infinitary tree with a certain complicated structure, and I'm defining a function (which I'll just call F) that takes in a (P : ptree) as well as some simpler inputs, and returns a ptree. Abstracting away some other details, the definitions look roughly like this:

Inductive ptree : Type :=
| node : nat -> ptree
| cons : nat -> ptree -> ptree
[...]
.

 

Fixpoint F (P : ptree) [...] : ptree :=
match P with
| node n => P
| cons n P' => cons n (F (F P'))
[...]
end.

Now, when I define F like this, I get the familiar "Cannot guess decreasing argument of fix" because of the double application of F. If I change "F (F P')" to "F P'" then the issue goes away, so on some level Coq recognizes that P gets simpler at each stage. However, when I try to tell Coq this by changing the first line to:

Fixpoint F (P : ptree) [...] {measure P} : ptree :=

Then I instead get the error message:

Only structural decreasing is supported for a non-Program Fixpoint

And I don't understand what this means, or how to tell Coq to recognize that P is simplifying, just like in the case where we have the single application F P' instead.

(I believe I know of a way to avoid this double application of F in my situation, but that workaround is tedious, and besides I'm quite interested in understanding what's going on here).