[Agda] about Null

[Sergei Meshveliani]

Sorry for noise.
I have found it, finally:

-----------------------------
¬Null→length>0 : {α : Level} → {A : Set α} → (xs : List A) → ¬ Null xs →
                                                          length xs > 0
¬Null→length>0 (_ ∷ _) _        =  suc>0
¬Null→length>0 []      ¬null-[] =  ⊥-elim (¬null-[] isNull)


postulate anything      : ∀ {a} {A : Set a} → A
          items         : ℕ → List ℕ
          a             : ℕ
          nullItems→a≢0 : Null (items a) → a ≢ 0
          lnItems>0→a≢0 : length (items a) > 0 → a ≢ 0

a≢0 : a ≢ 0
a≢0 = case  null? (items a)
      of \
      { (yes nullIts-a)   → nullItems→a≢0 nullIts-a
      ; (no notNullIts-a) → 
                       let ln>0 : length (items a) > 0
                           ln>0 = ¬Null→length>0 (items a) notNullIts-a
                       in  lnItems>0→a≢0 ln>0
      }
-----------------------------





On Mon, 2014-08-11 at 20:50 +0400, Sergei Meshveliani wrote:
> People,
> 
> I introduce 
> 
>   data Null {α} {A : Set α} : List A → Set α  where  isNull : Null []
> 
> for expressing the predicate  "a list is empty". 
> Then, I need to prove the following two simple statements
> (¬Null→length>0, a ≢ 0). And fail.
> Can you, please demonstrate a proof?
> 
> ------------------------------------------------------------------------
> open import Level using (Level)
> open import Function using (case_of_)
> open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
> open import Relation.Nullary using (Dec; yes; no; ¬_)
> open import Data.Empty       using (⊥; ⊥-elim)
> open import Data.Nat         using (ℕ; suc; _>_; _≤_; s≤s; z≤n)
> open import Data.List        using (List; []; _∷_; length)
> open import Data.Product     using (_,_)
> 
> data Null {α} {A : Set α} : List A → Set α  where  isNull : Null []
> 
> null? : {α : Level} → {A : Set α} → (xs : List A) → Dec (Null xs)
> null? []      = yes isNull
> null? (_ ∷ _) = no λ()
> 
> suc>0 : ∀ {n} → suc n > 0
> suc>0 = s≤s z≤n
> 
> ¬Null→length>0 : {α : Level} → {A : Set α} → (xs : List A) → ¬ Null xs →
>                                                            length xs > 0
> ¬Null→length>0 (_ ∷ _) _  =  suc>0
> ¬Null→length>0 [] ()                 -- fails
> 
> 
> -- Prove  a ≢ 0  from these postulated things:
> 
> postulate anything      : ∀ {a} {A : Set a} → A
>           items         : ℕ → List ℕ
>           a             : ℕ
>           nullItems→a≢0 : Null (items a) → a ≢ 0
>           lnItems>0→a≢0 : length (items a) > 0 → a ≢ 0
> 
> a≢0 : a ≢ 0
> a≢0 = go (items a) PE.refl (null? (items a))
>     where
>     go : (its : List ℕ) → its ≡ (items a) → Dec (Null (items a)) → a ≢ 0
>     go _ _ (yes nullIts-a)   =  nullItems→a≢0 nullIts-a
>     -- go _ _ (no notNullIts-a =  
>     -- ?
> -------------------------------------------------------------------------
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>