I opening a thread on `match`

with alias. Note that the cep link was not linking to the expected branch and thus to the expected document (in particular, the intention was that the extra new variable `w`

knows only the type, not the value, which may have induced confusion). The link has now the intended document.

Do we need a new construct? It seems that just letting the guard checker about syntactically equal terms would be sufficient.

There was a discussion a the Coq call about CEP #74. I have the impression that the discussion actually mixed two different questions.

There was a discussion on whether `Nat.sub`

, as it is validated by the guard condition (*), can be encoded with a recursor and the answer is: it needs first a generalization on the second variable.

But there was another discussion, independent of the guard in itself, which is how a recursor on a dependent type should be typed. E.g. taking the example of `nat`

:

```
nat_rect : forall P : nat -> Type,
P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n
```

I can write an identity function that copies the whole structure except the base case:

```
Definition id n := nat_rect (fun _ => nat) n (fun _ p => S p) n.
```

However, if I take the example of `Vector.t`

:

```
Vector.t_rect : forall (A : Type) (P : forall n : nat, t A n -> Type),
P 0 (nil A) ->
(forall (h : A) (n : nat) (t : t A n), P n t -> P (S n) (cons A h n t)) ->
forall (n : nat) (t : t A n), P n t
```

I cannot build the same identity function:

```
Fail Definition id A n v :=
Vector.t_rect A (fun n _ => Vector.t A n) v (fun h n _ v' => cons A h n v') n v.
```

Would it make sense to consider instead a dependent recursor which has this type:

```
Vector.t_rect : forall (A : Type) (P : forall n : nat, t A n -> Type),
(P 0 (nil A) -> P 0 (nil A)) ->
(forall (h : A) (n : nat) (t : t A n), P n t -> P (S n) (cons A h n t) -> P (S n) (cons A h n t)) ->
forall (n : nat) (t : t A n), P n t
```

with which one could write:

```
Fail Definition id A v :=
Vector.t_rect A (fun n _ => Vector.t A n)
(fun v_alias => v_alias)
(fun h n _ v' v_alias => cons A h n v') v.
```

where, at computation time, `v_alias`

is bound to the constructor. Would this still be strongly terminating?

(*) for the record:

```
Fixpoint sub (n m : nat) {struct n} : nat :=
match n with
| 0 => n
| S k => match m with
| 0 => n
| S l => sub k l (* implicit generalization needed in recursor to apply it to l *)
end
end
```

@Guillaume Melquiond

Do we need a new construct? It seems that just letting the guard checker about syntactically equal terms would be sufficient.

Yes, that would be an alternative, though maybe a bit tricky. If we ask strictly for syntactic equality and two inferred implicit arguments are e.g. different, that would not be caught. On the other side, if we expect full conversion, that may equate more terms than what we had intuitively wanted.

In my opinion, the `as`

syntax is worth having, as it might make the gallina more readable in some cases. But it should not be the solution for a deficiency of the guard checker. As for the guard checker, I would go for strict equality, and if the issue with implicit arguments ever occurs, the user can always fall back to `as`

, but it should only be as a last resort.

The example

```
Fail Definition id A n v :=
Vector.t_rect A (fun n _ => Vector.t A n) v (fun h n _ v' => cons A h n v') n v.
```

fails because the third argument of `Vector.t_rect`

should be of type `Vector.t A 0`

: it should be `Vector.nil A`

, not `v`

. The following definition type-checks:

```
Definition id A n v :=
Vector.t_rect A (fun n _ => Vector.t A n) (Vector.nil A) (fun h n _ v' => cons A h n v') n v.
```

(oops, I realize it is precisely your point: you want an alias for `v`

!)

I had not realized that this simple encoding from @Gaëtan Gilbert works (maybe @Thierry Martinez had it at some time too and I then apologize if I forgot):

