## Stream: Coq users

### Topic: Replacing a term in Dependent type without error

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

Hi everyone,

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 kinds of problems because I have been couple of times into these 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 needs 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):

The linked question does make sense.

#### 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.

#### Ana de Almeida Borges (Mar 25 2023 at 16:00):

There is already such a wiki: https://github.com/coq/coq/wiki/
I think anyone is welcome to add stuff to it (cf. instructions at https://github.com/coq/coq/wiki/HelpOnGithubWiki)

Last updated: Jun 16 2024 at 02:41 UTC