Сделать один аргумент больше другого в Idris

Я пытаюсь написать функцию mSmallest, которая принимает два натуральных числа, n и m в качестве входных данных, и создает вектор. Выходной вектор содержит m наименьших членов конечного набора с n элементами.

Например, предполагается, что mSmallest 5 3 производит [FS (FS Z), FS Z, Z], который является Vect 3 (Fin 5).

Я хотел бы ограничить входной аргумент m меньше n. Я пробовал что-то вроде этого:

mSmallest : (n : Nat) -> (m : Nat) -> {auto p : n > m = True} -> Vect m (Fin n)
mSmallest Z Z = ?c_3                                                                   
mSmallest Z (S k) = ?c_5                                                               
mSmallest (S k) m = ?c_2

Второй случай невозможен из-за ввода p. Как сделать так, чтобы случай Z (S k) исключался?

Кроме того, есть ли лучший способ определения функции mSmallest?


idris
person mushroom    schedule 20.04.2015    source источник

Ответы (1)


arrow_upward
6
arrow_downward

Я не думаю, что n > m = True достаточно конструктивен; если вместо этого вы используете предложение GT, вы можете исключить первые две ветви, поскольку в этом случае нет способа сопоставления с образцом для p:

-- Note that mSmallest is accepted as total with just this one case!
total mSmallest : (n : Nat) -> (m : Nat) -> {auto p : n `GT` m} -> Vect m (Fin n)
mSmallest (S k) m {p = LTESucc p} = replicate m FZ

(в этом случае используется фиктивная реализация mSmallest для интересного случая, поскольку она должна быть ортогональна исходному вопросу).

person Cactus    schedule 21.04.2015
comment
Спасибо! Я не очень понимаю часть {p = LTESucc p}. Я не верил, что это будет необходимо, и когда я удалил его, код все еще компилировался. Какова цель этого? - person mushroom; 21.04.2015
comment
Возможно, это не так... Его оставили там, так как я разделил регистр аргумента p, чтобы убедиться, что два других случая абсурдны. Хотя он может понадобиться для рекурсивных вызовов в реальной реализации mSmallest. - person Cactus; 21.04.2015
comment
Я думаю, что m > n = True на самом деле должно быть достаточно хорошим, хотя дух Дикого Запада в классах Idris, вероятно, затруднит выражение (т. е. вам, вероятно, потребуется явно вызвать канонический экземпляр Ord). Затем вы закончите тем, что будете делать доказательство от случая к случаю, которое копается в реализации compare для Nat, чтобы доказать, что, по модулю абсурда класса типов, n > m = True -> GT n m. Предполагая, что это возможно, это, вероятно, будет что-то уродливое с the и %instance и @ и фигурными скобками. - person dfeuer; 21.04.2015