In Agda, I'd expect to write something like `auto_fin`

below to let me input a concrete natural number and produce the corresponding fin of concrete size. However, in Coq it doesn't seem to work so well. As written, the implicit argument `prf`

is left unsolved (with `Check`

displaying `?prf : [ |- So (3 <? 5)]`

), and if I add `(prf:=I)`

, it complains with `The term "I" has type "True" while it is expected to have type "So (3 <? ?n)".`

(as if it didn't wait to unify `?n`

with `5`

, then find that `I`

actually does have the right type). How would I normally solve this problem in Coq? I could provide `n`

explicitly, but that produces a lot of repetition in my actual use case.

```
Require Fin.
Require Import PeanoNat.
Definition So (b : bool) : Prop := if b then True else False.
Definition So_eq {b : bool} : So b -> b = true :=
match b with
| true => fun _ => eq_refl
| false => False_rec _
end.
Definition auto_fin {n} m {prf : So (m <? n)} : Fin.t n :=
Fin.of_nat_lt (proj1 (Nat.ltb_lt _ _) (So_eq prf)).
Check auto_fin 3 : Fin.t 5.
```

James Wood said:

if I add

`(prf:=I)`

, it complains with`The term "I" has type "True" while it is expected to have type "So (3 <? ?n)".`

(as if it didn't wait to unify`?n`

with`5`

, then find that`I`

actually does have the right type).

Then you need to enable bidirectional typing (denoted by the ampersand below):

```
Arguments auto_fin {n} & m {prf}.
```

Ah, thanks! I had a look at the documentation about `&`

before, but found it a bit confusing (mostly for terminology clashes, I think, e.g using "check" to mean synthesise).

So what, precisely, does the type checking look like in this case? And why's it different to having `Arguments auto_fin & {n} m {prf}`

?

As far as I understand, it means that the arguments to the left of `&`

are inferred using the return type of the application rather than the converse. Putting `&`

in first position is the same as not putting it, since there is no argument to the left.

Weirdly it seems to be incompatible with `SProp`

, which I was trying out for a bit to get `prf`

to be solved automatically.

I'll use a `Notation`

instead.

A bit out of topic but `Fin`

is notoriously hard to use (ordinals from math-comp for instance are often more convenient https://github.com/math-comp/math-comp/blob/7a9bbcdcbcfbaa83f7fe1693b7e7aece9c5e1b52/mathcomp/ssreflect/fintype.v#L49 ). More generally, the fact that something is in the stdlib only reflects history, not the fact that it is state of the art. It is not uncommon that alternative libraries like stdpp or math-comp now offer better solutions.

James Wood has marked this topic as resolved.

Last updated: Jun 23 2024 at 01:02 UTC