[Agda] rewrite on the right?

[Andrea Vezzosi]

Yes, having rewrite on the right would be very nice.

It'd have to generate an helper like you did manually, that's how
rewrite on the left is implemented too, so it might not make sense as
an expression because it mangles the context, maybe it can have the
same status as the macros of reflection.

In your case you cannot really get away with just a subst, however you
can get somewhere if you have proven that get commutes with subst, so
you can fill the open goal here:

(λ { gbx≡gax → trans gbx≡gax (trans (cong (subst V a≡b) gax≡gay) ?) })

Best,
Andrea






On Wed, Jan 20, 2016 at 1:39 AM, Martin Stone Davis
<martin.stone.davis at gmail.com> wrote:
> 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
> Electronic Mail: martin.stone.davis at gmail.com
> Website: martinstonedavis.com
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>