Robert Dockins (Nov 13 2022 at 20:45): Robert Dockins (Nov 13 2022 at 20:45):I have a function I want to define with a... rather complicated recursion structure. I have been able to define other, somewhat simpler versions of this function directly via nested fixpoints. I would prefer to keep doing that rather than moving to definition via well-founded recursion if possible. When I attempt to get Coq to accept the definitions below, it complains about the recursive definition of inner being ill-defined. Given what I know about how fixpoints and matching work, I feel like this ought to be accepted. Does anyone have some insight here? Is this a bug in the guardedness checker, have I made some mistake?
Sorry for the complexity of this definition, I don't know how to make it much smaller and still exhibit the issue. See the attached file for the problematic definition. I am running Coq 8.16.0.
Pierre Courtieu (Nov 14 2022 at 11:39):I am not an expert on the guard condition but I think the way you switch from one structural argument to the other (x and y, xs and ys) is stressing the guard condition a little too far. I agree that his looks like a limitation of the guard condition, but I can't tell if it is easy nor possible to fix.
Robert Dockins (Nov 15 2022 at 01:07):In that case, I'll probably open a ticket about this, but try to proceed on my development using well-founded recursion.
Pierre Castéran (Nov 15 2022 at 07:25):Perhaps a recursion based on a size argument (like size x + size y) ?
The definition of BH_compareis quite hard to read. It may be useful to present it as a bunch of equations (semi-formally, or, better, using https://mattam82.github.io/Coq-Equations/ ) in order to have a better intuition of the issue.
Dominique Larchey-Wendling (Nov 15 2022 at 15:45):Robert Dockins said:
Sorry for the complexity of this definition, I don't know how to make it much smaller and still exhibit the issue. See the attached file for the problematic definition. I am running Coq 8.16.0.
First of all, refine is going to be your new best friend if not already !! This allows you to spot the problem easily and incrementally as in
Fixpoint BH_compare (x:BHForm) : BHForm -> ordering.
Proof.
refine (
fix inner (y:BHForm) : ordering :=
match x, y with
| BH xs0, BH ys0 => (fix compare_sequence (xs:list BHForm) : list BHForm -> ordering :=
fix compare_sequence_inner (ys:list BHForm) : ordering := _) xs0 ys0
end).
refine (match xs with
| [] => if bh_isZero y then EQ else LT
| [x] => match ys with
| [] => GT
| [y] => BH_compare x y
| _ => LT
end
| (x::xs) => _
end).
Guarded.
refine (if bh_isZero x then compare_sequence xs ys else
match ys with
| [] => GT
| (y::ytail) =>
if isNil ytail then LT else
if bh_isZero y then compare_sequence_inner ytail else _
end).
Guarded.
refine ( match nat_compare (length xs) (length ytail) with
| LT => LT
| EQ => match BH_compare x y with
| LT => (fix check_lt (xs:list BHForm) :=
match xs with
| [] => LT
| (x'::xs') =>
match BH_compare x' y with
| LT => check_lt xs'
| EQ => if bh_allZero (x'::xs') then EQ else GT
| GT => GT
end
end
) xs
| EQ => compare_sequence xs ytail
| GT => _
end
| GT => GT
end).
Guarded.
refine ((fix check_gt (ys':list BHForm) :=
match ys' with
| [] => GT
| (y'::ys'') =>
match _ with
| LT => LT
| EQ => if bh_allZero ys' then EQ else LT
| GT => check_gt ys''
end
end
) ytail).
Guarded.
refine (inner y').
(* y' < ys' comes from ytail < ys comes from ys0 < y, so indeed this should guard check, I agree *)
Guarded.
Admitted.
So indeed, I would agree with you that the call inner y, which is the problematic one, should be recognized as structurally smaller. There are no rewrites seemingly. May be a bug ?
If you want to go through well-founded induction, I would suggest you to use versatile induction principles for list based rose trees (which is your BHForm data-structure) such as ltree_rect (for dependent output) or the simpler ltree_recursion (from non-dependent output) from the Kruskal-Treesgithub library (available via opam). BHForm is isomorphic to rtree actually so maybe you could just copy-paste rtree_rect.
May be these principles would allow you to avoid so much fixpoint nesting. Also, you may want to specify your output inductively, and output a rich dependent type to prove your spec (possibly fixpoint equations) and write your code at the same time., following eg the Braga method.
You seem to compute a kind of total ordering on rose trees. Could you give an inductive characterization of the order, ie
Inductive BH_order : BH -> BH -> ordering -> Prop := ...
with BH_list_order : list BH -> list BH -> ordering -> Prop := ...
or may be nested if you can give a parameterized definition of list_order. And then get BH_compare x y : { o | BH_order x y } ?
Dominique Larchey-Wendling (Nov 15 2022 at 18:36):I might have been not careful enough in saying that the guard checker should say ok. Consider the following example that the guard-checker rightfully rejects. It contains similar nesting as your example:
(* loop1 false 1 1 -> loop2 false 1 1 -> loop2 true 2 0 -> loop1 false 1 1 -> ... *)
Fixpoint loop1 (b : bool) (n m : nat) { struct n } : unit.
Proof.
refine ((fix loop2 b n (m : nat) { struct m } : unit := _) b n m).
refine (match b with
| true => match n with
| 0 => tt
| S n => loop1 false n (1+m)
end
| false => match m with
| 0 => tt
| S m => loop2 true (1+n) m
end
end).
Guarded.
So the graph of sub-structural calls should have more properties that just "the call on the recursive argument occurs on a strict sub-term", like eg the absence of cycles.
Dominique Larchey-Wendling (Nov 16 2022 at 20:13):@Robert Dockins Since your problem reminded me of old developments when I needed a total strict order on trees, I decided to add an implementation of the nested short lex order on undecorated rose trees to the Kruskal-Trees library. The versatile rtree_rect induction principle for rose trees is indeed enough. No need to reason on trees height or size (which is what I did years ago, not knowing how to proceed otherwise).
The nested short lex order is strongly total and a strict (irreflexive, transitive). You can find the code in the following GH pull request. It contains simple decider which has some similarity with your highly nested BH_compare.
Robert Dockins (Nov 17 2022 at 02:24):Pierre Castéran said:
Perhaps a recursion based on a size argument (like
size x + size y) ?
The definition ofBH_compareis quite hard to read. It may be useful to present it as a bunch of equations (semi-formally, or, better, using https://mattam82.github.io/Coq-Equations/ ) in order to have a better intuition of the issue.
I will probably proceed with a size based argument for now. And, I totally agree, the definition is quite hard to read. My style thus far with similar functions has been to first get them to pass the guard checker, then recast them in a more sensible way using intermediate functions. I usually don't like to use the equations package, as I find the definitions are usually pretty hard to work with (to be fair, I haven't tried in awhile).
Robert Dockins (Nov 17 2022 at 02:47):@Dominique Larchey-Wendling , thanks for the pointers, I'll take a look. I'm not sure that rtree_rect will help me much, however, unless I'm missing something. The tricky thing with this definition is that some of the recursive calls decrease in x, and some decrease in y, but not always both. That is what lead to the nested fixpoints style. You can see the same basic structure here, in a much simpler version:
Inductive VForm : Set :=
| Z : VForm
| V : VForm -> VForm -> VForm.
Fixpoint VF_compare (x:VForm) : VForm -> ordering :=
fix inner (y:VForm) : ordering :=
match x, y with
| Z, Z => EQ
| Z, V _ _ => LT
| V _ _, Z => GT
| V a x' , V b y' =>
match VF_compare a b with
| LT => VF_compare x' y
| EQ => VF_compare x' y'
| GT => inner y'
end
end.
I usually prefer to state a bare algorithm and then do proofs about it, rather than doing dependent program/proof at the same time, especially if I'm actually interested in the algorithm (as I am here). Giving an inductive characterization might help; then I wouldn't care as much if I ended up with a fairly opaque dependent program. I'm already working with a semantic characterization of the order (i.e., the values I'm working with have denotations already equipped with the order I care about) so it would really just be bookeeping; but maybe it is a good strategy nonetheless.
Paolo Giarrusso (Nov 17 2022 at 04:05):Fwiw, if you use equations the definitions are expected to have ugly unfoldings, but you should never need to use them directly
Pierre Castéran (Nov 17 2022 at 07:10):My intuition (but I may be wrong) about the difficulty to read BH_compare's definition is that you have two kinds of inner fixdeclarations. Some come from the use of list based trees (to be compared with mutually inductive types) and the others from a well-known pattern (used for instance in mergelike functions). Look for instance at section 14.3 of https://www-sop.inria.fr/members/Yves.Bertot/coqart-chapter14.pdf
About Equations: splitting the definition into equations may increase code readability. Moreover, once the definition is accepted, you may easily prove several "paraphrase lemmas" which rephrase simply the automatically generated lemmas into a paper-pencil form, which you may use in your proofs.
Dominique Larchey-Wendling (Nov 17 2022 at 10:11):@Robert Dockins
Here is a development a the Braga method on your simpler example. Of course your code shows that structural fixpoint on the arguments is possible in that simple case (via nesting) but Braga proceeds by structural induction on an added domain argument, herein encoded as an accessibility predicate, and the Fixpoint can be written as your intend code, w/o nesting. Extraction is clean. You get the required fixpoint equations to reason about your function. Also, termination can be proved independently of the definition of the function. It even works in case you write partial functions (which is not the case here). I am pretty sure this will adapt to your more complex example. Possibly the termination proof could be based on a measure as well but I have not computed all your fixpoint equations so I am not 100 percent.
Require Import Wellfounded Arith Lia.
Section measure2_rect.
(* This is a convenient tool for induction on a measure with 2 args *)
Variable (X Y : Type) (m : X -> Y -> nat) (P : X -> Y -> Type).
Hypothesis F : (forall x y, (forall x' y', m x' y' < m x y -> P x' y') -> P x y).
Arguments F : clear implicits.
Let m' (c : X * Y) := match c with (x,y) => m x y end.
Notation R := (fun c d => m' c < m' d).
Let Rwf : well_founded R.
Proof. apply wf_inverse_image with (f := m'), lt_wf. Qed.
Definition measure2_rect x y : P x y :=
(fix loop x y (A : Acc R (x,y)) { struct A } :=
F x y (fun x' y' H' => loop x' y' (@Acc_inv _ _ _ A (_,_) H'))) _ _ (Rwf (_,_)).
End measure2_rect.
Tactic Notation "induction" "on" hyp(x) hyp(y) "as" ident(IH) "with" "measure" uconstr(f) :=
pattern x, y; revert x y; apply measure2_rect with (m := fun x y => f); intros x y IH.
Inductive ordering : Set := LT | EQ | GT.
Inductive VForm : Set :=
| Z : VForm
| V : VForm -> VForm -> VForm.
Fixpoint VForm_mes x :=
match x with
| Z => 0
| V x y => 1 + VForm_mes x + VForm_mes y
end.
Reserved Notation "[ x , y ] ~~> z" (at level 70, format "[ x , y ] ~~> z").
Inductive VF_compare_graph : VForm -> VForm -> ordering -> Prop :=
| VFcg_0 : [Z,Z] ~~> EQ
| VFcg_1 b y : [Z,V b y] ~~> LT
| VFcg_2 a x : [V a x,Z] ~~> GT
| VGcg_3 a x b y o : [a,b] ~~> LT
-> [x,V b y] ~~> o
-> [V a x, V b y] ~~> o
| VGcg_4 a x b y o : [a,b] ~~> EQ
-> [x,y] ~~> o
-> [V a x, V b y] ~~> o
| VGcg_5 a x b y o : [a,b] ~~> GT
-> [V a x,y] ~~> o
-> [V a x, V b y] ~~> o
where "[ x , y ] ~~> z" := (VF_compare_graph x y z).
Reserved Notation "x << y" (at level 70, format "x << y").
Inductive VF_subcall_call : (VForm * VForm) -> (VForm * VForm) -> Prop :=
| VFscc_0 a x b y : (a,b) << (V a x,V b y)
| VFscc_1 a x b y : [a,b] ~~> LT -> (x,V b y) << (V a x,V b y)
| VFscc_2 a x b y : [a,b] ~~> EQ -> (x,y) << (V a x,V b y)
| VFscc_3 a x b y : [a,b] ~~> GT -> (V a x,y) << (V a x,V b y)
where "x << y" := (VF_subcall_call x y).
Definition VF_compare_dom x y := Acc VF_subcall_call (x,y).
#[local] Hint Constructors VF_subcall_call : core.
(* We define a rich version of VF_compare independently of termination
pwc means: packed with conformity (to the spec) *)
Fixpoint VF_compare_pwc x y (d : VF_compare_dom x y) : { o | [x,y] ~~> o }.
Proof.
refine (
match x as u return x = u -> _ with
| Z => fun _ =>
match y with
| Z => exist _ EQ _
| V _ _ => exist _ LT _
end
| V a x' => fun ex =>
match y as v return y = v -> _ with
| Z => fun _ => exist _ GT _
| V b y' => fun ey =>
let (o,Ho) := VF_compare_pwc a b _
in match o return [a,b] ~~> o -> _ with
| LT => fun E => let (o',Ho') := VF_compare_pwc x' y _
in exist _ o' _
| EQ => fun E => let (o',Ho') := VF_compare_pwc x' y' _
in exist _ o' _
| GT => fun E => let (o',Ho') := VF_compare_pwc x y' _
in exist _ o' _
end Ho
end eq_refl
end eq_refl); try (constructor; eauto; fail).
1-2,4-5: apply Acc_inv with (1 := d); subst; eauto.
+ constructor 4; subst; auto.
+ constructor 6; subst; auto.
Qed.
(* We can show termination independently, here by induction on a measure
Notice that we could even deal with a *partial* domain *)
Fact VF_compare_total x y : VF_compare_dom x y.
Proof.
red.
induction on x y as IH with measure (VForm_mes x + VForm_mes y).
constructor; intros (x',y').
destruct x as [ | a x ].
1: inversion 1.
destruct y as [ | b y ].
1: inversion 1.
inversion 1; subst; apply IH; simpl; lia.
Qed.
Definition VF_compare x y := proj1_sig (VF_compare_pwc x y (VF_compare_total x y)).
Fact VF_compare_spec x y : [x,y] ~~> VF_compare x y.
Proof. apply (proj2_sig _). Qed.
(* We use functionality to show fixpoint equations *)
Fact VF_compare_graph_fun x y o1 o2 :
[x,y] ~~> o1 -> [x,y] ~~> o2 -> o1 = o2.
Proof.
intros H; revert H o2.
induction 1; inversion 1; subst; eauto.
all: now apply IHVF_compare_graph1 in H7.
Qed.
#[local] Hint Resolve VF_compare_spec VF_compare_graph_fun : core.
#[local] Hint Constructors VF_compare_graph : core.
Fact VF_compare_fix_0 : VF_compare Z Z = EQ.
Proof. eauto. Qed.
Fact VF_compare_fix_1 b y : VF_compare Z (V b y) = LT.
Proof. eauto. Qed.
Fact VF_compare_fix_2 a x : VF_compare (V a x) Z = GT.
Proof. eauto. Qed.
Fact VF_compare_fix_3 a x b y :
VF_compare a b = LT -> VF_compare (V a x) (V b y) = VF_compare x (V b y).
Proof.
intros H.
apply VF_compare_graph_fun with (1 := VF_compare_spec _ _); eauto.
apply VGcg_3; auto.
now rewrite <- H.
Qed.
Fact VF_compare_fix_4 a x b y :
VF_compare a b = EQ -> VF_compare (V a x) (V b y) = VF_compare x y.
Proof.
intros H.
apply VF_compare_graph_fun with (1 := VF_compare_spec _ _).
apply VGcg_4; auto.
now rewrite <- H.
Qed.
Fact VF_compare_fix_5 a x b y :
VF_compare a b = GT -> VF_compare (V a x) (V b y) = VF_compare (V a x) y.
Proof.
intros H.
apply VF_compare_graph_fun with (1 := VF_compare_spec _ _).
apply VGcg_5; auto.
now rewrite <- H.
Qed.
Require Import Extraction.
Extraction Inline VF_compare_pwc.
Extraction VF_compare.
But of course, since termination is so simple here, you can also proceed by measure induction directly as in
#[local] Hint Constructors VF_compare_graph : core.
Definition VF_compare_direct x y : { o | [x,y] ~~> o }.
Proof.
induction on x y as VF_compare_direct with measure (VForm_mes x + VForm_mes y).
refine (
match x as u return x = u -> _ with
| Z => fun _ =>
match y with
| Z => exist _ EQ _
| V _ _ => exist _ LT _
end
| V a x' => fun ex =>
match y as v return y = v -> _ with
| Z => fun _ => exist _ GT _
| V b y' => fun ey =>
let (o,Ho) := VF_compare_direct a b _
in match o return [a,b] ~~> o -> _ with
| LT => fun Ho => let (o',Ho') := VF_compare_direct x' y _
in exist _ o' _
| EQ => fun Ho => let (o',Ho') := VF_compare_direct x' y' _
in exist _ o' _
| GT => fun Ho => let (o',Ho') := VF_compare_direct x y' _
in exist _ o' _
end Ho
end eq_refl
end eq_refl); eauto.
1-2,4-5: subst; simpl; lia.
+ constructor 4; subst; auto.
+ constructor 6; subst; auto.
Qed.
@Dominique Larchey-Wendling your counter-example is a bit different in the fact that the inner fix takes the same arguments as the outer one. In the initial example this is not the case: the structural argument of the outer fix does not appear in the second. I think this makes the whole thing quite safe and could be accepted.
The link with lexicographic combination of orderings is quite obvious indeed.
Robert Dockins (Nov 18 2022 at 01:58):@Dominique Larchey-Wendling , thanks for working such a thorough example. It does seem like an elegant technique. Starting with an inductive characterization of the function graph is probably a good next step for me, so I'll get started on that.
Last updated: Oct 13 2024 at 01:02 UTC