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 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 ?? *)
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
The linked question does make sense.
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 :-)
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.
Sometimes you just fundamentally cannot prove the theorem without UIP or something, and that's the reason for the headache.
Even outside ssreflect in Coq we often avoid dependent types (specifically, indexed data) — not always but pretty often
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.
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: Oct 13 2024 at 01:02 UTC