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

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

I'm aware of this example in the stdlib, but I'm still confused; is `Definition`

never a constructor?

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

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.

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

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

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

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

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

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

Last updated: Jun 15 2024 at 08:01 UTC