Replacing a term in Dependent type without error · Coq users

What is the trick to replace a term by another term in a dependent type term without getting into "Abstracting over .... " error.
(I was trying to answer this question and I thought I knew how to solve these kind of problems because I have been couple of times into these kind of situations, but it seems I still don't know it. I can solve this particular case by using f_equal or unfold a but I am curious about a method that works. I believe this one https://github.com/coq/coq/blob/master/theories/Arith/Peano_dec.v#L40 but someone need to document it.)

Definition a := O.

Theorem a_is_zero : a = O.
Proof.
  reflexivity.
Qed.


Lemma ex_intro_gen : forall (P : nat -> Prop) (x y : nat)
  (Ha : x = y) (Hb : P x),
  ex_intro P x Hb = ex_intro P y (eq_rect x P Hb y Ha).
Proof.
  intros *; subst;
  cbn; exact eq_refl.
Qed.


Theorem test : forall (P : nat -> Prop) (Ha : P O),
  ex_intro P O Ha = ex_intro P a Ha.
Proof.
  intros *.
  Fail eapply ex_intro_gen.
  Fail rewrite a_is_zero.
  (*
    Reason is: Illegal application:
    The term "ex_intro" of type
    "∀ (A : Type) (P : A → Prop) (x : A), P x → ∃ y, P y"

    So let's generalize this.
  *)
  generalize (ex_intro _ a a_is_zero).
  intros (y & Hb).
  generalize (@eq_refl nat a).
  generalize a at 1.
  (* if I change to -1, it does not work *)
  intros ? Hc.
  (* I am chasing my tail ?? *)

Gaëtan Gilbert (Mar 24 2023 at 12:07):

ex_intro P a Ha is well typed only because of a convertible to 0 so I don't know if this question makes much sense

Paolo Giarrusso (Mar 24 2023 at 12:38):

Paolo Giarrusso (Mar 24 2023 at 12:43):

I'm not confident one can fix the rewrites in general, but writing automation around the change tactic (augmenting the def_rewrite answer) seems more promising :-)

Patrick Nicodemus (Mar 24 2023 at 20:55):

This question should have some kind of pinned wiki page where experienced users collaborate to describe high level strategy for avoiding this kind of error. I have asked this same question half a dozen times. I am better at dealing with it now than I used to. It seems that this is one of the fundamental motivations for SSReflect, to avoid getting into dependent type headaches as often.

Patrick Nicodemus (Mar 24 2023 at 20:57):

Sometimes you just fundamentally cannot prove the theorem without UIP or something, and that's the reason for the headache.

Paolo Giarrusso (Mar 24 2023 at 22:37):

Even outside ssreflect in Coq we often avoid dependent types (specifically, indexed data) — not always but pretty often

Mukesh Tiwari (Mar 25 2023 at 12:26):

I think it will be nice if we have a Wiki at Coq’s GitHub repo and we can put tutorials and experiences about Coq theorem prover.

Stream: Coq users

Topic: Replacing a term in Dependent type without error

Mukesh Tiwari (Mar 24 2023 at 12:00):