[Agda] congruence on dependent types

Sergei Meshveliani mechvel at botik.ru
Fri Jun 21 12:28:46 CEST 2013


On Fri, 2013-06-21 at 11:30 +0200, Andreas Abel wrote:
> 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.


But this  <a>  also needs to be an algebraic domain, with various
operations on it: of Setoid, of Semigroup,  and such.
Because a subsemigroup  <a>  also needs to be of a  Semigroup,  and so
on.
So, if you represent it as a relation, still you will need to relate
some type to it, and this type will depend on  a.

As to the language extension which I asked of, may be, this relates to 
conditional pattern matching (maybe, conditional unification) on the
type expressions. 
May be, this is a matter of  conditional rewriting rules  provided by
the programmer for the type expressions.
I do not know.

In principle, Agda expresses algebra (mathematics) much more adequately
than Haskell.
But let us point it out:

  there remains a certain disagreement between the Agda type system
  and domain membership proofs in algebra.
  Namely: in an algebra proof,  <a>  can be replaced with any 
          equivalent   <b>  in the statement  f ∈ <a>,
          while the Agda checker does not allow this for 
          f : P-Subsemigroup a.

Regards,

------
Sergei

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




More information about the Agda mailing list