Coq_practice

lecture2.v

(* https://www.math.nagoya-u.ac.jp/~garrigue/lecture/2017_AW/coq2.pdf *)

Section Coq2.
Variables P Q R : Prop.
Theorem imp_trans : (P -> Q) -> (Q -> R) -> P -> R.
Proof.
intros pq qr p.
apply qr; apply pq; assumption.
Qed.

Theorem not_false : ~False.
Proof.
unfold not.
intros f.
inversion f.
Qed.

Theorem double_neg : P -> ~~P.
Proof.
intros p.
unfold not.
intros pf.
apply pf.
assumption.
Qed.

Theorem contraposition : (P -> Q) -> ~Q -> ~P.
Proof.
unfold not.
intros pq qf p.
apply qf; apply pq. assumption.
Qed.

Theorem and_assoc : P /\ (Q /\ R) -> (P /\ Q) /\ R.
Proof.
intros pqr.
split. split. 
apply pqr. apply pqr. apply pqr.
Qed.

Theorem and_distr : P /\ (Q \/ R) -> (P /\ Q) \/ (P /\ R).
Proof.
intros pqr.
destruct pqr as [p qr].
destruct qr as [q | r].
left.
split. 
  assumption. 
assumption.
right. 
split.
  assumption.
assumption.
Qed.

Theorem absurd : P -> ~P -> Q.
Proof.
intros p pf.
contradiction.
Qed.

End Coq2.

lecture3.v

Section Coq3.
Variable A : Set.
Variable R : A -> A -> Prop.
Variables P Q : A -> Prop.

Theorem exists_postpone :
(exists x, forall y, R x y) -> (forall y, exists x, R x y).
Proof.
intros H.
intros a.
destruct H as [x r].
exists x.
apply r.
Qed.

Theorem or_exists : (exists x, P x) \/ (exists x, Q x) -> exists x, P x \/ Q x.
Proof.
intros H.
destruct H as [xp | xq].
destruct xp as [x p].
exists x.
left. assumption.
destruct xq as [x q].
exists x.
right. assumption.
Qed.

Theorem plus_0 : forall n, n + 0 = n.
Proof.
intros H.
induction H. reflexivity.
simpl. rewrite IHnat. reflexivity.
Qed.

Theorem plus_m_Sn : forall m n, m + (S n) = S (m + n).
Proof.
intros m n.
induction m.
simpl. reflexivity.
simpl. rewrite IHm. reflexivity.
Qed.

Theorem plus_comm : forall m n, m + n = n + m.
Proof.
intros m n.
induction m.
induction n.
reflexivity.
simpl. rewrite plus_0. reflexivity.
induction n.
rewrite plus_0. simpl. reflexivity.
simpl. rewrite IHm. rewrite plus_m_Sn. simpl. reflexivity.
Qed.

Lemma plus_assoc : forall m n p, m + (n + p) = (m + n) + p.
Proof.
intros m n p.
induction m.
simpl. (* 計算する *)
SearchPattern (?X = ?X). (* 反射率を調べる *)
apply eq_refl.
simpl.
rewrite IHm. (* 代入を行う *)
reflexivity. (* apply eq_refl と同じ *)
Qed.

Theorem plus_distr : forall m n p, (m + n) * p = m * p + n * p.
Proof.
intros m n p.
induction m.
simpl. reflexivity.
simpl. rewrite IHm. rewrite plus_assoc. reflexivity.
Qed.

Theorem mult_assoc : forall m n p, m * (n * p) = (m * n) * p.
Proof.
intros m n p.
induction m.
simpl. reflexivity.
simpl. rewrite plus_distr. rewrite IHm. reflexivity.
Qed.
End Coq3.