Stream: Coq users

Topic: ✔ Fin automation


view this post on Zulip James Wood (Apr 26 2022 at 09:01):

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.

view this post on Zulip 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}.

view this post on Zulip 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).

view this post on Zulip 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}?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip James Wood (Apr 26 2022 at 09:34):

I'll use a Notation instead.

view this post on Zulip 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.

view this post on Zulip Notification Bot (Apr 26 2022 at 15:53):

James Wood has marked this topic as resolved.


Last updated: Jan 31 2023 at 14:03 UTC