[Agda] Fwd: new InequalityReasoning

[Matthew Daggitt]

Hi Sergei,
 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.

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.
Thanks,
Matthew

On Wed, Mar 20, 2019 at 2:46 AM Sergei Meshveliani <mechvel at botik.ru> wrote:

> On Sun, 2019-03-17 at 15:24 +0300, Sergei Meshveliani wrote:
> > Dear standard library supporters,
> >
> > I am trying to use  inequality reasoning  provided in lib-0.18,
> > and have certain difficulties.
> >
> > Currently I use a non-standard  InequalityReasoning  by Ulf Norell
> > (see LtReasoning.agda attached).
> >
> > Now I need to replace it with the standard inequality reasoning  of
> > lib-0.18-candidate.
> >
> > I attach a file with small examples  test1 ... test6
> >
> > that work under InequalityReasoning by Ulf Norell.
> > They have been tested under
> >                       Agda-2.6.0-candidate, ghc-8.6.3.
> >
> > They show proofs for various combinations of the relations
> >                                           _≡_, _≈_; _≤_, _<_.
> >
> > Can you, please, demonstrate the corresponding code with using the
> > inequality reasoning of lib-0.18 ?
> >
>
>
> I discover now the responsible module in standard library
> 0.18-candidate:
>                 Relation.Binary.Reasoning.Base.Triple.
>
> Now, all examples work -- except  test3  below. test3 looks like a
> specialization of test2, and it is strange that it is not type-checked.
>
> Can people, please, tell what is the matter here? how to fix?
> It is possible to use PE.≡-Reasoning, with renaming constructors.
> But may be, its is possible some wiser usage of
> relation.Binary.Reasoning.Base.Triple -- ?
>
> Thanks,
>
> ------
> Sergei
>
>
> -----------------------------------------------------------------------
> open import Relation.Binary using (Rel; Transitive; _Respects₂_;
>                                                     DecTotalOrder)
> open import Relation.Binary.PropositionalEquality as PE using (_≡_)
> import Relation.Binary.Reasoning.Base.Triple as IneqReasoning
>
> module _ {c ℓ₁ ℓ₂} (dto : DecTotalOrder c ℓ₁ ℓ₂)
>                    (open DecTotalOrder dto using (_≈_; _≤_; isPreorder)
>                                            renaming (Carrier to C))
>                    (_<_      : Rel C ℓ₂)
>                    (<-resp-≈ : _<_ Respects₂ _≈_)
>   where
>   postulate
>     <-trans   : Transitive _<_
>     <⇒≤       : {x y : C} → x < y → x ≤ y
>     <-≤-trans : {x y z : C} → x < y → y ≤ z → x < z
>     ≤-<-trans : {x y z : C} → x ≤ y → y < z → x < z
>
>   open IneqReasoning isPreorder <-trans <-resp-≈ <⇒≤ <-≤-trans ≤-<-trans
>
>   test1 : {x y z : C} → x ≈ y → y ≈ z → x ≈ z
>   test1 {x} {y} {z} x≈y y≈z =
>                         begin-equality x   ≈⟨ x≈y ⟩
>                                        y   ≈⟨ y≈z ⟩
>                                        z
>                         ∎
>
>   test2 :  {x y z : C} → x ≈ y → y ≡ z → x ≈ z
>   test2 {x} {y} {z} x≈y y≡z =
>                             begin-equality x   ≈⟨ x≈y ⟩
>                                            y   ≡⟨ y≡z ⟩
>                                            z
>                             ∎
>
>   test3 :  {x y z : C} → x ≡ y → y ≡ z → x ≡ z       -- fails
>   test3 {x} {y} {z} x≡y y≡z =
>                              begin-equality x   ≡⟨ x≡y ⟩
>                                             y   ≡⟨ y≡z ⟩
>                                             z
>                              ∎
> ------------------------------------------------------------------------
>
>
> _______________________________________________
> 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/20190320/fe9705a6/attachment.html>