[Agda] [RFC stdlib v2.0] 1. Numeric ops with non-zero proofs
Matthew Daggitt
matthewdaggitt at gmail.com
Wed Jul 7 09:21:06 CEST 2021
Hi Philip,
I think the key point is that irrelevant arguments still have to be valid
members of the type. It's not that Agda doesn't require a valid value for
an irrelevant argument, it's that Agda doesn't care which particular valid
value you provide. So in your example "proof", you would not be able to
divide by "a - b" as you would not have a proof that it is non-zero.
However if in different circumstances you had *two* proofs that "a - b" is
non-zero then the irrelevancy would ensure that Agda wouldn't care which
one you used. In summary, using irrelevant arguments does not allow us to
prove 1 == 2.
There's also been some discussion on the type of irrelevance we should be
aiming for on this pull request that you might find interesting:
https://github.com/agda/agda-stdlib/pull/1538
Cheers,
Matthew
On Wed, Jul 7, 2021 at 2:22 AM Philip Wadler <wadler at inf.ed.ac.uk> wrote:
> There is a standard proof that 1 = 2. You are probably familiar with it;
> if not, see below. You write:
>
> Agda doesn't consider irrelevant arguments when proving propositional
>> equality. Therefore to prove m / n and x / y are propositionally equal
>> will only require that we prove m equals x and n equals y and will not
>> require us to explicitly prove that the result doesn't depend on the proofs
>> of non-zeroness.
>
>
> Does making the proof of nonzero divisor an irrelevant argument open up
> the possibility to prove 1 = 2? Go well, -- P
>
> https://www.quickanddirtytips.com/education/math/how-to-prove-that-1-2
>
> Here's how it works:
>
> -
>
> Assume that we have two variables *a* and *b*, and that: *a = b*
> -
>
> Multiply both sides by *a* to get: *a2 = **ab*
> -
>
> Subtract *b*2 from both sides to get: *a2 - b2 = ab - b2*
> -
>
> This is the tricky part: Factor the left side (using FOIL from
> algebra) to get (*a* + *b*)(*a* - *b*) and factor out *b* from the
> right side to get *b*(*a* - *b*). If you're not sure how FOIL or
> factoring works, don't worry—you can check that this all works by
> multiplying everything out to see that it matches. The end result is that
> our equation has become: *(a + b)(a - b) = b(a - b)*
> -
>
> Since (*a* - *b*) appears on both sides, we can cancel it to get:
> *a + b = b*
> -
>
> Since *a* = *b* (that's the assumption we started with), we can
> substitute *b* in for *a* to get: *b + b = b*
> -
>
> Combining the two terms on the left gives us: *2b = b*
> -
>
> Since *b* appears on both sides, we can divide through by *b* to get: *2
> = 1*
>
> Wait, what?! Everything we did there looked totally reasonable. How in the
> world did we end up proving that 2 = 1?
> . \ 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 Tue, 6 Jul 2021 at 05:43, Matthew Daggitt <matthewdaggitt at gmail.com>
> wrote:
>
>> This email was sent to you by someone outside the University.
>> You should only click on links or attachments if you are certain that the
>> email is genuine and the content is safe.
>>
>> Dear all,
>> To kick things off, the first RFC (request for comment) for v2.0 of the
>> Agda standard library is about proposed changes to how numeric operations
>> that require non-zero proofs (e.g. division) work.
>>
>> The current situation
>>
>> Currently operations such as division are defined as follows
>> <https://github.com/agda/agda-stdlib/blob/516c545f28aca931d695a86fbdf7941154b0a64f/src/Data/Nat/DivMod.agda#L43>
>> :
>>
>> _/_ : (dividend divisor : ℕ) {≢0 : False (divisor ≟ 0)} → ℕ
>>
>> taking an implicit proof that the result of the decision procedure of
>> testing whether it is zero reduces to false. This is preferable to
>> passing a direct proof of the form divisor ≢ 0 as it means that when
>> divisor normalises to something of the form suc n then the type of the
>> proof reduces to unit ⊤ which Agda automatically fills in. Consequently
>> you can write 7 / 3 or m / sucn without having to explicitly construct
>> the proof.
>>
>> The current problems
>>
>> 1. When the denominator is not in the form suc _, Agda can't infer
>> the proof and therefore it must always be passed explicitly even when the
>> proof is in scope. This leads to having to write the ugly code like the
>> following:
>>
>> ∀ m n {gcd≢0 : NonZero (gcd m n)} → Coprime ((m / gcd m n) {gcd≢0}) ((n / gcd m n) {gcd≢0})
>>
>>
>> 1.
>>
>> When proving equalities over _/_ you can't use cong₂ from
>> Relation.Binary.PropositionalEquality directly as Agda requires that
>> you explicitly prove the proofs of non-zeroness do not affect the result.
>> This makes it very finicky to use equational reasoning.
>> 2.
>>
>> The use of the decision procedure _≟_ means that the definition must
>> depend on Data.Nat.Properties where _≟_ lives. This means that a)
>> type-checking anything involving _/_ requires type-checking a much
>> larger proportion of the library that one would expect and b) _/_ can't
>> live in Data.Nat.Base.
>> 3.
>>
>> Constructing a proof of the type False (divisor ≟ 0) is much trickier
>> than a proof of divisor ≢ 0and requires extra imports from
>> Relation.Nullary.
>>
>> Proposed solution
>>
>> We propose to take a leaf out of Ulf Norell's Prelude library and instead
>> pass the proofs as *irrelevant*, *instance* arguments that use the new
>> NonZero predicates introduced in v1.5:
>>
>> _/_ : (dividend divisor : ℕ) {{.(NonZero divisor)}} → ℕ
>>
>> which preserves the ability to not provide the proofs for divisors of the
>> form suc _ and fixes the problems listed above as follows:
>>
>> 1. Agda automatically fills in instance arguments if they are in
>> scope, therefore removing the need to supply them to every place in the
>> expression where they can't be inferred. For example we would then be able
>> to write the much nicer:
>>
>> ∀ m n {{NonZero (gcd m n)}} → Coprime (m / gcd m n) (n / gcd m n)
>>
>>
>> 1.
>>
>> Agda doesn't consider irrelevant arguments when proving propositional
>> equality. Therefore to prove m / n and x / y are propositionally
>> equal will only require that we prove m equals x and n equals y and
>> will not require us to explicitly prove that the result doesn't depend on
>> the proofs of non-zeroness.
>> 2.
>>
>> The NonZero predicate is much more lightweight than the decidability
>> proof and lives in Data.Nat.Base rather than Data.Nat.Properties.
>> 3.
>>
>> The NonZero predicate comes with nice constructors nonZero-< and
>> nonZero-≢ that makes constructing such proofs much easier.
>>
>> This has an additional advantage in that for certain operations that
>> always result in a non-zero result, e.g. factorial, it will be possible to
>> declare a proof of the non-zeroness as an instance and you will never have
>> to explicitly pass a proof.
>>
>> Backwards incompatibilities
>>
>> In cases where the proof is already automatically inferred nothing will
>> need to change. In places where the proof has to be passed explicitly, then
>> the type of the proof will need to change and will need to be passed using
>> instance brackets {{_}} rather than implict brackets {_}. As mentioned
>> above, NonZero comes with constructors so constructing the new proofs
>> should be much easier.
>>
>> Feedback
>>
>> Any feedback would be greatly appreciated! Please feel free to reply in
>> one of the following issues:
>> https://github.com/agda/agda-stdlib/issues/921
>> https://github.com/agda/agda-stdlib/issues/1170
>> https://github.com/agda/agda-stdlib/issues/1408
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> 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/20210707/f5476712/attachment.html>
More information about the Agda
mailing list