How does the "intro ->" in Coq work on context?

Question

I am interested in how does dependent-typed theorem provers do substitution on the context. I find a thing called "intro ->" in Coq, as described in:

https://coq.inria.fr/refman/proof-engine/tactics.html#intropattern-rarrow-ex

In the example, it says the goal:

x, y, z : nat

H : x = y

y = z -> x = z

will become

x, z : nat

H : x = z

---

x = z

after an application of "intros ->".

I am not sure how is the step of substituting H:x = y into H:x = z be done, what is the rule of the logic of Coq is this step according to? It seems like a step of rewriting, and according to my current knowledge most of these rewriting are according to equalities, so the replacement from H:x = y into H:x = z should come from an equality like (H:x = y) = (H:x= z) ($\diamond$), but such an equality is ill-formed because, in principle, we require the LHS and RHS of an equality to have the same type, so the well-formedness of such equality ($\diamond$) depends on the assumption that y = z.

Could someone please help explaining how does "intro ->" work here? Do we need to get "equalities" like ($\diamond$) involved?

Answer 1

In Coq, rewriting on the context is a derived notion. The tactic intros -> in this case is roughly equivalent to the following tactics:

intros H'. rewrite H' in H. clear y H'.

The tactic rewrite H' in H., in turn, is roughly equivalent to

revert H. rewrite H'. intros H.

In words, to rewrite on the context, Coq first transfers all the relevant hypotheses to the goal, rewrites the goal and then brings the hypotheses back to the context.

Rewriting the goal uses the following elimination principle for the equality type:

forall [A : Type] [a : A] (P : A -> Prop), P a -> forall b : A, b = a -> P b

For rewriting H' above, we would have:

A := T
a := z
P := fun c => x = c -> x = z
b := y

so,

P b == x = y -> x = z
P a == x = z -> x = z

Indeed, ignoring the move steps to and from the context, Coq went from P b to P a when you performed the rewrite.