[Agda] Boolean And in Pair

Philippe de Rochambeau phiroc at free.fr
Mon May 4 14:03:36 CEST 2020


Hi Philip,

thank you very much for the pointer. I’ll have a look.

I’m am currently trying to write the two equations, which determine if Pairs A and B match.

Here’s my draft code so far.

Cheers,

Philippe


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

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

open Pair public

_eq_ : {A B : Set} → ((a a′ : A) → Bool) → ((b b′ : B) → Bool) → (ab ab′ : Pair A B) → Bool
(eqa eq eqb) record { fst = fst₁ ; snd = snd₁ } record { fst = fst ; snd = snd } = eqb snd snd

eqa : (a a' : ℕ) → Bool
eqa ℕ.zero a' = false
eqa (ℕ.suc a) a' = eqa a a'

eqb : (b b' : Bool) → Bool
eqb false b' = b'
eqb true b' = b'

p23₁ : Pair ℕ Bool
p23₁ = record { fst = 2; snd = true }

p23₂ : Pair ℕ Bool
p23₂ = record { fst = 2; snd = true }

p24 : Pair ℕ ℕ
p24 = record { fst = 2; snd = 4 }




> Le 4 mai 2020 à 13:56, Philip Wadler <wadler at inf.ed.ac.uk> a écrit :
> 
> Philippe,
> 
> You may find the following helpful:
>     https://plfa.github.io/Decidable/ <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/ <http://homepages.inf.ed.ac.uk/wadler/>
> 
> 
> 
> On Mon, 4 May 2020 at 03:01, Philippe de Rochambeau <phiroc at free.fr <mailto: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 <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 <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 <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 <https://lists.chalmers.se/mailman/listinfo/agda>
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200504/b601f072/attachment.html>


More information about the Agda mailing list