Coq's guard condition · Coq users

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):

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):

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):

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?

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

Stream: Coq users

Topic: Coq's guard condition

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