[Agda] new InequalityReasoning

[Sergei Meshveliani]

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