<div dir="ltr"><div class="gmail_quote"><div dir="ltr">Hi Sergei,<div> First of all you should be using "Relation.Binary.Reasoning.PartialOrder" (where the Poset is from your DecTotalOrder) which provides a nicer interface to the reasoning.</div><div><br></div><div>Secondly, yes the third example would fail. With the new reasoning you can now do `strict`, `non-strict` and `setoid equality` reasoning. We haven't added propositional equality to it yet. If you think such a feature would be useful, please create an issue on the Github page for the standard library or you could create a pull request adding it yourself.</div><div>Thanks,<br>Matthew</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Mar 20, 2019 at 2:46 AM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">On Sun, 2019-03-17 at 15:24 +0300, Sergei Meshveliani wrote:<br>
> Dear standard library supporters,<br>
> <br>
> I am trying to use  inequality reasoning  provided in lib-0.18, <br>
> and have certain difficulties.<br>
> <br>
> Currently I use a non-standard  InequalityReasoning  by Ulf Norell<br>
> (see LtReasoning.agda attached).<br>
> <br>
> Now I need to replace it with the standard inequality reasoning  of  <br>
> lib-0.18-candidate.<br>
> <br>
> I attach a file with small examples  test1 ... test6  <br>
> <br>
> that work under InequalityReasoning by Ulf Norell.<br>
> They have been tested under  <br>
>                       Agda-2.6.0-candidate, ghc-8.6.3.<br>
> <br>
> They show proofs for various combinations of the relations <br>
>                                           _≡_, _≈_; _≤_, _<_.<br>
> <br>
> Can you, please, demonstrate the corresponding code with using the <br>
> inequality reasoning of lib-0.18 ?<br>
>  <br>
<br>
<br>
I discover now the responsible module in standard library<br>
0.18-candidate:<br>
                Relation.Binary.Reasoning.Base.Triple.<br>
<br>
Now, all examples work -- except  test3  below. test3 looks like a<br>
specialization of test2, and it is strange that it is not type-checked.<br>
<br>
Can people, please, tell what is the matter here? how to fix?<br>
It is possible to use PE.≡-Reasoning, with renaming constructors. <br>
But may be, its is possible some wiser usage of<br>
relation.Binary.Reasoning.Base.Triple -- ?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
-----------------------------------------------------------------------<br>
open import Relation.Binary using (Rel; Transitive; _Respects₂_;<br>
                                                    DecTotalOrder)<br>
open import Relation.Binary.PropositionalEquality as PE using (_≡_)<br>
import Relation.Binary.Reasoning.Base.Triple as IneqReasoning<br>
<br>
module _ {c ℓ₁ ℓ₂} (dto : DecTotalOrder c ℓ₁ ℓ₂)<br>
                   (open DecTotalOrder dto using (_≈_; _≤_; isPreorder)<br>
                                           renaming (Carrier to C))<br>
                   (_<_      : Rel C ℓ₂)<br>
                   (<-resp-≈ : _<_ Respects₂ _≈_)<br>
  where<br>
  postulate<br>
    <-trans   : Transitive _<_<br>
    <⇒≤       : {x y : C} → x < y → x ≤ y<br>
    <-≤-trans : {x y z : C} → x < y → y ≤ z → x < z<br>
    ≤-<-trans : {x y z : C} → x ≤ y → y < z → x < z<br>
<br>
  open IneqReasoning isPreorder <-trans <-resp-≈ <⇒≤ <-≤-trans ≤-<-trans<br>
<br>
  test1 : {x y z : C} → x ≈ y → y ≈ z → x ≈ z<br>
  test1 {x} {y} {z} x≈y y≈z =<br>
                        begin-equality x   ≈⟨ x≈y ⟩<br>
                                       y   ≈⟨ y≈z ⟩<br>
                                       z<br>
                        ∎<br>
<br>
  test2 :  {x y z : C} → x ≈ y → y ≡ z → x ≈ z<br>
  test2 {x} {y} {z} x≈y y≡z =<br>
                            begin-equality x   ≈⟨ x≈y ⟩<br>
                                           y   ≡⟨ y≡z ⟩<br>
                                           z<br>
                            ∎<br>
<br>
  test3 :  {x y z : C} → x ≡ y → y ≡ z → x ≡ z       -- fails<br>
  test3 {x} {y} {z} x≡y y≡z =<br>
                             begin-equality x   ≡⟨ x≡y ⟩<br>
                                            y   ≡⟨ y≡z ⟩<br>
                                            z<br>
                             ∎<br>
------------------------------------------------------------------------<br>
<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>
</div></div>