Why does this Coq Definition fail? Coq Namespace error for Inductive Type

user_5166930 0
Viewed 65

I have the following Inductive Type and a test function:

Inductive parameter : Type :=
| Nop
| OneP : forall A, A -> parameter  
| TwoP : forall (A : Type) (r : nat) (b : A), parameter
.
Check (TwoP nat 1 5).


Definition test (p : parameter) : option (nat * nat) :=
match p with 
| TwoP nat x y => Some (x, y)
| _ => None
end.

The test function fails with the error:

The term "Some (x, y)" has type "option (Datatypes.nat * nat)" while it is expected to have type "option (Datatypes.nat * Datatypes.nat)".

I don't understand why my definition does not work. Is there a difference between nat and Datataypes.nat ?

Any help would be appreciated. Thanks!

coq
1 Answers

In Coq, it is not possible to test what a type is. Consider the following program:

Definition is_nat (A : Type) : bool :=
  match A with
  | nat => true
  | _   => false
  end.

If you try to run this, Coq tells you that the last branch is redundant, and rejects the definition. The issue is that nat is taken to be a variable name, not the nat data type from the standard library. Therefore, the first branch matches every type A, and the last branch is redundant. In your example, the pattern nat ends up masking the data type nat, which is why you end up seeing the qualified name Datatypes.nat.

One way of solving this issue is to use a type of codes instead of Type. For instance:

Inductive type : Type :=
| Bool
| Nat.

Definition type_denote t : Type :=
  match t with
  | Bool => bool
  | Nat => nat
  end.

Coercion type_denote : type >-> Sortclass.

Inductive parameter : Type :=
| Nop
| OneP : forall (A : type), A -> parameter
| TwoP : forall (A : type) (r : nat) (b : A), parameter
.
Check (TwoP Nat 1 5).

Definition test (p : parameter) : option (nat * nat) :=
match p with
| TwoP Nat x y => Some (x, y)
| _ => None
end.

There are two issues with this solution. First, it requires you to anticipate all types that you will need in parameter, and add those in the definition of type. Second, it forces you to program with dependent types, which can be hard to manipulate. It might be possible to refactor your definitions to avoid the problem of type matching altogether, although there is no one-size-fits-all solution -- it depends on your application.

user_16337700
Related