[Agda] Boolean And in Pair

[Philippe de Rochambeau]

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

open import Data.Nat using (ℕ)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Data.Bool

record Pair (A B : Set) : Set where
  field
    fst : A
    snd : B

open Pair public

{--                                                                                                                                                                     
_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_proc a 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> 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
>> 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/d874b7a5/attachment.html>