Field of rationals

[siddhartha-gadgil]

• We need to define a field for both this and #12
• Every rational number is uniquely n / (S k) with n an integer and k a natural number such that gcd(n, Sk) = 1, allowing the definition of a type.
• There is also a non-unique representation as p / q where we may have cancellations, with the operations easy in terms of this.
• By relating the two descriptions, one should construct the field of rational numbers, show it is a field and is the quotient field of Z

[SideArt]

How do we cite other people's code when we use their functions? Is it enough to cite them in a comment above the function?

[SideArt]

Given a type and an element of that type 'g', is it possible to construct another type whose elements are identical to those of the initial type with 'g' removed?

[siddhartha-gadgil]

How do we cite other people's code when we use their functions? Is it enough to cite them in a comment above the function?

Yes, cite them and point to the original file.

[siddhartha-gadgil]

Given a type and an element of that type 'g', is it possible to construct another type whose elements are identical to those of the initial type with 'g' removed?

Given a: A, you may want to use the sigma type of pairs (x, pf) with x : A and pf : x = a -> Void

[rathivrunda]

Idris does not allow us to define custom equalities on types and refl is the only way you can prove an equality. Hence, we can never use the equality type for Rational numbers, as each element will always have to be equal and we won't be able to make any significant progress using just Refl. Proving its a field without using the equality type, would not be possible. How can we get past this?

[siddhartha-gadgil]

Equality is freely generated by reflexivity, which gives several properties of equality:

• equality is symmetric
• equality is transitive
• given x = y for x, y: A and f: A -> B we get f(x) = f(y) (plus the dependent version of this).
• reflexivity is quite powerful, as any two terms that simplify to the same can be proved equal by reflexivity.

With all this, one can prove a lot. For me to answer more, you should narrow down to the simplest statement that you cannot prove.

[siddhartha-gadgil]

The main difficulty is proving that two proofs are equal. One approach (as Arka suggested) is to bypass this by changing the definition of rationals to just use successors of natural numbers

data Rats: Type where 
   Rat : (p : ZZ) -> (q : Nat) -> Rat

so that Rat p q is the rational number p/(q + 1)

[siddhartha-gadgil]

If you do use the definition of rationals as above you should modify all definitions, e.g.

add : Rats -> Rats -> Rats
add (Rat p1 q1) (Rat p2 q2) = Rat ((p1 * q2) + p1 + (p2 * q1) + p2) (q1 * q2 + q1 + q2)  

[siddhartha-gadgil]

Some code as an example is at https://github.com/siddhartha-gadgil/LTS2019/blob/master/Code/Q.idr - this was generated looking at required types, proving lemmas and applying functions. The auxiliary functions were defined looking up required types in atom.

There is no conceptual problem doing this, but it takes work and understanding.

[siddhartha-gadgil]

Workflow for proving equalities:

• Make the statement in Atom.
• Generate proof with holes.
• Split by cases based on both the statements and the definitions you use - for example addition and multiplication on ZZ are defined by cases, so one splits by these.
• See the type of the relevant holes. Idris simplifies this, and if the result has both sides equal just use reflexivity.
• Match the sides and find the smallest units in the two sides of the equation that are different according to Idris but are mathematically equal.
• Prove these are equal as a lemma - typically using cases, possibly using properties of equality.
• Deduce larger cases from these in steps using function application for equality.