✔ Fin automation · Coq users · Zulip Chat Archive

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.

Guillaume Melquiond (Apr 26 2022 at 09:06):

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

James Wood (Apr 26 2022 at 09:12):

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

James Wood (Apr 26 2022 at 09:21):

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}?

Guillaume Melquiond (Apr 26 2022 at 09:24):

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.

James Wood (Apr 26 2022 at 09:33):

Weirdly it seems to be incompatible with SProp, which I was trying out for a bit to get prf to be solved automatically.

James Wood (Apr 26 2022 at 09:34):

I'll use a Notation instead.

Pierre Roux (Apr 26 2022 at 12:36):

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.

Notification Bot (Apr 26 2022 at 15:53):

James Wood has marked this topic as resolved.

Last updated: Oct 05 2023 at 02:01 UTC

Stream: Coq users

Topic: ✔ Fin automation

James Wood (Apr 26 2022 at 09:01):