invalid constructor of `sum` · Coq users

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.

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.

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?

Ramkumar Ramachandra (Jun 02 2020 at 11:57):

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

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

Cyril Cohen (Jun 02 2020 at 12:35):

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

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

Théo Winterhalter (Jun 02 2020 at 12:49):

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

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)

Stream: Coq users

Topic: invalid constructor of `sum`

Ramkumar Ramachandra (Jun 02 2020 at 11:02):