Wie zu zeigen, dass, wenn Quadrate gleich sind, auch die Operanden gleich sind?

Question

Ich hatte ein Problem, den Beweis für diese Lemma Bearbeitung:

Lemma l1 : forall m n : nat, m * m = n * n -> m = n. 

jeder Hinweis sehr hilfreich wäre.

begann ich den Beweis wie folgt aus:

Require Import Arith Omega Nat. 
Lemma l1 : forall m n : nat, m * m = n * n -> m = n. 
Proof. 
intros. 
destruct (Nat.eq_dec m n). 
trivial. 
induction n. 
induction m. 
auto. 
simpl in H;congruence. 

Answer 1

Ein Hinweis: die Quadratwurzel der beiden Seiten Ihrer Hypothese nehmen, dann führt sofort zu dem Schluss. Für die Quadratwurzelfunktion verwenden Sie Nat.sqrt aus dem Arith Modul.

Erste Lösung:

Require Import Coq.Arith.Arith. 

Lemma l1 : forall m n : nat, m * m = n * n -> m = n. 
Proof. 
    intros m n H. apply (f_equal Nat.sqrt) in H. 
    now repeat rewrite Nat.sqrt_square in H. 
Qed. 

Zweite Lösung:

Das Lemma kann auch die nia Taktik bewiesen werden, ein unvollständiges Beweisverfahren für ganzzahlige nichtlineare Arithmetik:

Require Import Psatz. 

Lemma l1 m n : m * m = n * n -> m = n. 
Proof. nia. Qed. 

Dritte Lösung:

Lassen Sie uns ein paar Mal den Standard Nat.square_le_simpl_nonneg Lemma:

forall n m : nat, 0 <= m -> n * n <= m * m -> n <= m 

Hier gehen wir:

Require Import Coq.Arith.Arith. 

Lemma l1 (m n : nat) : 
    m * m = n * n -> m = n. 
Proof with (auto with arith). 
    intros H. 
    pose proof (Nat.eq_le_incl _ _ H) as Hle. 
    pose proof (Nat.eq_le_incl _ _ (eq_sym H)) as Hge. 
    apply Nat.square_le_simpl_nonneg in Hle... 
    apply Nat.square_le_simpl_nonneg in Hge... 
Qed. 

Vierte Lösung:

Hier ist eine klassische Beweis, basierend auf der folgenden Gleichheit

m * m - n * n = (m + n) * (m - n) 

Erstens müssen wir einen Helfer Lemma, die über Gleichheit zu beweisen (Überraschenderweise scheint es, dass die Standard-Bibliothek dieses Lemma fehlt):

Require Import Coq.Arith.Arith. 

(* can be proved using `nia` tactic *) 
Lemma sqr_diff (m n : nat) : 
    m * m - n * n = (m + n) * (m - n). 
Proof with (auto with arith). 
    destruct (Nat.lt_trichotomy m n) as [H | [H | H]]. 
    - pose proof H as H'. (* copy hypothesis *) 
    apply Nat.square_lt_mono_nonneg in H... 
    repeat match goal with 
     h : _ < _ |- _ => apply Nat.lt_le_incl, Nat.sub_0_le in h 
    end. 
    rewrite H, H'... 
    - now rewrite H, !Nat.sub_diag. 
    - rewrite Nat.mul_add_distr_r, !Nat.mul_sub_distr_l. 
    rewrite Nat.add_sub_assoc... 
    replace (n * m) with (m * n) by apply Nat.mul_comm. 
    rewrite Nat.sub_add... 
Qed. 

Und jetzt können wir das Haupt Lemma beweisen :

Lemma l1 (m n : nat) : 
    m * m = n * n -> m = n. 
Proof. 
    intros H. 
    pose proof (Nat.eq_le_incl _ _ H) as Hle; 
    pose proof (Nat.eq_le_incl _ _ (eq_sym H)) as Hge; clear H. 
    rewrite <- Nat.sub_0_le in *. 
    rewrite sqr_diff in *. 
    destruct (mult_is_O _ _ Hle) as [H | H]. 
    now destruct (plus_is_O _ _ H); subst. 
    destruct (mult_is_O _ _ Hge) as [H' | H']. 
    now destruct (plus_is_O _ _ H'); subst. 
    rewrite Nat.sub_0_le in *. 
    apply Nat.le_antisymm; assumption. 
Qed.