[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