## Stream: Coq users

### Topic: Proving properties of Field

#### Damir Gabitov (Oct 31 2022 at 09:03):

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

#### Karl Palmskog (Oct 31 2022 at 09:31):

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.

#### Damir Gabitov (Oct 31 2022 at 09:37):

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

#### Karl Palmskog (Oct 31 2022 at 09:38):

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

#### James Wood (Oct 31 2022 at 10:09):

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: Dec 05 2023 at 12:01 UTC