Damir Gabitov (Oct 31 2022 at 09:03): 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: Apr 20 2024 at 07:01 UTC