Comment Agda détermine un type est impossible

Question

Je suis en train de comprendre pourquoi ce code donne la coloration jaune autour du()

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

somef : sometype [] → ⊥ 
somef() 

Mais cela ne

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

somef : sometype [] → ⊥ 
somef() 

Les deux semblent tels que Quelque chose [] est vide, mais Agda n'arrive pas à comprendre le premier? Pourquoi? Quel est le code derrière cela? Puis-je définir somef de manière à faire fonctionner la première définition?

Answer 1

Agda ne peut pas supposer quoi que ce soit à propos de fonctions arbitraires comme ++. Supposons que nous avons défini ++ la manière suivante:

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

Dans ce cas, sometype [] → ⊥ est pas prouvable, et d'accepter le modèle absurde () serait une erreur. Dans votre second exemple, l'index de sometype doit être de la forme n ∷ (l1 ++ l2), qui est une expression de constructeur, car _∷_ est un constructeur de liste. Agda peut sans risque déduire qu'une liste _∷_-construite ne peut jamais être égale à []. En général, les constructeurs distincts peuvent être considérés comme impossibles à unifier. Ce que Agda peut faire avec les applications de fonction, c'est de les réduire autant que possible. Dans certains cas, la réduction donne des expressions constructeurs, dans d'autres cas ce n'est pas le cas, et nous devons écrire des preuves supplémentaires.

Pour prouver sometype [] → ⊥, nous devrions d'abord faire une généralisation. Nous ne pouvons pas faire correspondre pattern sur une valeur de sometype [] (en raison de l'++ dans l'index de type), mais nous pouvons correspondre sur sometype xs pour certains abstraite xs. Ainsi, notre lemme dit ce qui suit:

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

En d'autres termes, ∀ xs → sometype xs → xs ≢ []. Nous pouvons dériver la preuve désirée de ceci:

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