Coq Reals и Ssreflect GRings

Question

Я хотел бы использовать леммы ssreflect на реалах, определенных в Coq.Reals.Raxioms, Как я могу это сделать?

Например, я хотел бы иметь возможность использовать add, mulи т. д. операции, определенные для ssralg.GRing.Ring непосредственно на переменные типа Rdefintions.R и применить Num.real_closed_axiom непосредственно на реале.

Нужно ли проверять все структуры от eqType, choice, zmodule и т. Д. До ClosedReals? Если так, кто-то должен был сделать это раньше, но я не смог найти его. Есть ли какая-то другая разработка, которую я могу использовать?

Если нет, то как правильно сделать это с помощью аксиом? Нужно ли добавлять дополнительные принуждения и Canonical структура заявления.

Answer 1

Ответ Антона верный, этот вопрос обсуждался на недавнем собрании MathComp, и "официальные" экспериментальные привязки к реалам Кока можно найти по адресу https://github.com/math-comp/analysis/blob/master/Rstruct.v

Обратите внимание, что вышеупомянутая библиотека все еще находится в тяжелой разработке, я предлагаю вам напрямую обсудить с разработчиками дополнительную информацию.