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.

Ah.. Thanks.

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: Jun 24 2024 at 13:02 UTC