<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Hi Philippe, <br>
<br>
Indeed you cannot compare two values of arbitrary types for
equality.<br>
<br>
James' idea was to write a function that given two comparison
functions for the first and second projection <br>
of a pair, produces a comparison function for the pair as a whole.
<br>
<br>
The signature you wrote for _eq_ is correct<br>
and you should be able to implement, although its implementation
should take 4 parameters: `eq eqa eqb ab ab' = ?`<br>
Try putting a and a' in the hole on the RHS and pressing C-c C-C
to expand the cases. Now you can use eqa and eqb to compare<br>
the components of the pairs.<br>
<br>
On the use site, you know the type A at which you're comparing and
you can give a non-generic implementation of the two input
comparison functions,<br>
for example for Nat.<br>
<br>
Once you have an idea of how the implementation works in a
functional language, you can look at typeclasses in Agda to get a
definition that is a little<br>
easier to work with and does not require you to manually give the
comparison functions as parameters.<br>
<br>
Hope this helps,<br>
<br>
<br>
Arjen<br>
</p>
<div class="moz-cite-prefix">On 5/4/20 8:00 AM, Philippe de
Rochambeau wrote:<br>
</div>
<blockquote type="cite"
cite="mid:EF4ACBD8-74C8-4029-B13E-0C5E26C74F5E@free.fr">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
Good morning James,
<div class=""><br class="">
</div>
<div class="">I spent a few hours yesterday attempting to write
the <i class="">fst</i> description procedure, as suggested,
but to no avail.</div>
<div class="">For me, <i class="">fst_desc_proc</i> should
compare two values of type <i class="">A</i> and, if they are
equal, return <i class="">true</i>, otherwise, <i class="">false</i>.</div>
<div class="">But how how do you generically compare two A
values? ≡ won’t do.</div>
<div class=""><br class="">
</div>
<div class="">(In fact, I wouldn’t know either how to compare two
<i class="">Nats</i> for equality in Agda, since I could not
find an <i class="">==</i> operator in <i class="">Data.Nats</i>).</div>
<div class=""><br class="">
</div>
<div class="">Cheers,</div>
<div class=""><br class="">
</div>
<div class="">Philippe</div>
<div class="">
<div class=""><br class="">
</div>
<div class="">
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(237, 97, 27);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">open</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures"
class="">import</span><span style="font-variant-ligatures:
no-common-ligatures; color: #000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#c200ff" class="">Data.Nat</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures"
class="">using</span><span style="font-variant-ligatures:
no-common-ligatures; color: #000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">(</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#4500ff" class="">ℕ</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">)</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(194, 0, 255);"
class=""><span style="font-variant-ligatures:
no-common-ligatures; color: #ed611b" class="">open</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#ed611b" class="">import</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures"
class="">Relation.Binary.PropositionalEquality</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#ed611b" class="">using</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">(</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#4500ff" class="">_≡_</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">)</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(237, 97, 27);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">open</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures"
class="">import</span><span style="font-variant-ligatures:
no-common-ligatures; color: #000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#c200ff" class="">Data.Bool</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; min-height: 21px;" class=""><br
class="">
<span style="font-variant-ligatures: no-common-ligatures"
class=""></span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(237, 97, 27);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">record</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#4500ff" class="">Pair</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">(</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class="">A B </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">:</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#4500ff" class="">Set</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">)</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">:</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#4500ff" class="">Set</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures"
class="">where</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(237, 97, 27);"
class=""><span style="font-variant-ligatures:
no-common-ligatures; color: #000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures"
class="">field</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo;" class=""><span
style="font-variant-ligatures: no-common-ligatures"
class=""> </span><span style="font-variant-ligatures:
no-common-ligatures; color: #fb198d" class="">fst</span><span
style="font-variant-ligatures: no-common-ligatures"
class=""> </span><span style="font-variant-ligatures:
no-common-ligatures; color: #535353" class="">:</span><span
style="font-variant-ligatures: no-common-ligatures"
class=""> A</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo;" class=""><span
style="font-variant-ligatures: no-common-ligatures"
class=""> </span><span style="font-variant-ligatures:
no-common-ligatures; color: #fb198d" class="">snd</span><span
style="font-variant-ligatures: no-common-ligatures"
class=""> </span><span style="font-variant-ligatures:
no-common-ligatures; color: #535353" class="">:</span><span
style="font-variant-ligatures: no-common-ligatures"
class=""> B</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; min-height: 21px;" class=""><span
style="font-variant-ligatures: no-common-ligatures"
class=""></span><br class="">
</div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(237, 97, 27);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">open</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#c200ff" class="">Pair</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures"
class="">public</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; min-height: 21px;" class=""><span
style="font-variant-ligatures: no-common-ligatures"
class=""></span><br class="">
</div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(203, 36, 24);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">{--
</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(203, 36, 24);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">_eq_ : {A B : Set} → (a :
Pair A B) → (b : Pair A B) → Bool
</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(203, 36, 24);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">a eq b = (fst a ≡ fst b) ∧
(snd a ≡ snd b)
</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(203, 36, 24);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">--}</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; min-height: 21px;" class=""><span
style="font-variant-ligatures: no-common-ligatures"
class=""></span><br class="">
</div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(69, 0, 255);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">fst_desc_proc</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">:</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">{</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class="">A </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">:</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures"
class="">Set</span><span style="font-variant-ligatures:
no-common-ligatures; color: #535353" class="">}</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">→</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">(</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class="">a a' </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">:</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> A</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">)</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">→</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures"
class="">Bool</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(69, 0, 255);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">fst_desc_proc</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> a a' </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">=</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span style="text-decoration:
underline ; font-variant-ligatures: no-common-ligatures;
color: #b42419" class="">a</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span style="text-decoration:
underline ; font-variant-ligatures: no-common-ligatures;
color: #b42419" class="">≡</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span style="text-decoration:
underline ; font-variant-ligatures: no-common-ligatures;
color: #b42419" class="">a'</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(69, 0, 255);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">fst_desc_proc</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">=</span><span
style="font-variant-ligatures: no-common-ligatures; color:
#000000" class=""> </span><span
style="font-variant-ligatures: no-common-ligatures; color:
#535353" class="">{!!}</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; min-height: 21px;" class=""><span
style="font-variant-ligatures: no-common-ligatures"
class=""></span><br class="">
</div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(203, 36, 24);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">{--
</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(203, 36, 24);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">snd_desc_proc : {B : Set} →
(b b' : B) → Bool
</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(203, 36, 24);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">snd_desc_proc b b' = b == b'
→ true
</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(203, 36, 24);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">snd_desc_proc b b' = b != b'
→ false
</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(203, 36, 24);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">--}</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(203, 36, 24);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">-- _eq_ : {A B : Set} → ((a
a′ : A) → Bool) → ((b b′ : B) → Bool) → (ab ab′ : Pair A
B) → Bool</span></div>
<div style="margin: 0px; font-stretch: normal; line-height:
normal; font-family: Menlo; color: rgb(203, 36, 24);"
class=""><span style="font-variant-ligatures:
no-common-ligatures" class="">-- a eq a' = ?</span></div>
<div class=""><span style="font-variant-ligatures:
no-common-ligatures" class=""><br class="">
</span></div>
<div class=""><br class="">
</div>
<div class=""><br class="">
<div><br class="">
<blockquote type="cite" class="">
<div class="">Le 3 mai 2020 à 19:56, James Wood <<a
href="mailto:james.wood.100@strath.ac.uk" class=""
moz-do-not-send="true">james.wood.100@strath.ac.uk</a>>
a écrit :</div>
<br class="Apple-interchange-newline">
<div class="">
<div class="">Hi Philippe,<br class="">
<br class="">
You can see from the source code of
`Agda.Builtin.Bool` that it defines<br class="">
only `Bool`, `true`, and `false`. If you want some
operations on<br class="">
Booleans, you can either define them yourself or get
them from a<br class="">
library, e.g, stdlib's `Data.Bool`. It's best
practice to not import<br class="">
`Agda.Builtin` modules unless you really have to
(e.g, if you are<br class="">
writing your own base library). They may change
between versions.<br class="">
<br class="">
For making your `eq` generic, the simplest thing to
do would be to take<br class="">
as arguments decision procedures for the `fst`s and
`snd`s,<br class="">
respectively. The type should be `{A B : Set} → ((a
a′ : A) → Bool) →<br class="">
((b b′ : B) → Bool) → (ab ab′ : Pair A B) → Bool`.<br
class="">
<br class="">
Additionally, you might want to add `open Pair
public` after your<br class="">
definition of `Pair`, so that you don't have to
qualify `fst` and `snd`.<br class="">
There's an example of this in stdlib's definition of
`Σ` (somewhere<br class="">
around `Data.Product`).<br class="">
<br class="">
Regards,<br class="">
James<br class="">
<br class="">
On 03/05/2020 17:50, Philippe de Rochambeau wrote:<br
class="">
<blockquote type="cite" class="">Hello,<br class="">
<br class="">
when I load the following script, I get a « not in
scope ∧ » error.<br class="">
Why is that?<br class="">
Furthermore, how can I make the /eq/ function
generic, whichever the<br class="">
types used in the Pair, as long as the first type
is equal to the second?<br class="">
Many thanks.<br class="">
Philippe<br class="">
<br class="">
<br class="">
openimportAgda.Builtin.Nat<br class="">
openimportAgda.Builtin.String<br class="">
openimportAgda.Builtin.Bool<br class="">
<br class="">
recordPair (A B :Set):Setwhere<br class="">
field<br class="">
fst :A<br class="">
snd :B<br class="">
<br class="">
_eq_ :(a :Pair Nat Nat)→(b :Pair Nat Nat)→Bool<br
class="">
a eq b =(Pair.fst a == Pair.fst b)∧(Pair.snd a ==
Pair.snd b)<br class="">
<br class="">
<br class="">
_______________________________________________<br
class="">
Agda mailing list<br class="">
<a href="mailto:Agda@lists.chalmers.se" class=""
moz-do-not-send="true">Agda@lists.chalmers.se</a><br
class="">
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br
class="">
<br class="">
</blockquote>
_______________________________________________<br
class="">
Agda mailing list<br class="">
<a href="mailto:Agda@lists.chalmers.se" class=""
moz-do-not-send="true">Agda@lists.chalmers.se</a><br
class="">
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br
class="">
</div>
</div>
</blockquote>
</div>
<br class="">
</div>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<pre class="moz-quote-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>
</body>
</html>