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

[IKEGAMI Daisuke]

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