Browse Source

Some garbage.

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

+ 72
- 0
Yggdrasil/Rational.agda View File

@@ -0,0 +1,72 @@
1
+module Yggdrasil.Rational where
2
+
3
+open import Data.Bool using (true; false; T)
4
+open import Data.Integer using (ℤ; ∣_∣; _◃_; sign; +_) renaming (_+_ to _ℤ+_; _*_ to _ℤ*_)
5
+open import Data.Nat as ℕ using (ℕ; suc; zero) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
6
+open import Data.Nat.GCD using (GCD; gcd)
7
+open import Data.Nat.Divisibility using (_∣_; divides)
8
+open import Data.Nat.Coprimality using (coprime?; gcd-coprime)
9
+open import Data.Product renaming (_,_ to ⟨_,_⟩)
10
+open import Data.Rational using (ℚ; _÷_)
11
+open import Data.Unit using (⊤; tt)
12
+open import Data.Empty using (⊥)
13
+open import Data.Sign using (Sign) renaming (+ to s+; - to s-)
14
+open import Relation.Nullary using (yes; no; ¬_)
15
+open import Relation.Nullary.Decidable using (True; False; ⌊_⌋; fromWitness)
16
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
17
+
18
+open ℚ
19
+
20
+¬0*¬0≡¬0 : {a b : ℕ} → ¬ (a ≡ 0) → ¬ (b ≡ 0) → ¬ (a ℕ* b ≡ 0)
21
+¬0*¬0≡¬0 = ?
22
+
23
+¬0≡¬0*¬0 : {a b : ℕ} → ¬ (0 ≡ a ℕ* b) → ¬ (b ≡ 0)
24
+¬0≡¬0*¬0 = ?
25
+
26
+_+_ : ℚ → ℚ → ℚ
27
+a + b with gcd (suc (denominator-1 a)) (suc (denominator-1 b))
28
+... | ⟨ c , denom-gcd ⟩ with GCD.commonDivisor denom-gcd
29
+...   | ⟨ divides d₁ d₁*c≡da , divides d₂ d₂*c≡db ⟩ = let
30
+        d′ = d₁ ℕ* d₂ ℕ* c
31
+        n′ = ((numerator a) ℤ* (+ d₂)) ℤ+ ((numerator b) ℤ* (+ d₁))
32
+        d′≢0 = ?
33
+      in _÷_ n′ d′
34
+        {fromWitness (λ{ {i} ⟨ i∣n′ , i∣d′ ⟩ → 
35
+          -- Coprime because: d₁ coprime d₂, d₁ coprime n₁, d₂ coprime n₂, n₁,
36
+          -- n₂ coprime c
37
+          ?})}
38
+        {?}
39
+
40
+
41
+_*_ : ℚ → ℚ → ℚ
42
+a * b = ?
43
+
44
+_-_ : ℚ → ℚ → ℚ
45
+a - b = ?
46
+
47
+--data ℚ′ : Set where
48
+--  _÷′_ : ℤ → (d : ℕ) → {d≢0 : False (d ℕ.≟ 0)} → ℚ′
49
+--
50
+--∣◃∣-≡ : (n : ℕ) → (s : Sign) → ∣ s ◃ n ∣ ≡ n
51
+--∣◃∣-≡ = ?
52
+--
53
+--normalise : ℚ′ → ℚ
54
+--normalise (_÷′_ n zero {()})
55
+--normalise (n ÷′ suc d) with gcd ∣ n ∣ (suc d)
56
+----... | ⟨ 1 , gcd ⟩ = record
57
+----  { numerator = n
58
+----  ; denominator-1 = d
59
+----  ; isCoprime = fromWitness {Q = coprime? ∣ n ∣ (suc d)} (gcd-coprime gcd) }
60
+--... | ⟨ _ , gcd₁ ⟩ with GCD.commonDivisor gcd₁
61
+--...   | ⟨ divides n′ _ , divides d′ _ ⟩ with d′ | gcd n′ d′ | sign n
62
+--...     | suc d′ | ⟨ suc (suc m) , gcd₂ ⟩ | _ = ?
63
+--...     | suc d′ | ⟨ 1 , gcd₂ ⟩ | s+ = record
64
+--            { numerator = + n′
65
+--            ; denominator-1 = d′
66
+--            ; isCoprime = fromWitness {Q = coprime? n′ (suc d′)} (gcd-coprime gcd₂) }
67
+--with coprime? ∣ n ∣ (suc d)
68
+--... | yes cp = record
69
+--  { numerator = n
70
+--  ; denominator-1 = d
71
+--  ; isCoprime = fromWitness {Q = coprime? ∣ n ∣ (suc d)} cp }
72
+--... | no ¬cp = ?

Loading…
Cancel
Save