diff options
Diffstat (limited to 'src/Helium/Data/Pseudocode')
| -rw-r--r-- | src/Helium/Data/Pseudocode/Core.agda | 84 | ||||
| -rw-r--r-- | src/Helium/Data/Pseudocode/Types.agda | 264 |
2 files changed, 47 insertions, 301 deletions
diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda index 7b21824..a63cc39 100644 --- a/src/Helium/Data/Pseudocode/Core.agda +++ b/src/Helium/Data/Pseudocode/Core.agda @@ -8,9 +8,10 @@ module Helium.Data.Pseudocode.Core where -open import Data.Bool using (Bool) +open import Data.Bool using (Bool; true; false) open import Data.Fin using (Fin; #_) -open import Data.Nat as ℕ using (ℕ; suc) +open import Data.Nat as ℕ using (ℕ; zero; suc) +open import Data.Nat.Properties using (+-comm) open import Data.Product using (∃; _,_; proj₂; uncurry) open import Data.Vec using (Vec; []; _∷_; lookup; map) open import Data.Vec.Relation.Unary.All using (All; []; _∷_; reduce; all?) @@ -29,7 +30,6 @@ data Type : Set where fin : (n : ℕ) → Type real : Type bits : (n : ℕ) → Type - enum : (n : ℕ) → Type tuple : ∀ n → Vec Type n → Type array : Type → (n : ℕ) → Type @@ -42,7 +42,6 @@ data HasEquality : Type → Set where fin : ∀ {n} → HasEquality (fin n) real : HasEquality real bits : ∀ {n} → HasEquality (bits n) - enum : ∀ {n} → HasEquality (enum n) hasEquality? : Decidable HasEquality hasEquality? unit = no (λ ()) @@ -51,7 +50,6 @@ hasEquality? int = yes int hasEquality? (fin n) = yes fin hasEquality? real = yes real hasEquality? (bits n) = yes bits -hasEquality? (enum n) = yes enum hasEquality? (tuple n x) = no (λ ()) hasEquality? (array t n) = no (λ ()) @@ -66,7 +64,6 @@ isNumeric? int = yes int isNumeric? real = yes real isNumeric? (fin n) = no (λ ()) isNumeric? (bits n) = no (λ ()) -isNumeric? (enum n) = no (λ ()) isNumeric? (tuple n x) = no (λ ()) isNumeric? (array t n) = no (λ ()) @@ -95,8 +92,7 @@ data Literal : Type → Set where _′f : ∀ {n} → Fin n → Literal (fin n) _′r : ℕ → Literal real _′x : ∀ {n} → Vec Bool n → Literal (bits n) - _′e : ∀ {n} → Fin n → Literal (enum n) - _′a : ∀ {n t} → Vec (Literal t) n → Literal (array t n) + _′a : ∀ {n t} → Literal t → Literal (array t n) --- Expressions, references, statements, functions and procedures @@ -111,7 +107,8 @@ module Code {o} (Σ : Vec Type o) where infix 8 -_ infixr 7 _^_ - infixl 6 _*_ _/_ _and_ + infixl 6 _*_ _and_ _>>_ + -- infixl 6 _/_ infixl 5 _+_ _or_ _&&_ _||_ _∶_ infix 4 _≟_ _<?_ @@ -130,42 +127,37 @@ module Code {o} (Σ : Vec Type o) where _or_ : ∀ {n} → Expression Γ (bits n) → Expression Γ (bits n) → Expression Γ (bits n) [_] : ∀ {t} → Expression Γ t → Expression Γ (array t 1) unbox : ∀ {t} → Expression Γ (array t 1) → Expression Γ t - _∶_ : ∀ {m n t} → Expression Γ (asType t m) → Expression Γ (asType t n) → Expression Γ (asType t (m ℕ.+ n)) + _∶_ : ∀ {m n t} → Expression Γ (asType t m) → Expression Γ (asType t n) → Expression Γ (asType t (n ℕ.+ m)) slice : ∀ {i j t} → Expression Γ (asType t (i ℕ.+ j)) → Expression Γ (fin (suc i)) → Expression Γ (asType t j) cast : ∀ {i j t} → .(eq : i ≡ j) → Expression Γ (asType t i) → Expression Γ (asType t j) -_ : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → Expression Γ t _+_ : ∀ {t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ {isNumeric₁} {isNumeric₂}) _*_ : ∀ {t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ {isNumeric₁} {isNumeric₂}) - _/_ : Expression Γ real → Expression Γ real → Expression Γ real - _^_ : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → Expression Γ int → Expression Γ t - sint : ∀ {n} → Expression Γ (bits n) → Expression Γ int - uint : ∀ {n} → Expression Γ (bits n) → Expression Γ int + -- _/_ : Expression Γ real → Expression Γ real → Expression Γ real + _^_ : ∀ {t} {isNumeric : True (isNumeric? t)} → Expression Γ t → ℕ → Expression Γ t + _>>_ : Expression Γ int → ℕ → Expression Γ int rnd : Expression Γ real → Expression Γ int - get : ℕ → Expression Γ int → Expression Γ bit + -- get : ℕ → Expression Γ int → Expression Γ bit fin : ∀ {k ms n} → (All (Fin) ms → Fin n) → Expression Γ (tuple k (map fin ms)) → Expression Γ (fin n) asInt : ∀ {n} → Expression Γ (fin n) → Expression Γ int tup : ∀ {m ts} → All (Expression Γ) ts → Expression Γ (tuple m ts) - head : ∀ {m t ts} → Expression Γ (tuple (suc m) (t ∷ ts)) → Expression Γ t - tail : ∀ {m t ts} → Expression Γ (tuple (suc m) (t ∷ ts)) → Expression Γ (tuple m ts) call : ∀ {t m Δ} → Function Δ t → Expression Γ (tuple m Δ) → Expression Γ t if_then_else_ : ∀ {t} → Expression Γ bool → Expression Γ t → Expression Γ t → Expression Γ t data CanAssign {n} {Γ} where - state : ∀ {i} {i<o : True (i ℕ.<? o)} → CanAssign (state i {i<o}) - var : ∀ {i} {i<n : True (i ℕ.<? n)} → CanAssign (var i {i<n}) + state : ∀ i {i<o : True (i ℕ.<? o)} → CanAssign (state i {i<o}) + var : ∀ i {i<n : True (i ℕ.<? n)} → CanAssign (var i {i<n}) abort : ∀ {t} {e : Expression Γ (fin 0)} → CanAssign (abort {t = t} e) _∶_ : ∀ {m n t} {e₁ : Expression Γ (asType t m)} {e₂ : Expression Γ (asType t n)} → CanAssign e₁ → CanAssign e₂ → CanAssign (e₁ ∶ e₂) [_] : ∀ {t} {e : Expression Γ t} → CanAssign e → CanAssign [ e ] unbox : ∀ {t} {e : Expression Γ (array t 1)} → CanAssign e → CanAssign (unbox e) - slice : ∀ {i j t} {e₁ : Expression Γ (asType t (i ℕ.+ j))} {e₂ : Expression Γ (fin (suc i))} → CanAssign e₁ → CanAssign (slice e₁ e₂) - cast : ∀ {i j t} {e : Expression Γ (asType t i)} .{eq : i ≡ j} → CanAssign e → CanAssign (cast eq e) + slice : ∀ {i j t} {e₁ : Expression Γ (asType t (i ℕ.+ j))} → CanAssign e₁ → (e₂ : Expression Γ (fin (suc i))) → CanAssign (slice e₁ e₂) + cast : ∀ {i j t} {e : Expression Γ (asType t i)} .(eq : i ≡ j) → CanAssign e → CanAssign (cast eq e) tup : ∀ {m ts} {es : All (Expression Γ) {m} ts} → All (CanAssign ∘ proj₂) (reduce (λ {x} e → x , e) es) → CanAssign (tup es) - head : ∀ {m t ts} {e : Expression Γ (tuple (suc m) (t ∷ ts))} → CanAssign e → CanAssign (head e) - tail : ∀ {m t ts} {e : Expression Γ (tuple (suc m) (t ∷ ts))} → CanAssign e → CanAssign (tail e) canAssign? (lit x) = no λ () - canAssign? (state i) = yes state - canAssign? (var i) = yes var + canAssign? (state i) = yes (state i) + canAssign? (var i) = yes (var i) canAssign? (abort e) = yes abort canAssign? (e ≟ e₁) = no λ () canAssign? (e <? e₁) = no λ () @@ -178,22 +170,19 @@ module Code {o} (Σ : Vec Type o) where canAssign? [ e ] = map′ [_] (λ { [ e ] → e }) (canAssign? e) canAssign? (unbox e) = map′ unbox (λ { (unbox e) → e }) (canAssign? e) canAssign? (e ∶ e₁) = map′ (uncurry _∶_) (λ { (e ∶ e₁) → e , e₁ }) (canAssign? e ×-dec canAssign? e₁) - canAssign? (slice e e₁) = map′ slice (λ { (slice e) → e }) (canAssign? e) - canAssign? (cast eq e) = map′ cast (λ { (cast e) → e }) (canAssign? e) + canAssign? (slice e e₁) = map′ (λ e → slice e e₁) (λ { (slice e e₁) → e }) (canAssign? e) + canAssign? (cast eq e) = map′ (cast eq) (λ { (cast eq e) → e }) (canAssign? e) canAssign? (- e) = no λ () canAssign? (e + e₁) = no λ () canAssign? (e * e₁) = no λ () - canAssign? (e / e₁) = no λ () + -- canAssign? (e / e₁) = no λ () canAssign? (e ^ e₁) = no λ () - canAssign? (sint e) = no λ () - canAssign? (uint e) = no λ () + canAssign? (e >> e₁) = no λ () canAssign? (rnd e) = no λ () - canAssign? (get x e) = no λ () + -- canAssign? (get x e) = no λ () canAssign? (fin x e) = no λ () canAssign? (asInt e) = no λ () canAssign? (tup es) = map′ tup (λ { (tup es) → es }) (canAssignAll? es) - canAssign? (head e) = map′ head (λ { (head e) → e }) (canAssign? e) - canAssign? (tail e) = map′ tail (λ { (tail e) → e }) (canAssign? e) canAssign? (call x e) = no λ () canAssign? (if e then e₁ else e₂) = no λ () @@ -222,13 +211,34 @@ module Code {o} (Σ : Vec Type o) where _∙end : Statement Γ unit → Procedure Γ declare : ∀ {t} → Expression Γ t → Procedure (t ∷ Γ) → Procedure Γ - infixl 6 _<<_ _>>_ + infixl 6 _<<_ infixl 5 _-_ + + slice′ : ∀ {n Γ i j t} → Expression {n} Γ (asType t (i ℕ.+ j)) → Expression Γ (fin (suc j)) → Expression Γ (asType t i) + slice′ {i = i} e₁ e₂ = slice (cast (+-comm i _) e₁) e₂ + _-_ : ∀ {n Γ t₁ t₂} {isNumeric₁ : True (isNumeric? t₁)} {isNumeric₂ : True (isNumeric? t₂)} → Expression {n} Γ t₁ → Expression Γ t₂ → Expression Γ (combineNumeric t₁ t₂ {isNumeric₁} {isNumeric₂}) _-_ {isNumeric₂ = isNumeric₂} x y = x + (-_ {isNumeric = isNumeric₂} y) - _<<_ : ∀ {n Γ} → Expression {n} Γ int → Expression Γ int → Expression Γ int + _<<_ : ∀ {n Γ} → Expression {n} Γ int → ℕ → Expression Γ int x << n = rnd (x * lit (2 ′r) ^ n) - _>>_ : ∀ {n Γ} → Expression {n} Γ int → Expression Γ int → Expression Γ int - x >> n = rnd (x * lit (2 ′r) ^ - n) + get : ∀ {n Γ} → ℕ → Expression {n} Γ int → Expression Γ bit + get i x = if x - x >> suc i << suc i <? lit (2 ′i) ^ i then lit ((false ∷ []) ′x) else lit ((true ∷ []) ′x) + + uint : ∀ {n Γ m} → Expression {n} Γ (bits m) → Expression Γ int + uint {m = zero} x = lit (0 ′i) + uint {m = suc m} x = + lit (2 ′i) * uint {m = m} (slice x (lit ((# 1) ′f))) + + ( if slice′ x (lit ((# 0) ′f)) ≟ lit ((true ∷ []) ′x) + then lit (1 ′i) + else lit (0 ′i)) + + sint : ∀ {n Γ m} → Expression {n} Γ (bits m) → Expression Γ int + sint {m = zero} x = lit (0 ′i) + sint {m = suc zero} x = if x ≟ lit ((true ∷ []) ′x) then - lit (1 ′i) else lit (0 ′i) + sint {m = suc (suc m)} x = + lit (2 ′i) * sint (slice {i = 1} x (lit ((# 1) ′f))) + + ( if slice′ x (lit ((# 0) ′f)) ≟ lit ((true ∷ []) ′x) + then lit (1 ′i) + else lit (0 ′i)) diff --git a/src/Helium/Data/Pseudocode/Types.agda b/src/Helium/Data/Pseudocode/Types.agda index a545ddc..971ca12 100644 --- a/src/Helium/Data/Pseudocode/Types.agda +++ b/src/Helium/Data/Pseudocode/Types.agda @@ -77,82 +77,6 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ _/1 : ℤ → ℝ ⌊_⌋ : ℝ → ℤ - cast : ∀ {m n} → .(eq : m ≡ n) → Bits m → Bits n - cast eq x i = x $ Fin.cast (P.sym eq) i - - 2ℤ : ℤ - 2ℤ = 2 ℤ′.×′ 1ℤ - - getᵇ : ∀ {n} → Fin n → Bits n → Bit - getᵇ i x = x (opposite i) - - setᵇ : ∀ {n} → Fin n → Bit → Op₁ (Bits n) - setᵇ i b = updateAt (opposite i) λ _ → b - - sliceᵇ : ∀ {n} (i : Fin (suc n)) j → Bits n → Bits (toℕ (i - j)) - sliceᵇ zero zero x = [] - sliceᵇ {suc n} (suc i) zero x = getᵇ i x ∷ sliceᵇ i zero (tail x) - sliceᵇ {suc n} (suc i) (suc j) x = sliceᵇ i j (tail x) - - updateᵇ : ∀ {n} (i : Fin (suc n)) j → Bits (toℕ (i - j)) → Op₁ (Bits n) - updateᵇ {n} = Induction.<-weakInduction P (λ _ _ → id) helper - where - P : Fin (suc n) → Set b₁ - P i = ∀ j → Bits (toℕ (i - j)) → Op₁ (Bits n) - - eq : ∀ {n} {i : Fin n} → toℕ i ≡ toℕ (inject₁ i) - eq = P.sym $ Fₚ.toℕ-inject₁ _ - - eq′ : ∀ {n} {i : Fin n} j → toℕ (i - j) ≡ toℕ (inject₁ i - Fin.cast eq j) - eq′ zero = eq - eq′ {i = suc _} (suc j) = eq′ j - - helper : ∀ i → P (inject₁ i) → P (suc i) - helper i rec zero y = rec zero (cast eq (tail y)) ∘′ setᵇ i (y zero) - helper i rec (suc j) y = rec (Fin.cast eq j) (cast (eq′ j) y) - - hasBit : ∀ {n} → Fin n → Bits n → Bool - hasBit i x = does (getᵇ i x ≟ᵇ₁ 1𝔹) - - infixl 7 _div_ _mod_ - - _div_ : ∀ (x y : ℤ) → {y≉0 : False (y /1 ≟ʳ 0ℝ)} → ℤ - (x div y) {y≉0} = ⌊ x /1 ℝ.* toWitnessFalse y≉0 ℝ.⁻¹ ⌋ - - _mod_ : ∀ (x y : ℤ) → {y≉0 : False (y /1 ≟ʳ 0ℝ)} → ℤ - (x mod y) {y≉0} = x ℤ.+ ℤ.- y ℤ.* (x div y) {y≉0} - - infixl 5 _<<_ - _<<_ : ℤ → ℕ → ℤ - x << n = 2ℤ ℤ′.^′ n ℤ.* x - - module ShiftNotZero - (1<<n≉0 : ∀ n → False ((1ℤ << n) /1 ≟ʳ 0ℝ)) - where - - infixl 5 _>>_ - _>>_ : ℤ → ℕ → ℤ - x >> zero = x - x >> suc n = (x div (1ℤ << suc n)) {1<<n≉0 (suc n)} - - getᶻ : ℕ → ℤ → Bit - getᶻ n x = - if does ((x mod (1ℤ << suc n)) {1<<n≉0 (suc n)} <ᶻ? 1ℤ << n) - then 1𝔹 - else 0𝔹 - - sliceᶻ : ∀ n i → ℤ → Bits (n ℕ-ℕ i) - sliceᶻ zero zero x = [] - sliceᶻ (suc n) zero x = getᶻ n x ∷ sliceᶻ n zero x - sliceᶻ (suc n) (suc i) x = sliceᶻ n i (x >> 1) - - uint : ∀ {n} → Bits n → ℤ - uint x = ℤ′.sum λ i → if hasBit i x then 1ℤ << toℕ i else 0ℤ - - sint : ∀ {n} → Bits n → ℤ - sint {zero} x = 0ℤ - sint {suc n} x = uint x ℤ.+ ℤ.- (if hasBit (fromℕ n) x then 1ℤ << suc n else 0ℤ) - record Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ ⊔ b₂ ⊔ i₁ ⊔ i₂ ⊔ i₃ ⊔ r₁ ⊔ r₂ ⊔ r₃)) where field @@ -222,191 +146,3 @@ record Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : ; _/1 = _/1 ; ⌊_⌋ = ⌊_⌋ } - - open RawPseudocode rawPseudocode public - using - ( 2ℤ; cast; getᵇ; setᵇ; sliceᵇ; updateᵇ; hasBit - ; _div_; _mod_; _<<_; uint; sint - ) - - private - -- FIXME: move almost all of these proofs into a separate module - a<b⇒ca<cb : ∀ {a b c} → 0ℤ ℤ.< c → a ℤ.< b → c ℤ.* a ℤ.< c ℤ.* b - a<b⇒ca<cb {a} {b} {c} 0<c a<b = begin-strict - c ℤ.* a ≈˘⟨ ℤ.+-identityʳ _ ⟩ - c ℤ.* a ℤ.+ 0ℤ <⟨ ℤ.+-invariantˡ _ $ ℤ.0<a+0<b⇒0<ab 0<c 0<b-a ⟩ - c ℤ.* a ℤ.+ c ℤ.* (b ℤ.- a) ≈˘⟨ ℤ.distribˡ c a (b ℤ.- a) ⟩ - c ℤ.* (a ℤ.+ (b ℤ.- a)) ≈⟨ ℤ.*-congˡ $ ℤ.+-congˡ $ ℤ.+-comm b (ℤ.- a) ⟩ - c ℤ.* (a ℤ.+ (ℤ.- a ℤ.+ b)) ≈˘⟨ ℤ.*-congˡ $ ℤ.+-assoc a (ℤ.- a) b ⟩ - c ℤ.* ((a ℤ.+ ℤ.- a) ℤ.+ b) ≈⟨ ℤ.*-congˡ $ ℤ.+-congʳ $ ℤ.-‿inverseʳ a ⟩ - c ℤ.* (0ℤ ℤ.+ b) ≈⟨ (ℤ.*-congˡ $ ℤ.+-identityˡ b) ⟩ - c ℤ.* b ∎ - where - open ℤ-Reasoning - - 0<b-a : 0ℤ ℤ.< b ℤ.- a - 0<b-a = begin-strict - 0ℤ ≈˘⟨ ℤ.-‿inverseʳ a ⟩ - a ℤ.- a <⟨ ℤ.+-invariantʳ (ℤ.- a) a<b ⟩ - b ℤ.- a ∎ - - -‿idem : ∀ x → ℤ.- (ℤ.- x) ℤ.≈ x - -‿idem x = begin-equality - ℤ.- (ℤ.- x) ≈˘⟨ ℤ.+-identityˡ _ ⟩ - 0ℤ ℤ.- ℤ.- x ≈˘⟨ ℤ.+-congʳ $ ℤ.-‿inverseʳ x ⟩ - x ℤ.- x ℤ.- ℤ.- x ≈⟨ ℤ.+-assoc x (ℤ.- x) _ ⟩ - x ℤ.+ (ℤ.- x ℤ.- ℤ.- x) ≈⟨ ℤ.+-congˡ $ ℤ.-‿inverseʳ (ℤ.- x) ⟩ - x ℤ.+ 0ℤ ≈⟨ ℤ.+-identityʳ x ⟩ - x ∎ - where open ℤ-Reasoning - - -a*b≈-ab : ∀ a b → ℤ.- a ℤ.* b ℤ.≈ ℤ.- (a ℤ.* b) - -a*b≈-ab a b = begin-equality - ℤ.- a ℤ.* b ≈˘⟨ ℤ.+-identityʳ _ ⟩ - ℤ.- a ℤ.* b ℤ.+ 0ℤ ≈˘⟨ ℤ.+-congˡ $ ℤ.-‿inverseʳ _ ⟩ - ℤ.- a ℤ.* b ℤ.+ (a ℤ.* b ℤ.- a ℤ.* b) ≈˘⟨ ℤ.+-assoc _ _ _ ⟩ - ℤ.- a ℤ.* b ℤ.+ a ℤ.* b ℤ.- a ℤ.* b ≈˘⟨ ℤ.+-congʳ $ ℤ.distribʳ b _ a ⟩ - (ℤ.- a ℤ.+ a) ℤ.* b ℤ.- a ℤ.* b ≈⟨ ℤ.+-congʳ $ ℤ.*-congʳ $ ℤ.-‿inverseˡ a ⟩ - 0ℤ ℤ.* b ℤ.- a ℤ.* b ≈⟨ ℤ.+-congʳ $ ℤ.zeroˡ b ⟩ - 0ℤ ℤ.- a ℤ.* b ≈⟨ ℤ.+-identityˡ _ ⟩ - ℤ.- (a ℤ.* b) ∎ - where open ℤ-Reasoning - - a*-b≈-ab : ∀ a b → a ℤ.* ℤ.- b ℤ.≈ ℤ.- (a ℤ.* b) - a*-b≈-ab a b = begin-equality - a ℤ.* ℤ.- b ≈⟨ ℤ.*-comm a (ℤ.- b) ⟩ - ℤ.- b ℤ.* a ≈⟨ -a*b≈-ab b a ⟩ - ℤ.- (b ℤ.* a) ≈⟨ ℤ.-‿cong $ ℤ.*-comm b a ⟩ - ℤ.- (a ℤ.* b) ∎ - where open ℤ-Reasoning - - 0<a⇒0>-a : ∀ {a} → 0ℤ ℤ.< a → 0ℤ ℤ.> ℤ.- a - 0<a⇒0>-a {a} 0<a = begin-strict - ℤ.- a ≈˘⟨ ℤ.+-identityˡ _ ⟩ - 0ℤ ℤ.- a <⟨ ℤ.+-invariantʳ _ 0<a ⟩ - a ℤ.- a ≈⟨ ℤ.-‿inverseʳ a ⟩ - 0ℤ ∎ - where open ℤ-Reasoning - - 0>a⇒0<-a : ∀ {a} → 0ℤ ℤ.> a → 0ℤ ℤ.< ℤ.- a - 0>a⇒0<-a {a} 0>a = begin-strict - 0ℤ ≈˘⟨ ℤ.-‿inverseʳ a ⟩ - a ℤ.- a <⟨ ℤ.+-invariantʳ _ 0>a ⟩ - 0ℤ ℤ.- a ≈⟨ ℤ.+-identityˡ _ ⟩ - ℤ.- a ∎ - where open ℤ-Reasoning - - 0<-a⇒0>a : ∀ {a} → 0ℤ ℤ.< ℤ.- a → 0ℤ ℤ.> a - 0<-a⇒0>a {a} 0<-a = begin-strict - a ≈˘⟨ ℤ.+-identityʳ a ⟩ - a ℤ.+ 0ℤ <⟨ ℤ.+-invariantˡ a 0<-a ⟩ - a ℤ.- a ≈⟨ ℤ.-‿inverseʳ a ⟩ - 0ℤ ∎ - where open ℤ-Reasoning - - 0>-a⇒0<a : ∀ {a} → 0ℤ ℤ.> ℤ.- a → 0ℤ ℤ.< a - 0>-a⇒0<a {a} 0>-a = begin-strict - 0ℤ ≈˘⟨ ℤ.-‿inverseʳ a ⟩ - a ℤ.- a <⟨ ℤ.+-invariantˡ a 0>-a ⟩ - a ℤ.+ 0ℤ ≈⟨ ℤ.+-identityʳ a ⟩ - a ∎ - where open ℤ-Reasoning - - 0>a+0<b⇒0>ab : ∀ {a b} → 0ℤ ℤ.> a → 0ℤ ℤ.< b → 0ℤ ℤ.> a ℤ.* b - 0>a+0<b⇒0>ab {a} {b} 0>a 0<b = 0<-a⇒0>a $ begin-strict - 0ℤ <⟨ ℤ.0<a+0<b⇒0<ab (0>a⇒0<-a 0>a) 0<b ⟩ - ℤ.- a ℤ.* b ≈⟨ -a*b≈-ab a b ⟩ - ℤ.- (a ℤ.* b) ∎ - where open ℤ-Reasoning - - 0<a+0>b⇒0>ab : ∀ {a b} → 0ℤ ℤ.< a → 0ℤ ℤ.> b → 0ℤ ℤ.> a ℤ.* b - 0<a+0>b⇒0>ab {a} {b} 0<a 0>b = 0<-a⇒0>a $ begin-strict - 0ℤ <⟨ ℤ.0<a+0<b⇒0<ab 0<a (0>a⇒0<-a 0>b) ⟩ - a ℤ.* ℤ.- b ≈⟨ a*-b≈-ab a b ⟩ - ℤ.- (a ℤ.* b) ∎ - where open ℤ-Reasoning - - 0>a+0>b⇒0<ab : ∀ {a b} → 0ℤ ℤ.> a → 0ℤ ℤ.> b → 0ℤ ℤ.< a ℤ.* b - 0>a+0>b⇒0<ab {a} {b} 0>a 0>b = begin-strict - 0ℤ <⟨ ℤ.0<a+0<b⇒0<ab (0>a⇒0<-a 0>a) (0>a⇒0<-a 0>b) ⟩ - ℤ.- a ℤ.* ℤ.- b ≈⟨ -a*b≈-ab a (ℤ.- b) ⟩ - ℤ.- (a ℤ.* ℤ.- b) ≈⟨ ℤ.-‿cong $ a*-b≈-ab a b ⟩ - ℤ.- (ℤ.- (a ℤ.* b)) ≈⟨ -‿idem (a ℤ.* b) ⟩ - a ℤ.* b ∎ - where open ℤ-Reasoning - - a≉0+b≉0⇒ab≉0 : ∀ {a b} → a ℤ.≉ 0ℤ → b ℤ.≉ 0ℤ → a ℤ.* b ℤ.≉ 0ℤ - a≉0+b≉0⇒ab≉0 {a} {b} a≉0 b≉0 ab≈0 with ℤ.compare a 0ℤ | ℤ.compare b 0ℤ - ... | tri< a<0 _ _ | tri< b<0 _ _ = ℤ.irrefl (ℤ.Eq.sym ab≈0) $ 0>a+0>b⇒0<ab a<0 b<0 - ... | tri< a<0 _ _ | tri≈ _ b≈0 _ = b≉0 b≈0 - ... | tri< a<0 _ _ | tri> _ _ b>0 = ℤ.irrefl ab≈0 $ 0>a+0<b⇒0>ab a<0 b>0 - ... | tri≈ _ a≈0 _ | _ = a≉0 a≈0 - ... | tri> _ _ a>0 | tri< b<0 _ _ = ℤ.irrefl ab≈0 $ 0<a+0>b⇒0>ab a>0 b<0 - ... | tri> _ _ a>0 | tri≈ _ b≈0 _ = b≉0 b≈0 - ... | tri> _ _ a>0 | tri> _ _ b>0 = ℤ.irrefl (ℤ.Eq.sym ab≈0) $ ℤ.0<a+0<b⇒0<ab a>0 b>0 - - ab≈0⇒a≈0⊎b≈0 : ∀ {a b} → a ℤ.* b ℤ.≈ 0ℤ → a ℤ.≈ 0ℤ ⊎ b ℤ.≈ 0ℤ - ab≈0⇒a≈0⊎b≈0 {a} {b} ab≈0 with a ℤ.≟ 0ℤ | b ℤ.≟ 0ℤ - ... | yes a≈0 | _ = inj₁ a≈0 - ... | no a≉0 | yes b≈0 = inj₂ b≈0 - ... | no a≉0 | no b≉0 = ⊥-elim (a≉0+b≉0⇒ab≉0 a≉0 b≉0 ab≈0) - - 2a<<n≈a<<1+n : ∀ a n → 2ℤ ℤ.* (a << n) ℤ.≈ a << suc n - 2a<<n≈a<<1+n a zero = ℤ.*-congˡ $ ℤ.*-identityˡ a - 2a<<n≈a<<1+n a (suc n) = begin-equality - 2ℤ ℤ.* (a << suc n) ≈˘⟨ ℤ.*-assoc 2ℤ _ a ⟩ - (2ℤ ℤ.* _) ℤ.* a ≈⟨ ℤ.*-congʳ $ ℤ.*-comm 2ℤ _ ⟩ - a << suc (suc n) ∎ - where open ℤ-Reasoning - - 0<1 : 0ℤ ℤ.< 1ℤ - 0<1 with ℤ.compare 0ℤ 1ℤ - ... | tri< 0<1 _ _ = 0<1 - ... | tri≈ _ 0≈1 _ = ⊥-elim (1≉0 (ℤ.Eq.sym 0≈1)) - ... | tri> _ _ 0>1 = begin-strict - 0ℤ ≈˘⟨ ℤ.zeroʳ (ℤ.- 1ℤ) ⟩ - ℤ.- 1ℤ ℤ.* 0ℤ <⟨ a<b⇒ca<cb (0>a⇒0<-a 0>1) (0>a⇒0<-a 0>1) ⟩ - ℤ.- 1ℤ ℤ.* ℤ.- 1ℤ ≈⟨ -a*b≈-ab 1ℤ (ℤ.- 1ℤ) ⟩ - ℤ.- (1ℤ ℤ.* ℤ.- 1ℤ) ≈⟨ ℤ.-‿cong $ ℤ.*-identityˡ (ℤ.- 1ℤ) ⟩ - ℤ.- (ℤ.- 1ℤ) ≈⟨ -‿idem 1ℤ ⟩ - 1ℤ ∎ - where open ℤ-Reasoning - - 0<2 : 0ℤ ℤ.< 2ℤ - 0<2 = begin-strict - 0ℤ ≈˘⟨ ℤ.+-identity² ⟩ - 0ℤ ℤ.+ 0ℤ <⟨ ℤ.+-invariantˡ 0ℤ 0<1 ⟩ - 0ℤ ℤ.+ 1ℤ <⟨ ℤ.+-invariantʳ 1ℤ 0<1 ⟩ - 2ℤ ∎ - where open ℤ-Reasoning - - 1<<n≉0 : ∀ n → 1ℤ << n ℤ.≉ 0ℤ - 1<<n≉0 zero eq = 1≉0 1≈0 - where - open ℤ-Reasoning - 1≈0 = begin-equality - 1ℤ ≈˘⟨ ℤ.*-identity² ⟩ - 1ℤ ℤ.* 1ℤ ≈⟨ eq ⟩ - 0ℤ ∎ - 1<<n≉0 (suc zero) eq = ℤ.irrefl 0≈2 0<2 - where - open ℤ-Reasoning - 0≈2 = begin-equality - 0ℤ ≈˘⟨ eq ⟩ - 2ℤ ℤ.* 1ℤ ≈⟨ ℤ.*-identityʳ 2ℤ ⟩ - 2ℤ ∎ - 1<<n≉0 (suc (suc n)) eq = - [ (λ 2≈0 → ℤ.irrefl (ℤ.Eq.sym 2≈0) 0<2) , 1<<n≉0 (suc n) ]′ - $ ab≈0⇒a≈0⊎b≈0 $ ℤ.Eq.trans (2a<<n≈a<<1+n 1ℤ (suc n)) eq - - 1<<n≉0ℝ : ∀ n → (1ℤ << n) /1 ℝ.≉ 0ℝ - 1<<n≉0ℝ n eq = 1<<n≉0 n $ (begin-equality - 1ℤ << n ≈˘⟨ ⌊⌋∘/1≗id (1ℤ << n) ⟩ - ⌊ (1ℤ << n) /1 ⌋ ≈⟨ ⌊⌋.cong $ eq ⟩ - ⌊ 0ℝ ⌋ ≈⟨ ⌊⌋.0#-homo ⟩ - 0ℤ ∎) - where open ℤ-Reasoning - - open RawPseudocode rawPseudocode using (module ShiftNotZero) - - open ShiftNotZero (λ n → fromWitnessFalse (1<<n≉0ℝ n)) public |