Stream: math-comp users

Topic: How to do a rewrite between an elim and introducting IH


view this post on Zulip walker (Jan 26 2023 at 19:20):

I am having a huge elim that looks like this:

Tactic Notation "SynTypeElim" ident(Γ) ident(t) ident(T):=
elim => {Γ t T} =>
    [ Γ idx T Hdget HWfΓ
    | Γ lvl HWfΓ
    | Γ A B i j HtypeA IHA HtypeB IHB
    | Γ A B t l HtypeA IHA Htypet IHt
    | Γ A B m n Htypem IHm Htypen IHn
    | Γ A B i j HtypeA IHA HtypeB IHB
    | Γ m n A B i j HtypeA IHA HtypeB IHB Htypem IHm Htypen IHn
    | Γ m A B Htypem IHm
    | Γ m A B Htypem IHm
    | Γ T T' t HtypeT IHT HconvTT'
    ].

What I want to do is something like this (except for I want it to work):

Tactic Notation "SynTypeElim" ident(Γ) ident(t) ident(T):=
elim => {Γ t T};
    rewrite ?substE /=; (* note this line*)
    move =>
    [ Γ idx T Hdget HWfΓ
    | Γ lvl HWfΓ
    | Γ A B i j HtypeA IHA HtypeB IHB
    | Γ A B t l HtypeA IHA Htypet IHt
    | Γ A B m n Htypem IHm Htypen IHn
    | Γ A B i j HtypeA IHA HtypeB IHB
    | Γ m n A B i j HtypeA IHA HtypeB IHB Htypem IHm Htypen IHn
    | Γ m A B Htypem IHm
    | Γ m A B Htypem IHm
    | Γ T T' t HtypeT IHT HconvTT'
    ].

I am not sure where to even look for that in the man pages.

view this post on Zulip Paolo Giarrusso (Jan 26 2023 at 22:27):

https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/.E2.9C.94.20Rewrite.20in.20existential has an example

view this post on Zulip Paolo Giarrusso (Jan 26 2023 at 22:28):

See the !inE part. Note it needs mathcomp not just ssreflect, IIRC

view this post on Zulip Paolo Giarrusso (Jan 26 2023 at 22:29):

Hmm, /[!inE] I guess, or /[!substE]. (I'd have to try to be sure)

view this post on Zulip walker (Jan 26 2023 at 22:32):

wow what are the chances, it literally the last question

view this post on Zulip walker (Jan 26 2023 at 22:42):

it is more pain to work with than I thought, now I have to rewrite under binders. because this is generalized induction principle.

view this post on Zulip walker (Jan 26 2023 at 22:42):

rewrites never would have worked

view this post on Zulip Paolo Giarrusso (Jan 26 2023 at 22:48):

Ah, you'd have to introduce the binders first

view this post on Zulip Paolo Giarrusso (Jan 26 2023 at 22:50):

FWIW, ssreflect IMHO isn't quite focused at "inductive proofs on large inductives", but then it's reasonable to supplement it with ltac automation, such as rewrite -> substE in *, hoping that works

view this post on Zulip Paolo Giarrusso (Jan 26 2023 at 22:51):

At least it gained block introductions, elim => [^ prefix]

view this post on Zulip Paolo Giarrusso (Jan 26 2023 at 22:51):

(IIRC)

view this post on Zulip walker (Jan 27 2023 at 08:55):

I am not even sure if rewrite works the problem is induction hypothesis comes in form of forall X Y ..., subst(x, y ...)
So what I would need is setoid rewrite which I won't use here because it will make things very very slow.

view this post on Zulip Paolo Giarrusso (Jan 27 2023 at 09:44):

rewrite can work, and there's a rule.

view this post on Zulip Paolo Giarrusso (Jan 27 2023 at 09:46):

Say you want to rewrite foo to bar. Does foo mention X Y, or not? If not, you're fine. If yes, then you need something extra.

view this post on Zulip Paolo Giarrusso (Jan 27 2023 at 09:46):

(either setoid_rewrite, or ssreflect over/under).

view this post on Zulip Paolo Giarrusso (Jan 27 2023 at 09:47):

To check this rule, make sure to specialize your "foo" and "bar" to your goal first.

view this post on Zulip Paolo Giarrusso (Jan 27 2023 at 09:47):

Here's where I should show an example, but I don't have one now.

view this post on Zulip walker (Jan 27 2023 at 10:09):

no worries, I just went on with manual rewrites after specialization when needed! that should do for now


Last updated: Jul 15 2024 at 20:02 UTC