[Agda] congruence on dependent types
Dominique Devriese
dominique.devriese at cs.kuleuven.be
Fri Jun 21 12:27:55 CEST 2013
I believe that Georges Gonthier mentioned he used this approach as
well in his POPL 2013 talk about the proof of the odd order theorem.
Regards,
Dominique
2013/6/21 Andreas Abel <andreas.abel at ifi.lmu.de>:
> 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/
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
More information about the Agda
mailing list