Как систематически нормализовать неравенства до <(lt) и <= (le) в Coq?

Question

При доказательстве фактов о неравенствах (для вещественных чисел) существует <, <=, > и >=. Довольно утомительно записывать и использовать теоремы/леммы для обеих этих форм.

В настоящее время я конвертирую их только < и <= вручную с помощью первого assert, а затем доказывая тривиальный подцель. Мне было интересно, можно ли автоматически нормализовать все неравенства до < и <= в гипотезах и целях?

Answer 1

gt и ge - это функции, которые вызывают lt и le соответственно при замененных аргументах. Чтобы избавиться от них, просто разворачивайте их.

unfold gt, ge. 

Вы можете разворачиваться lt, а также: она определена в терминах le. Поскольку в определении gt используется lt, сначала разверните gt.

unfold gt, ge, lt. 

Вы можете сказать Coq попробовать это при попытке доказать цель с auto.

Hint Unfold gt ge lt.