Как Agda определяет тип невозможно

Question

Так что я пытаюсь понять, почему этот код дает желтую подсветку вокруг()

data sometype : List ℕ → Set where 
    constr : (l1 l2 : List ℕ)(n : ℕ) → sometype (l1 ++ (n ∷ l2)) 

somef : sometype [] → ⊥ 
somef() 

Но это не

data sometype : List ℕ → Set where 
    constr : (l1 l2 : List ℕ)(n : ℕ) → sometype (n ∷ (l1 ++ l2)) 

somef : sometype [] → ⊥ 
somef() 

И, кажется, таким образом, что sometype [] пуст, но Agda не может определить первый из них? Зачем? Что это за код? Могу ли я определить somef, чтобы сделать работу над первым определением?

Answer 1

Agda ничего не может принять за произвольные функции, такие как ++. Предположим, что мы определили ++ следующим образом:

_++_ : {A : Set} → List A → List A → List A 
xs ++ ys = [] 

В этом случае sometype [] → ⊥ не доказуемо, и принимая () абсурдную картину было бы ошибкой.

В вашем втором примере индекс sometype должен иметь форму n ∷ (l1 ++ l2), которая является выражением конструктора, поскольку _∷_ является конструктором списка. Agda может смело заключить, что список _∷_ не может быть равен []. В целом, различные конструкторы можно рассматривать как невозможные для унификации.

Что может сделать Agda с приложениями функций, это как можно меньше. В некоторых случаях сокращение дает выражения конструктора, в других случаях это не так, и нам нужно написать дополнительные доказательства.

Чтобы доказать sometype [] → ⊥, мы должны сначала сделать обобщение. Мы не можем сопоставлять соответствие по значению sometype [] (из-за ++ в индексе типа), но мы можем сопоставить sometype xs для некоторых абстрагированных xs. Итак, наша лемма говорит следующее:

someF' : ∀ xs → sometype xs → xs ≡ [] → ⊥ 
someF' .(n ∷ l2)   (constr [] l2 n)() 
someF' .(n' ∷ l1 ++ n ∷ l2) (constr (n' ∷ l1) l2 n)() 

Другими словами, ∀ xs → sometype xs → xs ≢ []. Мы можем получить требуемое доказательство из этого:

someF : sometype [] → ⊥ 
someF p = someF' [] p refl