[Agda] rewrite on the right?

[Martin Stone Davis]

I've found myself wishing that 'rewrite' or with-abstractions were
invokable from lambda expressions. A (contrived) case in point is as
follows, where a helper function is used to complete 'foo'. NB, I realize
that, in this case, I could have simply used a with-abstraction (as in
'bar'), but there are other cases (not shown here) where one of the
variables being ≟-compared only exists on the rhs, thus requiring a call to
'case_of_'.

Is there a way to 'subst' my way out of the need for foo-helper?

module RewriteOnRight where
  open import Data.Product using (∃ ; _,_)
  open import Relation.Nullary using (Dec ; yes ; no)
  open import Function using (case_of_)
  open import Relation.Nullary.Negation using (contradiction)
  open import Relation.Binary using (IsDecEquivalence)
  open import Relation.Binary.PropositionalEquality using (_≡_ ; subst ;
trans ; refl)

  postulate
    K : Set
    V : K → Set
    M : Set
    _∈_ : K → M → Set
    get : ∀ {k : K} {m : M} → k ∈ m → V k
    isDecEquivalence/K : IsDecEquivalence {A = K} _≡_

  open IsDecEquivalence isDecEquivalence/K using (_≟_ ; sym)

  foo-helper :
    ∀ {x : M}
      {y : M}
      {a : K}
      {b : K}
      {a∈x : a ∈ x}
      {b∈x : b ∈ x}
      {a∈y : a ∈ y}
      (gax≡gay : get a∈x ≡ get a∈y)
      (a≡b : a ≡ b)
      (gbx≡gax : get b∈x ≡ subst V a≡b (get a∈x))
      → get b∈x ≡ get (subst (λ k → k ∈ y) a≡b a∈y)
  foo-helper gax≡gay a≡b gbx≡gax rewrite a≡b = trans gbx≡gax gax≡gay

  foo : ∀ {x : M}
          {y : M}
          (a : K)
          (b : K)
          {a∈x : a ∈ x}
          {b∈x : b ∈ x}
          {a∈y : a ∈ y}
          (gax≡gay : get a∈x ≡ get a∈y)
        → Dec (∃ λ (a≡b : a ≡ b) → (gbx≡gax : get b∈x ≡ subst V a≡b (get
a∈x)) → get b∈x ≡ get (subst (λ k → k ∈ y) a≡b a∈y))
  foo a b gax≡gay = case a ≟ b of λ
    { (yes a≡b) → yes (a≡b , (λ {gbx≡gax → foo-helper gax≡gay a≡b gbx≡gax}))
    ; (no a≢b) → no (λ { (a≡b , _) → contradiction a≡b a≢b })
    }

  bar : ∀ {x : M}
          {y : M}
          (a : K)
          (b : K)
          {a∈x : a ∈ x}
          (b∈x : b ∈ x)
          {a∈y : a ∈ y}
          (gax≡gay : get a∈x ≡ get a∈y)
        → Dec (∃ λ (a≡b : a ≡ b) → (gbx≡gax : get b∈x ≡ subst V a≡b (get
a∈x)) → get b∈x ≡ get (subst (λ k → k ∈ y) a≡b a∈y))
  bar a  b _   _       with a ≟ b
  bar _ ._ b∈x gax≡gay | yes refl = yes (refl , (λ {gbx≡gax → trans gbx≡gax
gax≡gay}))
  bar _  _ _   _       | no a≢b = no (λ { (a≡b , _) → contradiction a≡b a≢b
})

--
Martin Stone Davis

Postal/Residential:
1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160119/edd7b175/attachment.html