## Stream: Coq users

### Topic: Coq's guard condition

#### Yann Leray (Nov 18 2022 at 02:01):

I found an instance where the guard condition in a recursive call is false at first but becomes true if I reduce a previous definition. Why does the condition not work with terms in normal form (at least when it can't conclude with unreduced terms) ?
Also, I now have issues surrounding this : how should I handle everything ?

#### Théo Winterhalter (Nov 18 2022 at 14:08):

Do you have a small enough example that you could show here?

#### Pierre-Marie Pédrot (Nov 18 2022 at 14:11):

The standard counter-example to WN but non-SN is precisely due to the fact we (used to) not to reduce.

#### Pierre-Marie Pédrot (Nov 18 2022 at 14:12):

namely `fix F (u : unit) := (fun _ => 0) (F tt)`.

#### Pierre-Marie Pédrot (Nov 18 2022 at 14:13):

@Yann Leray what version are you using? The guard condition was changed in 8.16 (IIRC) to handle this situation

#### Yann Leray (Nov 19 2022 at 01:07):

Funny you should say that; I was porting code which worked in 8.14 to 8.16; I also just checked and it works as is with Coq 8.15.2
I'll make a small example now

#### Yann Leray (Nov 19 2022 at 03:11):

I wouldn't know how to make this smaller :

``````Inductive two := A | B.

Implicit Types (t : two) (l : list two).

Definition P (on_list : list two -> Type) l t :=
prod unit (match t with A | B => on_list l end).

Definition P_size {on_list} (on_list_size : forall l, on_list l -> nat) l t (w : P on_list l t) : nat :=
match t return P _ _ t -> nat with
| A | B => fun tu => on_list_size _ (snd tu)
end w.

Inductive All_fold_two {P_on_list : list two -> two -> Type} : list two -> Type :=
| fold_nil : All_fold_two nil
| fold_cons_abs l : All_fold_two l -> P_on_list l A -> All_fold_two (cons A l)
| fold_cons_def l : All_fold_two l -> P_on_list l B -> All_fold_two (cons B l).
Arguments All_fold_two : clear implicits.

Definition All_fold_two_size0 P_on_list (P_on_list_size : forall l t, P_on_list l t -> nat) : forall l, All_fold_two P_on_list l -> nat :=
fix fold l w :=
match w with
| fold_nil => 0
| fold_cons_abs l' w' p
| fold_cons_def l' w' p => P_on_list_size _ _ p + fold _ w'
end.

Definition All_fold_two_size {on_list} on_list_size :=
(* Eval unfold All_fold_two_size0, P_size in *)
All_fold_two_size0 (P on_list) (P_size on_list_size).

Inductive on_list (l : list two) : Type :=
| on_list_intro : All_fold_two (P on_list) l -> on_list l.

Fixpoint on_list_size l (d : on_list l) {struct d} : nat :=
match d with
| on_list_intro _ a => All_fold_two_size on_list_size l a
end.
``````

#### Yann Leray (Nov 22 2022 at 00:14):

(In Coq 8.16, this doesn't compile until you uncomment the `Eval` part, in Coq 8.15.2 it compiles no matter what)

#### Paolo Giarrusso (Nov 22 2022 at 00:34):

Is it possible that unfolding removes an occurrence of on_list_size that violates the guard condition? If yes, the change seems to be intended based on the changelog?

https://coq.inria.fr/refman/changes.html#id2

Changed: Fixpoints are now expected to be guarded even in subterms erasable by reduction, thus getting rid of an artificial obstacle preventing to lift the assumption of weak normalization of Coq to an assumption of strong normalization; for instance (barring implementation bugs) termination of the type-checking algorithm of Coq is now restored (of course, as usual, up to the assumption of the consistency of set theory and type theory, i.e., equivalently, up to the weak normalization of type theory, a "physical" assumption, which has not been contradicted for decades and which specialists commonly believe to be a truth) (#15434, incidentally fixes the complexity issue #5702, by Hugo Herbelin).

#### Yann Leray (Nov 23 2022 at 03:09):

I managed to simplify it down more and it does indeed appear that an occurence that violates the guard condition is erased by reduction.
My question is now why the following code violates the guard condition (this is pretty much what gets erased) :

``````Inductive box P := box_intro : P -> box P.
Inductive P := P_intro : box P -> P.

Fixpoint size (d : P) {struct d} : nat :=
let 'P_intro p := d in
match tt as t
return box (match t with tt => P end) -> nat
with
| tt => fun tu =>
let 'box_intro _ tu' := tu in
size tu'
end p.
``````

`Recursive call to size has principal argument equal to "tu'" instead of one of the following variables: "p" "tu".`

#### Paolo Giarrusso (Nov 23 2022 at 03:17):

well, `tu'` is a subterm of `tu`, which isn't a subterm of `p` until beta-reduction

#### Paolo Giarrusso (Nov 23 2022 at 03:20):

but it seems _some_ reduction still happens during guard checking, and I wouldn't know why _this_ redex isn't reduced.

#### Paolo Giarrusso (Nov 23 2022 at 03:26):

said otherwise, I don't know if the unreduced term admits an infinite reduction sequence — all I can say is that the guard condition isn't (AFAIK) expected to be complete

#### Yann Leray (Nov 23 2022 at 04:22):

I guess I wouldn't be as surprised if `tu` weren't cited in the list of possible variables, but now that it is I'm curious why my `tu'` isn't accepted

#### Yann Leray (Nov 23 2022 at 04:38):

It should also be noted that replacing `match t with tt => P end` with `match tt with tt => P end` makes Coq accept the function

#### Guillaume Melquiond (Nov 23 2022 at 07:50):

The guard condition becomes really peculiar when the expression involves a `match` with a `return` clause. Here, by stating that `tu` has type `box (match t with tt => P end)` (instead of, e.g., `match t with tt => box P end`), you are confusing the checker. I don't know if it is an implementation issue or if there is a good reason that makes this case hard to recognize.

#### Yann Leray (Nov 24 2022 at 21:22):

Is there some documentation or paper I can read which would explain why `tu` is a valid subterm but `tu'` isn't ? I tried reading the code but I don't have enough background knowledge to understand the names used and lost myself as I tried to follow the flow

#### Kazuhiko Sakaguchi (Nov 24 2022 at 21:31):

If you want something rigid, I would recommend reading Codifying Guarded Definitions with Recursive Schemes and then Structural Recursive Definitions in Type Theory. But, I guess the current implementation in Coq is explained nowhere (except for `inductive.ml` in the kernel).

#### Kazuhiko Sakaguchi (Nov 24 2022 at 21:55):

Anyways I do not think these papers explain what happens in your example.

Last updated: Oct 04 2023 at 22:01 UTC