[Agda] signature for `with' branch

[Ulf Norell]

The problem you have is that you can't talk about the aux function. You can
use
named where modules to make it visible which enables proving the relevant
lemma for it:

open import Function using (flip)
open import Relation.Binary using (Rel; Tri; StrictTotalOrder)
open import Relation.Binary.PropositionalEquality as PE using (_≡_)
open import Data.Empty

module _ {α α= α<} (sto : StrictTotalOrder α α= α<)
  where
  open StrictTotalOrder sto using (_≈_; _<_; compare)
                            renaming (Carrier to C)
  _>_ = flip _<_
  open Tri

  min : (x y : C) → C
  min x y = aux (compare x y)
    module min where
          aux : Tri (x < y) (x ≈ y) (x > y) → C
          aux (tri< _ _ _) = x
          aux (tri≈ _ _ _) = x
          aux (tri> _ _ _) = y

  lemma-aux : ∀ {x y} → x < y → (t : Tri (x < y) (x ≈ y) (x > y)) → min.aux
x y t ≡ x
  lemma-aux x<y (tri< a ¬b ¬c) = _≡_.refl
  lemma-aux x<y (tri≈ ¬a b ¬c) = _≡_.refl
  lemma-aux x<y (tri> ¬a ¬b c) = ⊥-elim (¬a x<y)

  lemma :  ∀ x y → x < y → min x y ≡ x
  lemma x y x<y = lemma-aux x<y (compare x y)

/ Ulf

On Wed, Mar 1, 2017 at 7:25 AM, Sergei Meshveliani <mechvel at botik.ru> wrote:

> On Tue, 2017-02-28 at 16:00 +0100, Nils Anders Danielsson wrote:
> > On 2017-02-28 12:49, Sergei Meshveliani wrote:
> > > I knew that it is not reduced. But how to make it reduced there without
> > > using `with' or `case' ?
> >
> > Use regular pattern matching.
> >
>
>
> Can anybody show, please, how to prove in Agda
>
>     lemma :  ∀ x y → x < y → min x y ≡ x
>
> by using a regular pattern matching, and without using `with' or 'case'
> ?
>
> min  is defined here:
>
> -------------------------------------------------------------------
> open import Function using (flip)
> open import Relation.Binary using (Rel; Tri; StrictTotalOrder)
> open import Relation.Binary.PropositionalEquality as PE using (_≡_)
>
> module _ {α α= α<} (sto : StrictTotalOrder α α= α<)
>   where
>   open StrictTotalOrder sto using (_≈_; _<_; compare)
>                             renaming (Carrier to C)
>   _>_ = flip _<_
>   open Tri
>
>   min : (x y : C) → C
>   min x y =
>           aux (compare x y)
>           where
>           aux : Tri (x < y) (x ≈ y) (x > y) → C
>           aux (tri< _ _ _) = x
>           aux (tri≈ _ _ _) = x
>           aux (tri> _ _ _) = y
>
>   lemma :  ∀ x y → x < y → min x y ≡ x
>   lemma x y x<y =
>                 ?
> -------------------------------------------------------------------
>
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170301/7b96fc61/attachment.html>