------------------------------------------------------------------------
-- Some counterexamples
------------------------------------------------------------------------

{-# OPTIONS --without-K --safe --sized-types #-}

module Bisimilarity.Up-to.Counterexamples where

open import Equality.Propositional
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Size

open import Bijection equality-with-J using (_↔_)
open import Equality.Decision-procedures equality-with-J
open import Fin equality-with-J
open import Function-universe equality-with-J hiding (id; _∘_)
open import Surjection equality-with-J using (_↠_)

open import Indexed-container using (Container; ν; ⟦_⟧; force)
open import Labelled-transition-system
import Up-to

import Bisimilarity
import Bisimilarity.Classical
open import Bisimilarity.Comparison
import Bisimilarity.Equational-reasoning-instances
import Bisimilarity.Step
import Bisimilarity.Up-to
open import Equational-reasoning
open import Relation

private

  -- A combination of some parametrised modules.

  module Combination {} (lts : LTS ) where

    open Bisimilarity lts public
    open Bisimilarity.Classical lts public using (Progression)
    open Bisimilarity.Step lts (LTS._[_]⟶_ lts) (LTS._[_]⟶_ lts) public
      using (Step; Step↔StepC)
    open Bisimilarity.Up-to lts public
    open LTS lts public hiding (_[_]⟶_)

-- There is a size-preserving relation transformer that is neither
-- monotone nor extensive.

∃size-preserving׬[monotone⊎extensive] :
   λ (lts : LTS lzero) 
  let open Combination lts in
   λ (F : Trans₂ (# 0) Proc) 
      Size-preserving F × ¬ (Monotone F  Extensive F)
∃size-preserving׬[monotone⊎extensive] =
  one-loop , F , F-pres , [ ¬-F-mono , ¬-F-extensive ]
  where
  open Combination one-loop

  F : Trans₂ (# 0) Proc
  F R = ¬_  R

  ¬-F-mono : ¬ Monotone F
  ¬-F-mono =
    Monotone F                                                   ↝⟨  mono  mono {_}) 
    ((λ _  )   _   _ )  F  _  )  F  _   _ ))  ↔⟨⟩
    ((λ _  )   _   _ )   _  ¬ )   _  ¬  _ ))  ↝⟨ _$ _ 
     _  ¬ )   _  ¬  _ )                                ↝⟨  hyp  hyp {tt}) 
    (¬   ¬  _ )                                              ↝⟨ _$ ⊥-elim 
    ¬  _                                                       ↝⟨ _$ _ ⟩□
                                                                

  ¬-F-extensive : ¬ Extensive F
  ¬-F-extensive =
    Extensive F        ↝⟨  hyp  hyp _) 
    ( _   ¬  _ )  ↝⟨ (_$ _)  (_$ _) ⟩□
                      

  total :  {i x y}  [ i ] x  y
  total = reflexive

  F-pres : Size-preserving F
  F-pres _ _ = total

-- A slight strengthening of the previous result, with a somewhat more
-- complicated proof: There are (at least two) size-preserving
-- relation transformers that are neither monotone nor extensive.

