CODEWITHSUNDEEP
coq
Lepticed
Lepticed

Reputation: 381

Rewrite proposition using equivalence in Coq

My current environment is:

1 subgoal
p1, p2 : Entity -> Prop
H : forall s : Entity, p1 s <-> p2 s
t : Entity
FoS1 : (forall w : Entity, p1 w -> PoS w t) /\
       (forall v : Entity, PoS v t -> exists w : Entity, p1 w /\ OoS v w)
______________________________________(1/1)
(forall w : Entity, p2 w -> PoS w t) /\
(forall v : Entity, PoS v t -> exists w : Entity, p2 w /\ OoS v w)

The only difference between the goal and the hypothesis FoS1 is the use p1/p2. I have hypothesis H that says that p1 and p2 are equivalent. Is there a way to rewrite the goal using the equivalence? This way, I could use assumption FoS1 (or auto) to end my proof.

I tried to use rewrite, but it doesn’t work. I need to cut the expression until it is very simple, and then I can use rewrite. But maybe there is a quicker way?

Upvotes: 1

Views: 82

Answers (1)

yiyuan-cao
yiyuan-cao

Reputation: 157

Use setoid_rewrite instead.

From Coq manual:

rewrite won't find occurrences inside forall that refer to variables bound by the forall; use the more advanced setoid_rewrite if you want to find such occurrences.

Assume the context you've given, the script below works:

Proof.
  repeat (setoid_rewrite <- H).
  assumption.
Qed.

Upvotes: 3

Related Questions