<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&#39;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&#39;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⟩ 𝑼⟨&lt;⟩}<br>  {Key : Set 𝑼⟨Key⟩} (Value : Key → Set 𝑼⟨Value⟩)<br>  {_&lt;_ : Rel Key 𝑼⟨&lt;⟩}<br>  (isStrictTotalOrder : IsStrictTotalOrder _≡_ _&lt;_)<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 _&lt;⁺_<br><br>_&lt;⁺_ : Key⁺ → Key⁺ → Set 𝑼⟨&lt;⟩<br>⊥⁺    &lt;⁺ [ _ ] = Lift ⊤<br>⊥⁺    &lt;⁺ ⊤⁺    = Lift ⊤<br>[ x ] &lt;⁺ [ y ] = x &lt; y<br>[ _ ] &lt;⁺ ⊤⁺    = Lift ⊤<br>_     &lt;⁺ _     = Lift ⊥<br>  <br>infixr 6 _∷_<br>data OrderedList (l u : Key⁺) : Set (𝑼⟨Key⟩ ⊔ 𝑼⟨&lt;⟩) where<br>  [] : {{l&lt;u : l &lt;⁺ u}} → OrderedList l u<br>  _∷_ : ∀<br>         (k : Key)<br>         {{_ : l &lt;⁺ [ k ]}}<br>         (ku : OrderedList [ k ] u) →<br>         OrderedList l u<br><br>data _∈_ {l u} (k : Key) : OrderedList l u → Set (𝑼⟨&lt;⟩ ⊔ 𝑼⟨Key⟩) where<br>  here : ∀ {ks : OrderedList [ k ] u} {{p : l &lt;⁺ [ k ] }} → k ∈ (k ∷ ks)<br>  succ : ∀ {k&#39; : Key} {ks : OrderedList [ k&#39; ] u} {{p : l &lt;⁺ [ k&#39; ] }} → k ∈ ks → k ∈ (k&#39; ∷ ks)<br><br><br>{- The first of three attempts at the lemma. -}<br>lem1 : ∀ {l u} (y : OrderedList l u) (l&lt;u : l &lt;⁺ 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&lt;u_72 : _l_70 Value isStrictTotalOrder y l&lt;u k &lt;⁺<br>  _u_71 Value isStrictTotalOrder y l&lt;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&lt;u ∀k→k∈y→k∈[] = {!!}<br>lem1 (k ∷ y) l&lt;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&#39;m not clear on why. <br>-}<br>lem2 : ∀ {l u} (y : OrderedList l u) (l&lt;u : l &lt;⁺ u) → (x : ∀ (k : Key) → (k ∈ y → _∈_ {l} k [])) → [] ≡ y<br>lem2 {l} {u} [] l&lt;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&lt;u ∀k→k∈y→k∈[] ≡<br>        _x_106 Value isStrictTotalOrder l&lt;u ∀k→k∈y→k∈[]<br>  ————————————————————————————————————————————————————————————<br>  ∀k→k∈y→k∈[]<br>           : (k : Key) → k ∈ [] → k ∈ []<br>  l&lt;u      : l &lt;⁺ u<br>  .l&lt;u     : l &lt;⁺ u<br>  u        : Key⁺<br>  l        : Key⁺<br>  isStrictTotalOrder<br>           : IsStrictTotalOrder _≡_ _&lt;_<br>  _&lt;_      : Rel Key 𝑼⟨&lt;⟩<br>  Value    : Key → Set 𝑼⟨Value⟩<br>  Key      : Set 𝑼⟨Key⟩<br>  𝑼⟨&lt;⟩     : Level.Level<br>  𝑼⟨Value⟩ : Level.Level<br>  𝑼⟨Key⟩   : Level.Level<br><br>I&#39;m unable to refine by typing C-c C-r, but I have no explanation (yet) for why it won&#39;t refine. Agda simply says &quot;cannot refine&quot;. QUESTION: Should I be able to tell why it won&#39;t refine given the information above?<br><br>Here&#39;s the error message if I (by brute force) replace the hole with refl:<br> <br>  l&lt;u != .l&lt;u of type l &lt;⁺ 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&#39;m wrong, but couldn&#39;t (shouldn&#39;t?) Agda have divulged this business about l&lt;u when I hit C-c C-. ?<br><br>It turns out that .l&lt;u is an implicit argument to the first explicit argument ([] or y). COMPLAINT: It isn&#39;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&#39;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&#39;m confused about the meaning of this error message. It sounds like Agda is saying that, while l&lt;u and .l&lt;u are both of the same type, they aren&#39;t (somehow) &quot;the same&quot;. 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&lt;u ∀k→k∈y→k∈[] = {!!}<br><br><br>{- I&#39;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&lt;⁺u&#39; : ∀ {l u} (y : OrderedList l u) → l &lt;⁺ u<br>l&lt;⁺u&#39; [] = {!!} -- COMPLAINT: C-c C-a yields the syntactically incorrect .l&lt;u<br>l&lt;⁺u&#39; (k ∷ y) = {!!}<br><br>l&lt;⁺u : ∀ {l u} (y : OrderedList l u) → l &lt;⁺ u<br>l&lt;⁺u ([] {{l&lt;u}}) = l&lt;u<br>l&lt;⁺u (_∷_ k {{l&lt;⁺[k]}} y) = {!!} -- exercise for the reader<br><br>trans⁺ : ∀ l {m u} → l &lt;⁺ m → m &lt;⁺ u → l &lt;⁺ u<br>trans⁺ = {!!} -- exercise for the reader<br><br>{- Here&#39;s my last try at the lemma. -}<br>lem3 : ∀ {l u} (y : OrderedList l u) → (x : ∀ (k : Key) (l&#39; u&#39; : Key⁺) (l&#39;&lt;u&#39; : l&#39; &lt;⁺ u&#39;) → (k ∈ y → _∈_ {l&#39;} {u&#39;} k ([] {{l&#39;&lt;u&#39;}}))) → [] {{l&lt;⁺u y}} ≡ y<br>lem3 {l} {u} ([] {{l&lt;u}}) ∀k→k∈y→k∈[] = {!refl!}<br>{-<br>Here&#39;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&#39; u&#39; : Key⁺) (l&#39;&lt;u&#39; : l&#39; &lt;⁺ u&#39;) → k ∈ [] → k ∈ []<br>  l&lt;u      : l &lt;⁺ u<br>  u        : Key⁺<br>  l        : Key⁺<br>  isStrictTotalOrder<br>           : IsStrictTotalOrder _≡_ _&lt;_<br>  _&lt;_      : Rel Key 𝑼⟨&lt;⟩<br>  Value    : Key → Set 𝑼⟨Value⟩<br>  Key      : Set 𝑼⟨Key⟩<br>  𝑼⟨&lt;⟩     : 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&#39;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>