[Agda] Boolean And in Pair

[a.j.rouvoet]

Hi Philippe,

Indeed you cannot compare two values of arbitrary types for equality.

James' idea was to write a function that given two comparison functions 
for the first and second projection
of a pair, produces a comparison function for the pair as a whole.

The signature you wrote for _eq_ is correct
and you should be able to implement, although its implementation should 
take 4 parameters: `eq eqa eqb ab ab' = ?`
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
the components of the pairs.

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,
for example for Nat.

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
easier to work with and does not require you to manually give the 
comparison functions as parameters.

Hope this helps,


Arjen

On 5/4/20 8:00 AM, Philippe de Rochambeau wrote:
> Good morning James,
>
> I spent a few hours yesterday attempting to write the /fst/ 
> description procedure, as suggested, but to no avail.
> For me, /fst_desc_proc/ should compare two values of type /A/ and, if 
> they are equal, return /true/, otherwise, /false/.
> But how how do you generically compare two A values? ≡ won’t do.
>
> (In fact, I wouldn’t know either how to compare two /Nats/ for 
> equality in Agda, since I could not find an /==/ operator in /Data.Nats/).
>
> Cheers,
>
> Philippe
>
> openimportData.Natusing(ℕ)
> openimportRelation.Binary.PropositionalEqualityusing(_≡_)
> openimportData.Bool
>
> recordPair(A B :Set):Setwhere
> field
> fst:A
> snd:B
>
> openPairpublic
>
> {--
> _eq_ : {A B : Set} → (a : Pair A B) → (b : Pair A B) → Bool
> a eq b = (fst a ≡ fst b) ∧ (snd a ≡ snd b)
> --}
>
> fst_desc_proc:{A :Set}→(a a' :A)→Bool
> fst_desc_proca a' =a≡a'
> fst_desc_proc={!!}
>
> {--
> snd_desc_proc : {B : Set} → (b b' : B) → Bool
> snd_desc_proc b b' = b == b' → true
> snd_desc_proc b b' = b != b' → false
> --}
> -- _eq_ : {A B : Set} → ((a a′ : A) → Bool) → ((b b′ : B) → Bool) → 
> (ab ab′ : Pair A B) → Bool
> -- a eq a' = ?
>
>
>
>
>> Le 3 mai 2020 à 19:56, James Wood <james.wood.100 at strath.ac.uk 
>> <mailto:james.wood.100 at strath.ac.uk>> a écrit :
>>
>> Hi Philippe,
>>
>> You can see from the source code of `Agda.Builtin.Bool` that it defines
>> only `Bool`, `true`, and `false`. If you want some operations on
>> Booleans, you can either define them yourself or get them from a
>> library, e.g, stdlib's `Data.Bool`. It's best practice to not import
>> `Agda.Builtin` modules unless you really have to (e.g, if you are
>> writing your own base library). They may change between versions.
>>
>> For making your `eq` generic, the simplest thing to do would be to take
>> as arguments decision procedures for the `fst`s and `snd`s,
>> respectively. The type should be `{A B : Set} → ((a a′ : A) → Bool) →
>> ((b b′ : B) → Bool) → (ab ab′ : Pair A B) → Bool`.
>>
>> Additionally, you might want to add `open Pair public` after your
>> definition of `Pair`, so that you don't have to qualify `fst` and `snd`.
>> There's an example of this in stdlib's definition of `Σ` (somewhere
>> around `Data.Product`).
>>
>> Regards,
>> James
>>
>> On 03/05/2020 17:50, Philippe de Rochambeau wrote:
>>> Hello,
>>>
>>> when I load the following script, I get a « not in scope ∧ » error.
>>> Why is that?
>>> Furthermore, how can I make the /eq/ function generic, whichever the
>>> types used in the Pair, as long as the first type is equal to the 
>>> second?
>>> Many thanks.
>>> Philippe
>>>
>>>
>>> openimportAgda.Builtin.Nat
>>> openimportAgda.Builtin.String
>>> openimportAgda.Builtin.Bool
>>>
>>> recordPair (A B :Set):Setwhere
>>>   field
>>>     fst :A
>>>     snd :B
>>>
>>> _eq_ :(a :Pair Nat Nat)→(b :Pair Nat Nat)→Bool
>>> a eq b =(Pair.fst a == Pair.fst b)∧(Pair.snd a == Pair.snd b)
>>>
>>>
>>> _______________________________________________
>>> Agda mailing list
>>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>> https://lists.chalmers.se/mailman/listinfo/agda
>>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200504/12323387/attachment.html>