## Stream: Coq users

### Topic: invalid constructor of `sum`

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

#### 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):

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

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

#### 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)

#### Ramkumar Ramachandra (Jun 02 2020 at 12:53):

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

Last updated: Sep 23 2023 at 14:01 UTC