Stream: Coq devs & plugin devs

Topic: case quiz


view this post on Zulip Gaëtan Gilbert (Mar 17 2022 at 13:29):

in context Require Vector., what happens for each check?

Check (fun n (x: Vector.t True (S n)) =>
  match x in Vector.t _ (S m) return True with
    |Vector.cons _ h _ _ => h
  end).

Check (fun n (x: Vector.t True (S n)) =>
  match x in Vector.t _ _ return True with
    |Vector.cons _ h _ _ => h
  end).

Check (fun n (x: Vector.t True (S n)) =>
  match x in Vector.t _ _ with
    |Vector.cons _ h _ _ => h
  end).

Check (fun n (x: Vector.t True (S n)) =>
  match x in Vector.t@{} _ _ with
    |Vector.cons _ h _ _ => h
  end).

Check (fun n (x: Vector.t True (S n)) =>
  match x in Vector.t True _ with
    |Vector.cons _ h _ _ => h
  end).

view this post on Zulip Guillaume Melquiond (Mar 17 2022 at 13:32):

I think the 5th one fails because of the constant argument True. And I suppose (otherwise you would not ask) that the 4th one fails due to the nonsensical universe constraint.

view this post on Zulip Gaëtan Gilbert (Mar 17 2022 at 13:34):

what do you mean nonsensical? Check Vector.t@{}. works fine

view this post on Zulip Guillaume Melquiond (Mar 17 2022 at 13:35):

I mean that it is the same as for the 5th case. Universes have no impact on the matching, so they do not make sense there, same as constant argument.

view this post on Zulip Pierre-Marie Pédrot (Mar 17 2022 at 13:36):

Universes have no impact on the matching

unfortunately that's not really true at least from the kernel point of view

view this post on Zulip Guillaume Melquiond (Mar 17 2022 at 13:37):

Do you mean that it would make sense to match on a universe and then use it in the return clause?

view this post on Zulip Gaëtan Gilbert (Mar 17 2022 at 13:38):

not match on it, but consider how fun x => match x in bool with _ => tt end constraints the type of x, parameters and univs in the in clause could also constraint the discriminee

view this post on Zulip Guillaume Melquiond (Mar 17 2022 at 13:40):

But matching with a pure wildcard is such a degenerate case. Not sure it is worth making things more complicated just for it.

view this post on Zulip Gaëtan Gilbert (Mar 17 2022 at 13:42):

the data is there in the kernel so we should have a way to print it. then it's natural to also parse it.

view this post on Zulip Guillaume Melquiond (Mar 17 2022 at 13:44):

Actually, I am surprised it is there in the first place. I would have expected only the binders to appear in the kernel in clause, not the full inductive type.

view this post on Zulip Pierre-Marie Pédrot (Mar 17 2022 at 13:57):

About the return clause, the kernel sees the instance, the parameters and that's about it (the names are also there but not relevant).


Last updated: Oct 13 2024 at 01:02 UTC