[Agda] difficult module instantiation

Sergei Meshveliani mechvel at botik.ru
Fri Nov 7 15:07:27 CET 2014


People,

I have a fragment 

module _ {α α= ℓp : Level} (upMon : UpMonoid α α=)
  where
  monoid = UpMonoid.monoid upMon
  open Monoid monoid using (upDSet; upSemigroup)

  module SubmonPack = SubmonoidPack {α} {α=} {ℓp} upMon

  Test : (upSubsemig : UpSubsemigroup {α} {α=} {ℓp} upSemigroup) →
         SubmonPack.Submonoid upSubsemig                         → Set _

  Test upSubsemig extSubmon =
    let
      module SM = SubmonPack.Submonoid

      extSubDSet1 : SubDSet upDSet
      extSubDSet1 = SM.extSubDSet extSubmon

      subMon  = SM.submonoid  extSubmon
      subUpMg = SM.subUpMagma extSubmon
      sub-ε   = SM.sub-ε      extSubmon

      {-
      open SM extSubmon using ()                                  -- (1)
                 renaming (extSubDSet to esd; submonoid to subMon'; 
                           subUpMagma to subUpMg'; sub-ε to sub-ε')
      -}
    in
    ⊤


in which the module  (SM extSubmon)  (as I think) is used 4 times with
selecting items from it.

