如何在agda中添加兩個理性？

Question

如何添加兩個理性..我正在嘗試這個，但這是不正確的。因爲我無法證明這個coprime部分。

open import Data.Rational 
open import Data.Integer 
open import Data.Nat 

_add_ : ℚ -> ℚ -> ℚ 
x add y = (nx Data.Integer.* dy Data.Integer.+ dx Data.Integer.* ny) ÷ 
      (dx′ Data.Nat.* dy′) 
    where 
    nx = ℚ.numerator x 
    dx = ℚ.denominator x 
    dx′ = ℕ.suc (ℚ.denominator-1 x) 

    ny = ℚ.numerator y 
    dy = ℚ.denominator y 
    dy′ = ℕ.suc (ℚ.denominator-1 y) 

Answer 1

您需要簡化(nx * dy + dx * ny)/(dx * dy)以確保其分子和分母是coprimes。

以下代碼通過簡化一對自然數x和suc y-1（即非零y）向您顯示解決方案的核心。擴展它來處理分子的跡象應該是一個簡單的練習。繁重的工作由Data.Nat.Coprimality.Bézout-coprime完成。

open import Data.Nat 
open import Data.Nat.GCD 
open import Data.Nat.Coprimality hiding (sym) 
open import Relation.Binary.PropositionalEquality 
open import Data.Product 
open import Data.Nat.Divisibility 
open import Data.Empty 

record Simp (x : ℕ) (y : ℕ) : Set where 
    constructor MkSimp 
    field 
    x′ y′ : ℕ 
    eq-prf : x * y′ ≡ x′ * y 
    coprime-prf : Coprime x′ y′ 

1+≢*0 : ∀ x y → suc x ≢ y * 0 
1+≢*0 x zero() 
1+≢*0 x (suc y) = 1+≢*0 x y 

simp : ∀ x y-1 → Simp x (suc y-1) 
simp x y-1 with Bézout.lemma x (suc y-1) 
simp x y-1 | Bézout.result 0 (GCD.is (_ , divides y′ y-eq) _) _ = ⊥-elim (1+≢*0 y-1 y′ y-eq) 
simp x y-1 | Bézout.result (suc d-1) (GCD.is (divides x′ x-eq , divides y′ y-eq) _) bézout = MkSimp x′ y′ eq-prf (Bézout-coprime bézout′) 
    where 
    y = suc y-1 
    d = suc d-1 

    bézout′ : Bézout.Identity d (x′ * d) (y′ * d) 
    bézout′ = subst₂ (Bézout.Identity d) x-eq y-eq bézout 

    open Relation.Binary.PropositionalEquality.≡-Reasoning 
    open import Data.Nat.Properties.Simple 

    eq-prf : x * y′ ≡ x′ * y 
    eq-prf = begin 
     x * y′   ≡⟨ cong (λ z → z * y′) x-eq ⟩ 
     x′ * d * y′ ≡⟨ *-assoc x′ d y′ ⟩ 
     x′ * (d * y′) ≡⟨ sym (cong (_*_ x′) (*-comm y′ d)) ⟩ 
     x′ * (y′ * d) ≡⟨ sym (cong (_*_ x′) y-eq) ⟩ 
     x′ * y   ∎