I was trying to prove that for
f(x) = x², if
f(x) = x, then x is 0.
So I did:
Definition f3 (x:nat) : nat := x*x.
and tried the proof like
Theorem f3_fix_is_O : forall x:nat, ((f3 x) = x) -> (x = 0). Proof. intros. induction x. - reflexivity. (* Not sure what should've been done from here, but just tried rewrite *) - rewrite <- H.
How can this be finished?
This is wrong. The square function has two fixed points, 0 and 1.
Could this be okay?
Theorem f3_fix_is_O : forall x:nat, ((f3 x) = x) -> (x = 0) \/ (x = 1). Proof. intros. induction x. - now left. - right.
Here's a proof.
Lemma sqr_fxp n : n * n = n -> n = 0 \/ n = 1. destruct n; [left;trivial|]. destruct n ; [right; trivial | ]. simpl. injection 1; intro; exfalso. lia. Qed.
Last updated: Oct 05 2023 at 02:01 UTC