Jak Agda określa typ jest niemożliwa

Question

Więc staram się zrozumieć, dlaczego ten kod daje żółte podświetlenie wokół()

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

somef : sometype [] → ⊥ 
somef() 

Ale to nie

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

somef : sometype [] → ⊥ 
somef() 

Oba wydają się tak, że sometype [] jest puste, ale Agda nie potrafi wykreślić pierwszego? Czemu? Jaki jest kod tego działania? Czy mogę zdefiniować coś w taki sposób, aby pierwsza definicja działała?

Answer 1

Agda nie może zakładać niczego na temat dowolnych funkcji, takich jak ++. Załóżmy, że mamy zdefiniowane ++ następujący sposób:

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

w tym przypadku sometype [] → ⊥ nie jest do udowodnienia, a przyjmując () absurdalny wzór byłby błąd.

W drugim przykładzie indeksmusi mieć postać n ∷ (l1 ++ l2), która jest wyrażeniem konstruktora, ponieważ _∷_ jest konstruktorem list. Agda może bezpiecznie wnioskować, że stworzona lista nie może być równa []. Ogólnie rzecz biorąc, różne konstruktory mogą być postrzegane jako niemożliwe do ujednolicenia.

To, co Agda może zrobić z aplikacjami funkcyjnymi, zmniejsza je w miarę możliwości. W niektórych przypadkach redukcja daje wyrażenia konstruktorów, w innych przypadkach nie, i musimy napisać dodatkowe dowody.

Aby udowodnić, że sometype [] → ⊥, powinniśmy najpierw wykonać pewne uogólnienie. Nie można dopasować wzorca na wartość sometype [] (ze względu na indeks ++ w indeksie typu), ale możemy dopasować na sometype xs dla niektórych abstrakcyjnych xs. Tak więc nasz lemat mówi:

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

Innymi słowy, ∀ xs → sometype xs → xs ≢ []. Możemy wyprowadzić pożądany dowód z tego:

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