∃-2-size-preserving׬[monotone⊎extensive] :
   λ (lts : LTS lzero) 
  let open Combination lts in
   λ (F : Trans₂ (# 0) Proc) 
   λ (G : Trans₂ (# 0) Proc) 
    Size-preserving F × ¬ (Monotone F  Extensive F) ×
    Size-preserving G × ¬ (Monotone G  Extensive G) ×
    F  G
∃-2-size-preserving׬[monotone⊎extensive] =
    lts
  , F  , F 
  , F-pres , [ ¬-F-mono , ¬-F-extensive ]
  , F-pres , [ ¬-F-mono , ¬-F-extensive ]
  , F⊤≢F⊥
  where
  lts : LTS lzero
  lts = record
    { Proc      = Bool
    ; Label     = 
    ; _[_]⟶_    = λ _ ()
    ; is-silent = λ ()
    }

  open Combination lts

  F : Set  Trans₂ (# 0) Bool
  F A R p@(true  , false) = R p × A
  F A R p@(false , true)  = R p
  F A R p                 = ¬ R p

  ¬-F-mono :  {A}  ¬ Monotone (F A)
  ¬-F-mono {A} =
    Monotone (F A)                                                   ↝⟨  mono  mono {_}) 
    ((λ _  )   _   _ )  F A  _  )  F A  _   _ ))  ↝⟨  hyp {p}  hyp _ {p}) 
    F A  _  )  F A  _   _ )                                ↝⟨  hyp  hyp {true , true}) 
    (¬   ¬  _ )                                                  ↝⟨ _$ ⊥-elim 
    ¬  _                                                           ↝⟨ _$ _ ⟩□
                                                                    

  ¬-F-extensive :  {A}  ¬ Extensive (F A)
  ¬-F-extensive {A} =
    Extensive (F A)    ↝⟨  hyp  hyp  _   _ ) {true , true}) 
    ( _   ¬  _ )  ↝⟨ (_$ _)  (_$ _) ⟩□
                      

  F-pres :  {A}  Size-preserving (F A)
  F-pres R⊆∼i {true  , false} = R⊆∼i  proj₁
  F-pres R⊆∼i {false , true}  = R⊆∼i
  F-pres _    {true  , true}  = λ _  true 
  F-pres _    {false , false} = λ _  false 

  F⊤≢F⊥ : F   F 
  F⊤≢F⊥ =
    F   F                                                        ↝⟨ subst  F  F  _  ) (true , false)) 
    (F    _  ) (true , false)  F   _  ) (true , false))  ↔⟨⟩
    ( ×    × )                                                 ↝⟨ proj₂  (_$ _) ⟩□
                                                                   

-- There is a container C such that there are (at least two) relation
-- transformers satisfying λ F → ∀ {i} → F (ν C i) ⊆ ν C i that are
-- not up-to techniques with respect to C.

