[Agda] `abstract' fail
mechvel at scico.botik.ru
mechvel at scico.botik.ru
Sun Oct 4 23:35:26 CEST 2015
Can people tell, please,
why in the _attached code_ `abstract' is not allowed in Agda 2.4.2.4
?
half-n=n-div-2 is implemented via `case'.
If it is not under `abstract', then it is type checked.
Is this a bug in Agda ?
Thanks,
------
Sergei
-------------- next part --------------
module BugPretend-oct4-2015 where
open import Level using (Level) renaming (zero to 0ℓ)
open import Function using (_$_; _∘_; flip; case_of_)
open import Algebra using (CommutativeSemiring; module CommutativeSemiring)
open import Relation.Nullary using (Dec; yes; no; ¬_)
open import Relation.Binary using
(Rel; Symmetric; IsEquivalence; module IsEquivalence; Setoid;
module Setoid; DecSetoid; module DecSetoid; DecTotalOrder;
module DecTotalOrder; StrictTotalOrder; module StrictTotalOrder;
_Preserves_⟶_; _Respects_
)
renaming (Decidable to Decidable₂)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_; _≗_)
renaming (cong to ≡cong; cong₂ to ≡cong₂)
open PE.≡-Reasoning renaming (_≡⟨_⟩_ to _≡[_]_; begin_ to ≡begin_;
_∎ to _≡end)
open import Data.Empty using (⊥-elim; ⊥)
open import Data.Unit using (⊤)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (_×_; _,_; proj₁; proj₂; ∃)
open import Data.Nat as Nat
using (ℕ; suc; pred; _>_; _≯_; _<_; _≮_; _≤_; _≰_; z≤n; s≤s;
_≥_; _+_; _*_; _∸_; ⌊_/2⌋; module ≤-Reasoning
)
open import Data.Nat.Properties as NatProp using
(commutativeSemiring; ≤-step; m≤m+n; n∸n≡0; pred-mono; n∸m≤n;
m+n∸m≡n; ∸-mono; +-∸-assoc; _+-mono_; _*-mono_; ⌊n/2⌋-mono
)
open import Data.Nat.DivMod as DM using (_divMod_; _div_)
open import Data.Fin as Fin using (Fin; toℕ; fromℕ≤)
open import Data.Fin.Properties as FinProp using (prop-toℕ-≤)
open ≤-Reasoning using () renaming (begin_ to ≤begin_; _∎ to _≤end;
_≡⟨_⟩_ to _≡≤[_]_; _≤⟨_⟩_ to _≤[_]_)
------------------------------------------------------------------------------
natDTO = Nat.decTotalOrder
natSTO = NatProp.strictTotalOrder
natDecSetoid = DecTotalOrder.Eq.decSetoid natDTO
natSetoid = DecSetoid.setoid natDecSetoid
natEquiv = Setoid.isEquivalence natSetoid
open IsEquivalence natEquiv using () renaming (refl to ≡refl; sym to ≡sym;
trans to ≡trans)
open DecTotalOrder natDTO using (_≟_; _≤?_)
renaming (reflexive to ≤refl; trans to ≤trans;
antisym to ≤antisym)
open StrictTotalOrder natSTO using (compare; <-resp-≈)
renaming (irrefl to <-irrefl; trans to <-trans)
open CommutativeSemiring commutativeSemiring using ()
renaming (+-assoc to +assoc; +-comm to +comm;
*-comm to *comm; distribʳ to rDistrib)
≢sym : ∀ {a} {A : Set a} → Symmetric (_≢_ {A = A})
≢sym x≢y = x≢y ∘ PE.sym
half : ℕ → ℕ
half = ⌊_/2⌋
+cong₁ : {y : ℕ} → (\x → x + y) Preserves _≡_ ⟶ _≡_
+cong₁ {y} = PE.cong (\x → x + y)
+cong₂ : {x : ℕ} → (_+_ x) Preserves _≡_ ⟶ _≡_
+cong₂ {x} = PE.cong (_+_ x)
∸cong₁ : {y : ℕ} → (\x → x ∸ y) Preserves _≡_ ⟶ _≡_
∸cong₁ {y} = PE.cong (\x → x ∸ y)
∸cong₂ : {x : ℕ} → (_∸_ x) Preserves _≡_ ⟶ _≡_
∸cong₂ {x} = PE.cong (_∸_ x)
*cong₁ : {y : ℕ} → (\x → x * y) Preserves _≡_ ⟶ _≡_
*cong₁ {y} = PE.cong (\x → x * y)
*cong₂ : {x : ℕ} → (_*_ x) Preserves _≡_ ⟶ _≡_
*cong₂ {x} = PE.cong (_*_ x)
1* : ∀ x → 1 * x ≡ x
1* x = +comm x 0
*1 : ∀ x → x * 1 ≡ x
*1 x = PE.trans (*comm x 1) $ 1* x
*0 : ∀ n → n * 0 ≡ 0
*0 n = PE.trans (*comm n 0) PE.refl
2* : ∀ x → 2 * x ≡ x + x
2* x = PE.cong (_+_ x) $ 1* x
_<?_ : Decidable₂ _<_
_<?_ m = _≤?_ (suc m)
_>?_ : Decidable₂ _>_
_>?_ m n = _<?_ n m
suc>0 : ∀ {n} → suc n > 0
suc>0 = s≤s z≤n
n≤n : ∀ {n} → n ≤ n
n≤n = ≤refl PE.refl
n≢suc-n : ∀ {n} → n ≢ suc n
n≢suc-n ()
n<suc-n : ∀ {n} → n < suc n
n<suc-n = n≤n
≤0→≡ : ∀ {n} → n ≤ 0 → n ≡ 0
≤0→≡ z≤n = PE.refl
≮0 : ∀ {n} → n ≮ 0
≮0 ()
n≤suc-n : ∀ {n} → n ≤ suc n
n≤suc-n = ≤-step $ ≤refl ≡refl
suc≰0 : ∀ {n} → suc n ≰ 0
suc≰0 ()
suc≮0 : ∀ {n} → suc n ≮ 0
suc≮0 ()
suc∘pred : ∀ {n} → n > 0 → suc (pred n) ≡ n -- 1 ≤ n
suc∘pred {suc _} _ = PE.refl
suc∘pred {0} ()
1≤n' : ∀ {n} → 1 ≤ suc n
1≤n' = s≤s z≤n
1<n'' : ∀ {n} → 1 < suc (suc n) -- 2 ≤ suc suc n
1<n'' = s≤s $ s≤s z≤n
⊎→≤ : ∀ {m n} → m < n ⊎ m ≡ n → m ≤ n
⊎→≤ (inj₂ m=n) = ≤refl m=n
⊎→≤ (inj₁ m<n) = ≤trans m≤m' m<n where
m≤m' = ≤-step $ ≤refl ≡refl
<→≤ : ∀ {m n} → m < n → m ≤ n
<→≤ = ⊎→≤ ∘ inj₁
<→≢ : ∀ {m n} → m < n → m ≢ n
<→≢ {_} {n} m<n m=n = <-irrefl ≡refl n<n where
resp = proj₂ <-resp-≈
n<n = resp m=n m<n
>→≢ : ∀ {m n} → m > n → m ≢ n
>→≢ {_} {n} m>n = <→≢ m>n ∘ ≡sym
>→≰ : ∀ {m n} → m > n → m ≰ n
>→≰ m>n m≤n = <→≢ n<m n=m where n<m = m>n
n≤m = <→≤ n<m
n=m = ≤antisym n≤m m≤n
suc≢0 : ∀ {n} → suc n ≢ 0
suc≢0 ()
0≢suc : ∀ {n} → 0 ≢ suc n
0≢suc = suc≢0 ∘ PE.sym
<1→=0 : ∀ {n} → n < 1 → n ≡ 0
<1→=0 {n} = ≤0→≡ ∘ pred-mono
≤1→0or1 : ∀ n → n ≤ 1 → n ≡ 0 ⊎ n ≡ 1
≤1→0or1 0 _ = inj₁ PE.refl
≤1→0or1 (suc 0) _ = inj₂ PE.refl
≤1→0or1 (suc (suc n)) n''≤1 = ⊥-elim $ n''≰1 n''≤1
where
n''≰1 = >→≰ $ s≤s $ s≤s z≤n
------------------------------------------------------------------------------
half-n*2 : ∀ n → half (n * 2) ≡ n
half-n*2 0 = ≡refl
half-n*2 (suc n) = ≡cong suc $ half-n*2 n
half-1+n*2 : ∀ n → half (suc (n * 2)) ≡ n
half-1+n*2 0 = PE.refl
half-1+n*2 (suc n) =
≡begin
half (suc ((1 + n) * 2)) ≡[ PE.cong half $ PE.cong suc $
rDistrib 2 1 n ]
half (suc (2 + (n * 2))) ≡[ PE.refl ]
half (suc (suc (suc (n * 2)))) ≡[ PE.refl ]
suc (half (suc (n * 2))) ≡[ PE.cong suc $ half-1+n*2 n ]
suc n
≡end
half≤ : (n : ℕ) → half n ≤ n
half≤ 0 = z≤n
half≤ (suc 0) = z≤n
half≤ (suc (suc n)) = ≤begin half (suc (suc n)) ≡≤[ ≡refl ]
suc (half n) ≤[ s≤s $ half≤ n ]
suc n ≤[ n≤suc-n ]
suc (suc n)
≤end
half-suc-n≤n : (n : ℕ) → half (suc n) ≤ n
half-suc-n≤n 0 = z≤n
half-suc-n≤n (suc n) = ≤begin half (suc (suc n)) ≡≤[ ≡refl ]
suc (half n) ≤[ s≤s $ half≤ n ]
suc n
≤end
------------------------------------------------------------------------------
half<4+> : (m : ℕ) → half (4 + m) ≡ 2 + half m
half<4+> _ = ≡refl
half<4+m>≤2+m : (m : ℕ) → half (4 + m) ≤ 2 + m
half<4+m>≤2+m m =
≤begin half (4 + m) ≡≤[ half<4+> m ]
suc (suc (half m)) ≤[ s≤s $ s≤s $ half≤ m ]
suc (suc m)
≤end
------------------------------------------------------------------------------
-- why `abstract' is not allowed here?
abstract
half-n=n-div-2 : ∀ n → half n ≡ (n div 2)
half-n=n-div-2 n =
case
rN ≟ 0
of \
{ (yes rN=0) → let n=q*2 = PE.trans n=rN+q*2 (+cong₁ rN=0)
in
≡begin half n ≡[ PE.cong half n=q*2 ]
half (q * 2) ≡[ half-n*2 q ]
q ≡[ q=n-div-2 ]
n div 2
≡end
; (no rN/=0) →
let rN=1 : rN ≡ 1
rN=1 = case rN=0or1 of \ { (inj₁ rN=0) → ⊥-elim $ rN/=0 rN=0
; (inj₂ rN=1) → rN=1
}
n=1+q*2 : n ≡ suc (q * 2)
n=1+q*2 = ≡begin n ≡[ n=rN+q*2 ]
rN + (q * 2) ≡[ +cong₁ rN=1 ]
1 + (q * 2)
≡end
in
≡begin half n ≡[ PE.cong half n=1+q*2 ]
half (suc (q * 2)) ≡[ half-1+n*2 q ]
q ≡[ q=n-div-2 ]
n div 2
≡end
}
where
open DM.DivMod
res = n divMod 2
q = quotient res
r = remainder res
rN = toℕ r
n=rN+q*2 = property res
q=n-div-2 : q ≡ (n div 2)
q=n-div-2 = PE.refl
rN≤1 = prop-toℕ-≤ {2} r
rN=0or1 : rN ≡ 0 ⊎ rN ≡ 1
rN=0or1 = ≤1→0or1 rN rN≤1
More information about the Agda
mailing list