Stream: Coq users

Topic: invalid constructor of `sum`


view this post on Zulip Ramkumar Ramachandra (Jun 02 2020 at 11:02):

Why does Coq say "invalid constructor" when matching inl in ind? Isn't inl a constructor of sum A B?

  Definition sum (A B : Type) := { x : Bool & if x then A else B }.

  Definition inl {A B : Type} a : sum A B := (true; a).
  Definition inr {A B : Type} b : sum A B := (false; b).

  Definition ind {A B : Type} {C : sum A B -> Type} (f : forall a, C (inl a))
   (g : forall b, C (inr b)) : forall x : sum A B, C x :=
   fun x => match x return C x with
   | inl a => f a
   | inr b => g b
   end.

view this post on Zulip Théo Winterhalter (Jun 02 2020 at 11:19):

inl isn't a constructor and sum ins't an inductive type using your definition.
This only works for constructs using the keyword Inductive.

Inductive sum (A B : Type) :=
| inl : A -> sum A B
| inr : B -> sum A B.

view this post on Zulip Ramkumar Ramachandra (Jun 02 2020 at 11:30):

I'm aware of this example in the stdlib, but I'm still confused; is Definition never a constructor?

view this post on Zulip Ramkumar Ramachandra (Jun 02 2020 at 11:57):

I'm trying to coerce my sigma type into some form of inductive now.

view this post on Zulip Théo Winterhalter (Jun 02 2020 at 12:22):

I mean pattern-matching only matches on terms of an inductive type. So yeah, Definition will never something that is a pattern. In your case you can write something like

match x with
| (true ; a) => f a
| (false ; b) => f b
end

I think.

view this post on Zulip Kenji Maillard (Jun 02 2020 at 12:25):

@Théo Winterhalter , not exactly a beginner question, but how far are positive records such as the sigma type employed by @Ramkumar Ramachandra from single constructors inductives ? Up to implementation discrepancies I would expect the two to be equivalent in a strong sense...

view this post on Zulip Cyril Cohen (Jun 02 2020 at 12:35):

I renamed the topic using more specific keywords than "beginner questions", feel free to adjust.

view this post on Zulip Gaëtan Gilbert (Jun 02 2020 at 12:46):

AFAICT the original code would pass if inl/inr were Notation instead of Definition
definitions in patterns are never (? or at least rarely) unfolded but notations are just syntactic sugar for the match ThéoW posted

view this post on Zulip Théo Winterhalter (Jun 02 2020 at 12:49):

Positive records are a special case of inductive types with a single constructor.

view this post on Zulip Gaëtan Gilbert (Jun 02 2020 at 12:49):

@Kenji Maillard non-"primitive" records are syntactic sugar over single constructor inductives, and in addition they enable the use of canonical structures and they get extracted to ocaml records
the kernel only stores "this is a non primitive record" so that extraction can get the information through functors (getting non kernel information about stuff in a functor is quite hard)

view this post on Zulip Ramkumar Ramachandra (Jun 02 2020 at 12:53):

Thanks! Using a notation is a good solution to the problem :)


Last updated: Jan 31 2023 at 13:02 UTC