∃special-case-of-size-preserving׬up-to :
   λ (I : Set) 
   λ (C : Container I I) 
   λ (F : Trans (# 0) I) 
   λ (G : Trans (# 0) I) 
    (∀ {i}  F (ν C i)  ν C i) × ¬ Up-to.Up-to-technique C F ×
    (∀ {i}  G (ν C i)  ν C i) × ¬ Up-to.Up-to-technique C G ×
    F  G
∃special-case-of-size-preserving׬up-to =
    (Proc × Proc)
  , StepC
  , G  , G 
  , bisimilarity-pre-fixpoint
  , ¬-up-to
  , bisimilarity-pre-fixpoint
  , ¬-up-to
  , G⊤≢G⊥
  where

  data Proc : Set where
    p q r : Proc

  data _⟶_ : Proc  Proc  Set where
    p : p  p
    q : q  r

  lts = record
    { Proc      = Proc
    ; Label     = 
    ; _[_]⟶_    = λ p _ q  p  q
    ; is-silent = λ _  false
    }

  open Combination lts hiding (Proc)

  G : Set  Trans₂ (# 0) Proc
  G A R x = R (r , r)  ¬ R (p , r)  R x × A

  p≁r :  {i}  ¬ Bisimilarity i (p , r)
  p≁r hyp with left-to-right hyp p
  ... | _ , () , _

  bisimilarity-pre-fixpoint :
     {A i}  G A (Bisimilarity i)  Bisimilarity i
  bisimilarity-pre-fixpoint hyp = proj₁ (hyp reflexive p≁r)

  data S : Rel₂ (# 0) Proc where
    pq : S (p , q)

  S⊆StepGS :  {A}  S  Step (G A S)
  Step.left-to-right (S⊆StepGS pq) p = r , q , λ ()
  Step.right-to-left (S⊆StepGS pq) q = p , p , λ ()

  p≁q : ¬ Bisimilarity  (p , q)
  p≁q hyp with left-to-right hyp p
  ... | r , q , p∼r = p≁r (force p∼r)

  ¬-up-to :  {A}  ¬ Up-to-technique (G A)
  ¬-up-to {A} =
    Up-to-technique (G A)                         ↝⟨  up-to  up-to) 
    (S   StepC  (G A S)  S  Bisimilarity )  ↝⟨  hyp below  hyp (Step↔StepC _  below)) 
    (S  Step (G A S)  S  Bisimilarity )       ↝⟨ _$ S⊆StepGS 
    S  Bisimilarity                             ↝⟨ _$ pq 
    Bisimilarity  (p , q)                        ↝⟨ p≁q ⟩□
                                                 

  G⊤≢G⊥ : G   G 
  G⊤≢G⊥ =
    G   G                                                     ↝⟨ subst  G  G (uncurry _≡_) (q , q)) 
    (G  (uncurry _≡_) (q , q)  G  (uncurry _≡_) (q , q))      ↔⟨⟩
    ((r  r  p  r  q  q × )  (r  r  p  r  q  q × ))  ↝⟨ _$  _ _  refl , _) 
    (r  r  p  r  q  q × )                                  ↝⟨ proj₂  (_$ λ ())  (_$ refl) ⟩□
                                                                

-- There is a container C such that there are (at least two) relation
-- transformers satisfying λ F → ∀ {i} → F (ν C i) ⊆ ν C i that are
-- not size-preserving with respect to C.

∃special-case-of-size-preserving׬size-preserving :
   λ (I : Set) 
   λ (C : Container I I) 
   λ (F : Trans (# 0) I) 
   λ (G : Trans (# 0) I) 
    (∀ {i}  F (ν C i)  ν C i) × ¬ Up-to.Size-preserving C F ×
    (∀ {i}  G (ν C i)  ν C i) × ¬ Up-to.Size-preserving C G ×
    F  G
∃special-case-of-size-preserving׬size-preserving =
  Σ-map id (Σ-map id (Σ-map id (Σ-map id (Σ-map id
    (Σ-map (_∘ Up-to.size-preserving→up-to _) (Σ-map id
       (Σ-map (_∘ Up-to.size-preserving→up-to _) id)))))))
    ∃special-case-of-size-preserving׬up-to

-- There is a monotone, extensive and size-preserving relation
-- transformer that is not compatible.

∃monotone×extensive×size-preserving׬compatible :
   λ (lts : LTS lzero) 
  let open Combination lts in
   λ (F : Trans₂ (# 0) Proc) 
    Monotone F × Extensive F × Size-preserving F × ¬ Compatible F
∃monotone×extensive×size-preserving׬compatible =
    one-transition
  , F
  , mono
  , extensive
  , pres
  , ¬comp

  where

  -- An LTS with two distinct processes and one transition from one to
  -- the other.

  one-transition : LTS lzero
  one-transition = record
    { Proc      = Bool
    ; Label     = 
    ; _[_]⟶_    = λ x _ y  T (x  not y)
    ; is-silent = λ _  false
    }

  open Combination one-transition

  -- A relation transformer.

  F : Trans₂ (# 0) Proc
  F R (true , true) = R (false , false)  R (true , true)
  F R               = R

  -- F is monotone.

  mono : Monotone F
  mono R⊆S {true  , true}  = ⊎-map R⊆S R⊆S
  mono R⊆S {true  , false} = R⊆S
  mono R⊆S {false , true}  = R⊆S
  mono R⊆S {false , false} = R⊆S

  -- F is extensive.

  extensive : Extensive F
  extensive R {true  , true}  = inj₂
  extensive R {true  , false} = id
  extensive R {false , true}  = id
  extensive R {false , false} = id

  -- Bisimilarity of size i is a pre-fixpoint of F.

  pre :  {i}  F (Bisimilarity i)  Bisimilarity i
  pre {x = true  , true}  = λ _  true 
  pre {x = true  , false} = id
  pre {x = false , true}  = id
  pre {x = false , false} = id

  -- F is size-preserving.

  pres : Size-preserving F
  pres = _⇔_.from (monotone→⇔ mono)  {_ x}  pre {x = x})

  -- A relation.

  R : Rel₂ (# 0) Proc
  R _ = 

  -- A lemma.

  StepRff : Step R (false , false)
  Step.left-to-right StepRff ()
  Step.right-to-left StepRff ()

  -- F is not compatible.

  ¬comp : ¬ Compatible F
  ¬comp =
    Compatible F                                                     ↝⟨  comp {x}  comp {x = x}) 

    F ( StepC  R)   StepC  (F R)                                ↝⟨  le  le {true , true}) 

    (F ( StepC  R) (true , true)   StepC  (F R) (true , true))  ↔⟨⟩

    ( StepC  R (false , false)   StepC  R (true , true) 
      StepC  (F R) (true , true))                                  ↝⟨ _$ inj₁ (_⇔_.to (Step↔StepC _) StepRff) 

     StepC  (F R) (true , true)                                    ↝⟨  step  StepC.left-to-right {p = true} {q = true} step {p′ = false} _ ) 

    ( λ y  T (not y) × F R (false , y))                            ↔⟨⟩

    ( λ y  T (not y) × )                                          ↝⟨ proj₂  proj₂ ⟩□

                                                                    

-- An LTS used in a couple of lemmas below, along with some
-- properties.

module PQR where

  -- An LTS with two sets of processes, three "to the left", and three
  -- "to the right".

  Side : Set
  Side = Bool

  pattern left  = true
  pattern right = false

  data Process : Set where
    p q r : Side  Process

  data Label : Set where
    pq pr : Label
    qq rr : Side  Label

  infix 4 _[_]⟶_

  data _[_]⟶_ : Process  Label  Process  Set where
    pq :  {s}  p s [ pq ]⟶ q s
    pr :  {s}  p s [ pr ]⟶ r s
    qq :  {s}  q s [ qq s ]⟶ q s
    rr :  {s}  r s [ rr s ]⟶ r s

  lts : LTS lzero
  lts = record
    { Proc      = Process
    ; Label     = Label
    ; _[_]⟶_    = _[_]⟶_
    ; is-silent = λ _  false
    }

  open Combination lts public hiding (Label)

  -- Two relation transformers: F and G both add (at most) one pair to
  -- the underlying relation.

  data F (R : Rel₂ (# 0) Proc) : Rel₂ (# 0) Proc where
    qq  : F R (q left , q right)
    [_] :  {x}  R x  F R x

  data G (R : Rel₂ (# 0) Proc) : Rel₂ (# 0) Proc where
    rr  : G R (r left , r right)
    [_] :  {x}  R x  G R x

  -- A relation that adds one pair to reflexivity.

  data S : Rel₂ (# 0) Proc where
    pp   : S (p left , p right)
    refl :  {x}  S (x , x)

  -- S progresses to F (G S).

  S-prog : Progression S (F (G S))
  S-prog pp   = Step.⟨  where
                          pq  _ , pq , qq
                          pr  _ , pr , [ rr ])
                     ,  where
                          pq  _ , pq , qq
                          pr  _ , pr , [ rr ])
                     
  S-prog refl = Step.⟨  where
                          pq  _ , pq , [ [ refl ] ]
                          pr  _ , pr , [ [ refl ] ]
                          qq  _ , qq , [ [ refl ] ]
                          rr  _ , rr , [ [ refl ] ])
                     ,  where
                          pq  _ , pq , [ [ refl ] ]
                          pr  _ , pr , [ [ refl ] ]
                          qq  _ , qq , [ [ refl ] ]
                          rr  _ , rr , [ [ refl ] ])
                     

  S-prog′ : S   StepC  (F (G S))
  S-prog′ Sx = _⇔_.to (Step↔StepC _) (S-prog Sx)

  -- The two processes q left and q right are not bisimilar.

  q≁q : ¬ q left  q right
  q≁q =
    q left  q right                                ↝⟨  rel  StepC.left-to-right rel qq) 
    ( λ y  q right [ qq left ]⟶ y × q left ∼′ y)  ↝⟨  { (_ , () , _) }) ⟩□
                                                   

  -- The two processes r left and r right are not bisimilar.

  r≁r : ¬ r left  r right
  r≁r =
    r left  r right                                ↝⟨  rel  StepC.left-to-right rel rr) 
    ( λ y  r right [ rr left ]⟶ y × r left ∼′ y)  ↝⟨  { (_ , () , _) }) ⟩□
                                                   

  -- F ∘ G is not an up-to technique.

  ¬-F∘G-up-to : ¬ Up-to-technique (F  G)
  ¬-F∘G-up-to =
    Up-to-technique (F  G)                    ↝⟨  up-to  up-to S-prog′) 
    S  Bisimilarity                          ↝⟨  le  le pp) 
    p left  p right                           ↝⟨  rel  StepC.left-to-right rel pq) 
    ( λ y  p right [ pq ]⟶ y × q left ∼′ y)  ↝⟨  { (.(q right) , pq , rel)  rel }) 
    q left ∼′ q right                          ↝⟨  rel  q≁q (force rel)) 
                                              

  -- F is not equal to G.

  F≢G : F  G
  F≢G =
    F  G                                                              ↝⟨ subst  F  F  _  ) (q left , q right)) 
    (F  _  ) (q left , q right)  G  _  ) (q left , q right))  ↝⟨ _$ qq 
    G  _  ) (q left , q right)                                     ↝⟨  { [ () ] }) ⟩□
                                                                      

  module F-lemmas where

    -- F is monotone.

    mono : Monotone F
    mono R⊆S qq      = qq
    mono R⊆S [ Rxy ] = [ R⊆S Rxy ]

    -- F is extensive.

    ext : Extensive F
    ext = λ _  [_]

    -- F is not size-preserving.

    ¬-pres : ¬ Size-preserving F
    ¬-pres =
      Size-preserving F                    ↝⟨  pres  _⇔_.to (monotone→⇔ mono) pres) 
      F (Bisimilarity )  Bisimilarity   ↝⟨ _$ qq 
      q left  q right                     ↝⟨ q≁q ⟩□
                                          

    -- F is an up-to technique.

    module _ {R} (R-prog′ : R   StepC  (F R)) where

      R-prog : Progression R (F R)
      R-prog Rx = _⇔_.from (Step↔StepC _) (R-prog′ Rx)

      ¬rr :  {s}  ¬ R (r s , r (not s))
      ¬rr rel with Progression.left-to-right R-prog rel rr
      ¬rr {true}  _ | _ , () , _
      ¬rr {false} _ | _ , () , _

      ¬qq :  {s}  ¬ R (q s , q (not s))
      ¬qq rel with Progression.left-to-right R-prog rel qq
      ¬qq {true}  _ | _ , () , _
      ¬qq {false} _ | _ , () , _

      ¬pp :  {s}  ¬ R (p s , p (not s))
      ¬pp rel with Progression.left-to-right R-prog rel pr
      ... | .(r _) , pr , [ rel′ ] = ¬rr rel′

      ¬pq :  {s₁ s₂}  ¬ R (p s₁ , q s₂)
      ¬pq rel with Progression.left-to-right R-prog rel pq
      ... | _ , () , _

      ¬qp :  {s₁ s₂}  ¬ R (q s₁ , p s₂)
      ¬qp rel with Progression.right-to-left R-prog rel pq
      ... | _ , () , _

      ¬pr :  {s₁ s₂}  ¬ R (p s₁ , r s₂)
      ¬pr rel with Progression.left-to-right R-prog rel pq
      ... | _ , () , _

      ¬rp :  {s₁ s₂}  ¬ R (r s₁ , p s₂)
      ¬rp rel with Progression.right-to-left R-prog rel pq
      ... | _ , () , _

      ¬qr :  {s₁ s₂}  ¬ R (q s₁ , r s₂)
      ¬qr rel with Progression.right-to-left R-prog rel rr
      ... | _ , () , _

      ¬rq :  {s₁ s₂}  ¬ R (r s₁ , q s₂)
      ¬rq rel with Progression.left-to-right R-prog rel rr
      ... | _ , () , _

      up-to : R  Bisimilarity 
      up-to {p left  , p left}  rel = reflexive
      up-to {p left  , p right} rel = ⊥-elim (¬pp rel)
      up-to {p right , p left}  rel = ⊥-elim (¬pp rel)
      up-to {p right , p right} rel = reflexive
      up-to {p _     , q _}     rel = ⊥-elim (¬pq rel)
      up-to {p _     , r _}     rel = ⊥-elim (¬pr rel)
      up-to {q _     , p _}     rel = ⊥-elim (¬qp rel)
      up-to {q left  , q left}  rel = reflexive
      up-to {q left  , q right} rel = ⊥-elim (¬qq rel)
      up-to {q right , q left}  rel = ⊥-elim (¬qq rel)
      up-to {q right , q right} rel = reflexive
      up-to {q _     , r _}     rel = ⊥-elim (¬qr rel)
      up-to {r _     , p _}     rel = ⊥-elim (¬rp rel)
      up-to {r _     , q _}     rel = ⊥-elim (¬rq rel)
      up-to {r left  , r left}  rel = reflexive
      up-to {r left  , r right} rel = ⊥-elim (¬rr rel)
      up-to {r right , r left}  rel = ⊥-elim (¬rr rel)
      up-to {r right , r right} rel = reflexive

  module G-lemmas where

    -- G is monotone.

    mono : Monotone G
    mono R⊆S rr      = rr
    mono R⊆S [ Rxy ] = [ R⊆S Rxy ]

    -- G is extensive.

    ext : Extensive G
    ext = λ _  [_]

    -- G is not size-preserving.

    ¬-pres : ¬ Size-preserving G
    ¬-pres =
      Size-preserving G                    ↝⟨  pres  _⇔_.to (monotone→⇔ mono) pres) 
      G (Bisimilarity )  Bisimilarity   ↝⟨ _$ rr 
      r left  r right                     ↝⟨ r≁r ⟩□
                                          

    -- G is an up-to technique.

    module _ {R} (R-prog′ : R   StepC  (G R)) where

      R-prog : Progression R (G R)
      R-prog Rx = _⇔_.from (Step↔StepC _) (R-prog′ Rx)

      ¬rr :  {s}  ¬ R (r s , r (not s))
      ¬rr rel with Progression.left-to-right R-prog rel rr
      ¬rr {true}  _ | _ , () , _
      ¬rr {false} _ | _ , () , _

      ¬qq :  {s}  ¬ R (q s , q (not s))
      ¬qq rel with Progression.left-to-right R-prog rel qq
      ¬qq {true}  _ | _ , () , _
      ¬qq {false} _ | _ , () , _

      ¬pp :  {s}  ¬ R (p s , p (not s))
      ¬pp rel with Progression.left-to-right R-prog rel pq
      ... | .(q _) , pq , [ rel′ ] = ¬qq rel′

      ¬pq :  {s₁ s₂}  ¬ R (p s₁ , q s₂)
      ¬pq rel with Progression.left-to-right R-prog rel pq
      ... | _ , () , _

      ¬qp :  {s₁ s₂}  ¬ R (q s₁ , p s₂)
      ¬qp rel with Progression.right-to-left R-prog rel pq
      ... | _ , () , _

      ¬pr :  {s₁ s₂}  ¬ R (p s₁ , r s₂)
      ¬pr rel with Progression.left-to-right R-prog rel pq
      ... | _ , () , _

      ¬rp :  {s₁ s₂}  ¬ R (r s₁ , p s₂)
      ¬rp rel with Progression.right-to-left R-prog rel pq
      ... | _ , () , _

      ¬qr :  {s₁ s₂}  ¬ R (q s₁ , r s₂)
      ¬qr rel with Progression.right-to-left R-prog rel rr
      ... | _ , () , _

      ¬rq :  {s₁ s₂}  ¬ R (r s₁ , q s₂)
      ¬rq rel with Progression.left-to-right R-prog rel rr
      ... | _ , () , _

      up-to : R  Bisimilarity 
      up-to {p left  , p left}  rel = reflexive
      up-to {p left  , p right} rel = ⊥-elim (¬pp rel)
      up-to {p right , p left}  rel = ⊥-elim (¬pp rel)
      up-to {p right , p right} rel = reflexive
      up-to {p _     , q _}     rel = ⊥-elim (¬pq rel)
      up-to {p _     , r _}     rel = ⊥-elim (¬pr rel)
      up-to {q _     , p _}     rel = ⊥-elim (¬qp rel)
      up-to {q left  , q left}  rel = reflexive
      up-to {q left  , q right} rel = ⊥-elim (¬qq rel)
      up-to {q right , q left}  rel = ⊥-elim (¬qq rel)
      up-to {q right , q right} rel = reflexive
      up-to {q _     , r _}     rel = ⊥-elim (¬qr rel)
      up-to {r _     , p _}     rel = ⊥-elim (¬rp rel)
      up-to {r _     , q _}     rel = ⊥-elim (¬rq rel)
      up-to {r left  , r left}  rel = reflexive
      up-to {r left  , r right} rel = ⊥-elim (¬rr rel)
      up-to {r right , r left}  rel = ⊥-elim (¬rr rel)
      up-to {r right , r right} rel = reflexive

