CODEWITHSUNDEEP
coq
Max Heiber
Max Heiber

Reputation: 15492

replacing/rewriting inside existential hypothesis

I have the following proof state:

H: exists x : A, f x = y /\ In x l
----------------------
Goal: exists x0 : A, f x0 = y /\ In x0 (x :: l)

I know that In x l implies In x (x :: l). So I'd like to finish off the proof with a rewrite something like this:

rewrite ___ in H.

leading to the proof state:

H: exists x : A, f x = y /\ In x (x :: l)
----------------------
Goal: exists x0 : A, f x0 = y /\ In x0 (x :: l)

Which can be completed (I think) with:

exact H.

Is such a rewrite possible? Is there a valid technique I can use along these lines?

rewrite fails and replace in the hypothesis doesn't seem to actually change the hypothesis.

Upvotes: 2

Views: 458

Answers (2)

Li-yao Xia
Li-yao Xia

Reputation: 33389

After destructing the hypothesis to get f x = y /\ In x l, we can do setoid rewriting using in_cons : In x l -> In x (x' :: l) (from the List module) but with a bit of extra work.

We somehow have to first beta-expand the lemma to in_cons : impl (In x l) (In x (x' :: l)) (below, using the fold tactic), so it gets recognized as a rewrite rule (impl is registered as a rewriting relation, whereas -> is sugar for primitive syntax, that's not recognized by the rewriting plugin).

As far as I can tell, it's not possible to rewrite while the exists is there, even with the setoid_rewrite variant that works under binders in the right situations.

Require Import List.

Lemma foo {A B} (f : A -> B) (x' : A) (y : B) (l : list A)
  (H: exists x : A, f x = y /\ In x l) :
exists x0 : A, f x0 = y /\ In x0 (x' :: l).
Proof.
  destruct H.
  pose proof (in_cons x' x l) as E.
  fold (Basics.impl (In x l) (In x (x' :: l))) in E.
  rewrite E in H.
  eauto.
Qed.

Upvotes: 2

user5876164
user5876164

Reputation: 503

No, such rewrite is not possible, as far as I know.

But you might want to try destruct H as [x H]. exists x.. This will give you x that satisfies f x = y /\ In x 1.

Upvotes: 3

Related Questions