Using an equivalence in the context to force reduction

Question

The setting for this question is the same "merge of sorted lists" example from this earlier question.

{-# OPTIONS --sized-types #-}

open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P hiding (trans)

module ListMerge
   {𝒂 ℓ}
   (A : Set 𝒂)
   {_<_ : Rel A ℓ}
   (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_) where

   open import Data.Product
   open import Data.Unit
   open import Level
   open import Size

   data SortedList (l u : A) : {ι : Size} → Set (𝒂 ⊔ ℓ) where
      [] : {ι : _} → .(l < u) → SortedList l u {↑ ι}
      _∷[_]_ : {ι : _} (x : A) → .(l < x) → (xs : SortedList x u {ι}) →
               SortedList l u {↑ ι}

As before, I'm using sized types so that Agda can determine that the following merge function terminates:

   open IsStrictTotalOrder isStrictTotalOrder

   merge : ∀ {l u} → {ι : _} → SortedList l u {ι} →
                      {ι′ : _} → SortedList l u {ι′} → SortedList l u
   merge xs ([] _) = xs
   merge ([] _) ys = ys
   merge (x ∷[ l<x ] xs) (y ∷[ l<y ] ys) with compare x y
   ... | tri< _ _ _ = x ∷[ l<x ] (merge xs (y ∷[ _ ] ys))
   merge (x ∷[ l<x ] xs) (.x ∷[ _ ] ys) | tri≈ _ P.refl _ =
      x ∷[ l<x ] (merge xs ys)
   ... | tri> _ _ _ = y ∷[ l<y ] (merge (x ∷[ _ ] xs) ys)

What I'm trying to do is prove the following associativity theorem:

   assoc : ∀ {l u} → {ι₁ : _} → (x : SortedList l u {ι₁}) →
                     {ι₂ : _} → (y : SortedList l u {ι₂}) →
                     {ι₃ : _} → (z : SortedList l u {ι₃}) →
           merge (merge x y) z ≡ merge x (merge y z)

The cases where at least one list is [] follow easily by definition, but I'll include them for completeness.

   assoc ([] _) ([] _) ([] _) = P.refl
   assoc ([] _) ([] _) (_ ∷[ _ ] _) = P.refl
   assoc ([] _) (_ ∷[ _ ] _) ([] _) = P.refl
   assoc (_ ∷[ _ ] _) ([] _) ([] _) = P.refl
   assoc ([] _) (y ∷[ _ ] _) (z ∷[ _ ] _) with compare y z
   assoc ([] _) (y ∷[ _ ] ys) (.y ∷[ _ ] zs) | tri≈ _ P.refl _ = P.refl
   ... | tri< _ _ _ = P.refl
   ... | tri> _ _ _ = P.refl
   assoc (x ∷[ _ ] _) ([] _) (z ∷[ _ ] _) with compare x z
   assoc (x ∷[ _ ] xs) ([] _) (.x ∷[ _ ] zs) | tri≈ _ P.refl _ = P.refl
   ... | tri< _ _ _ = P.refl
   ... | tri> _ _ _ = P.refl
   assoc (x ∷[ _ ] _) (y ∷[ _ ] _) ([] _) with compare x y
   assoc (x ∷[ _ ] xs) (.x ∷[ _ ] ys) ([] _) | tri≈ _ P.refl _ = P.refl
   ... | tri< _ _ _ = P.refl
   ... | tri> _ _ _ = P.refl

However, I'm getting stuck trying to prove the remaining case, which has many sub-cases. In particular, I don't know how to "reuse" facts such as compare x y ≡ tri< .a .¬b .¬c inside proof contexts beneath the top level (without, say, introducing an auxiliary lemma).

I'm aware of, and have had some success with, the inspect (on steroids) idiom mentioned here, but my problem seems to be that the context in which I want to "reuse" the relevant fact isn't yet established when I use rewrite to simplify with the equality I've saved using inspect.

So for example in the following sub-case, I can capture the values of compare x y and compare y z using the following inspect calls:

   assoc (x ∷[ _ ] _) (y ∷[ _ ] _) (z ∷[ _ ] _)
         with compare x y | compare y z
         | P.inspect (hide (compare x) y) unit
         | P.inspect (hide (compare y) z) unit

and then rewrite to simplify:

   assoc {l} {u} (x ∷[ l<x ] xs) (y ∷[ _ ] ys) (.y ∷[ _ ] zs)
         | tri< _ _ _ | tri≈ _ P.refl _ | P.[ eq ] | P.[ eq′ ] rewrite eq | eq′ =

But I think the rewrite will only affect the goal which is active at that point. In particular, if in the body of the proof I use cong to shift into a nested context which permits more reduction, I may expose new occurrences of those comparisons which will not have been rewritten. (See the {!!} below for the location I mean.) My understanding of exactly how reduction proceeds is a little hazy, so I'd welcome any correction or clarification on this.

      begin
         x ∷[ _ ] merge (merge xs (y ∷[ _ ] ys)) (y ∷[ _ ] zs)
      ≡⟨ P.cong (λ xs → x ∷[ l<x ] xs) (assoc xs (y ∷[ _ ] ys) (y ∷[ _ ] zs)) ⟩
         x ∷[ _ ] merge xs (merge (y ∷[ _ ] ys) (y ∷[ _ ] zs))
      ≡⟨ P.cong (λ xs′ → x ∷[ _ ] merge xs xs′)
                {merge (y ∷[ _ ] ys) (y ∷[ _ ] zs)} {y ∷[ _ ] merge ys zs} {!!} ⟩
         x ∷[ _ ] merge xs (y ∷[ _ ] merge ys zs)
      ∎ where open import Relation.Binary.EqReasoning (P.setoid (SortedList l u))

(The implicit arguments to cong need to be made explicit here.)

When I put the cursor in the hole, I can see that the goal (somewhat paraphrased) is

merge (y ∷[ _ ] ys) (y ∷[ _ ] zs) | compare y y ≡ y ∷[ _ ] merge ys zs

despite the earlier rewrite eq′. Moreover in my context I have

eq′  : compare y y ≡ tri≈ .¬a refl .¬c

which seems to be exactly what I need to allow reduction to make progress so that refl will complete the proof-case.

Here's the placeholder for the remaining sub-cases.

   assoc (x ∷[ _ ] _) (_ ∷[ _ ] _) (z ∷[ _ ] _) | _ | _ | _ | _ = {!!}

I'm a little unconfident here; I don't know whether I'm misusing inspect on steroids, going about the proof the wrong way entirely, or just being stupid.

Is there a way to use the eq′ equivalence from the context to allow reduction to proceed?

Answer 1

Yes, as per Vitus' comment, one needs to pattern-match again on the outcome of the comparison. I ended up defining 3 helper lemmas, one for each branch of the trichotomy, and then using each lemma twice in the final proof.

merge≡ : ∀ {x l u} (l<x : l < x) {ι₁ : _} (xs : SortedList x u {ι₁}) {ι₂ : _} (ys : SortedList x u {ι₂}) →
         merge (x ∷[ l<x ] xs) (x ∷[ l<x ] ys) ≡ x ∷[ l<x ] merge xs ys
merge≡ {x} _ _ _ with compare x x
merge≡ _ _ _ | tri< _ x≢x _ = ⊥-elim (x≢x refl)
merge≡ _ _ _ | tri≈ _ refl _ = refl
merge≡ _ _ _ | tri> _ x≢x _ = ⊥-elim (x≢x refl)

merge< : ∀ {x y l u} (l<x : l < x) (l<y : l < y) (x<y : x < y)
         {ι₁ : _} (xs : SortedList x u {ι₁}) {ι₂ : _} (ys : SortedList y u {ι₂}) →
         merge (x ∷[ l<x ] xs) (y ∷[ l<y ] ys) ≡ x ∷[ l<x ] merge xs (y ∷[ x<y ] ys)
merge< {x} {y} _ _ _ _ _ with compare x y
merge< _ _ _ _ _ | tri< _ _ _ = refl
merge< _ _ x<y _ _ | tri≈ x≮y _ _ = ⊥-elim (x≮y x<y)
merge< _ _ x<y _ _ | tri> x≮y _ _ = ⊥-elim (x≮y x<y)

merge> : ∀ {x y l u} (l<x : l < x) (l<y : l < y) (y<x : y < x)
         {ι₁ : _} (xs : SortedList x u {ι₁}) {ι₂ : _} (ys : SortedList y u {ι₂}) →
         merge (x ∷[ l<x ] xs) (y ∷[ l<y ] ys) ≡ y ∷[ l<y ] merge (x ∷[ y<x ] xs) ys
merge> {x} {y} _ _ _ _ _ with compare x y
merge> _ _ y<x _ _ | tri< _ _ y≮x = ⊥-elim (y≮x y<x)
merge> _ _ y<x _ _ | tri≈ _ _ y≮x = ⊥-elim (y≮x y<x)
merge> _ _ _ _ _ | tri> _ _ _ = refl

Still, this is an unsatisfying amount of boilerplate; I'm guessing (with little first-hand experience) that Coq would fare better.