<div dir="ltr">The following can also be found at <a href="http://lpaste.net/144919">http://lpaste.net/144919</a>.<br><div><br>{- In the below, I define an OrderedList and attempt to prove a lemma: that if every element in such a list is also in the empty list, then the list in question must be the empty list. I don't succeed, but I do come up with a number of QUESTIONs and COMPLAINTs. I hope my story will help inspire someone to write-up a comprehensive explanation of error messages in Agda. Or (better) to modify Agda so that error messages don't require so much explanation! :) I suspect that Issue 771 [<a href="https://github.com/agda/agda/issues/771">https://github.com/agda/agda/issues/771</a>] might pertain to some of my complaints. -}<br><br>open import Relation.Binary<br>open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)<br><br>module Enagda05-need-more-help-from-agda<br> {𝑼⟨Key⟩ 𝑼⟨Value⟩ 𝑼⟨<⟩}<br> {Key : Set 𝑼⟨Key⟩} (Value : Key → Set 𝑼⟨Value⟩)<br> {_<_ : Rel Key 𝑼⟨<⟩}<br> (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)<br> where<br><br>open import Data.Unit using (⊤)<br>open import Data.Empty using (⊥)<br>open import Level using (_⊔_; Lift)<br><br>data Key⁺ : Set 𝑼⟨Key⟩ where<br> ⊥⁺ ⊤⁺ : Key⁺<br> [_] : (k : Key) → Key⁺<br> <br>infix 4 _<⁺_<br><br>_<⁺_ : Key⁺ → Key⁺ → Set 𝑼⟨<⟩<br>⊥⁺ <⁺ [ _ ] = Lift ⊤<br>⊥⁺ <⁺ ⊤⁺ = Lift ⊤<br>[ x ] <⁺ [ y ] = x < y<br>[ _ ] <⁺ ⊤⁺ = Lift ⊤<br>_ <⁺ _ = Lift ⊥<br> <br>infixr 6 _∷_<br>data OrderedList (l u : Key⁺) : Set (𝑼⟨Key⟩ ⊔ 𝑼⟨<⟩) where<br> [] : {{l<u : l <⁺ u}} → OrderedList l u<br> _∷_ : ∀<br> (k : Key)<br> {{_ : l <⁺ [ k ]}}<br> (ku : OrderedList [ k ] u) →<br> OrderedList l u<br><br>data _∈_ {l u} (k : Key) : OrderedList l u → Set (𝑼⟨<⟩ ⊔ 𝑼⟨Key⟩) where<br> here : ∀ {ks : OrderedList [ k ] u} {{p : l <⁺ [ k ] }} → k ∈ (k ∷ ks)<br> succ : ∀ {k' : Key} {ks : OrderedList [ k' ] u} {{p : l <⁺ [ k' ] }} → k ∈ ks → k ∈ (k' ∷ ks)<br><br><br>{- The first of three attempts at the lemma. -}<br>lem1 : ∀ {l u} (y : OrderedList l u) (l<u : l <⁺ u) → (x : ∀ (k : Key) → (k ∈ y → _∈_ k [])) → [] ≡ y<br>{- <br>The yellow highlights in the above type specification are associated with error messages like this:<br><br> _l_70 : Key⁺ [ at Enagda05-need-more-help-from-agda.agda:41,83-86 ]<br> _u_71 : Key⁺ [ at Enagda05-need-more-help-from-agda.agda:41,83-86 ]<br> _l<u_72 : _l_70 Value isStrictTotalOrder y l<u k <⁺<br> _u_71 Value isStrictTotalOrder y l<u k [ at Enagda05-need-more-help-from-agda.agda:41,89-91 ]<br><br>QUESTION: What exactly do these errors mean?<br>-}<br>lem1 {l} {u} [] l<u ∀k→k∈y→k∈[] = {!!}<br>lem1 (k ∷ y) l<u ∀k→k∈y→k∈[] = {!!}<br><br>{- <br>Moving on, in lem2, I avoid the errors mentioned in lem1 by adding a specification of just one of the implicit arguments, {l}. Somehow this works to remove the yellow highlighting, but I'm not clear on why. <br>-}<br>lem2 : ∀ {l u} (y : OrderedList l u) (l<u : l <⁺ u) → (x : ∀ (k : Key) → (k ∈ y → _∈_ {l} k [])) → [] ≡ y<br>lem2 {l} {u} [] l<u ∀k→k∈y→k∈[] = {!refl!}<br>{- <br>Executing C-c C-. on the hole shows:<br><br> Goal: [] ≡ []<br> Have: _x_106 Value isStrictTotalOrder l<u ∀k→k∈y→k∈[] ≡<br> _x_106 Value isStrictTotalOrder l<u ∀k→k∈y→k∈[]<br> ————————————————————————————————————————————————————————————<br> ∀k→k∈y→k∈[]<br> : (k : Key) → k ∈ [] → k ∈ []<br> l<u : l <⁺ u<br> .l<u : l <⁺ u<br> u : Key⁺<br> l : Key⁺<br> isStrictTotalOrder<br> : IsStrictTotalOrder _≡_ _<_<br> _<_ : Rel Key 𝑼⟨<⟩<br> Value : Key → Set 𝑼⟨Value⟩<br> Key : Set 𝑼⟨Key⟩<br> 𝑼⟨<⟩ : Level.Level<br> 𝑼⟨Value⟩ : Level.Level<br> 𝑼⟨Key⟩ : Level.Level<br><br>I'm unable to refine by typing C-c C-r, but I have no explanation (yet) for why it won't refine. Agda simply says "cannot refine". QUESTION: Should I be able to tell why it won't refine given the information above?<br><br>Here's the error message if I (by brute force) replace the hole with refl:<br> <br> l<u != .l<u of type l <⁺ u<br> when checking that the expression refl has type [] ≡ []<br><br>It looks to me like Agda has now given me some more clues as to why it had refused to refine. COMPLAINT: Please correct me if I'm wrong, but couldn't (shouldn't?) Agda have divulged this business about l<u when I hit C-c C-. ?<br><br>It turns out that .l<u is an implicit argument to the first explicit argument ([] or y). COMPLAINT: It isn't always obvious where dotted variables are coming from, so I wish Agda would tell me this. It may be asking too much to have a semi-automated way of bringing these hidden variables into scope. I'm just saying that there needs to be more clues given as to how the programmer might bring the given variable into scope.<br><br>Furthermore, I'm confused about the meaning of this error message. It sounds like Agda is saying that, while l<u and .l<u are both of the same type, they aren't (somehow) "the same". Okay, but so what? Why should that have something to do with checking that refl has type [] ≡ [] ? QUESTION: How am I to interpret the error message?<br>-}<br>lem2 (k ∷ y) l<u ∀k→k∈y→k∈[] = {!!}<br><br><br>{- I'm still not ready to give up the fight. Inspired by the meager clue in the previous error message, I come up with a reformulatation the lemma. As it turns out, I need to define a function that gives a proof of the bounds for an OrderedList. -}<br><br>-- This one fails comically.<br>l<⁺u' : ∀ {l u} (y : OrderedList l u) → l <⁺ u<br>l<⁺u' [] = {!!} -- COMPLAINT: C-c C-a yields the syntactically incorrect .l<u<br>l<⁺u' (k ∷ y) = {!!}<br><br>l<⁺u : ∀ {l u} (y : OrderedList l u) → l <⁺ u<br>l<⁺u ([] {{l<u}}) = l<u<br>l<⁺u (_∷_ k {{l<⁺[k]}} y) = {!!} -- exercise for the reader<br><br>trans⁺ : ∀ l {m u} → l <⁺ m → m <⁺ u → l <⁺ u<br>trans⁺ = {!!} -- exercise for the reader<br><br>{- Here's my last try at the lemma. -}<br>lem3 : ∀ {l u} (y : OrderedList l u) → (x : ∀ (k : Key) (l' u' : Key⁺) (l'<u' : l' <⁺ u') → (k ∈ y → _∈_ {l'} {u'} k ([] {{l'<u'}}))) → [] {{l<⁺u y}} ≡ y<br>lem3 {l} {u} ([] {{l<u}}) ∀k→k∈y→k∈[] = {!refl!}<br>{-<br>Here's the result of C-c C-. this time:<br><br> Goal: [] ≡ []<br> Have: _x_150 Value isStrictTotalOrder ∀k→k∈y→k∈[] ≡<br> _x_150 Value isStrictTotalOrder ∀k→k∈y→k∈[]<br> ————————————————————————————————————————————————————————————<br> ∀k→k∈y→k∈[]<br> : (k : Key) (l' u' : Key⁺) (l'<u' : l' <⁺ u') → k ∈ [] → k ∈ []<br> l<u : l <⁺ u<br> u : Key⁺<br> l : Key⁺<br> isStrictTotalOrder<br> : IsStrictTotalOrder _≡_ _<_<br> _<_ : Rel Key 𝑼⟨<⟩<br> Value : Key → Set 𝑼⟨Value⟩<br> Key : Set 𝑼⟨Key⟩<br> 𝑼⟨<⟩ : Level.Level<br> 𝑼⟨Value⟩ : Level.Level<br> 𝑼⟨Key⟩ : Level.Level<br><br>This looks pretty similar to what we saw in lem2. It turns out that the refl in the hole will refine, but, weirdly, the result is a yellow-highlighted error:<br><br>_139 : [] ≡ [] [ at Enagda05-need-more-help-from-agda.agda:114,42-46 ]<br>_140 : [] ≡ [] [ at Enagda05-need-more-help-from-agda.agda:114,42-46 ]<br><br>I suspect the meaning of the above error is that there's some unification problem, but I feel like Agda could be telling me more. QUESTION: What does it mean?<br>-}<br>lem3 (k ∷ y) ∀k→k∈y→k∈[] = {!!}<br><br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
</div></div>