[Agda] "metavariable" message

[Andreas Abel]

The error about the metavariable indicates that you overlooked a dependency.

Your proof is easy with 'with'.  'case' is obviously the wrong strategy 
because you are proving something about functions that were defined with 
'with'.

Here is the proof:

toDgs'-suc=toDgs-suc : ∀ n → toDgs' (suc n) =l toDgs (suc n)
toDgs'-suc=toDgs-suc 0       = blRefl
toDgs'-suc=toDgs-suc (suc n) with toDigits 2 (suc (suc n))
toDgs'-suc=toDgs-suc (suc n) | [] , ()
toDgs'-suc=toDgs-suc (suc n) | 0b ∷ [] , ()
toDgs'-suc=toDgs-suc (suc n) | sucF 0b ∷ [] , ()
toDgs'-suc=toDgs-suc (suc n) | sucF (sucF ()) ∷ [] , _
toDgs'-suc=toDgs-suc (suc n) | 0b ∷ b' ∷ bs , p = LP.refl PE.refl
toDgs'-suc=toDgs-suc (suc n) | sucF b ∷ b' ∷ bs , p = LP.refl PE.refl

Cheers,
Andreas


On 03.11.2013 19:22, Sergei Meshveliani wrote:
> People,
> I have the two questions about the below program.
>
> 1) Why the checker reports about "metavariable" ?
>
>     (Agda 2.3.2.2 MAlonzo).
>
> 2) How to prove  toDgs'-suc=toDgs-suc ?
>
> The statement looks as trivial,
> and  " → blRefl"  needs to be sufficient in the last branch.
> But it fails.
>
> Thank you in advance for explanation,
>
> ------
> Sergei
>
>
> --------------------------------------------------------------
> open import Function using (_$_; _∘_; case_of_)
> open import Relation.Binary using
>       (IsEquivalence; module IsEquivalence; Setoid;
>        module Setoid; DecSetoid; module DecSetoid;
>        DecTotalOrder; module DecTotalOrder
>       )
> open import Relation.Binary.PropositionalEquality as PE
>                                                    using (_≡_)
> open import Data.Empty      using (⊥; ⊥-elim)
> open import Data.Unit       using (⊤)
> open import Data.Fin as Fin using (Fin)
>                              renaming (zero to 0b; suc to sucF)
> import Data.Fin.Props as FinP using (decSetoid)
> open import Data.Digit using (Bit)
> open import Data.Bin   using (Bin⁺)
> open import Data.Digit using (toDigits; fromDigits)
> open import Data.Product    using (_×_; _,_; proj₁; proj₂; ∃)
> open import Data.Nat as Nat using (ℕ; suc)
>                              renaming (decTotalOrder to natDTO)
> open import Data.List     using (List; []; _∷_)
> open import Relation.Binary.List.Pointwise as LP using ()
>
> -------------------------------------------------------------------
> bitDecSetoid = FinP.decSetoid 2
> open DecSetoid bitDecSetoid using () renaming (setoid to bitSetoid)
> blSetoid = LP.setoid bitSetoid
> open Setoid blSetoid using ()
>                    renaming (_≈_ to _=l_; isEquivalence to blEquiv)
> open IsEquivalence blEquiv using ()
>                             renaming (refl to blRefl; sym to blSym)
>
> postulate anything : ∀ {a} {A : Set a} → A  -- for debug
>
> toDgs = proj₁ ∘ toDigits 2
>
> toDigits' : (n : ℕ) → ∃ \ (bs : Bin⁺) → fromDigits bs ≡ n
> toDigits' n  with  toDigits 2 n
>
> ... | ([]      , eq) =  ([]     , eq)  -- inaccessible
> ... | (0b ∷ [] , eq) =  ([]     , eq)
> ... | (b ∷ bs  , eq) =  (b ∷ bs , eq)
> --
> -- It differs from  toDigits  only at  n = 0.
>
> toDgs' = proj₁ ∘ toDigits'
>
> toDgs'-suc=toDgs-suc : ∀ n → toDgs' (suc n) =l toDgs (suc n)
> toDgs'-suc=toDgs-suc 0       = blRefl
> toDgs'-suc=toDgs-suc (suc n) =
>    case
>        toDigits 2 (suc (suc n))
>    of \
>    { ([]                    , ())
>    ; (0b ∷ []               , ())
>    ; ((sucF 0b) ∷ []        , ())
>    ; ((sucF (sucF ())) ∷ [] , _ )
>    ; (b ∷ b' ∷ bs           , _ ) →
>           let gl : toDgs' (suc $ suc n) =l (b ∷ b' ∷ bs)
>                                           -- toDgs (suc $ suc n)
>               gl = anything
>           in  gl
>    }
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>