<div dir="ltr">The problem you have is that you can't talk about the aux function. You can use<div>named where modules to make it visible which enables proving the relevant</div><div>lemma for it:</div><div><br></div><div><div>open import Function using (flip)</div><div>open import Relation.Binary using (Rel; Tri; StrictTotalOrder)</div><div>open import Relation.Binary.PropositionalEquality as PE using (_≡_)</div><div>open import Data.Empty</div><div><br></div><div>module _ {α α= α<} (sto : StrictTotalOrder α α= α<)</div><div>  where</div><div>  open StrictTotalOrder sto using (_≈_; _<_; compare)</div><div>                            renaming (Carrier to C)</div><div>  _>_ = flip _<_</div><div>  open Tri</div><div><br></div><div>  min : (x y : C) → C</div><div>  min x y = aux (compare x y)</div><div>    module min where</div><div>          aux : Tri (x < y) (x ≈ y) (x > y) → C</div><div>          aux (tri< _ _ _) = x</div><div>          aux (tri≈ _ _ _) = x</div><div>          aux (tri> _ _ _) = y</div><div><br></div><div>  lemma-aux : ∀ {x y} → x < y → (t : Tri (x < y) (x ≈ y) (x > y)) → min.aux x y t ≡ x</div><div>  lemma-aux x<y (tri< a ¬b ¬c) = _≡_.refl</div><div>  lemma-aux x<y (tri≈ ¬a b ¬c) = _≡_.refl</div><div>  lemma-aux x<y (tri> ¬a ¬b c) = ⊥-elim (¬a x<y)</div><div><br></div><div>  lemma :  ∀ x y → x < y → min x y ≡ x</div><div>  lemma x y x<y = lemma-aux x<y (compare x y)</div></div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Mar 1, 2017 at 7:25 AM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Tue, 2017-02-28 at 16:00 +0100, Nils Anders Danielsson wrote:<br>
> On 2017-02-28 12:49, Sergei Meshveliani wrote:<br>
> > I knew that it is not reduced. But how to make it reduced there without<br>
> > using `with' or `case' ?<br>
><br>
> Use regular pattern matching.<br>
><br>
<br>
<br>
</span>Can anybody show, please, how to prove in Agda<br>
<br>
    lemma :  ∀ x y → x < y → min x y ≡ x<br>
<br>
by using a regular pattern matching, and without using `with' or 'case'<br>
?<br>
<br>
min  is defined here:<br>
<br>
------------------------------<wbr>------------------------------<wbr>-------<br>
open import Function using (flip)<br>
open import Relation.Binary using (Rel; Tri; StrictTotalOrder)<br>
open import Relation.Binary.<wbr>PropositionalEquality as PE using (_≡_)<br>
<br>
module _ {α α= α<} (sto : StrictTotalOrder α α= α<)<br>
  where<br>
  open StrictTotalOrder sto using (_≈_; _<_; compare)<br>
                            renaming (Carrier to C)<br>
  _>_ = flip _<_<br>
  open Tri<br>
<br>
  min : (x y : C) → C<br>
  min x y =<br>
          aux (compare x y)<br>
          where<br>
          aux : Tri (x < y) (x ≈ y) (x > y) → C<br>
          aux (tri< _ _ _) = x<br>
          aux (tri≈ _ _ _) = x<br>
          aux (tri> _ _ _) = y<br>
<br>
  lemma :  ∀ x y → x < y → min x y ≡ x<br>
  lemma x y x<y =<br>
                ?<br>
------------------------------<wbr>------------------------------<wbr>-------<br>
<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>