<div dir="ltr">Philippe,<div><br></div><div>You may find the following helpful:</div><div> <a href="https://plfa.github.io/Decidable/">https://plfa.github.io/Decidable/</a></div><div><br></div><div>In my experience, you rarely want to use Bool in Agda, and Dec is better instead. The standard library has support for decidable equality on naturals _≟_, and for combining two decidable properties to decide a property of pairs _×-dec_. </div><div><br></div><div>Yours, -- P</div><div><br></div><div><div><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div dir="ltr"><div><div dir="ltr">. \ Philip Wadler, Professor of Theoretical Computer Science,<br>. /\ School of Informatics, University of Edinburgh<br></div><div>. / \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div><div dir="ltr"><br></div></div></div></div></div></div></div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 4 May 2020 at 03:01, Philippe de Rochambeau <<a href="mailto:phiroc@free.fr">phiroc@free.fr</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div style="overflow-wrap: break-word;">Good morning James,<div><br></div><div>I spent a few hours yesterday attempting to write the <i>fst</i> description procedure, as suggested, but to no avail.</div><div>For me, <i>fst_desc_proc</i> should compare two values of type <i>A</i> and, if they are equal, return <i>true</i>, otherwise, <i>false</i>.</div><div>But how how do you generically compare two A values? ≡ won’t do.</div><div><br></div><div>(In fact, I wouldn’t know either how to compare two <i>Nats</i> for equality in Agda, since I could not find an <i>==</i> operator in <i>Data.Nats</i>).</div><div><br></div><div>Cheers,</div><div><br></div><div>Philippe</div><div><div><br></div><div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(237,97,27)"><span style="font-variant-ligatures:no-common-ligatures">open</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures">import</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(194,0,255)">Data.Nat</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures">using</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">(</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(69,0,255)">ℕ</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">)</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(194,0,255)"><span style="font-variant-ligatures:no-common-ligatures;color:rgb(237,97,27)">open</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(237,97,27)">import</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures">Relation.Binary.PropositionalEquality</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(237,97,27)">using</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">(</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(69,0,255)">_≡_</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">)</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(237,97,27)"><span style="font-variant-ligatures:no-common-ligatures">open</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures">import</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(194,0,255)">Data.Bool</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;min-height:21px"><br><span style="font-variant-ligatures:no-common-ligatures"></span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(237,97,27)"><span style="font-variant-ligatures:no-common-ligatures">record</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(69,0,255)">Pair</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">(</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)">A B </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">:</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(69,0,255)">Set</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">)</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">:</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(69,0,255)">Set</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures">where</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(237,97,27)"><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures">field</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo"><span style="font-variant-ligatures:no-common-ligatures"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(251,25,141)">fst</span><span style="font-variant-ligatures:no-common-ligatures"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">:</span><span style="font-variant-ligatures:no-common-ligatures"> A</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo"><span style="font-variant-ligatures:no-common-ligatures"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(251,25,141)">snd</span><span style="font-variant-ligatures:no-common-ligatures"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">:</span><span style="font-variant-ligatures:no-common-ligatures"> B</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;min-height:21px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(237,97,27)"><span style="font-variant-ligatures:no-common-ligatures">open</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(194,0,255)">Pair</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures">public</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;min-height:21px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(203,36,24)"><span style="font-variant-ligatures:no-common-ligatures">{-- </span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(203,36,24)"><span style="font-variant-ligatures:no-common-ligatures">_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)"><span style="font-variant-ligatures:no-common-ligatures">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)"><span style="font-variant-ligatures:no-common-ligatures">--}</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;min-height:21px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(69,0,255)"><span style="font-variant-ligatures:no-common-ligatures">fst_desc_proc</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">:</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">{</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)">A </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">:</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures">Set</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">}</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">→</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">(</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)">a a' </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">:</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> A</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">)</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">→</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures">Bool</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(69,0,255)"><span style="font-variant-ligatures:no-common-ligatures">fst_desc_proc</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> a a' </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">=</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="text-decoration:underline;font-variant-ligatures:no-common-ligatures;color:rgb(180,36,25)">a</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="text-decoration:underline;font-variant-ligatures:no-common-ligatures;color:rgb(180,36,25)">≡</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="text-decoration:underline;font-variant-ligatures:no-common-ligatures;color:rgb(180,36,25)">a'</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(69,0,255)"><span style="font-variant-ligatures:no-common-ligatures">fst_desc_proc</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">=</span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(0,0,0)"> </span><span style="font-variant-ligatures:no-common-ligatures;color:rgb(83,83,83)">{!!}</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;min-height:21px"><span style="font-variant-ligatures:no-common-ligatures"></span><br></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(203,36,24)"><span style="font-variant-ligatures:no-common-ligatures">{-- </span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(203,36,24)"><span style="font-variant-ligatures:no-common-ligatures">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)"><span style="font-variant-ligatures:no-common-ligatures">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)"><span style="font-variant-ligatures:no-common-ligatures">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)"><span style="font-variant-ligatures:no-common-ligatures">--}</span></div><div style="margin:0px;font-stretch:normal;line-height:normal;font-family:Menlo;color:rgb(203,36,24)"><span style="font-variant-ligatures:no-common-ligatures">-- _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)"><span style="font-variant-ligatures:no-common-ligatures">-- a eq a' = ?</span></div><div><span style="font-variant-ligatures:no-common-ligatures"><br></span></div><div><br></div><div><br><div><br><blockquote type="cite"><div>Le 3 mai 2020 à 19:56, James Wood <<a href="mailto:james.wood.100@strath.ac.uk" target="_blank">james.wood.100@strath.ac.uk</a>> a écrit :</div><br><div><div>Hi Philippe,<br><br>You can see from the source code of `Agda.Builtin.Bool` that it defines<br>only `Bool`, `true`, and `false`. If you want some operations on<br>Booleans, you can either define them yourself or get them from a<br>library, e.g, stdlib's `Data.Bool`. It's best practice to not import<br>`Agda.Builtin` modules unless you really have to (e.g, if you are<br>writing your own base library). They may change between versions.<br><br>For making your `eq` generic, the simplest thing to do would be to take<br>as arguments decision procedures for the `fst`s and `snd`s,<br>respectively. The type should be `{A B : Set} → ((a a′ : A) → Bool) →<br>((b b′ : B) → Bool) → (ab ab′ : Pair A B) → Bool`.<br><br>Additionally, you might want to add `open Pair public` after your<br>definition of `Pair`, so that you don't have to qualify `fst` and `snd`.<br>There's an example of this in stdlib's definition of `Σ` (somewhere<br>around `Data.Product`).<br><br>Regards,<br>James<br><br>On 03/05/2020 17:50, Philippe de Rochambeau wrote:<br><blockquote type="cite">Hello,<br><br>when I load the following script, I get a « not in scope ∧ » error.<br>Why is that?<br>Furthermore, how can I make the /eq/ function generic, whichever the<br>types used in the Pair, as long as the first type is equal to the second?<br>Many thanks.<br>Philippe<br><br><br>openimportAgda.Builtin.Nat<br>openimportAgda.Builtin.String<br>openimportAgda.Builtin.Bool<br><br>recordPair (A B :Set):Setwhere<br> field<br> fst :A<br> snd :B<br><br>_eq_ :(a :Pair Nat Nat)→(b :Pair Nat Nat)→Bool<br>a eq b =(Pair.fst a == Pair.fst b)∧(Pair.snd a == Pair.snd b)<br><br><br>_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br><br></blockquote>_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br><a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br></div></div></blockquote></div><br></div></div></div></div>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>