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