这会在什么时候结束？
这会在什么时候结束？
提问于 2015-06-22 08:54:50
我实际上想证明一个定理，但我认为，如果我在另一边证明的话，那也很好。
我定义了一系列积极的理据，如：
one : ℤ
one = + 1
next : pair → pair
next q = if (n eq one) then (mkPair (+ m Data.Integer.+ one) 1)
else (mkPair (n Data.Integer.- one) (m Nat.+ 1))
where
n = getX q
m = getY q
-- eq is defined correctly for equivalence of two integer.
rational : Stream pair
rational = iterate next (mkPair one 1)
RQ : pair → Stream pair → Stream pair
RQ q (x ∷ xs) = (x add q) ∷ ♯ (RQ q (♭ xs))
positiveRat : Stream pair
positiveRat = RQ (mkPair (+ 0) (1)) rational 这里，pair是ℤ和ℕ字段的记录：
--records of rational number
record pair : Set where
field
x : ℤ
y : ℕ
mkPair : ℤ → ℕ → pair
mkPair a b = record { x = a; y = b}现在，我要证明，在positiveRat中的每个rational都是正的。
open import Data.Stream
open import Data.Nat
open import Data.Rational
open import Data.Integer
open import Coinduction
open import Data.Unit
lemma : (x : pair) → (x ∈ positiveRat) → (+ 0 Data.Integer.≤ pair.x x)
lemma .(record { x = + 1 ; y = 1 }) here = +≤+ z≤n
lemma .(record { x = + 2 ; y = 1 }) (there here) = +≤+ z≤n
lemma .(record { x = + 1 ; y = 2 }) (there (there here)) = {!!}
lemma q (there (there (there pf))) = {!!}我在pf上分页写证据。但这是不可阻挡的。
回答 1
Stack Overflow用户
发布于 2015-06-22 14:08:43
在这个模拟示例中，这很容易解决，因为stream是周期性的：
lemma : (x : ℚ) → (x ∈ stream) → (+ 0 Data.Integer.≤ ℚ.numerator x)
lemma .(record { numerator = + 1}) here = +≤+ z≤n
lemma .(record { numerator = + 2}) (there here) = +≤+ z≤n
lemma .(record { numerator = + 3}) (there (there here)) = +≤+ z≤n
lemma q (there (there (there pf))) = lemma q pf但是，我想在您的实际示例中，stream不是周期性的。没有通用的答案；lemma的正确证明取决于如何定义真实的stream，因此您必须发布这个答案。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/30975746
复制相关文章
相似问题
腾讯云开发者
