#coq
#coq
Вопрос:
Предположим, я уже определил floor (от R до Z ). Теперь я хочу доказать, что n <= x это подразумевает n <= floor(x) , где n : Z , x : R .
Я пытался:
Lemma l: forall (n:Z) (x:R), (IZR n) <= x -> n <= (floor x).
но я получаю сообщение об ошибке The term n has type Z while it is expected to have type R.
Как я должен это написать? Есть ли способ, который я могу использовать <= для Z и R одновременно?
Ответ №1:
Чтобы переопределить интерпретацию обозначения по умолчанию, вы можете открыть область обозначения локально, используя %key :
Lemma l : forall n x, (IZR n <= x)%R -> (n <= floor x)%Z.