Stream: Coq users

Topic: Confusing match

view this post on Zulip Philip Zucker (Jun 04 2020 at 21:36):

I was trying something that was a little complicated and couldn't get it to go through. I asked someone and they suggested it might not be possible to define such a function because -> isn't injective?

Inductive Foo (g : Type -> Type) : Type -> Type :=
  foo : forall a b, (g a -> g b) -> Foo g (a -> b).
Definition run {a b g} (f : Foo g (a -> b))  : g a -> g b :=
  match f with
  | foo _ _ _ f' => f'
  end.

view this post on Zulip Gaëtan Gilbert (Jun 04 2020 at 22:00):

Indeed Foo g T is equivalent to { a & { b & ((g a -> g b) * (T = (a -> b))) } }
(in case that's easier to read, if it was in Prop that would be exists (a b : Type) (_ : g a -> g b), T = (a -> b))

Last updated: Oct 01 2023 at 17:01 UTC