Hello. For example, I have the set R={0,1}, and addition and multiplication operations. Addition operation adds entires from R like this:

0+0=0; 1+1=0 ; 0+1=1; 1+0=1. Multiplication operation is also non-standart, but I won't write it here. I want, for example, prove that addition operation is commutative. Question : How define set R and additon function in Coq?

I have tried like this:

Inductive bin:Type :=

|0

|1.

Definition plus(a:bin) (b:bin):bin :=

match a with

|0=>match b with

|0=>0

|1=>1

end

|1=>match b with

|0=>1

|1=>1

end

end .

But Coq gives an error: Syntax error: [constructor] expected after '|' (in [constructors_or_record]).

I've tried to use natural numbers , but I think it's incorrect, because the set R contains only 0 and 1.

Another quesiton :

I've tried to define "plus" functin like this:

Definition plus2(a:bin) (b:bin):bin :=

match a with

|b => 0

|_=>1

end .

But Coq gives a message that underscore symbol is redudant. From definiton of addition operation we can notice, that if a and b are equal , than result is 0, and 1 in another case. Definition of "plus2" is easy, but I don't understand how to define it correct

There are essentially three ways to formalize structures like fields in Coq: functors (module types), typeclasses, and canonical structures. For typeclasses, I recommend looking at this paper and this library. For canonical structures, I recommend reading this book and using this library.

Thank you. At this moment I know only simple structure, like nat, bool etc. What is a canonical structure.?

https://coq.inria.fr/refman/language/extensions/canonical.html

Syntax error: [constructor] expected after '|' (in [constructors_or_record]).

This is a lexical problem. Identifiers (e.g constructor names) cannot start with a digit. Try renaming `0`

and `1`

to `c0`

and `c1`

, or `O`

and `I`

, or something.

But Coq gives a message that underscore symbol is redudant. From definiton of addition operation we can notice, that if a and b are equal , than result is 0, and 1 in another case.

The `b`

in the `match`

case shadows the `b`

bound earlier, so the pattern `b`

matches everything rather than being an equality test. Many types don't support decidable equality, so this behaviour is the most uniform one. To implement `plus2`

this way, you'll have to define your own equality test for `bin`

.

Last updated: Feb 06 2023 at 00:03 UTC