Я часто получаю проверочные термины в виде:
Lemma of_nat_gt_0: forall (n: nat),
(Z.of_nat n >=? Int32.unsigned (Int32.repr 0)) = true.
Теорема очевидно верна (Z натурального всегда будет >= 0. Аналогично, unsigned repr 0 даст 0.
Однако, они просто прямо раздражают , потому что мне нужно иметь дело с
Int32 из модуля CompCert.Integers Z.of_nat конверсий.
Часто у меня также есть термины из Pos и N определений.
Эти доказательства включают в себя несколько ручных переписываний, чтобы жонглировать в некоторую стандартную форму, а затем omega вызов.
Есть ли какой-нибудь способ "нормализовать" все это в единое унифицированное представление?
Я понимаю, что это подразумевает передачу между разными кольцами (например, Int32 - это Z/(2^32 - 1)). Было бы неплохо, если бы был какой-то способ справиться с этим, потому что это доказательства, которые становятся раздражающе длинными.