CODEWITHSUNDEEP
equalitycoq
thor
thor

Reputation: 22460

How to prove image equality for functions: x = y -> f x = f y in Coq?

Intuitively, I know that if x = y then f x = f y, for any function f. But I don't know how to prove this in Coq. What I have so far is:

Theorem eq_img: forall {X:Type} (f: X->X) (x y :X), x = y -> f x = f y.
Proof.  intros X f x y eq1.

and the state is:

1 subgoals
X : Type
f : X -> X
x : X
y : X
eq1 : x = y
______________________________________(1/1)
f x = f y

Any pointers on how should I proceed?

Thanks.

Upvotes: 0

Views: 867

Answers (1)

thor
thor

Reputation: 22460

I figured it out. Just needed to use rewrite to eliminate x or y, then it's reflexivity.

Theorem eq_img: forall {X:Type} (f: X->X) (x y :X), x = y -> f x = f y.
Proof.  intros X f x y eq1. rewrite <- eq1. reflexivity. Qed.

Upvotes: 1

Related Questions