rewrite works for = but not for <-> (iff) in Coq

Link:

https://stackoverflow.com/q/34239906

Question

Adapting @Matt's example,

Require Export Coq.Setoids.Setoid.

Inductive R1 : Prop -> Prop -> Prop :=
| T1_refl : forall P, R1 P P.

Inductive R2 : Prop -> Prop -> Prop :=
| T2_refl : forall P, R2 P P.


R1 = R2

Admitted.


forall x y : Prop, R1 x y <-> R2 x y

Admitted.


forall y : Prop, R2 y y -> exists x : Prop, R1 x x


forall y : Prop, R2 y y -> exists x : Prop, R1 x x

  
y: Prop
H: R2 y y
exists x : Prop, R1 x x
 
y: Prop
H: R1 y y
exists x : Prop, R1 x x
 
y: Prop
H: R1 y y
exists x : Prop, R2 x x

Abort.


forall y : Prop, R2 y y -> exists x : Prop, R1 x x


forall y : Prop, R2 y y -> exists x : Prop, R1 x x

  
y: Prop
H: R2 y y
exists x : Prop, R1 x x
 
y: Prop
H: R1 y y
exists x : Prop, R1 x x
 
Found no subterm matching "R1 ?P ?P0" in the current goal.
y: Prop
H: R1 y y
exists x : Prop, R1 x x

What confuses me is why the last step has to fail.

1 subgoal

  y : Prop
  H : R1 y y
  ============================
  exists x : Prop, R1 x x

Is this failure related to functional extensionality?

The error message is particularly confusing:

The command has indeed failed with message:
Found no subterm matching "R1 ?P ?P0" in the current goal.

There is exactly one subterm matching R1 _ _, namely R1 x x.

Also, per @larsr, the rewrite works if eexists is used

forall y : Prop, R2 y y -> exists x : Prop, R1 x x


forall y : Prop, R2 y y -> exists x : Prop, R1 x x

  
y: Prop
H: R2 y y
exists x : Prop, R1 x x
 
y: Prop
H: R2 y y
R1 ?x ?x
 
y: Prop
H: R2 y y
R2 ?x ?x
 apply H.
Qed.

What did eexists add here?

Answer

The rewrite cannot go under the existential quantifier. You'll need to instantiate t' first before you can do the rewrite. Note that econstructor may be a useful tactic in this case, which can replace the existential quantifier with a unification variable.

EDIT in response to OP's comment

This will still not work for equality. As an example, try:

Inductive R1 : Prop -> Prop -> Prop :=
| T1_refl : forall P, R1 P P.

Inductive R2 : Prop -> Prop -> Prop :=
| T2_refl : forall P, R2 P P.


forall x y : Prop, R1 x y = R2 x y

Admitted.


forall y : Prop, R2 y y -> exists x : Prop, R1 x x


forall y : Prop, R2 y y -> exists x : Prop, R1 x x

  
y: Prop
H: R2 y y
exists x : Prop, R1 x x
 
Found no subterm matching "R1 ?M160 ?M161" in the current goal.
y: Prop
H: R2 y y
exists x : Prop, R1 x x

The issue is not actually about equality vs. iff, the issue relates to rewriting under a binding (in this case a lambda). The implementation of exists x : A, P is really just syntax for ex A (fun x => P x), so the rewrite is failing not because of the iff, but because the rewrite tactic does not want to go under the binding for x in (fun x => P x). It seems as though there might be a way to do this with setoid_rewrite, however, I don't have any experience with this.

A: Require Import Coq.Setoids.Setoid. and then setoid_rewrite Requiv. should work under the existential quantifier.