Fix followed by fun

Using Coq
1

A recursive abstraction (fix) followed by an lambda abstraction (fun) seems to be converted by the reader into a fix with extra arguments. For instance,

Set Printing All.
Check fix add x := fun y =>
  match x with
  | O => y
  | S x' => S (add x' y)
  end.

yields

fix add (x y : nat) {struct x} : nat :=
  match x return nat with
  | O => y
  | S x' => S (add x' y)
  end
     : forall (_ : nat) (_ : nat), nat

But it’s not just the reader, it’s a conversion rule. Consider

Definition foo :=
  fix F x := fun y => match x with
                   | O => y
                   | S x' => S y
                   end.

Definition foo' x y :=
  match x with
  | 0 => y
  | S x' => S y
  end.

Goal foo = foo'.
  Fail reflexivity.
Abort.

Goal foo = fix F x := foo' x.
reflexivity.
Qed.

I’m puzzled. Did this enter the kernel with \eta-conversion? Or was it there before and I’m just ignorant of the conversion rule? Or is there some other explanation? I would be very thankful for pointers. Gert

1 Like
2

Internally a fixpoint is a term for the type of the fixpoint (nat -> nat -> nat for addition), a term for the body (fun x y => match ... with the fixpoint variable add free) and an index indicating which argument is the principal one (the first one for addition) (a bit more complicated for mutual fixpoints but same idea).
This means that any arguments after the principal argument are not special, they’re just normal lambdas.

So a printed form which looks similar to the internal representation might be fix add {struct 1} : nat -> nat -> nat := fun x y => match .... To make it look nicer we put as many arguments to the left of the := as possible (and this lets us use a name instead of an index in struct), thus fix add (x y : nat) {struct x} : nat := match ...

Does that make sense?

1 Like
3

Implementation-wise it does. But it implements a conversion rule, AFAICS.

4

Ok, I see. That fix always ends after the recursive argument and the printer always merges the following lambdas into the fix explains it all. Thanks.

5

yes‮‮‮‮‮‮‮‮‮‮‮‮‮‮‮‮‮‮‮‮