Stream: Coq users

Topic: Replacing a term in Dependent type without error


view this post on Zulip 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 ?? *)

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Mar 24 2023 at 12:38):

The linked question does make sense.

view this post on Zulip 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 :-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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