Полное доказательство при выполнении индукции по одному аргументу конструктора - PullRequest
Новая
       6

Полное доказательство при выполнении индукции по одному аргументу конструктора

3 голосов
/ 16 января 2020

У нас есть следующий тип с одним конструктором: 

-- IsTwice n is inhabited if n = k + k for some k
data IsTwice : Nat -> Type where
  Twice : (k : Nat) -> IsTwice (k + k)

Я пытаюсь определить функцию на IsTwice n для любого n, но с помощью индукции для аргумента k конструктору Twice, а не n аргументу IsTwice. Моя проблема в том, что я не могу заставить Идриса принять мое определение как total.

Вот конкретный c пример. Допустим, у нас есть второй тип: 

data IsEven : Nat -> Type where
  IsZero : IsEven 0
  PlusTwo : (n : Nat) -> IsEven n -> IsEven (2 + n)

Я бы хотел доказать, что IsTwice n подразумевает IsEven n. Моя интуиция такова: мы знаем, что любое значение (свидетель) типа IsTwice n имеет форму Twice k для некоторого k, поэтому этого должно быть достаточно, чтобы индуктивно показать, что

  • Twice Z : IsTwice Z подразумевает IsEven Z и
  • , если Twice k : IsTwice (k+k) подразумевает IsEven (k+k),
    , тогда Twice (S k) : IsTwice ((S k) + (S k)) подразумевает IsEven ((S k) + (S k)). 
total isTwiceImpliesIsEven : IsTwice n -> IsEven n
isTwiceImpliesIsEven (Twice Z) = IsZero
isTwiceImpliesIsEven (Twice (S k))
  = let twoKIsEven = isTwiceImpliesIsEven (Twice k) in
    let result = PlusTwo (plus k k) twoKIsEven in
    rewrite sym (plusSuccRightSucc k k) in result

Это работает за исключением тот факт, что Идрис не уверен, что доказательство является total: 

Main.isTwiceImpliesIsEven is possibly not total due to recursive path Main.isTwiceImpliesIsEven --> Main.isTwiceImpliesIsEven

Как я могу сделать это total?

1 Ответ

5 голосов
/ 17 января 2020

Даже если k меньше, чем S k, средство проверки совокупности не может определить, что k + k меньше, чем S k + S k, поскольку оно уменьшится только до S (k + S k). Тем не менее, это может помочь с sizeAccessible (k + k) в Prelude.WellFounded. При каждом рекурсивном вызове вы предоставляете LTE доказательство k + k всегда становится меньше. 

LTERightSucc : (k:Nat) -> LTE k (S k)
LTERightSucc Z = LTEZero
LTERightSucc (S k) = LTESucc $ LTERightSucc k

total
isTwiceImpliesIsEven : IsTwice n -> IsEven n
isTwiceImpliesIsEven (Twice k) with (sizeAccessible (k + k))
  isTwiceImpliesIsEven (Twice Z) | acc = IsZero
  isTwiceImpliesIsEven (Twice (S k)) | (Access rec) =
    let twoKIsEven = (isTwiceImpliesIsEven (Twice k) |
      rec _ (LTESucc $ rewrite plusCommutative k (S k) in LTERightSucc (k+k))) in
        let result = PlusTwo (plus k k) twoKIsEven in
    rewrite sym (plusSuccRightSucc k k) in result
...