rewriting.agda

-- ...
  where
    xyz : t-to (t-from A') ≡ A'
    xyz = t-to∘from A'
    helper : Δ' T.∋ A'
    helper rewrite sym Δ≡Δ' | xyz = {!S∋→T∋ (ρ x)!}

-- Goal: c-to Δ T.∋ A'
-- Have: c-to Δ T.∋ t-to (t-from A')
-- ————————————————————————————————————————————————————————————
-- ...
-- A'≡A : t-from A' ≡ A
-- ...

The Goal and Have pertain to the hole. I am able to prove `xyz`, but rewriting with `xyz` has no effect,
even though the RHS of `xyz` matches a subexpression of (what we) Have: `t-to (t-from A')` .

Interestingly, rewriting with `sym xyz` has an effect: `t-to (t-from A')` gets rewritten to `t-to (t-from (t-to (t-from A')))`.
Similarly, rewriting by `A'≡A` causes `t-to (t-from A')` to get rewritten to `t-to A`.

Why wouldn't rewriting by `xyz` have any effect?

So, the problem in the full example https://github.com/PiotrJander/thesis/blob/06d467b535b2614a8940abfab4e15491eb0040ed/Bisimulation.lagda#L112 was really simple: you are trying to rewrite by t-to A ≡ A' but t-to A appears nowhere in the goal or context, so of course it has no effect. You need to rewrite the other way.

Here is a simpler example:

open import Agda.Builtin.Equality

postulate
  A : Set
  x y : A
  eq : x ≡ y
  P : A → Set
  px : P x

symeq : y ≡ x
symeq rewrite eq = refl

-- error, because rewrite eq has no effect. agda says just:
--   Goal: P y
-- so there are no x's to rewrite!
fail : P y
fail rewrite eq = {!px!}

ok₁ : P y
ok₁ rewrite symeq = px

ok₂ : P y
ok₂ = help₁ px
  where
  -- before rewrite:
  --   Goal: P x → P y
  -- after:
  --   Goal: P y → P y
  help₁ : P x → P y
  help₁ rewrite eq = λ py → py

  -- before rewrite:
  --   Goal: P y
  --   ————————————————————————————————————————————————————————————
  --   px : P x
  -- after:
  --   Goal: P y
  --   ————————————————————————————————————————————————————————————
  --   px : P y
  help₂ : P x → P y
  help₂ px rewrite eq = px