Доказательство "слабости" не меняет значение числа - PullRequest
Новая
       12

Доказательство "слабости" не меняет значение числа

0 голосов
/ 16 мая 2018

Допустим, мы хотим доказать, что ослабление верхней границы Data.Fin не меняет значение числа.Интуитивно понятный способ заявить это: 

weakenEq : (num : Fin n) -> num = weaken num

Давайте теперь сгенерируем определенное ... Держись!Давайте немного подумаем об этом утверждении.num и weaken num имеют разные типы .Можем ли мы заявить о равенстве в этом случае?

Документация по = предполагает, что мы можем попытаться сделать это, но мы могли бы вместо этого использовать ~=~.Ну, во всяком случае, давайте продолжим и создадим определение и разделение регистра, в результате чего 

weakenEq : (num : Fin n) -> num = weaken num
weakenEq FZ = ?weakenEq_rhs_1
weakenEq (FS x) = ?weakenEq_rhs_2

Цель в дыре weakenEq_rhs_1 равна FZ = FZ, что все еще имеет смысл с точки зрения ценности,Таким образом, мы оптимистично заменим дыру на Refl, но потерпим неудачу: 

When checking right hand side of weakenEq with expected type
        FZ = weaken FZ

Unifying k and S k would lead to infinite value

Несколько загадочное сообщение об ошибке, поэтому нам интересно, действительно ли это связано с различными типами.

В любом случае, давайте попробуем еще раз, но теперь с ~=~ вместо =.К сожалению, ошибка все та же.

Итак, как можно заявить и доказать, что weaken x не меняет значение x?Это действительно имеет смысл?Что мне делать, если это часть большого доказательства, где я могу захотеть rewrite a Vect n (Fin k) с Vect n (Fin (S k)), полученным map ping weaken по сравнению с исходным вектором?

Ответы [ 2 ]

0 голосов
/ 17 мая 2018

К вашей второй проблеме / комментарию Маркуса о map (Data.Fin.finToNat) v = map (Data.Fin.finToNat . Data.Fin.weaken) v: 

vectorWeakenEq : (v: Vect n (Fin k)) -> 
                 map Fin.finToNat v = map (Fin.finToNat . Fin.weaken) v
vectorWeakenEq [] = Refl
vectorWeakenEq (x :: xs) =
  rewrite sym $ weakenEq x in
  cong {f=(::) (finToNat x)} (vectorWeakenEq xs)

И чтобы понять, почему num = weaken num не сработает, давайте взглянем на контрпример: 

getSize : Fin n -> Nat
getSize _ {n} = n

Теперь с x : Fin n, getSize x = n != (n + 1) = getSize (weaken x).Этого не произойдет с функциями, которые зависят только от конструкторов, таких как finToNat.Таким образом, вы должны ограничиться этим и доказать, что они так себя ведут.

0 голосов
/ 17 мая 2018

Если вы действительно хотите доказать, что значение Fin n не изменяется после применения ослабленной функции, вам необходимо доказать равенство этих значений: 

weakenEq: (num: Fin n) -> finToNat num = finToNat $ weaken num
weakenEq FZ     = Refl
weakenEq (FS x) = cong $ weakenEq x
...