diff --git a/acorn.agda-lib b/acorn.agda-lib index 3837c04..527ec1b 100644 --- a/acorn.agda-lib +++ b/acorn.agda-lib @@ -1,4 +1,5 @@ name: acorn depend: - agda2hs + agda2hs-base + agda2hs-containers include: src diff --git a/src/Algebra/Order.agda b/src/Algebra/Order.agda index 834cc25..edf1241 100644 --- a/src/Algebra/Order.agda +++ b/src/Algebra/Order.agda @@ -7,6 +7,7 @@ open import Haskell.Prim.Either open import Haskell.Prim using (⊥) open import Haskell.Prim.Tuple +open import Tool.Logic open import Tool.ErasureProduct open import Tool.Relation open import Algebra.Setoid diff --git a/src/Algebra/SemiRing.agda b/src/Algebra/SemiRing.agda index aac0e88..8c8c5ad 100644 --- a/src/Algebra/SemiRing.agda +++ b/src/Algebra/SemiRing.agda @@ -11,9 +11,9 @@ open import Agda.Builtin.Unit open import Agda.Builtin.FromNat open import Agda.Builtin.Nat using (zero; suc) open import Agda.Builtin.Int using (pos; negsuc) -open import Haskell.Prim.Tuple using (_↔_) open import Haskell.Prim using (⊥) +open import Tool.Logic open import Tool.Relation open import Algebra.Setoid diff --git a/src/Algebra/Setoid.agda b/src/Algebra/Setoid.agda index 9ca4688..fa6f91c 100644 --- a/src/Algebra/Setoid.agda +++ b/src/Algebra/Setoid.agda @@ -8,6 +8,7 @@ open import Haskell.Prim using (⊥) open import Haskell.Prim.Tuple open import Haskell.Prim.Either +open import Tool.Logic open import Tool.Relation record Setoid (a : Set) : Set₁ where diff --git a/src/Function/AlternatingSeries.agda b/src/Function/AlternatingSeries.agda index b75b2bc..4b06ea4 100644 --- a/src/Function/AlternatingSeries.agda +++ b/src/Function/AlternatingSeries.agda @@ -58,6 +58,9 @@ precision 2^k such as n*2^k < epsilon/2. -- This way, we can have only one stream and ensure -- the denominator is not zero. +-- Whether we are near enough to zero that +-- we can stop here. +-- -- We define this that way because -- we will need exactly this function -- in sumAlternatingStream. @@ -75,14 +78,13 @@ thatNearToZero xk ε k = let prec = ratLog2Floor (proj₁ ε) {proj₂ ε} + neg prec) + shift one prec) ≤# proj₁ (halvePos ε) - {- - ball (halvePos ε) - (appDiv (num xk) (den xk) (denNotNull xk) - prec - + shift one prec) - null) - -} {-# COMPILE AGDA2HS thatNearToZero #-} + +-- A proposition-as-type meaning that +-- for all ε, there exists a member in the stream +-- which is near enough to zero +-- (and we can stop there). +-- This also means that the series converges to zero. HasThatNearToZero : {a : Set} {{ara : AppRational a}} -> Stream (Frac a) -> Set HasThatNearToZero xs = ∀ (ε : PosRational) -> Σ0 Nat (λ k -> IsTrue (thatNearToZero (index xs k) ε k)) {-# COMPILE AGDA2HS HasThatNearToZero #-} @@ -112,9 +114,9 @@ autoHasThatNearToZero xs ε = go xs ε 0 -- we will need a tuple here IsAlternating : {a : Set} {{ara : AppRational a}} -> Stream (Frac a) -> Set -IsAlternating xs = Tuple0 (HasThatNearToZero xs) - ( (∀ (i : Nat) -> abs (index xs (suc i)) < abs (index xs i)) -- decreasing - × (∀ (i : Nat) -> index xs i * index xs (suc i) < null) ) -- alternating +IsAlternating xs = Tuple0 (HasThatNearToZero xs) -- converging to 0 + ( (∀ (i : Nat) -> abs (index xs (suc i)) < abs (index xs i)) -- decreasing + × (∀ (i : Nat) -> index xs i * index xs (suc i) < null) ) -- alternating {-# COMPILE AGDA2HS IsAlternating #-} -- The sum of the first n elements of a stream. diff --git a/src/Function/Exp.agda b/src/Function/Exp.agda index 324d152..d27efe5 100644 --- a/src/Function/Exp.agda +++ b/src/Function/Exp.agda @@ -58,17 +58,9 @@ smallExpQ : ∀ {a : Set} {{ara : AppRational a}} -- The seed is going to be a Nat × Frac a tuple, -- containing the index of the step (starting from 1) and the previous fraction. smallExpQ (x :&: _) = let xs = (coiteStream snd (λ {(n , fra) -> suc n , MkFrac (num fra * x) (den fra * cast (pos n)) cheat}) (1 , one)) in - sumAlternatingStream xs - -- the index for K&S 5.1: - {- - ∣xᵏ/k!∣ + ε/2k + ε/2k ≤ ε/2 - ∣xᵏ/k!∣ + ε/k ≤ ε/2 - huh; that won't be easy - but if we have a proof with a rough overapproximation, - we can put it into autoHasThatNearToZero - and now, we can cheat it away - -} - (autoHasThatNearToZero xs cheat :&: cheat) + sumAlternatingStream + xs + (autoHasThatNearToZero xs cheat :&: cheat) {-# COMPILE AGDA2HS smallExpQ #-} -- From Krebbers and Spitters: diff --git a/src/Operator/Decidable.agda b/src/Operator/Decidable.agda index 5765d68..128204e 100644 --- a/src/Operator/Decidable.agda +++ b/src/Operator/Decidable.agda @@ -7,9 +7,10 @@ module Operator.Decidable where open import Agda.Builtin.Bool open import Agda.Builtin.Equality open import Haskell.Prim.Either -open import Haskell.Prim.Tuple using (_↔_) +open import Haskell.Prim.Tuple open import Haskell.Prim using (IsTrue; if_then_else_) +open import Tool.Logic open import Algebra.Setoid open import Tool.Relation open import Algebra.Order diff --git a/src/RealTheory/AppRational.agda b/src/RealTheory/AppRational.agda index 35059da..4bc75d0 100644 --- a/src/RealTheory/AppRational.agda +++ b/src/RealTheory/AppRational.agda @@ -29,6 +29,7 @@ open import Haskell.Prim using (id; const; IsTrue) open import Tool.Cheat +open import Tool.Logic open import Tool.ErasureProduct open import Algebra.SemiRing open import Algebra.Ring diff --git a/src/Tool/Logic.agda b/src/Tool/Logic.agda new file mode 100644 index 0000000..eae616c --- /dev/null +++ b/src/Tool/Logic.agda @@ -0,0 +1,15 @@ +-- Some shortenings that don't already exist +-- in the agda2hs library. +{-# OPTIONS --erasure #-} +module Tool.Logic where + +open import Agda.Primitive +open import Haskell.Prim.Tuple + +-- I don't erase this for now; +-- maybe there are some proofs needing those witnesses. +-- But then, Haskell tuples only work with Set₀. +infixr 2 _↔_ +_↔_ : Set -> Set -> Set +A ↔ B = (A -> B) × (B -> A) + diff --git a/src/Tool/Witness.agda b/src/Tool/Witness.agda index 00cce80..95eadf9 100644 --- a/src/Tool/Witness.agda +++ b/src/Tool/Witness.agda @@ -7,9 +7,10 @@ module Tool.Witness where open import Agda.Builtin.Nat open import Agda.Builtin.Bool open import Agda.Builtin.Equality -open import Haskell.Prim.Tuple using (_↔_; _,_; fst) +open import Haskell.Prim.Tuple using (_,_; fst) open import Haskell.Prim using (IsTrue; itsTrue) +open import Tool.Logic open import Tool.PropositionalEquality open import Tool.ErasureProduct