Redundant clause in match

coq

Solution

There are quite a few wrong things about this.

`False` is not a data constructor, and since there is no syntactic difference between data constructors and variable names in Coq, it understands your `| False =>` as a pattern matching anything and giving it the name `False`, in the same way as you could have written:

Definition inv (a: Prop): Prop :=
  match a with
  | x => True
  | y => False
  end.

This is why it tells you that the second clause is redundant (since the first pattern matches everything).

Now another thing you should know is that the type `Prop` is not inductively-defined, and therefore values of type `Prop` cannot be matched against anything: in fact it would not make sense, since it is an open type that you keep expanding everytime you define a new inductive property.

So there is no way to write a function `inv` the way you write it.

Problem

When I run the following script: ``` Definition inv (a: Prop): Prop := match a with | False => True | True => False end. ``` I get "Error: This clause is redundant." Any idea why this happens? Thanks, Marcus.

Original source