[Agda] how to set level

[Sergei Meshveliani]

On Mon, 2018-04-30 at 16:42 +0300, Sergei Meshveliani wrote:
> Please, what is wrong in the below program?
> 
> I define Expression over a Semiring, and the relations _=e_ and _<e_ on
> Expression.
> But Agda 2.5.3 does not solve the level values.
> First it forces the level  α=  for Expression.
> And then, I cannot satisfy it with the level values for _<e_ and for the
> Lift calls.
> [..]


> --**********************************************************************
> open import Level    using (_⊔_; Lift)
> open import Algebra  using (Semiring)
> open import Algebra.FunctionProperties as FuncProp using (Op₂)
> open import Relation.Binary using (Rel; IsStrictTotalOrder) 
>                             renaming (Decidable to Decidable₂)
> open import Relation.Binary.PropositionalEquality using (_≡_)
> open import Data.Empty   using (⊥) 
> open import Data.Unit    using (⊤) 
> open import Data.Sum     using (_⊎_)
> open import Data.Product using (_×_; _,_)
> open import Data.Nat     using (ℕ) renaming (_≟_ to _≟n_; _<_ to _<n_) 
> 
> -------------------------------------------------------------------------
> postulate anything : ∀ {a} {A : Set a} → A      -- for debug    

> module Foo {α α= β} (R : Semiring α α=) 
>                  (open Semiring R using (_≈_) renaming (Carrier to C))
>                  (_≟_   : Decidable₂ _≈_)  
>                  (_<_   : Rel C β)  
>                  (isDTO : IsStrictTotalOrder _≈_ _<_)
>   where  
>   open Semiring R using (_+_) 
> 
>   data Expression : Set α where cf   : C → Expression
>                                 var  : ℕ → Expression  
>                                 _:+_ : Op₂ Expression 
>   infixl 6 _:+_
> 
>   data _=e_ : Expression → Expression → Set α=
>     where
>     cfEq  :  ∀ {a b} → a ≈ b → cf a =e cf b 
>     varEq :  ∀ {i j} → i ≡ j → var i =e var j
>     +eq   :  ∀ {x x' y y'} → x =e x' → y =e y' → (x :+ y) =e (x' :+ y')
> 
> 
>   _<e_ :  Rel Expression β        -- inverse lexicographic ordering
>                          -- (α= ⊔ β) ?
> 
>   (cf a) <e (cf b)   =  (a < b)   -- Lift  will be forced if ...
>   (cf _) <e (var _)  =  Lift ⊤ 
>   (cf _) <e (_ :+ _) =  Lift ⊤ 
> 
>   (var i) <e (var j)  =  Lift (i <n j)
>   (var _) <e (cf _)   =  Lift ⊥
>   (var _) <e (_ :+ _) =  Lift ⊤
> 
>   (_ :+ _) <e (cf _)   =  Lift ⊥ 
>   (_ :+ _) <e (var _)  =  Lift ⊥
>   (x :+ y) <e (z :+ u) =  Lift (x <e z  ⊎  (x =e z × y <e u))
>                           -- anything
> --**************************************************************************


I find now the needed code:


  _<e_ :  Rel Expression (α= ⊔ β) 

  (cf a) <e (cf b)   =  Lift {β} {α=} (a < b)   -- **  
  (cf _) <e (var _)  =  Lift ⊤ 
  (cf _) <e (_ :+ _) =  Lift ⊤ 

  (var i) <e (var j)  =  Lift (i <n j)
  (var _) <e (cf _)   =  Lift ⊥
  (var _) <e (_ :+ _) =  Lift ⊤

  (_ :+ _) <e (cf _)   =  Lift ⊥ 
  (_ :+ _) <e (var _)  =  Lift ⊥
  (x :+ y) <e (z :+ u) =  Lift (x <e z  ⊎  (x =e z × y <e u))
    

First, wildcard does not help here, and one needs to guess of the
minimal level expression of  α= ⊔ β. 
Second, one needs to set the needed hidden values {β} and {α=} for Lift.
This does not look like a great problem, though.

------
Sergei









__
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda