Browse Source

Some work on rationals.

gas-move-test
Thomas Kerber 6 months ago
parent
commit
437071102b
Signed by: Thomas Kerber <tk@drwx.org> GPG Key ID: 8489B911F9ED617B
1 changed files with 30 additions and 4 deletions
  1. 30
    4
      Yggdrasil/Rational.agda

+ 30
- 4
Yggdrasil/Rational.agda View File

@@ -3,23 +3,49 @@ module Yggdrasil.Rational where
3 3
 open import Data.Bool using (true; false; T)
4 4
 open import Data.Integer as ℤ using (ℤ; +_)
5 5
 open import Data.Nat as ℕ using (ℕ; suc; zero)
6
-open import Data.Nat.GCD using (GCD; gcd)
6
+open import Data.Nat.GCD as GCD using (GCD; gcd)
7 7
 open import Data.Nat.Divisibility using (_∣_; divides)
8
-open import Data.Nat.Coprimality using (coprime?; gcd-coprime)
8
+open import Data.Nat.Coprimality using (coprime?; gcd-coprime; Bézout-coprime)
9
+open import Data.Nat.Properties using (*-comm; *-assoc)
9 10
 open import Data.Product renaming (_,_ to ⟨_,_⟩)
10 11
 open import Data.Rational using (ℚ) renaming (_÷_ to _÷†_)
11 12
 open import Data.Unit using (⊤; tt)
12
-open import Data.Empty using (⊥)
13
+open import Data.Empty using (⊥; ⊥-elim)
13 14
 open import Data.Sign using (Sign) renaming (+ to s+; - to s-)
14 15
 open import Relation.Nullary using (yes; no; ¬_)
15 16
 open import Relation.Nullary.Decidable using (True; False; ⌊_⌋; fromWitness)
16
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
17
+import Relation.Binary.PropositionalEquality as Eq
18
+open Eq using (_≡_; _≢_; refl; subst₂; sym; cong)
19
+open Eq.≡-Reasoning using (_≡⟨_⟩_; _∎; begin_)
17 20
 
18 21
 open ℚ
19 22
 
20 23
 infixl 6 _+_ _-_
21 24
 infixl 7 _*_ _÷_
22 25
 
26
+1+≢*0 : ∀ x y → suc x ≢ y ℕ.* 0
27
+1+≢*0 x zero ()
28
+1+≢*0 x (suc y) = 1+≢*0 x y
29
+
30
+simp : ∀ x y-1 → ℚ
31
+simp x y-1 with GCD.Bézout.lemma x (suc y-1)
32
+... | GCD.Bézout.result 0 (GCD.is ⟨ _ , divides y′ y-eq ⟩ _) _ = ⊥-elim (1+≢*0 y-1 y′ y-eq)
33
+... | GCD.Bézout.result (suc d-1) (GCD.is ⟨ divides x′ x-eq , divides y′ y-eq ⟩ _) bézout = _÷†_ (+ x′) y′ {fromWitness {!(Bézout-coprime bézout′)!}}
34
+  where
35
+    y = suc y-1
36
+    d = suc d-1
37
+
38
+    bézout′ : GCD.Bézout.Identity d (x′ ℕ.* d) (y′ ℕ.* d)
39
+    bézout′ = subst₂ (GCD.Bézout.Identity d) x-eq y-eq bézout
40
+
41
+    eq-prf : x ℕ.* y′ ≡ x′ ℕ.* y
42
+    eq-prf = begin
43
+      x ℕ.* y′           ≡⟨ cong (λ z → z ℕ.* y′) x-eq ⟩
44
+      x′ ℕ.* d ℕ.* y′    ≡⟨ *-assoc x′ d y′ ⟩
45
+      x′ ℕ.* (d ℕ.* y′)  ≡⟨ sym (cong (ℕ._*_ x′) (*-comm y′ d)) ⟩
46
+      x′ ℕ.* (y′ ℕ.* d)  ≡⟨ sym (cong (ℕ._*_ x′) y-eq)  ⟩
47
+      x′ ℕ.* y           ∎
48
+
23 49
 postulate
24 50
   _÷_ : ℤ → (d : ℕ) → {d≢0 : False (d ℕ.≟ 0)} → ℚ
25 51
 

Loading…
Cancel
Save