[Agda] A proof of the irrationality of the square root in Agda

[Arseniy Alekseyev]

I know of three ways of representing positive numbers:

1. The thing you've written. In this case you have to define
operations on NatStar independently.
2. Nat1 = ∃ (λ x → x > 0)

_+₁_ : Nat1 → Nat1 → Nat1
(zero , ()) +₁ _
_ +₁ (zero , ())
(suc a , _) +₁ (suc b , _) = suc a + suc b , s≤s z≤n

3. Use the isomorphism to Nats you've noticed and define something like:
_+₁_ : ℕ → ℕ → ℕ
m +₁ n = suc (m + n)

_*₁_ : ℕ → ℕ → ℕ
m *₁ n = pred (suc m * suc n)

You can also wrap it into a record to avoid confusion with normal naturals:


record ℕ1 : Set where
  constructor suc
  field
   pred : ℕ

As for proving the operations properties, approaches 2 and 3 look
nicer than 1. I don't know which of those I prefer.

Arseniy.

On 7 November 2011 06:03, IKEGAMI Daisuke <ikegami.da at gmail.com> wrote:
> 2011/11/5 Nils Anders Danielsson <nad at chalmers.se>:
>> On 2011-11-04 15:10, IKEGAMI Daisuke wrote:
>>>
>>> TODO (still working)
>>> - the natural numbers without zero with multiplication is cancellative
>>
>> This is proved in the standard library (more or less).
>
> I found a proposition 'cancel-*-right' in Data.Nat.Properties.
> It seems useful to prove that ({1, 2, 3, ...}, _*_) is cancelative.
>
>>> - 2 is prime
>>
>> It should be easy to prove this. Let me try:
>> (snip)
>
> Thanks, Nils. It helps a lot!
>
>> I'll add some definitions to the library.
>
> Yes, please.
>
> BTW, I have a question how to define the natural numbers
> without zero ({1,2,3,...}, _*_).
>
> To give the record CommutativeMonoid in module Algebra,
> we need a Set, called Carrier. Therefore I defined NatStar.
>
>  data NatStar : Set where
>    one : NatStar
>    suc : NatStar -> NatStar
>
> However, the above definition is same of Nat in Data.Nat as type.
> Since operators in Agda should be total, the definition of _*_ on
> NatStar seems not equal to _*_ on Nat in Data.Nat, I think.
> Can we define the natural numbers without zero using Data.Nat?
> How to avoid to prove similar properties for NatStar to Nat?
>
> I will give a talk about this work to translate Thierry's proof
> in Agda1/Alfa to Agda2 with Agda standard library on the meeting:
>  7th Theorem Proving and Provers meeting at Japan
>  http://staff.aist.go.jp/reynald.affeldt/tpp2011/program.html
> Unfortunately, registration has been already closed.
>
> One of the aim of the talk is to introduce features of Agda2
> by an example:
>
> - https://gist.github.com/1344224
>    a proposition in Alfa (natural deduction style, but, not simple)
> - https://gist.github.com/1344227
>    the same proposition in Agda2 (short, readable with Agda library)
>
> Nils, I'm pleased to add your name to the title of the talk, as
>  "joint work with Nils Anders Danielsson".
>  Thank every contributers of Agda and especially you.
>
> Best wishes,
> Ike
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>