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.

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.

In that case, I'll probably open a ticket about this, but try to proceed on my development using well-founded recursion.

Perhaps a recursion based on a size argument (like `size x + size y`

) ?

The definition of `BH_compare`

is 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.

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-Trees`

github 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*.

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.

@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`

.

Pierre Castéran said:

Perhaps a recursion based on a size argument (like

`size x + size y`

) ?

The definition of`BH_compare`

is 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).

@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.

Fwiw, if you use equations the definitions are expected to have ugly unfoldings, but you should never need to use them directly

My intuition (but I may be wrong) about the difficulty to read `BH_compare`

's definition is that you have two kinds of inner `fix`

declarations. 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 `merge`

like functions).

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.

@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.

@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: Jan 28 2023 at 05:02 UTC