So I'm trying to define an inductive set in coq that has integers from 0 to 10:
Inductive OD : Set := 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10.
I get this message:
Syntax error: '.' expected after [vernac:gallina] (in [vernac_aux]).
Nothing I tried has really worked
On
Your question mixes objects of a different nature. When you say "an inductive type that has integers from 0 to 10", you are actually describing a situation that is impossible.
It is the nature of inductive types that their elements are distinct from elements of any other types. So you can decide to define an inductive with eleven elements, named in a way that reminds of the 11 integers 0 to 10, but this new inductive you wish to define does not have these integers. In other words, the integers 0 to 10 are not members of this type.
So a first solution is the one presented by Lolo in a different answer, repeated here:
Inductive OD : Set := N0 | N1 | N2 | N3 | N4 | N5 | N6 | N7 | N8 | N9 | N10.
However, the elements N0.. N10 are not integers, they are elements of type OD. You cannot use them in operations that require integers.
This an inherent difference between Type Theory, the theory that underlies the Coq system and set theory, the theory that people are accustomed to use when performing practicing mathematics.
To reduce the gap between type OD and integers, there is another approach than the notation approach shown above. We can provide coercions between the type of integers and and the type OD. Here is my solution:
Open Scope Z.
Definition Z_of_OD (x : OD) :=
match x with
N0 => 0
| N1 => 1
| N2 => 2
| N3 => 3
| N4 => 4
| N5 => 5
| N6 => 6
| N7 => 7
| N8 => 8
| N9 => 9
| N10 => 10
end.
Coercion Z_of_OD : OD >-> Z.
Check ( 135 + N0).
Definition OD_of_Z (x : Z) :=
match x with
0 => N0
| 1 => N1
| 2 => N2
| 3 => N3
| 4 => N4
| 5 => N5
| 6 => N6
| 7 => N7
| 8 => N8
| 9 => N9
| _ => N10
end.
Coercion OD_of_Z : Z >-> OD.
Check 8 : OD.
As you can see with the two Check commands, you now have a type OD containing 11 elements, which associated to integers (but they are not integers) thanks to the two provided coercions Z_of_OD and OD_of_Z. Thanks to these coercions, any integer can be viewed as an element of OD, the integers that are outside the range of OD being mapped to N10. So you can use an object of type OD where you would expect an integer and you can use an object of type Z where you would expect an element of OD.
In practice, the Coq system maintain the distinction, so that OD does not have the integers 0 to 10, but in day-to-day usage, this simulates what you want, I believe.
For instance you can define a function that maps the elements of OD to a circular notion of successor.
Definition OD_succ (x : OD) :=
match x with
N0 => N1
| N1 => N2
| N2 => N3
| N3 => N4
| N4 => N5
| N5 => N6
| N6 => N7
| N7 => N8
| N8 => N9
| N9 => N10
| N10 => N0
end.
The function OD_succ requires an argument of type OD and returns a result in type OD, but we can write the following expression:
Compute (1 + OD_succ 10).
This returns 1 because
OD, so 10 is replaced by OD_of_Z 10OD_of_Z computes to N0OD_succ (OD_of_Z 10) is not an integer, so it cannot be used in an integer operation, it is replaced by Z_of_OD (OD_succ (OD_of_Z 10)Z_of_OD (OD_succ (OD_of_Z 10) returns the integer 0On the other hand, if require
Compute OD_succ 10.
The result has type OD and is displayed as N0. So the distinction between types is maintained by the Coq system. The coercions simply makes this distinction more comfortable to live with.
This approach still has some drawbacks, for instance, we need a little more work to talk about the subset of integers that corresponds to OD, but there are other solutions for this. If you want to go in that direction, I suggest you study the treatment of finite types and intial segments of the natural numbers (named ordinal types) in the library mathematical components
Unfortunately the parser is expecting a constructor not a number after
:=. You can bypass this usingNotation.