Then I try to join these selection operations into one `open'
declaration: un-comment (1).

Agda 2.4.2 reports to this

  (SubmonPack.Submonoid upSubsemig) !=< (UpSubsemigroup upSemigroup)
   of type (Set (suc' ℓp ⊔ (suc' α= ⊔ suc' α)))
   when checking that the expression extSubmon has type
   UpSubsemigroup upSemigroup

Is (1) an adequate replacement for these 4 selections?
I wonder: how to open the needed module?

I tried  "open SM using ... renaming ...",
and then  
         item extSubmon

works for each of the 4 imported item. But this needs adding  extSubmon
into each item.

Something is strange here with instantiating module parameters.
I have got confused.

The whole module  att.agda  in attached. It has  335 lines.
The code is not full.
But may be you could look into parametric modules in  att.agda  and
tell?


Thanks,

------
Sergei




-------------- next part --------------
<standard import> ...

-- of my Application ---
open import OfShow   using (Show) 
open import DPrelude using 
     (setoidLevel; subcarrierLevel; tuple31; tuple32; tuple33; Closed; 
      Closed₂; CongMember; DecCongMember; Subset; DecSubset; module DecSubset;
      decSubset; decSubsetoid
     )
open import List2  using (module Membership2; IsFullList)
open import OfMaps using 
                   (FiniteEnumeration; module FiniteEnumeration; finEnum′; 
                    DecFiniteEnumeration; module DecFiniteEnumeration) 
open import AlgClasses1 using
     (DSet; module DSet; dSet′; UpDSet; upDSet′; DecCommutative; 
      module DecCommutative; Magma; module Magma; UpMagma; upMagma′;
      module UpMagma; Unity; unity?; RightQuotient; Semigroup; semigroup′; 
      module Semigroup; UpSemigroup; upSemigroup′; Inverse
     )
open import AlgClasses2 using 
     (Monoid; module Monoid; UpMonoid; upMonoid′; Group; group′; module Group;
      UpGroup; module UpGroup; upGroup′ 
     )



------------------------------------------------------------------------------
record SubDSet {a ℓ p} (upDSet : UpDSet a ℓ) :  Set (suc' (a ⊔ ℓ ⊔ p))
  where
  constructor subDSet′

  subsetℓ       = a ⊔ p 
  baseDecSetoid = UpDSet.decSetoid upDSet

  baseUpDSet : UpDSet a ℓ
  baseUpDSet = upDSet 

  baseDSet : DSet baseDecSetoid
  baseDSet = UpDSet.dSet upDSet

  baseSetoid  = DecSetoid.setoid baseDecSetoid
  baseCarrier = Setoid.Carrier baseSetoid
  private  C = baseCarrier 
  open IsEquivalence (Setoid.isEquivalence baseSetoid) using
                                                       (refl; sym; trans)

  field  decCongMember : DecCongMember {a} {ℓ} {p} baseSetoid
  -----

  cMember = proj₁ decCongMember
  member? = proj₂ decCongMember
  member  = proj₁ cMember
  congMem = proj₂ cMember

  private _≈_ = Setoid._≈_ baseSetoid

  subDecSetoid : DecSetoid subsetℓ _
  subDecSetoid = decSubsetoid baseDecSetoid decCongMember

  subsetoid : Setoid subsetℓ ℓ
  subsetoid = DecSetoid.setoid subDecSetoid
 
  open Setoid subsetoid public using () 
              renaming (Carrier to subC; _≈_ to _=s_; isEquivalence to sEquiv)

  subcarrier = subC

  open FiniteEnumeration 
  open DecFiniteEnumeration 

  subDSet : DSet subDecSetoid
  subDSet = dSet′ subShow sMbFinEnum
    where
    postulate subShow : Show subC
    postulate sMbFinEnum : Maybe $ DecFiniteEnumeration subsetoid 

        
  upSubDSet : UpDSet subsetℓ ℓ
  upSubDSet = upDSet′ subDecSetoid subDSet

  embed : subcarrier → baseCarrier 
  embed = proj₁ 

  open DSet subDSet public



------------------------------------------------------------------------------
record Submagma {a ℓ p} (upM : UpMagma a ℓ)
                (eSubDSet : SubDSet {a} {ℓ} {p} $ UpMagma.upDSet upM) :  
                                                                   Set (a ⊔ p)
  where
  constructor submagma′
 
  baseUpMagma = upM
  baseMagma   = UpMagma.magma upM
  extSubDSet  = eSubDSet 

  private open Magma baseMagma using (_≈_; _∙_; divRightMb) 
                           renaming (setoid to baseSetoid; dSet to baseDSet; 
                                                       Carrier to baseCarrier)
          open SubDSet extSubDSet using (subsetoid; subcarrier; _=s_; 
                                                   subsetℓ; upSubDSet; member)
          module FP≈  = FuncProp _≈_
          module FP=s = FuncProp _=s_
 
  field  closed∙ : Closed₂ {_} {_} {baseCarrier} member _∙_ 
  -----

  _∙s_ : Op₂ subcarrier
  (x , mem-x) ∙s (y , mem-y) =  (xy , member-xy)
                                              where
                                              xy = x ∙ y
                                              member-xy = closed∙ mem-x mem-y

  ----------------------------------------------------------------------------
  submagma : Magma {subsetℓ} {ℓ} upSubDSet
  submagma = record{ _∙_  = _∙s_                         
                   ; ∙cong = \ {x y u v} → cong-sub {x} {y} {u} {v}
                   ; mbCommutative = mbComm-sub  
                   ; divRightMb    = divMb-sub }
    where
    cong-sub : _∙s_ Preserves₂ _=s_ ⟶ _=s_ ⟶ _=s_

    cong-sub {(x , _)} {(y , _)} {(u , _)} {(v , _)} = 
                                         Magma.∙cong baseMagma {x} {y} {u} {v}
    open DecCommutative 

    restrictCommut : FP≈.Commutative _∙_ → FP=s.Commutative _∙s_
    restrictCommut bComm (x , _) (y , _) =  bComm x y 

    postulate 
      mbComm-sub : Maybe $ DecCommutative subsetoid _∙s_
      restrictUnity : (lU : Unity baseSetoid _∙_) → 
                      (member $ proj₁ lU) → Unity subsetoid _∙s_
      divMb-sub : (x' y' : subcarrier) → 
                              Maybe $ Dec $ RightQuotient subsetoid _∙s_ x' y'

  subUpMagma : UpMagma subsetℓ ℓ 
  subUpMagma = upMagma′ upSubDSet submagma

  open Magma   submagma   public
  open SubDSet extSubDSet public using (subsetoid; subcarrier; _=s_; 
                                        upSubDSet; member; member?; subsetℓ)

------------------------------------------------------------------------------
record UpSubmagma {a ℓ p} (upMg : UpMagma a ℓ) : Set (subcarrierLevel a ℓ p)
  where
  constructor upSubmagma′

  upMagma : UpMagma a ℓ
  upMagma = upMg

  private upDSet : UpDSet a ℓ 
          upDSet = UpMagma.upDSet upMg

  field  extSubDSet  : SubDSet {a} {ℓ} {p} upDSet 
         extSubmagma : Submagma upMg extSubDSet 


------------------------------------------------------------------------------
record Subsemigroup {a ℓ p} (upSmg : UpSemigroup a ℓ) 
                    (eSubDSet : SubDSet {a} {ℓ} {p} $ Semigroup.upDSet $ 
                                                UpSemigroup.semigroup upSmg) : 
                                                                   Set (a ⊔ p)
  where
  constructor subsemigroup′

  baseUpSemigroup = upSmg
  baseUpMagma     = UpSemigroup.upMagma   upSmg 
  baseSemigroup   = UpSemigroup.semigroup upSmg 

  field  extSubmagma : Submagma baseUpMagma eSubDSet 
  -----
  open Submagma extSubmagma using (submagma; subUpMagma; subsetℓ)
  open Magma    submagma    using () renaming (_∙_ to _∙s_; _≈_ to _=s_)

  subsemigroup : Semigroup subUpMagma
  subsemigroup = semigroup′ sub-associative
     where
     module FP=s = FuncProp _=s_ 

     sub-associative : FP=s.Associative _∙s_ 
     sub-associative (x , _) (y , _) ( z , _) = 
                                        Semigroup.∙assoc baseSemigroup x y z

  subUpSemigroup : UpSemigroup subsetℓ ℓ 
  subUpSemigroup = upSemigroup′ subUpMagma subsemigroup

  open Semigroup subsemigroup public
  open Submagma  extSubmagma  public using (_∙s_; extSubDSet; submagma;
                                                              subUpMagma)

------------------------------------------------------------------------------
record UpSubsemigroup {a ℓ p} (upSmg : UpSemigroup a ℓ) :  
                                                   Set (subcarrierLevel a ℓ p)
  where
  constructor upSubsemigroup′ 

  upSemigroup : UpSemigroup a ℓ
  upSemigroup = upSmg

  semigroup = UpSemigroup.semigroup upSmg

  private upMg = UpSemigroup.upMagma upSemigroup

  field  upSubmagma : UpSubmagma {a} {ℓ} {p} upMg
  -----
  private extSubDSet = UpSubmagma.extSubDSet upSubmagma

  field  extSubsemigroup : Subsemigroup upSmg extSubDSet  
  -----
  open Subsemigroup extSubsemigroup public



------------------------------------------------------------------------------
module SubmonoidPack {α α= ℓp : Level} (upMon : UpMonoid α α=)
  where
  private 
    Mon = UpMonoid.monoid upMon
    open Monoid Mon using (_≈_; ≈equiv; _∙_; dSet; upDSet; unity; ε; invMb; 
                                                                     _^_; ^-0)
                renaming (setoid to baseSetoid; magma to Mg; upMagma to upMg; 
                                         Carrier to C; upSemigroup to upSemig)
  subsetℓ = subcarrierLevel α α= ℓp
  ----------------------------------------------------------------------------
  submonoid-aux : 
            (upSubSemig : UpSubsemigroup {α} {α=} {ℓp} upSemig) → 
            let extSubsemig = UpSubsemigroup.extSubsemigroup upSubSemig
                extSubDSet  = UpSubsemigroup.extSubDSet upSubSemig
                member      = SubDSet.member extSubDSet
                open Subsemigroup extSubsemig using (subUpSemigroup)
            in
            member ε → Monoid subUpSemigroup 

  submonoid-aux upSubsemig mem-ε =  record{ unity = unity-sub
                                          ; _^_   = _^′_
                                          ; ^-0   = \ {x′} → ^-0-sub {x′}
                                          ; ^-suc = \ {x′} → ^-suc-sub {x′}
                                          ; invMb = invMb-sub }
    where
    extSubsemig = UpSubsemigroup.extSubsemigroup upSubsemig
    extSubDSet  = Subsemigroup.extSubDSet extSubsemig
    open Subsemigroup extSubsemig using (_∙s_) 
                     renaming (subUpMagma to subUpMg; submagma to subMg; 
                                                      extSubmagma to extSubMg)
    open SubDSet extSubDSet using (subDSet; member; member?; _=s_; subsetoid; 
                                                                      congMem)
                            renaming (subcarrier to subC)
    
    ≈refl  = IsEquivalence.refl  ≈equiv 
    ≈sym   = IsEquivalence.sym   ≈equiv 
    ≈trans = IsEquivalence.trans ≈equiv 

    subEquiv = DSet.isEquivalence subDSet 
    sRefl    = IsEquivalence.refl subEquiv 

    1proofMap : unity? baseSetoid _∙_ ε
    1proofMap = proj₂ unity

    ε′ : subC         
    ε′ = (ε , mem-ε)  

    BaseInverse = Inverse upMg    ε
    Sub-Inverse = Inverse subUpMg ε′


    unity-sub : Unity subsetoid _∙s_
    unity-sub = (ε′ , unity-sub-map)
                               where unity-sub-map : unity? subsetoid _∙s_ ε′ 
                                     unity-sub-map (x , _) = 1proofMap x
    postulate    
      _^′_ : subC → ℕ → subC 
      ^-0-sub : {x′ : subC} → (x′ ^′ 0) =s ε′
      ^-suc-sub : {x′ : subC} → {n : ℕ} → 
                                        (x′ ^′ (suc n)) =s (x′ ∙s (x′ ^′ n))
      invMb-sub : (a' : subC) → Maybe $ Dec $ Sub-Inverse a'

  ----------------------------------------------------------------------------
  record Submonoid (upSubsemig : UpSubsemigroup {α} {α=} {ℓp} upSemig) :  
                                                                   Set subsetℓ
    where
    constructor submonoid′ 

    upSubsemigroup  = upSubsemig
    extSubsemigroup = UpSubsemigroup.extSubsemigroup upSubsemig

    open Subsemigroup extSubsemigroup using (extSubDSet; subUpSemigroup)
    open SubDSet extSubDSet using (member)

    field  member-ε : member ε
    -----
    submonoid : Monoid subUpSemigroup
    submonoid = submonoid-aux upSubsemig member-ε

    sub-ε = Monoid.ε submonoid

    subUpMonoid : UpMonoid (α ⊔ ℓp) α= 
    subUpMonoid = upMonoid′ subUpSemigroup submonoid

    open SubDSet      extSubDSet      public using (_=s_)
    open Subsemigroup extSubsemigroup public

  open Submonoid public hiding (upSubsemigroup)



------------------------------------------------------------------------------
module _ {α α= ℓp : Level} (upMon : UpMonoid α α=)                        
  where
  monoid = UpMonoid.monoid upMon 
  open Monoid monoid using (upDSet; upSemigroup) 
                                                      
  module SubmonPack = SubmonoidPack {α} {α=} {ℓp} upMon  

  Test : (upSubsemig : UpSubsemigroup {α} {α=} {ℓp} upSemigroup) → 
         SubmonPack.Submonoid upSubsemig                         → Set _

  Test upSubsemig extSubmon = 
       let 
         module SM = SubmonPack.Submonoid 

         extSubDSet1 : SubDSet upDSet
         extSubDSet1 = SM.extSubDSet extSubmon 

         subMon  = SM.submonoid  extSubmon
         subUpMg = SM.subUpMagma extSubmon
         sub-ε   = SM.sub-ε      extSubmon

         open SM extSubmon using () 
                    renaming (extSubDSet to esd; submonoid to subMon'; 
                              subUpMagma to subUpMg'; sub-ε to sub-ε')
       in
       ⊤  


More information about the Agda mailing list