<div dir="ltr">The full code is pasted here: <a href="http://lpaste.net/139721">http://lpaste.net/139721</a><br><div><br>{- This uses Agda and agda-stdlib 2.4.2.3 -}<br><br>{- In the below, lemJoinˡ⁺IsCorrect, I am trying to prove that if a key is in the left-hand tree given to Data.AVL.Indexed.joinˡ⁺ then it will still be present in the joined tree. Unforunately, I have only been successful in about half of the cases. Would someone be so kind as to clue me in as to what might be going wrong? -}<br><br>open import Relation.Binary<br>open import Relation.Binary.PropositionalEquality as P using (_≡_)<br><br>module Enagda03<br> {k v ℓ}<br> {Key : Set k} (Value : Key → Set v)<br> {_<_ : Rel Key ℓ}<br> (isStrictTotalOrder : IsStrictTotalOrder P._≡_ _<_) where<br><br>open import Data.Product<br>open import Level using (_⊔_)<br>open import Data.AVL Value isStrictTotalOrder using (KV; module Extended-key; module Height-invariants; module Indexed)<br>open Extended-key<br>open Height-invariants<br>open Indexed<br><br>open IsStrictTotalOrder isStrictTotalOrder<br><br>data _∈_ {lb ub} (key : Key) : ∀ {n} → Tree lb ub n → Set (k ⊔ v ⊔ ℓ) where<br> here : ∀ {hˡ hʳ h v}<br> {lk : Tree lb [ key ] hˡ}<br> {ku : Tree [ key ] ub hʳ}<br> {bal : hˡ ∼ hʳ ⊔ h} →<br> key ∈ node (key , v) lk ku bal<br> left : ∀ {hˡ hʳ h k′} {v′ : Value k′}<br> {lk′ : Tree lb [ k′ ] hˡ}<br> {k′u : Tree [ k′ ] ub hʳ}<br> {bal : hˡ ∼ hʳ ⊔ h} →<br> key ∈ lk′ →<br> key ∈ node (k′ , v′) lk′ k′u bal<br> right : ∀ {hˡ hʳ h k′} {v′ : Value k′}<br> {lk′ : Tree lb [ k′ ] hˡ}<br> {k′u : Tree [ k′ ] ub hʳ}<br> {bal : hˡ ∼ hʳ ⊔ h} →<br> key ∈ k′u →<br> key ∈ node (k′ , v′) lk′ k′u bal<br><br>open import Data.Nat.Base<br><br>lemJoinˡ⁺IsCorrect : ∀ { l r hˡ hʳ h }<br> { k′ : Key }<br> { v′ : Value k′ }<br> ( tˡ⁺ : ∃ λ i → Tree l [ k′ ] ( i ⊕ hˡ ) )<br> ( tʳ : Tree [ k′ ] r hʳ )<br> ( bal : hˡ ∼ hʳ ⊔ h )<br> { key : Key }<br> ( k∈tˡ : key ∈ proj₂ tˡ⁺ ) →<br> key ∈ proj₂ ( joinˡ⁺ ( k′ , v′ ) tˡ⁺ tʳ bal )<br>lemJoinˡ⁺IsCorrect ( 1# , node _ _ ( node _ _ _ _ ) ∼+ ) _ ∼- here = left here<br>lemJoinˡ⁺IsCorrect ( 1# , node _ _ ( node _ _ _ _ ) ∼+ ) _ ∼- ( left k∈tˡ ) = left ( left k∈tˡ )<br>lemJoinˡ⁺IsCorrect ( 1# , node _ _ ( node _ _ _ _ ) ∼+ ) _ ∼- ( right here ) = here<br>lemJoinˡ⁺IsCorrect ( 1# , node _ _ ( node _ _ _ _ ) ∼+ ) _ ∼- ( right ( left k∈tʳˡ ) ) = left ( right k∈tʳˡ )<br>lemJoinˡ⁺IsCorrect ( 1# , node _ _ ( node _ _ _ _ ) ∼+ ) _ ∼- ( right ( right k∈tʳʳ ) ) = right ( left k∈tʳʳ )<br>{- This is the first case that doesn't work. -}<br>lemJoinˡ⁺IsCorrect ( 1# , node _ _ _ ∼- ) _ ∼- here = {!here!}<br>{- <br> If I fill-out the term as follows <br><br> lemJoinˡ⁺IsCorrect ( 1# , node _ _ _ ∼- ) _ ∼- here = here<br><br> then I get the following error:<br><br> suc (_h_217 Value isStrictTotalOrder .k .lk .ku .tʳ)<br> !=<br> proj₁ (joinˡ⁺ (.k′ , .v′) (1# , node .k .lk .ku ∼-) .tʳ ∼-) ⊕ (1 + suc .hʳ)<br> of type ℕ<br> when checking that the expression here has type<br> proj₁ .k ∈ proj₂ (joinˡ⁺ (.k′ , .v′) (1# , node .k .lk .ku ∼-) .tʳ ∼-)<br><br> Thinking it would help, I tried to get around the above error by specifying the implicit variable h:<br><br> lemJoinˡ⁺IsCorrect { hʳ = hʳ } ( 1# , node _ _ _ ∼- ) _ ∼- here = here { h = suc hʳ }<br><br> But that just results in a different error:<br><br> suc (suc hʳ) !=<br> proj₁ (joinˡ⁺ (.k′ , .v′) (1# , node .k .lk .ku ∼-) .tʳ ∼-) ⊕ (1 + suc hʳ)<br> of type ℕ<br> when checking that the expression here {h = suc hʳ} has type<br> proj₁ .k ∈ proj₂ (joinˡ⁺ (.k′ , .v′) (1# , node .k .lk .ku ∼-) .tʳ ∼-)<br><br> Notice that, from the definition of joinˡ⁺, the first and second lines in the above-reported error are actually equivalent. So, what's going on? Is it not "eta reducing"? And how would I get it to reduce?<br>-}<br>lemJoinˡ⁺IsCorrect ( 1# , node _ _ _ ∼- ) _ ∼- ( left k∈tˡˡ ) = {!left k∈tˡˡ!}<br>lemJoinˡ⁺IsCorrect ( 1# , node _ _ _ ∼- ) _ ∼- ( right k∈tˡʳ ) = {!right ( left ( k∈tˡʳ ) )!}<br>lemJoinˡ⁺IsCorrect ( 1# , node _ _ _ ∼0 ) _ ∼- here = {!here!}<br>lemJoinˡ⁺IsCorrect ( 1# , node _ _ _ ∼0 ) _ ∼- ( left k∈tˡˡ ) = {!left k∈tˡˡ!}<br>lemJoinˡ⁺IsCorrect ( 1# , node _ _ _ ∼0 ) _ ∼- ( right k∈tˡʳ ) = {!right ( left ( k∈tˡʳ ) )!}<br>lemJoinˡ⁺IsCorrect ( 1# , _ ) _ ∼0 k∈tˡ = {!left k∈tˡ!}<br>lemJoinˡ⁺IsCorrect ( 1# , _ ) _ ∼+ k∈tˡ = {!left k∈tˡ!}<br>lemJoinˡ⁺IsCorrect ( 0# , _ ) _ _ k∈tˡ = left k∈tˡ<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>