<div dir="ltr">I&#39;ve found myself wishing that &#39;rewrite&#39; or with-abstractions were invokable from lambda expressions. A (contrived) case in point is as follows, where a helper function is used to complete &#39;foo&#39;. NB, I realize that, in this case, I could have simply used a with-abstraction (as in &#39;bar&#39;), 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 &#39;case_of_&#39;. <br><br>Is there a way to &#39;subst&#39; my way out of the need for foo-helper?<br><br>module RewriteOnRight where<br>  open import Data.Product using (∃ ; _,_)<br>  open import Relation.Nullary using (Dec ; yes ; no)<br>  open import Function using (case_of_)<br>  open import Relation.Nullary.Negation using (contradiction)<br>  open import Relation.Binary using (IsDecEquivalence)<br>  open import Relation.Binary.PropositionalEquality using (_≡_ ; subst ; trans ; refl)<br><br>  postulate<br>    K : Set<br>    V : K → Set<br>    M : Set<br>    _∈_ : K → M → Set<br>    get : ∀ {k : K} {m : M} → k ∈ m → V k<br>    isDecEquivalence/K : IsDecEquivalence {A = K} _≡_<br><br>  open IsDecEquivalence isDecEquivalence/K using (_≟_ ; sym)<br><br>  foo-helper :<br>    ∀ {x : M}<br>      {y : M}<br>      {a : K}<br>      {b : K}<br>      {a∈x : a ∈ x}<br>      {b∈x : b ∈ x}<br>      {a∈y : a ∈ y}<br>      (gax≡gay : get a∈x ≡ get a∈y)<br>      (a≡b : a ≡ b)<br>      (gbx≡gax : get b∈x ≡ subst V a≡b (get a∈x))<br>      → get b∈x ≡ get (subst (λ k → k ∈ y) a≡b a∈y)<br>  foo-helper gax≡gay a≡b gbx≡gax rewrite a≡b = trans gbx≡gax gax≡gay<br><br>  foo : ∀ {x : M}<br>          {y : M}<br>          (a : K)<br>          (b : K)<br>          {a∈x : a ∈ x}<br>          {b∈x : b ∈ x}<br>          {a∈y : a ∈ y}<br>          (gax≡gay : get a∈x ≡ get a∈y)<br>        → 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))<br>  foo a b gax≡gay = case a ≟ b of λ<br>    { (yes a≡b) → yes (a≡b , (λ {gbx≡gax → foo-helper gax≡gay a≡b gbx≡gax}))<br>    ; (no a≢b) → no (λ { (a≡b , _) → contradiction a≡b a≢b })<br>    }<br><br>  bar : ∀ {x : M}<br>          {y : M}<br>          (a : K)<br>          (b : K)<br>          {a∈x : a ∈ x}<br>          (b∈x : b ∈ x)<br>          {a∈y : a ∈ y}<br>          (gax≡gay : get a∈x ≡ get a∈y)<br>        → 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))<br>  bar a  b _   _       with a ≟ b<br>  bar _ ._ b∈x gax≡gay | yes refl = yes (refl , (λ {gbx≡gax → trans gbx≡gax gax≡gay}))<br>  bar _  _ _   _       | no a≢b = no (λ { (a≡b , _) → contradiction a≡b a≢b })<br><br clear="all"><div><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
</div></div>