search

advancedresearch / poi

a pragmatic point-free theorem prover assistant
Apache License 2.0
136 stars 7 forks source link

Anti-commutativity #550

Open bvssvni opened 4 years ago

bvssvni commented 4 years ago

Quaternions are non-commutative, so some equivalences e.g. (a * b) <=> (b * a) are not sound.

bvssvni commented 4 years ago

One idea is to introduce a swap_sign(a, b) function that returns the sign given that a and b are swapped.

bvssvni commented 4 years ago

Another problem is that when you take the exponential, multiplication turns into addition, so anti-commutativity on multiplication implies anti-commutativity on addition. This leads to unsoundness in quaternion algebra, because addition is commutative.

bvssvni commented 4 years ago

One idea is to lift quaternions into vectors and multiplication into quaternion multiplication.

bvssvni commented 4 years ago

One idea is to use type judgements on quaternions. Pattern matching for binding variables could fail by default on type judgement.