<html>
<head>
<meta content="text/html; charset=UTF-8" http-equiv="Content-Type">
</head>
<body text="#000000" bgcolor="#FFFFFF">
<div class="moz-cite-prefix">You will find an (operational)
explanation at the bottom of<br>
<a class="moz-txt-link-freetext" href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.PatternMatching">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.PatternMatching</a><br>
<br>
So order of arguments (and order of clauses) matter, because of
the semantics in terms of case trees.<br>
<br>
Jacques<br>
<br>
On 2015-08-10 05:49 , Martin Stone Davis wrote:<br>
</div>
<blockquote
cite="mid:CAH_qHWADzYTPFQuMHbaoYVbMvGT0uPs8C9OW8XVXci_XBcirEA@mail.gmail.com"
type="cite">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<div dir="ltr">(NB: Crossposted to <a moz-do-not-send="true"
href="http://stackoverflow.com/q/31913210/1312174">http://stackoverflow.com/q/31913210/1312174</a>)<br>
<div><br>
While trying to come up with a solution to a question I posed
[here](<a moz-do-not-send="true"
href="http://stackoverflow.com/questions/31900036/proof-help-in-agda-node-balancing-in-data-avl">http://stackoverflow.com/questions/31900036/proof-help-in-agda-node-balancing-in-data-avl</a>),
I discovered that the acceptability (by Agda) of a refl proof
depends in a strange way on the order of arguments of a
function that is called on one side of the equation. <br>
<br>
In code below, see how all but one of the bottom 4 theorems
are proved with refl. It's important to note that `join` and
`join'` differ only in the order of arguments.
Correspondingly, I would think that the `thm`s that invoke
them should be proved equivalently, but apparently that is not
so.<br>
<br>
Why the discrepancy? Does this represent a bug in Agda? How
would I prove the remaining theorem (`thm1`)?<br>
<br>
open import Data.Nat<br>
open import Data.Product<br>
<br>
-- Stolen (with little modification) from Data.AVL<br>
<br>
data ℕ₂ : Set where<br>
0# : ℕ₂<br>
1# : ℕ₂<br>
<br>
infixl 6 _⊕_<br>
<br>
_⊕_ : ℕ₂ → ℕ → ℕ<br>
0# ⊕ n = n<br>
1# ⊕ n = suc n<br>
<br>
infix 4 _∼_⊔_<br>
<br>
data _∼_⊔_ : ℕ → ℕ → ℕ → Set where<br>
∼+ : ∀ {n} → n ∼ suc n ⊔ suc n<br>
∼0 : ∀ {n} → n ∼ n ⊔ n<br>
∼- : ∀ {n} → suc n ∼ n ⊔ suc n<br>
<br>
max∼ : ∀ {i j m} → i ∼ j ⊔ m → m ∼ i ⊔ m<br>
max∼ ∼+ = ∼-<br>
max∼ ∼0 = ∼0<br>
max∼ ∼- = ∼0<br>
<br>
∼max : ∀ {i j m} → i ∼ j ⊔ m → j ∼ m ⊔ m<br>
∼max ∼+ = ∼0<br>
∼max ∼0 = ∼0<br>
∼max ∼- = ∼+<br>
<br>
-- for simplicity, this tree has no keys<br>
data Tree : ℕ → Set where<br>
leaf : Tree 0<br>
node : ∀ {l u h}<br>
(L : Tree l)<br>
(U : Tree u)<br>
(bal : l ∼ u ⊔ h) →<br>
Tree (suc h)<br>
<br>
-- similar to joinˡ⁺ from Data.AVL<br>
<br>
join : ∀ {hˡ hʳ h : ℕ} →<br>
(∃ λ i → Tree (i ⊕ hˡ)) →<br>
Tree hʳ →<br>
(bal : hˡ ∼ hʳ ⊔ h) →<br>
∃ λ i → Tree (i ⊕ (suc h))<br>
join (1# , node t₁<br>
(node t₃ t₅ bal)<br>
∼+) t₇ ∼- = (0# , node <br>
(node t₁ t₃ (max∼
bal))<br>
(node t₅ t₇ (∼max
bal))<br>
∼0)<br>
join (1# , node t₁ t₃ ∼-) t₅ ∼- = (0# , node t₁ (node t₃
t₅ ∼0) ∼0)<br>
join (1# , node t₁ t₃ ∼0) t₅ ∼- = (1# , node t₁ (node t₃
t₅ ∼-) ∼+)<br>
join (1# , t₁) t₃ ∼0 = (1# , node t₁ t₃ ∼-)<br>
join (1# , t₁) t₃ ∼+ = (0# , node t₁ t₃ ∼0)<br>
join (0# , t₁) t₃ bal = (0# , node t₁ t₃ bal)<br>
<br>
-- just like join but with "bal" earlier in the argument
list<br>
join' : ∀ {hˡ hʳ h : ℕ} →<br>
(bal : hˡ ∼ hʳ ⊔ h) →<br>
(∃ λ i → Tree (i ⊕ hˡ)) →<br>
Tree hʳ →<br>
∃ λ i → Tree (i ⊕ (suc h))<br>
join' ∼- (1# , node t₁<br>
(node t₃ t₅ bal)<br>
∼+) t₇ = (0# , node <br>
(node t₁ t₃ (max∼
bal))<br>
(node t₅ t₇ (∼max
bal))<br>
∼0)<br>
join' ∼- (1# , node t₁ t₃ ∼-) t₅ = (0# , node t₁ (node t₃
t₅ ∼0) ∼0)<br>
join' ∼- (1# , node t₁ t₃ ∼0) t₅ = (1# , node t₁ (node t₃
t₅ ∼-) ∼+)<br>
join' ∼0 (1# , t₁) t₃ = (1# , node t₁ t₃ ∼-)<br>
join' ∼+ (1# , t₁) t₃ = (0# , node t₁ t₃ ∼0)<br>
join' bal (0# , t₁) t₃ = (0# , node t₁ t₃ bal)<br>
<br>
open import Relation.Binary.PropositionalEquality<br>
<br>
thm0 : ∀ {h : ℕ} (tl : Tree h ) (tr : Tree (suc h))
→ join (0# , tl) tr ∼+ ≡ (0# , node tl tr ∼+)<br>
thm0 tl tr = refl<br>
<br>
thm1 : ∀ {h : ℕ} (tl : Tree (suc h)) (tr : Tree (suc h))
→ join (1# , tl) tr ∼+ ≡ (0# , node tl tr ∼0)<br>
thm1 tl tr = {!!} -- FIXME refl doesn't work here!<br>
<br>
thm0' : ∀ {h : ℕ} (tl : Tree h ) (tr : Tree (suc h))
→ join' ∼+ (0# , tl) tr ≡ (0# , node tl tr ∼+)<br>
thm0' tl tr = refl<br>
<br>
thm1' : ∀ {h : ℕ} (tl : Tree (suc h)) (tr : Tree (suc h))
→ join' ∼+ (1# , tl) tr ≡ (0# , node tl tr ∼0)<br>
thm1' tl tr = refl -- refl works fine here, and all I did
was switch the order of arguments to join(')<br>
<br>
If I try to prove `thm1` with refl, I get the following error:<br>
<br>
proj₁ (join (1# , tl) tr ∼+) != 0# of type ℕ₂<br>
when checking that the expression refl has type<br>
join (1# , tl) tr ∼+ ≡ (0# , node tl tr ∼0)<br>
<br>
NB: This is using Agda 2.4.2.3 and the stdlib of the same
version (pulled from github [here](<a moz-do-not-send="true"
href="https://github.com/agda/agda-stdlib/tree/2.4.2.3">https://github.com/agda/agda-stdlib/tree/2.4.2.3</a>).<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
moz-do-not-send="true" href="tel:3106993578" value="+13106993578"
target="_blank">(310)
699-3578</a><br>
Electronic
Mail: <a
moz-do-not-send="true"
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 moz-do-not-send="true"
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>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
</blockquote>
<br>
</body>
</html>