Stream: Coq users

Topic: Coq's guard condition


view this post on Zulip Yann Leray (Nov 18 2022 at 02:01):

typing_size: forall (Γ : context) (t T : term), typing Γ t T -> size
Γ: context
a: well_typed Γ
n := (fix well_typed_size (Γ : context) (w : well_typed Γ) {struct w} : size :=
           match w with
           | welltyped_nil => base
           | welltyped_cons_abs Γ' t wt' p =>
               (typing_size Γ' t p.2.π1 p.2.π2.2 + well_typed_size Γ' wt')%nat
           | welltyped_cons_def Γ' b t wt' p =>
               (typing_size Γ' b t p.1.1 +
                typing_size Γ' t p.2.π1 p.2.π2.2 +
                well_typed_size Γ' wt')%nat
           end) Γ a : nat

I'm defining typing_size as a fixpoint where the structural argument is Constr Γ a (here destructured), and I want to return n as defined here.
However, Coq tells me that the recursive definition is ill-formed. The issue specifically comes from p.1.1 as when I replace it with a dummy value, Coq doesn't complain anymore. I wonder why p.2.π2.2 is accepted but p.1.1 not
(.1 and .2 are fst and snd, .π1 and .π2 are the first and second projection on a sigT)
(Hopefully I didn't remove the issue when I simplified the example)

view this post on Zulip Théo Winterhalter (Nov 18 2022 at 14:08):

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

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Nov 18 2022 at 14:12):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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).

view this post on Zulip 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 :=
  match d with
  | P_intro p =>
      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
  end.

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Kazuhiko Sakaguchi (Nov 24 2022 at 21:55):

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


Last updated: Feb 06 2023 at 13:03 UTC