## Stream: Coq users

### Topic: Proof of a function

#### Julin S (Jun 13 2022 at 07:26):

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?

#### Guillaume Melquiond (Jun 13 2022 at 07:27):

This is wrong. The square function has two fixed points, 0 and 1.

Ah.. Thanks.

#### Julin S (Jun 13 2022 at 07:29):

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.
``````

#### Pierre Castéran (Jun 13 2022 at 07:50):

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