-- There are monotone and extensive up-to techniques F and G such
-- that F ∘ G is not an up-to-technique.
--
-- Pous and Sangiorgi discuss another instance of this property in
-- Section 6.5.4 of "Enhancements of the bisimulation proof method".

∃[monotone×extensive×up-to]²×¬∘-up-to :
   λ (lts : LTS lzero) 
  let open Combination lts in
   λ (F : Trans₂ (# 0) Proc) 
   λ (G : Trans₂ (# 0) Proc) 
    Monotone F × Extensive F × Up-to-technique F ×
    Monotone G × Extensive G × Up-to-technique G ×
    ¬ Up-to-technique (F  G)
∃[monotone×extensive×up-to]²×¬∘-up-to =
    lts
  , F
  , G
  , F-lemmas.mono
  , F-lemmas.ext
  , F-lemmas.up-to
  , G-lemmas.mono
  , G-lemmas.ext
  , G-lemmas.up-to
  , ¬-F∘G-up-to
  where
  open PQR

-- It is not the case that every monotone and extensive up-to
-- technique is size-preserving.

¬monotone×extensive×up-to→size-preserving :
   λ (lts : LTS lzero) 
  let open Combination lts in
  ¬ (∀ {F}  Monotone F  Extensive F  Up-to-technique F 
             Size-preserving F)
¬monotone×extensive×up-to→size-preserving =
    lts
  , λ up-to→pres 
      ¬-F∘G-up-to $
      size-preserving→up-to $
      ∘-closure (up-to→pres F-lemmas.mono F-lemmas.ext F-lemmas.up-to)
                (up-to→pres G-lemmas.mono G-lemmas.ext G-lemmas.up-to)
  where
  open PQR

-- Up-to-technique is not closed under composition, not even for
-- monotone and extensive relation transformers.

¬-∘-closure :
   λ (lts : LTS lzero) 
  let open Combination lts in
  ¬ ({F G : Trans₂ (# 0) Proc} 
     Monotone F  Extensive F 
     Monotone G  Extensive G 
     Up-to-technique F 
     Up-to-technique G 
     Up-to-technique (F  G))
¬-∘-closure =
    lts
  , λ ∘-closure 
        ¬-F∘G-up-to (∘-closure F-lemmas.mono F-lemmas.ext
                               G-lemmas.mono G-lemmas.ext
                               F-lemmas.up-to G-lemmas.up-to)
  where
  open PQR

-- There are (at least two) monotone and extensive up-to techniques
-- that are not size-preserving.

∃monotone×extensive×up-to׬size-preserving :
   λ (lts : LTS lzero) 
  let open Combination lts in
   λ (F : Trans₂ (# 0) Proc) 
   λ (G : Trans₂ (# 0) Proc) 
    Monotone F × Extensive F × Up-to-technique F × ¬ Size-preserving F ×
    Monotone G × Extensive G × Up-to-technique G × ¬ Size-preserving G ×
    F  G
∃monotone×extensive×up-to׬size-preserving =
    lts
  , F , G
  , F-lemmas.mono
  , F-lemmas.ext
  , F-lemmas.up-to
  , F-lemmas.¬-pres
  , G-lemmas.mono
  , G-lemmas.ext
  , G-lemmas.up-to
  , G-lemmas.¬-pres
  , F≢G
  where
  open PQR