[Agda] how to set level

[Sergei Meshveliani]

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.
If I replace the last line RHS with `anything', then I can satisfy it.

I wonder what level expressions to set, where to set Lift, and with what
levels.

Thanks,
-------

Sergei


--**********************************************************************
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
--**************************************************************************

[Sergei Meshveliani]

Post by Sergei Meshveliani
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









__

Post by Sergei Meshveliani
Agda mailing list
https://lists.chalmers.se/mailman/listinfo/agda

[Sergei Meshveliani]

Post by Sergei Meshveliani
_<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))

This works, but leads to complications in using _<e_.
For example, a proof for

from-cf-mono-< : ∀ {a b} → cf a <e cf b → a < b

needs inserting Lift and `lift' in various places.
I was not able to prove it. Instead I prove

from-cf-mono-< : ∀ {a b} → cf a <e cf b → Lift {_} {_} (a < b)

Deriving _<e?_ : Decidable _<e_ from _<?_ involves more
complications with levels.

I think now that the source of these complications is defining _<e_ as a
function.
Defining it as `data' removes the problem:

data _<e_ : Expression → Expression → Set β
where
cf<cf : ∀ {a b} → a < b → cf a <e cf b
cf<var : ∀ {a i} → cf a <e var i
cf<+ : ∀ {a e e'} → cf a <e (e :+ e')

var<+ : ∀ {i e e'} → var i <e (e :+ e')


from-cf-mono-< : ∀ {a b} → cf a <e cf b → (a < b)
from-cf-mono-< (cf<cf a<b) = a<b

open IsStrictTotalOrder isSTO using (_<?_)

_<e?_ : Decidable₂ _<e_

(cf a) <e? (cf b) = case a <? b of \
{ (yes a<b) → yes (cf<cf a<b)
; (no a≮b) → no (a≮b ∘ from-cf-mono-<)
}
(cf _) <e? (var _) = yes cf<var
(cf _) <e? (_ :+ _) = yes cf<+

(var _) <e? (cf _) = no λ()
...


This seems to work fine.

------
Sergei