```
Definition id A n v :=
Vector.t_rect A (fun n _ => Vector.t A n -> Vector.t A n)
(fun v => v) (fun h n t v' _ => cons A h n (v' t)) n v v.
```

Assuming the two `v`

reduced similarly in parallel, the algorithmic content is also the same (up to the extra beta).

I'm really not convinced by this: it means that every iota-reduction does one more substitution as well. I would much prefer that the guard realize that in `match p with S n => foo (S n)`

S n and p have the same size. It would be exactly what a translation to well-founded recursion would do, e.g. enrich every `match`

with an equality (the usual convoy pattern) so that we can use `p = S n`

to justify recursive calls.

I was always a little worried about allowing constructor-headed terms to be considered subterms, thinking it might fire fixpoint reductions we don't want, but in retrospect, the only way to get to this `S n`

term (in fixpoint principal argument position) is to have reduced the match on `p`

, so `p`

is already convertible to `S n`

for some `n`

Also, when we go do strong reduction in the bodies of fixpoints, we don't bind the prototypes to the fixpoint block itself, so we can't get into infinite reductions from this either.

I would much prefer that the guard realize that in

`match p with S n => foo (S n) S n`

and`p`

have the same size.

Why not. We can try to see how to implement a guard which accepts constructed smaller subterms (maybe by memoizing the trace of the subterm relation?).

the usual convoy pattern

Indeed, my understanding (after Gaëtan's remark) is that this `as`

clause is exactly a convoy pattern in "direct style".

After thinking again to it, I don't see how to support constructed recursive arguments. If I define:

```
Fixpoint f n := match n with S (S p) => f (S p) | _ => 0 end.
```

then, `f (S q)`

reduces to `match q with S p => f (S p) | _ => 0 end`

where `f`

is not anymore a variable, so it reduces infinitely many often (in strong reduction).

Hmm right! We would need to rewrite the fixpoint so that the calls are on the variables but then you have the typing issues again...

Still I don't like the idea that every iota reduction will have a new term being substituted just because of a deficiency of the guard checker...

Thierry M. made experiments and it seems to work for the guard if we just use a generalization (since the size of term traverses `match`

s).

So, to me, the question reduces now only to whether we are interesting in providing a "direct style" for a generalization over the term being matched or better not, that is whether we want the extra substitution of a term to derive from a generalization or being implemented directly. That is, to evaluate how the sometimes antagonistic requirements for minimality, comfort, efficiency, uniformity, etc. balance each other.

Oh you mean, if we abstract over a vector i in the return predicate and pass that to rec calls. It means “as” is something we can elaborate

Exactly.

I have another argument in favor of hard-wiring the notion of alias: it is that its emulation forces to go outside the class of complexity we may want to control.

Consider for instance the generalization of primitive recursion to dependent types. To simulate a match with alias in this context, we have to locally enter the syntax of Ackermann-like functions, which is morally wrong.

Here is another argument about `match`

with alias, this time regarding evaluation.

Consider the definition of `pred`

as it is now:

```
Definition pred n := match n with 0 => n | S p => p end.
```

and reduce it in call-by-name, as `simpl`

would e.g. do, that is considering the two occurrences of `n`

as distinct in the definition:

```
Eval simpl in pred (id 0).
(* gives "(id 0)" because simpl reduces only the occurrence triggering a iota *)
```

If we had instead written:

```
Definition pred n := match n with 0 as q => q | S p => p end.
```

Then, in call-by-name, there would be only one occurrence of `n`

to reduce whose evaluation would be shared by `q`

.

In comparison, in the emulated form:

```
Definition pred n := match n with 0 => fun q => q | S p => fun _ => p end n.
```

there would also be two distinct occurrences.

That is, `match`

with alias is neither exactly an expansion nor exactly a generalization, but something inbetween, behaving for computation like an expansion sharing the internal representation, and behaving for typing like a generalization.

Last updated: Oct 13 2024 at 01:02 UTC