элементы группы с ограничениями

Question

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

Definition groupmin (sn maxlimit maxsn: nat) : nat := 
   let avg := div maxlimit maxsn in 
   (sn*avg) - (avg - 1).

 Definition groupmax (sn maxlimit maxsn: nat) : nat := 
   let avg := div maxlimit maxsn in sn*avg.

Answer 1

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

Чтобы иметь функцию, которая выглядит как деление натуральных чисел, я предлагаю вам загрузить библиотеку Arith. Тогда вам будет разрешено использовать обозначение a / b для деления.

Вот пример:

Require Import Arith.
Check (fun x y => x / y).
(* this returns : fun x y : nat => x / y : nat -> nat -> nat *)
Compute (12 / 5).
(* this returns : = 2 : nat *)
Locate "_ / _".
(* this returns : "x / y" := Nat.div x y : nat_scope *)

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