[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