[Agda] Boolean And in Pair

[Philip Wadler]

Philippe,

You may find the following helpful:
    https://plfa.github.io/Decidable/

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_.

Yours, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/



On Mon, 4 May 2020 at 03:01, Philippe de Rochambeau <phiroc at free.fr> 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
>
> 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
>
>
> _______________________________________________
> 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/2ff8b958/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200504/2ff8b958/attachment.ksh>