Historical questions concerning inductive types (guard condition, accessibility)

Dear Coq pioneers and experts,

I’m curious about two issues with inductive types that changed since Giménez tutorial (1998; 2006 with Pierre Castérand) and the Coq’ Art Book (2004, Coq V8.0)

  1. In the Ssreflect tutorial (2009) a direct definition of an Euclidean division function appears exploiting an extended guard condition. This is in sharp contrast to Giménez’ tutorial and the Coq’ Art book where division is done with Acc-recursion.
    My question: Was the guard condition adapted to do this example, or was the possibility to write Euclidean division directly overlooked before? Definition appears below.

  2. Our days Coq generates an computational eliminator Acc_rect for ACC exploiting that ACC allows computational elimination. In the Coq’ Art book the computational eliminator for ACC is realized by moving the match to a propositional context, a technique that appears before in Giménez. Giménez in fact says that the single proof constructor must be non-recursive to enable computational elimination (the “non-recursive” is dropped in the Coq’ Art book and today’s Coq).
    My question: When did Coq first generate the standard eliminator Acc_rect? Is there a preference for one of the two computational eliminators for Acc as it comes to extraction? Definitions appear below.

Thanks in advance, Gert

Fixpoint div x y :=
  match x - y with
  | 0 => 0
  | S z => S (div z y)
  end.

Section Acc.
  Variable X: Type.
  Variable R: X -> X -> Prop.
  Inductive Acc (x: X) : Prop := AccI (f: forall y, R y x -> Acc y).
  Variable p: X -> Type.
  Variable H: forall x, (forall y, R y x -> p y) -> p x.
  Fixpoint elim (x: X) (a: Acc x) : p x :=
    H x (fun y r => elim y (match a with AccI _ f => f y r end)).
  Fixpoint elim' (x: X) (a: Acc x) : p x :=
    match a with AccI _ f => H x (fun y r => elim' y (f y r)) end.
End Acc.
1 Like

I heard a story about 1 before, and I could find the relevant commit:
https://github.com/coq/coq/commit/1f195b9b69b12ace9152b5fc815417f29fe54245
The definition of div that uses minus passes the (awfully syntactic) termination check only after this commit. In particular returning n (which values 0 in that branch) and not 0 (the constant) helps the termination checker propagate size info (which is attached to variables).

3 Likes

Hi @gert-smolka

  1. In the Ssreflect tutorial (2009) a direct definition of an Euclidean division function appears exploiting an extended guard condition. This is in sharp contrast to Giménez’ tutorial and the Coq’ Art book where division is done with Acc-recursion.
    My question : Was the guard condition adapted to do this example, or was the possibility to write Euclidean division directly overlooked before? Definition appears below.

To my knowledge, it is just that this way to write Euclidean division directly was overlooked before. As indicated in the commit shown by @gares, I heard first about it from Benjamin Werner and Assia Mahboubi and if I remember correctly, this was found by Georges Gonthier. There is no change of the guard condition involved.

  1. Our days Coq generates an computational eliminator Acc_rect for ACC exploiting that ACC allows computational elimination. In the Coq’ Art book the computational eliminator for ACC is realized by moving the match to a propositional context, a technique that appears before in Giménez. Giménez in fact says that the single proof constructor must be non-recursive to enable computational elimination (the “non-recursive” is dropped in the Coq’ Art book and today’s Coq).
    My question : When did Coq first generate the standard eliminator Acc_rect? Is there a preference for one of the two computational eliminators for Acc as it comes to extraction? Definitions appear below.

In this case, it is a change of the guard condition, which appears in commit
https://github.com/coq/coq/commit/16084065ebcff9eeba7231e687611fd9acb54887 (at the time of Coq version 8.2). There was no reason not to accept this direct elimination since it was anyway definable.

I don’t know if it matters for extraction. If H uses its argument, I suspect that it should not matter so much, but I did not really think closely at it.

1 Like