[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