So I'm trying to understand why this code gives yellow highlighting around the ()
data sometype : List ℕ → Set where
constr : (l1 l2 : List ℕ)(n : ℕ) → sometype (l1 ++ (n ∷ l2))
somef : sometype [] → ⊥
somef ()
But this does not
data sometype : List ℕ → Set where
constr : (l1 l2 : List ℕ)(n : ℕ) → sometype (n ∷ (l1 ++ l2))
somef : sometype [] → ⊥
somef ()
Both seem to such that sometype [] is empty, but Agda can't figure the first one out? Why? What is the code behind this doing? And Can I define somef in a way to make the first definition work?
Agda can't assume anything about arbitrary functions like ++
. Suppose we defined ++
the following way:
_++_ : {A : Set} → List A → List A → List A
xs ++ ys = []
In this case, sometype [] → ⊥
isn't provable, and accepting the ()
absurd pattern would be an error.
In your second example, the index of sometype
must be of the form n ∷ (l1 ++ l2)
, which is a constructor expression, since _∷_
is a list constructor. Agda can safely infer that a _∷_
-constructed list can never be equal to []
. In general, distinct constructors can be seen as impossible to unify.
What Agda can do with function applications is reducing them as far as possible. In some cases reduction yields constructor expressions, in other cases it doesn't, and we need to write additional proofs.
To prove sometype [] → ⊥
, we should do some generalization first. We can't pattern match on a value of sometype []
(because of the ++
in the type index), but we can match on sometype xs
for some abstracted xs
. So, our lemma says the following:
someF' : ∀ xs → sometype xs → xs ≡ [] → ⊥
someF' .(n ∷ l2) (constr [] l2 n) ()
someF' .(n' ∷ l1 ++ n ∷ l2) (constr (n' ∷ l1) l2 n) ()
In other words, ∀ xs → sometype xs → xs ≢ []
. We can derive the desired proof from this:
someF : sometype [] → ⊥
someF p = someF' [] p refl
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With