Skip to content

Instantly share code, notes, and snippets.

@kencoba
Created March 19, 2024 08:46
Show Gist options
  • Save kencoba/dbb17ed72dd6bef968379efe5dd84c4a to your computer and use it in GitHub Desktop.
Save kencoba/dbb17ed72dd6bef968379efe5dd84c4a to your computer and use it in GitHub Desktop.
Sample proofs from books.
(* 新妻弘,「演習 群・環・体 入門」,共立出版株式会社 より *)
Require Import ZArith.
Open Scope Z_scope.
Theorem thm_1_1 : forall a b c : Z , a + b = a + c -> b = c.
Proof.
intros a b c H.
apply Z.add_cancel_l with (p := a).
assumption.
Qed.
Theorem thm_1_2_1 : forall a : Z , 0 * a = 0.
Proof.
intros a.
auto.
Qed.
Theorem thm1_2_2 : forall a : Z , a * 0 = 0.
Proof.
intros.
rewrite Z.mul_0_r.
reflexivity.
Qed.
Theorem thm1_2_3 : forall a : Z , a * 0 = 0 * a.
Proof.
simpl.
intro a.
apply thm1_2_2.
Qed.
Theorem thm1_3_1 : forall a : Z , - ( - a ) = a.
Proof.
intros.
rewrite <- Z.opp_involutive.
reflexivity.
Qed.
(* 山田俊行,「はじめての数理論理学」,森北出版 より *)
Theorem thm_p_61 :
forall P Q R S : Prop, (P /\ Q) /\ (P -> R /\ S) -> S.
Proof.
intros.
destruct H.
destruct H.
destruct H0 as [H2].
exact H.
exact H0.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment