mirror of
https://github.com/Smaug123/agdaproofs
synced 2025-12-15 03:25:43 +00:00
Tidy up groups (#64)
This commit is contained in:
Patrick Stevens
GitHub
87
Numbers/Rationals/Definition.agda
Normal file
87
Numbers/Rationals/Definition.agda
Normal file
@@ -0,0 +1,87 @@
|
||||
{-# OPTIONS --safe --warning=error #-}
|
||||
|
||||
open import LogicalFormulae
|
||||
open import Numbers.Naturals.Naturals
|
||||
open import Numbers.Integers.Integers
|
||||
open import Groups.Groups
|
||||
open import Groups.Definition
|
||||
open import Groups.Lemmas
|
||||
open import Rings.Definition
|
||||
open import Rings.Orders.Total.Definition
|
||||
open import Rings.Orders.Partial.Definition
|
||||
open import Fields.Fields
|
||||
open import Numbers.Primes.PrimeNumbers
|
||||
open import Setoids.Setoids
|
||||
open import Setoids.Orders
|
||||
open import Functions
|
||||
open import Sets.EquivalenceRelations
|
||||
|
||||
module Numbers.Rationals.Definition where
|
||||
|
||||
open import Fields.FieldOfFractions.Setoid ℤIntDom
|
||||
open import Fields.FieldOfFractions.Addition ℤIntDom
|
||||
open import Fields.FieldOfFractions.Multiplication ℤIntDom
|
||||
open import Fields.FieldOfFractions.Ring ℤIntDom
|
||||
open import Fields.FieldOfFractions.Field ℤIntDom
|
||||
open import Fields.FieldOfFractions.Order ℤIntDom ℤOrderedRing
|
||||
|
||||
ℚ : Set
|
||||
ℚ = fieldOfFractionsSet
|
||||
|
||||
_+Q_ : ℚ → ℚ → ℚ
|
||||
a +Q b = fieldOfFractionsPlus a b
|
||||
|
||||
_*Q_ : ℚ → ℚ → ℚ
|
||||
a *Q b = fieldOfFractionsTimes a b
|
||||
|
||||
ℚRing : Ring fieldOfFractionsSetoid _+Q_ _*Q_
|
||||
ℚRing = fieldOfFractionsRing
|
||||
|
||||
0Q : ℚ
|
||||
0Q = Ring.0R ℚRing
|
||||
|
||||
injectionQ : ℤ → ℚ
|
||||
injectionQ z = z ,, (nonneg 1 , λ ())
|
||||
|
||||
ℚField : Field ℚRing
|
||||
ℚField = fieldOfFractions
|
||||
|
||||
_<Q_ : ℚ → ℚ → Set
|
||||
_<Q_ = fieldOfFractionsComparison
|
||||
|
||||
_=Q_ : ℚ → ℚ → Set
|
||||
a =Q b = Setoid._∼_ fieldOfFractionsSetoid a b
|
||||
|
||||
reflQ : {x : ℚ} → (x =Q x)
|
||||
reflQ {x} = Equivalence.reflexive (Setoid.eq fieldOfFractionsSetoid) {x}
|
||||
|
||||
_≤Q_ : ℚ → ℚ → Set
|
||||
a ≤Q b = (a <Q b) || (a =Q b)
|
||||
|
||||
negateQ : ℚ → ℚ
|
||||
negateQ a = Group.inverse (Ring.additiveGroup ℚRing) a
|
||||
|
||||
_-Q_ : ℚ → ℚ → ℚ
|
||||
a -Q b = a +Q negateQ b
|
||||
|
||||
a-A : (a : ℚ) → (a -Q a) =Q 0Q
|
||||
a-A a = Group.invRight (Ring.additiveGroup ℚRing) {a}
|
||||
|
||||
ℚPartialOrder : SetoidPartialOrder fieldOfFractionsSetoid fieldOfFractionsComparison
|
||||
ℚPartialOrder = fieldOfFractionsOrder
|
||||
|
||||
ℚTotalOrder : SetoidTotalOrder fieldOfFractionsOrder
|
||||
ℚTotalOrder = fieldOfFractionsTotalOrder
|
||||
|
||||
open SetoidTotalOrder fieldOfFractionsTotalOrder
|
||||
open SetoidPartialOrder partial
|
||||
open Setoid fieldOfFractionsSetoid
|
||||
|
||||
negateQWellDefined : (a b : ℚ) → (a =Q b) → (negateQ a) =Q (negateQ b)
|
||||
negateQWellDefined a b a=b = inverseWellDefined (Ring.additiveGroup ℚRing) {a} {b} a=b
|
||||
|
||||
ℚPOrdered : PartiallyOrderedRing ℚRing partial
|
||||
ℚPOrdered = fieldOfFractionsPOrderedRing
|
||||
|
||||
ℚOrdered : TotallyOrderedRing ℚPOrdered
|
||||
ℚOrdered = fieldOfFractionsOrderedRing
|
||||
142
Numbers/Rationals/Lemmas.agda
Normal file
142
Numbers/Rationals/Lemmas.agda
Normal file
@@ -0,0 +1,142 @@
|
||||
{-# OPTIONS --safe --warning=error #-}
|
||||
|
||||
open import WellFoundedInduction
|
||||
open import LogicalFormulae
|
||||
open import Numbers.Naturals.Naturals
|
||||
open import Numbers.Integers.Integers
|
||||
open import Numbers.Integers.Order
|
||||
open import Groups.Groups
|
||||
open import Groups.Definition
|
||||
open import Rings.Definition
|
||||
open import Rings.Orders.Partial.Definition
|
||||
open import Rings.Orders.Total.Definition
|
||||
open import Fields.Fields
|
||||
open import Numbers.Primes.PrimeNumbers
|
||||
open import Setoids.Setoids
|
||||
open import Setoids.Orders
|
||||
open import Functions
|
||||
open import Sets.EquivalenceRelations
|
||||
open import Numbers.Rationals.Definition
|
||||
open import Semirings.Definition
|
||||
open import Orders
|
||||
|
||||
module Numbers.Rationals.Lemmas where
|
||||
|
||||
open PartiallyOrderedRing ℤPOrderedRing
|
||||
open import Rings.Orders.Total.Lemmas ℤOrderedRing
|
||||
open SetoidTotalOrder (totalOrderToSetoidTotalOrder ℤOrder)
|
||||
|
||||
evenOrOdd : (a : ℕ) → (Sg ℕ (λ i → i *N 2 ≡ a)) || (Sg ℕ (λ i → succ (i *N 2) ≡ a))
|
||||
evenOrOdd zero = inl (zero , refl)
|
||||
evenOrOdd (succ zero) = inr (zero , refl)
|
||||
evenOrOdd (succ (succ a)) with evenOrOdd a
|
||||
evenOrOdd (succ (succ a)) | inl (a/2 , even) = inl (succ a/2 , applyEquality (λ i → succ (succ i)) even)
|
||||
evenOrOdd (succ (succ a)) | inr (a/2-1 , odd) = inr (succ a/2-1 , applyEquality (λ i → succ (succ i)) odd)
|
||||
|
||||
parity : (a b : ℕ) → succ (2 *N a) ≡ 2 *N b → False
|
||||
parity zero (succ b) pr rewrite Semiring.commutative ℕSemiring b (succ (b +N 0)) = bad pr
|
||||
where
|
||||
bad : (1 ≡ succ (succ ((b +N 0) +N b))) → False
|
||||
bad ()
|
||||
parity (succ a) (succ b) pr rewrite Semiring.commutative ℕSemiring b (succ (b +N 0)) | Semiring.commutative ℕSemiring a (succ (a +N 0)) | Semiring.commutative ℕSemiring (a +N 0) a | Semiring.commutative ℕSemiring (b +N 0) b = parity a b (succInjective (succInjective pr))
|
||||
|
||||
sqrt0 : (p : ℕ) → p *N p ≡ 0 → p ≡ 0
|
||||
sqrt0 zero pr = refl
|
||||
sqrt0 (succ p) ()
|
||||
|
||||
-- So as to give us something easy to induct down, introduce a silly extra variable
|
||||
evil' : (k : ℕ) → ((a b : ℕ) → (0 <N a) → (pr : k ≡ a +N b) → a *N a ≡ (b *N b) *N 2 → False)
|
||||
evil' = rec <NWellfounded (λ z → (x x₁ : ℕ) (pr' : 0 <N x) (x₂ : z ≡ x +N x₁) (x₃ : x *N x ≡ (x₁ *N x₁) *N 2) → False) go
|
||||
where
|
||||
go : (k : ℕ) (indHyp : (k' : ℕ) (k'<k : k' <N k) (r s : ℕ) (0<r : 0 <N r) (r+s : k' ≡ r +N s) (x₇ : r *N r ≡ (s *N s) *N 2) → False) (a b : ℕ) (0<a : 0 <N a) (a+b : k ≡ a +N b) (pr : a *N a ≡ (b *N b) *N 2) → False
|
||||
go k indHyp a b 0<a a+b pr = contr
|
||||
where
|
||||
open import Semirings.Solver ℕSemiring multiplicationNIsCommutative
|
||||
aEven : Sg ℕ (λ i → i *N 2 ≡ a)
|
||||
aEven with evenOrOdd a
|
||||
aEven | inl x = x
|
||||
aEven | inr (a/2-1 , odd) rewrite equalityCommutative odd =
|
||||
-- Derive a pretty mechanical contradiction using the automatic solver.
|
||||
-- This line looks hellish, but it was almost completely mechanical.
|
||||
exFalso (parity (a/2-1 +N (a/2-1 *N succ (a/2-1 *N 2))) (b *N b) (transitivity (
|
||||
-- truly mechanical bit starts here
|
||||
from (succ (plus (plus (const a/2-1) (times (const a/2-1) (succ (times (const a/2-1) (succ (succ zero)))))) (plus (plus (const a/2-1) (times (const a/2-1) (succ (times (const a/2-1) (succ (succ zero)))))) (times zero (plus (const a/2-1) (times (const a/2-1) (succ (times (const a/2-1) (succ (succ zero))))))))))
|
||||
to succ (plus (times (const a/2-1) (succ (succ zero))) (times (times (const a/2-1) (succ (succ zero))) (succ (times (const a/2-1) (succ (succ zero))))))
|
||||
-- truly mechanical bit ends here
|
||||
by applyEquality (λ i → succ (a/2-1 +N i)) (
|
||||
-- Grinding out some manipulations
|
||||
transitivity (equalityCommutative (Semiring.+Associative ℕSemiring a/2-1 _ _)) (applyEquality (a/2-1 +N_) (transitivity (Semiring.commutative ℕSemiring (a/2-1 *N (a/2-1 +N a/2-1)) _) (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring a/2-1 _ _)) (applyEquality (a/2-1 +N_) (transitivity (equalityCommutative (Semiring.+Associative ℕSemiring a/2-1 _ _)) (applyEquality (a/2-1 +N_) (transitivity (equalityCommutative (Semiring.+DistributesOver* ℕSemiring a/2-1 _ _)) (applyEquality (a/2-1 *N_) (equalityCommutative (Semiring.+Associative ℕSemiring a/2-1 _ _))))))))))
|
||||
)) (transitivity pr (multiplicationNIsCommutative (b *N b) 2))))
|
||||
|
||||
next : (underlying aEven *N 2) *N (underlying aEven *N 2) ≡ (b *N b) *N 2
|
||||
next with aEven
|
||||
... | a/2 , even rewrite even = pr
|
||||
|
||||
next2 : (underlying aEven *N 2) *N underlying aEven ≡ b *N b
|
||||
next2 = productCancelsRight 2 _ _ (le 1 refl) (transitivity (equalityCommutative (Semiring.*Associative ℕSemiring (underlying aEven *N 2) _ _)) next)
|
||||
|
||||
next3 : b *N b ≡ (underlying aEven *N underlying aEven) *N 2
|
||||
next3 = equalityCommutative (transitivity (transitivity (equalityCommutative (Semiring.*Associative ℕSemiring (underlying aEven) _ _)) (multiplicationNIsCommutative (underlying aEven) _)) next2)
|
||||
|
||||
halveDecreased : underlying aEven <N a
|
||||
halveDecreased with aEven
|
||||
halveDecreased | zero , even rewrite equalityCommutative even = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) 0<a)
|
||||
halveDecreased | succ a/2 , even = le a/2 (transitivity (applyEquality succ (transitivity (Semiring.commutative ℕSemiring a/2 _) (applyEquality succ (transitivity (doubleIsAddTwo a/2) (multiplicationNIsCommutative 2 a/2))))) even)
|
||||
|
||||
reduced : b +N underlying aEven <N k
|
||||
reduced with lessRespectsAddition b halveDecreased
|
||||
... | bl rewrite a+b = identityOfIndiscernablesLeft _<N_ bl (Semiring.commutative ℕSemiring _ b)
|
||||
|
||||
0<b : 0 <N b
|
||||
0<b with TotalOrder.totality ℕTotalOrder 0 b
|
||||
0<b | inl (inl 0<b) = 0<b
|
||||
0<b | inl (inr ())
|
||||
0<b | inr 0=b rewrite equalityCommutative 0=b = exFalso (PartialOrder.irreflexive (TotalOrder.order ℕTotalOrder) {0} (identityOfIndiscernablesRight _<N_ 0<a (sqrt0 a pr)))
|
||||
|
||||
contr : False
|
||||
contr = indHyp (b +N underlying aEven) reduced b (underlying aEven) 0<b refl next3
|
||||
|
||||
evil : (a b : ℕ) → (0 <N a) → a *N a ≡ (b *N b) *N 2 → False
|
||||
evil a b 0<a = evil' (a +N b) a b 0<a refl
|
||||
|
||||
absNonneg : (x : ℕ) → abs (nonneg x) ≡ nonneg x
|
||||
absNonneg x with totality (nonneg 0) (nonneg x)
|
||||
absNonneg x | inl (inl 0<x) = refl
|
||||
absNonneg x | inr 0=x = refl
|
||||
|
||||
absNegsucc : (x : ℕ) → abs (negSucc x) ≡ nonneg (succ x)
|
||||
absNegsucc x with totality (nonneg 0) (negSucc x)
|
||||
absNegsucc x | inl (inr _) = refl
|
||||
|
||||
toNats : (numerator denominator : ℤ) → (denominator ≡ nonneg 0 → False) → (abs numerator) *Z (abs numerator) ≡ ((abs denominator) *Z (abs denominator)) *Z nonneg 2 → Sg (ℕ && ℕ) (λ nats → ((_&&_.fst nats *N _&&_.fst nats) ≡ (_&&_.snd nats *N _&&_.snd nats) *N 2) && (_&&_.snd nats ≡ 0 → False))
|
||||
toNats (nonneg num) (nonneg 0) pr _ = exFalso (pr refl)
|
||||
toNats (nonneg num) (nonneg (succ denom)) _ pr = (num ,, (succ denom)) , (nonnegInjective (transitivity (transitivity (equalityCommutative (absNonneg (num *N num))) (absRespectsTimes (nonneg num) (nonneg num))) pr) ,, λ ())
|
||||
toNats (nonneg num) (negSucc denom) _ pr = (num ,, succ denom) , (nonnegInjective (transitivity (transitivity (equalityCommutative (absNonneg (num *N num))) (absRespectsTimes (nonneg num) (nonneg num))) pr) ,, λ ())
|
||||
toNats (negSucc num) (nonneg (succ denom)) _ pr = (succ num ,, succ denom) , (nonnegInjective pr ,, λ ())
|
||||
toNats (negSucc num) (negSucc denom) _ pr = (succ num ,, succ denom) , (nonnegInjective pr ,, λ ())
|
||||
|
||||
sqrt2Irrational : (a : ℚ) → (a *Q a) =Q (injectionQ (nonneg 2)) → False
|
||||
sqrt2Irrational (numerator ,, (denominator , denom!=0)) pr = bad
|
||||
where
|
||||
-- We have in hand `pr`, which is the following (almost by definition):
|
||||
pr' : (numerator *Z numerator) ≡ (denominator *Z denominator) *Z nonneg 2
|
||||
pr' = transitivity (equalityCommutative (transitivity (Ring.*Commutative ℤRing) (Ring.identIsIdent ℤRing))) pr
|
||||
|
||||
-- Move into the naturals so that we can do nice divisibility things.
|
||||
lemma1 : abs ((denominator *Z denominator) *Z nonneg 2) ≡ (abs denominator *Z abs denominator) *Z nonneg 2
|
||||
lemma1 = transitivity (absRespectsTimes (denominator *Z denominator) (nonneg 2)) (applyEquality (_*Z nonneg 2) (absRespectsTimes denominator denominator))
|
||||
amenableToNaturals : (abs numerator) *Z (abs numerator) ≡ ((abs denominator) *Z (abs denominator)) *Z nonneg 2
|
||||
amenableToNaturals = transitivity (equalityCommutative (absRespectsTimes numerator numerator)) (transitivity (applyEquality abs pr') lemma1)
|
||||
|
||||
naturalsStatement : Sg (ℕ && ℕ) (λ nats → ((_&&_.fst nats *N _&&_.fst nats) ≡ (_&&_.snd nats *N _&&_.snd nats) *N 2) && (_&&_.snd nats ≡ 0 → False))
|
||||
naturalsStatement = toNats numerator denominator denom!=0 amenableToNaturals
|
||||
|
||||
bad : False
|
||||
bad with naturalsStatement
|
||||
bad | (num ,, 0) , (pr1 ,, pr2) = exFalso (pr2 refl)
|
||||
bad | (num ,, succ denom) , (pr1 ,, pr2) = evil num (succ denom) 0<num pr1
|
||||
where
|
||||
0<num : 0 <N num
|
||||
0<num with TotalOrder.totality ℕTotalOrder 0 num
|
||||
0<num | inl (inl 0<num) = 0<num
|
||||
0<num | inr 0=num rewrite equalityCommutative 0=num = exFalso (naughtE pr1)
|
||||
Reference in New Issue
Block a user