Доказать So (0 < m) -> (п ** т = S п)

Я пытаюсь сделать функцию Идрис типа (j : Nat) -> {auto p : So (j < n)} -> Fin n для преобразования Nat в Fin n. Чтобы получить Z дело работать (и выход FZ), Я пытаюсь доказать, что доказательства 0 < n достаточны для того, чтобы сделать FZ : Fin n.Но я не могу понять, как это сделать.Доказать So (0 < m) -> (п ** т = S п)

Я открыт для создания совершенно другой функции, до тех пор, пока он может преобразовать значения Nat в значения Fin n (где они существуют). Моя цель - иметь еще одну функцию, которая может конвертировать любой Nat в значение Mod n, поэтому на, например, 15 : Nat отображается на 3 : Mod 4. В моем Mod тип имеет один конструктор, mkMod : Fin n -> Mod n.

источник

2014-11-15 James Wood

Возможно, это будет лучше обслуживаться в [CS] (http://cs.stackexchange.com/)? –

@ LasseV.Karlsen Я думаю, что это проблема программирования, а не что-то еще. Существуют похожие (ответные) доказательства на SO (например, [this] (http://stackoverflow.com/questions/23519043/i-cant-prove-n-0-n-with-idris?rq=1)), и я с большей вероятностью получаю ответ здесь. –

Узнав о LT : Nat -> Nat -> Type, я принял другой подход. Я начал с заявления:

natToFin : (j : Nat) -> {auto p : j `LT` n} -> Fin n 
natToFin {n} j {p} = ?natToFin_rhs_1

. Case-расщепление на n, а затем на p в n = Z случае в результате:

natToFin : (j : Nat) -> {auto p : j `LT` n} -> Fin n 
natToFin {n = (S k)} j {p = p} = ?natToFin_rhs_2

, который по существу является доказательством того, я просил. Оттуда мой случай-раскол на j и наполнили нулевого случая, в результате чего:

natToFin : (j : Nat) -> {auto p : j `LT` n} -> Fin n 
natToFin {n = (S k)} Z = FZ 
natToFin {n = (S k)} (S j) {p = p} = ?natToFin_rhs_3

. Я хотел заполнить ?natToFin_rhs_3FS (natToFin j), но контролер типа не позволял мне. Однако, после того, как случай разделить на p, это было прекрасно:

natToFin : (j : Nat) -> {auto p : j `LT` n} -> Fin n 
natToFin {n = (S k)} Z = FZ 
natToFin {n = (S k)} (S j) {p = (LTESucc x)} = FS (natToFin j)

Наконец, я добавил total, и все это проверили.

Единственная проблема сейчас в том, что Идрис не может найти LT доказательства автоматически. Вот что происходит:

λΠ> the (Fin 6) (natToFin 2) 
When elaborating argument p to function mod2.natToFin: 
     Can't solve goal 
       LT (fromInteger 2) (fromInteger 6)

Есть ли способ исправить это?

источник

2014-11-16 23:01:03

Доказать So (0 < m) -> (п ** т = S п)

ответ

Смежные вопросы