[Agda] congruence on dependent types
Andreas Abel
andreas.abel at ifi.lmu.de
Fri Jun 21 11:30:54 CEST 2013
Probably this does not answer your question, but if you wonder how to
treat ideals <a> in Agda, I would model them as predicates, not as types.
< a > : C -> Set
< a > b = exists \ x -> b == x * a
Basically < a > b is just "a divides b".
If you want to prove that associated a, b give rise to identical ideals,
you would prove logical equivalence of predicates.
Cheers,
Andreas
On 20.06.13 8:49 PM, Sergei Meshveliani wrote:
> We wrote
>
>>> I knew the meaning of dotted patterns, but decided to avoid them --
>>> while possible, and see further. I have forgotten of them, and now
>>> was
>>> not able to use them in this concrete example.
>>>
>>> Further, I have a feeling that something is strange in the Language.
>>> Suppose that a type
>>> Foo a
>>>
>>> depends on a : C, A : Setoid, C = Carrier A,
>>> the equivalence p : a \~~ b is proved,
>>> f : Foo a is built,
>>> and we need to return f : Foo b,
>>> and also somehow to express that f : Foo a can be replaced with
>>> f : Foo b if a \~~ b.
>>>
>>> Can this be expressed in Agda ?
>
>> No, you can't prove this for any dependent type `Foo`. If it is true
>> in your particular case, you will need to prove it specifically for
>> that.
>>
>> To see why it's not true in general, pick any `a : C`, and define
>>
>> Foo : C → Set
>> Foo x = a ≡ x
>>
>> Now, if you had:
>>
>> cong≈ : (a ≈ b) → Foo a → Foo b
>>
>> you could prove:
>>
>> discr : (b : C) → a ≈ b → a ≡ b
>> discr b p = cong≈ p refl
>>
>> which, abstracted on `a`, would imply that `A` is discrete.
>
>
> There remains a certain deviation of Agda from mathematics.
> Consider the example.
> For a CommutativeMonoid M, an element a ∈ M,
> call a p-Subsemigroup <a> in M a semigroup of the set
> {x ∙ a | x ∈ M}. Hence <a> and
> Hence <a> and <b> is the same p-subsemigroup in M iff
> associated a b
> where
> associated a b = ∃₂ λ (x y : C) → (x ∙ a) ≈ b × (y ∙ b) ≈ a
>
> -- that is a and b divide each other.
>
> Hence, if assoc-a-b : associated a b, then f ∈ <a>
> can be replaced with f ∈ <b>
> in a mathematical proof.
>
> Now, it is desirable for an algebraic domain to be expressed in Agda as a
> _dependent type_. Respectively, f ∈ <a> need to correspond to f : PSSmg a,
> where PSSmg a is the type expressing <a>.
>
> I can express in Agda the Set of all p-subsemigroups in M, and the equality
> _=pss_ on this set, with _=pss_ defined via associated a b.
> But for p : associated a b the type checker will not allow to replace
> f : PSSmg a with f : PSSmg b.
>
> Is it possible to add some construct foo to the language so that the checker
> would allow to replace f : PSSmg a with f : PSSmg b, if p : associated a b
> and foo is set for PSSmg
> ?
>
> May be, this is rather naive.
> All right, if this is not possible, still dependent types make a great deal.
>
> Here is the implementation for the Set of all p-subsemigroups which I keep in mind:
>
> ------------------------------------------------------------------------
> module SubsemigroupPack (c l : Level) (M : CommutativeMonoid c l)
> where
> C = CommutativeMonoid.Carrier M
> _≈_ = CommutativeMonoid._≈_ M
> _∙_ = CommutativeMonoid._∙_ M
>
> associated : C → C → Set _ -- a and b divide each other
> associated a b = ∃₂ λ (x y : C) → (x ∙ a) ≈ b × (y ∙ b) ≈ a
> --
> -- <a> == <b> iff associated a b
>
> record PSSmg (a : C) : Set (c ⊔L l) -- p-Subsemigroup generated by a
> where
> constructor pSSmg
>
> field factor : C
>
> element : C
> element = factor ∙ a
>
> -- Example. pSSmg 3 : PSSmg 5
> -- expresses 15 as an element of the subsemigroup of <5>.
>
> _=s_ : Rel C _
> x =s y = (x ∙ a) ≈ (y ∙ a)
>
> data PSSmgs : Set (c ⊔L l) where -- the set of p-subsemigroups in M
> pssmg : (a : C) → PSSmg a → PSSmgs
>
> _=pss_ : Rel PSSmgs _
> (pssmg a smg) =pss (pssmg b smg') = associated a b
> ---------------------------------------------------------------------------
>
> So a p-subsemigroup <a> is a type, and it can be made a Semigroup, and
> a program can compute over <a>.
> And also a program can compare <a> and <b>, and to have the Setoid of
> p-subsemigroups in M.
> And there remains this difference:
>
> What to add to the language in order to make this possible:
> postulate p0 : extSmg@(pssmg a smg) =pss extSmg'@(pssmg b smg')
> postulate f : smg
> g : smg'
> g = f
> ?
>
>
>
>
>
>
>
>
>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY
andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
More information about the Agda
mailing list