Come Agda determina un tipo è impossibile

Question

quindi sto cercando di capire il motivo per cui questo codice dà evidenziazione giallo attorno al()

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

somef : sometype [] → ⊥ 
somef() 

ma questo non

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

somef : sometype [] → ⊥ 
somef() 

Entrambi sembrano tali che Qualcosa [] è vuoto, ma Agda non riesce a capire il primo? Perché? Qual è il codice che sta dietro a questo? E posso definire un po 'in un modo per far funzionare la prima definizione?

Answer 1

Agda non può assumere nulla sulle funzioni arbitrarie come ++. Supponiamo abbiamo definito ++ seguente modo:

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

In questo caso, sometype [] → ⊥ non è dimostrabile, e accettando il modello assurdo () sarebbe un errore.

Nel secondo esempio, l'indice di sometype deve avere il formato n ∷ (l1 ++ l2), che è un'espressione di costruttore, poiché _∷_ è un costruttore di elenchi. Agda può tranquillamente dedurre che un elenco di _∷_ non può mai essere uguale a []. In generale, i diversi costruttori possono essere visti come impossibili da unificare.

Ciò che Agda può fare con le applicazioni di funzione li sta riducendo il più possibile. In alcuni casi la riduzione produce espressioni di costruzione, in altri casi no, e abbiamo bisogno di scrivere ulteriori prove.

Per provare sometype [] → ⊥, dovremmo prima fare qualche generalizzazione. Non è possibile eseguire lo schema di corrispondenza su un valore di ++ nell'indice di tipo, ma è possibile farlo corrispondere a sometype xs per alcuni numeri astratti xs. Quindi, il nostro lemma dice il seguente:

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

In altre parole, ∀ xs → sometype xs → xs ≢ []. Possiamo ricavare la prova desiderata da questo:

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