real-number

3зной

1ответ

Как вы переводите дробную часть короткого действительного числа, возвращенного сопроцессором 8087?

Я написал простую программу, которая загружает pi в верхнюю часть стека регистров в 8087, а затем возвращает эту константу в короткую переменную реальной памяти. FLDPI ;load pi FSTP DWORD PTR sh

3зной

1ответ

Функция Matlab, которая генерирует случайные вещественные числа в замкнутом интервале

В Matlab есть функция, которая генерирует случайные действительные числа в интервале времени. Я нашел что-то с unifrnd(), но он генерирует числа в открытом интервале. Если я использую unifrnd(x,y);, я

2зной

1ответ

Как автоматически доказать простое равенство вещественных чисел в Coq?

Что я ищу это auto -как тактика, которая может доказать, простые равенства, как: 1/2 = 2/4 До сих пор, что я попытался вручную, чтобы использовать ring_simplify и field_simplify доказать равенства.

4зной

1ответ

Как легко доказать простое неравенство вещественных чисел в Coq?

Есть ли способ автоматически доказать простые неравенства, как 1/2 >= 0?, Т.е. Require Export Coq.Reals.RIneq. Local Open Scope Z_scope. Local Open Scope R_scope. Example test: /2 >= 0. У меня н

6зной

2ответ

Как «меньше» определено для действительных чисел в Coq?

Мне просто интересно, как отношение «меньше» определено для действительных чисел. Я понимаю, что для натуральных чисел (nat), < может быть определена рекурсивно в терминах одного числа, являющегося (1

3зной

1ответ

Библиотека Coquelicot для базового студенческого исчисления

Я установил Coquelicot поверх mathcomp/SSreflect. Я хочу выполнить очень простой реальный анализ с ним, даже если я до сих пор не владею стандартным Coq. Это моя первая лемма: Definition fsquare (x :