↑Programmieren in Gallina

Elementare Algebra

Inhaltsverzeichnis

1. Subtraktion
2. Gleichungen
3. Ungleichungen
4. Äquivalenzumformungen

Subtraktion

Die Subtraktion lässt sich mit unfold auf die Addition des negierten Subtrahenden zurückführen.

Require Import ZArith.
Local Open Scope Z_scope.

Theorem plus_minus_assoc (a b c: Z):
  (a + b) - c = a + (b - c).
Proof.
  unfold Zminus.
  rewrite Zplus_assoc.
  reflexivity.
Qed.

Require Import Reals.
Local Open Scope R_scope.

Theorem plus_minus_assoc (a b c: R):
  (a + b) - c = a + (b - c).
Proof.
  unfold Rminus.
  rewrite Rplus_assoc.
  reflexivity.
Qed.

Gleichungen

Require Import Reals.
Local Open Scope R_scope.

Goal forall (x: R),
  2*x + 1 = 0 -> x = -1/2.
Proof.
  intro x. intro h.
  apply (f_equal (fun t => t - 1)) in h.
  unfold Rminus in h.
  rewrite Rplus_assoc in h.
  rewrite Rplus_opp_r in h.
  rewrite Rplus_0_r in h.
  rewrite Rplus_0_l in h.
  apply (f_equal (fun t => t/2)) in h.
  unfold Rdiv in h at 1.
  rewrite Rmult_comm in h.
  rewrite <- Rmult_assoc in h.
  rewrite (Rmult_comm (/ 2) 2) in h.
  rewrite Rinv_r in h by trivial.
  rewrite Rmult_1_l in h.
  exact h.
Qed.

Mit automatisierter Vereinfachung:

Goal forall (x: R),
  2*x + 1 = 0 <-> x = -1/2.
Proof.
  intro x.
  split.
  * intro h.
    apply (f_equal (fun t => t - 1)) in h.
    field_simplify in h.
    apply (f_equal (fun t => t/2)) in h.
    field_simplify in h.
    exact h.
  * intro h. rewrite h. field.
Qed.

Ungleichungen

Require Import Reals.
Local Open Scope R_scope.

Theorem pos_half: 0 < 1/2.
Proof.
  unfold Rdiv.
  rewrite Rmult_1_l.
  apply (Rinv_0_lt_compat 2).
  replace 2 with (1 + 1) by trivial.
  apply Rplus_lt_0_compat.
  exact Rlt_0_1.
  exact Rlt_0_1.
Qed.

Goal forall x: R, 2*x - 1 < 0 -> x < 1/2.
Proof.
  intro x. intro h.
  About Rplus_lt_compat_r.
  apply (Rplus_lt_compat_r 1) in h.
  unfold Rminus in h.
  rewrite Rplus_assoc in h.
  rewrite Rplus_opp_l in h.
  rewrite Rplus_0_r in h.
  rewrite Rplus_0_l in h.
  apply (Rmult_lt_compat_r (1/2) _ _ pos_half) in h.
  rewrite Rmult_1_l in h.
  rewrite Rmult_comm in h.
  rewrite <- Rmult_assoc in h.
  unfold Rdiv in h at 1.
  rewrite Rmult_1_l in h.
  rewrite Rinv_l in h by trivial.
  rewrite Rmult_1_l in h.
  exact h.
Qed.

Äquivalenzumformungen

Bislang wurde eine Äquivalenz aufgetrennt in Implikation und umgekehrte Implikation, deren Beweise jeweils für sich erbracht wurden. Es ist aber auch die äquivalente Umformung einer Gleichung innerhalb einer Aussage durchführbar. Wir erinnern uns hierfür daran, dass setoid es ermöglicht, die Taktik rewrite ebenfalls für die Umschreibung von Aussagen zu nutzen. Somit steht jede vorhandene Äquivalenz zur Umformung zur Verfügung.

Require Import Reals.
Local Open Scope R_scope.

Theorem equi_sub (x y z: R):
  x = y <-> x - z = y - z.
Proof. Admitted.

Theorem equi_div2 (x y: R):
  x = y <-> x / 2 = y / 2.
Proof. Admitted.

Goal forall (x: R),
  2*x + 1 = 0 <-> x = -1/2.
Proof.
  intro x.
  rewrite (equi_sub _ 0 1).
  unfold Rminus at 1.
  rewrite Rplus_assoc.
  rewrite Rplus_opp_r.
  rewrite Rplus_0_r.
  unfold Rminus.
  rewrite Rplus_0_l.
  rewrite equi_div2.
  unfold Rdiv at 1.
  rewrite Rmult_comm.
  rewrite <- Rmult_assoc.
  rewrite (Rmult_comm (/ 2) 2).
  rewrite Rinv_r by trivial.
  rewrite Rmult_1_l.
  apply iff_refl.
Qed.