(* Midland Graduate School 2008: COQ *) Section More. Variables P Q R : Prop. Variable D : Set. Variables PP QQ: D -> Prop. Variable RR : D -> D -> Prop. Lemma allAnd : (forall x:D,PP x) /\ (forall y:D,QQ y) <-> forall z:D,PP z /\ QQ z. split. intro. intro. destruct H. split. apply H. apply H0. intros. split. intro. elim (H x). intros. assumption. firstorder. (* cut (PP x /\ QQ x). intros. elim H0. auto. apply H. *) Qed. Goal (forall x:D,PP x) /\ (forall y:D,QQ y) <-> forall z:D,PP z /\ QQ z. firstorder. Qed. Lemma existsOr : (exists x:D,PP x) \/ (exists y:D,QQ y) <-> exists z:D,PP z \/ QQ z. split. intros. elim H. intros. elim H0. intros. exists x. left. assumption. firstorder. firstorder. Qed. Goal forall a b:D,a = b -> b = a. intros. rewrite H. reflexivity. Require Import Arith. (* This library prove a number of basic results about the arithmentic operators +, *: Lemma plus_0_l : forall n, 0 + n = n. Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p. Lemma plus_comm : forall n m, n + m = m + n. i.e. (nat,+,0) is a commutative semigroup. Do you know another semi-group? Do you know a non-commutative group? And why is it semi? (check wikipedia, commutative=abelian, btw) Lemma mult_1_l : forall n, 1 * n = n. Lemma mult_comm : forall n m, n * m = m * n. Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p. i.e. (nat,*,1) is a commutative semigroup. Lemma mult_0_l : forall n, 0 * n = 0. Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p. (nat,+,0,*,1 ) is a commutative semi-ring. Why only semi? *) Lemma binom : forall a b : nat, (a + b)*(a + b) = a*a + 2*a*b + b*b. intros. simpl. rewrite plus_0_r. repeat rewrite mult_plus_distr_r. repeat rewrite mult_plus_distr_l. pattern (b * a). rewrite mult_comm. repeat rewrite plus_assoc. reflexivity. Qed. Goal forall a b : nat, (a + b)*(a + b) = a*a + 2*a*b + b*b. intros. ring. Qed.