Stream: Coq users

Topic: Proof of a function

view this post on Zulip 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?

view this post on Zulip Guillaume Melquiond (Jun 13 2022 at 07:27):

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

view this post on Zulip Julin S (Jun 13 2022 at 07:28):

Ah.. Thanks.

view this post on Zulip 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.

view this post on Zulip 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: Oct 13 2024 at 01:02 UTC