coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Program Fixpoint and Nested fix expressions
- Date: Tue, 15 Sep 2020 13:30:44 +0200 (CEST)
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.
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.
- [Coq-Club] Program Fixpoint and Nested fix expressions, Tj Barclay, 09/14/2020
- Re: [Coq-Club] Program Fixpoint and Nested fix expressions, Castéran Pierre, 09/14/2020
- Re: [Coq-Club] Program Fixpoint and Nested fix expressions, Matthieu Sozeau, 09/14/2020
- Re: [Coq-Club] Program Fixpoint and Nested fix expressions, Dominique Larchey-Wendling, 09/14/2020
- Re: [Coq-Club] Program Fixpoint and Nested fix expressions, Christian Doczkal, 09/14/2020
- Re: [Coq-Club] Program Fixpoint and Nested fix expressions, Gert Smolka, 09/14/2020
- Re: [Coq-Club] Program Fixpoint and Nested fix expressions, Gert Smolka, 09/14/2020
- Re: [Coq-Club] Program Fixpoint and Nested fix expressions, Jim Fehrle, 09/14/2020
- Re: [Coq-Club] Program Fixpoint and Nested fix expressions, Christian Doczkal, 09/14/2020
- Re: [Coq-Club] Program Fixpoint and Nested fix expressions, Matthieu Sozeau, 09/15/2020
- Re: [Coq-Club] Program Fixpoint and Nested fix expressions, Dominique Larchey-Wendling, 09/15/2020
- Re: [Coq-Club] Program Fixpoint and Nested fix expressions, Tj Barclay, 09/15/2020
Archive powered by MHonArc 2.6.19+.