exercises_3
From mathcomp Require Import all_ssreflect all_algebra.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Definition sorry {T} : T. Admitted.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Definition sorry {T} : T. Admitted.
Exercise: prove
Lemma exbig1 : \sum_(1 ≤ i < 4) i.*2 = 12.
Proof. Admitted.
Lemma exbig2 n : \sum_(i < n) (2 × i + 1) = n ^ 2.
Proof. Admitted.
Proof. Admitted.
Lemma exbig2 n : \sum_(i < n) (2 × i + 1) = n ^ 2.
Proof. Admitted.
Prove the following statement using only big operator theorems. big_cat_nat, big_nat_cond, big_mkcondl, big1
Lemma sum_prefix_0 (f : nat → nat) n m : n ≤ m →
(∀ k, k < n → f k = 0) →
\sum_(0 ≤ i < m) f i = \sum_(n ≤ i < m) f i.
Proof. Admitted.
Open Scope ring_scope.
Import GRing.Theory.
Variable (R : comRingType).
Variables (m n : nat).
Implicit Types (A B C : 'M[R]_(m,m)).
(∀ k, k < n → f k = 0) →
\sum_(0 ≤ i < m) f i = \sum_(n ≤ i < m) f i.
Proof. Admitted.
Open Scope ring_scope.
Import GRing.Theory.
Variable (R : comRingType).
Variables (m n : nat).
Implicit Types (A B C : 'M[R]_(m,m)).
Exercise: prove
Lemma exa1 (x : R) n : x *+ n.+1 = x *+ n + x.
Proof. Admitted.
Proof. Admitted.
Exercise: prove
Lemma exm1 (c : R) A B : c *: (A + B) = c *: B + c *: A.
Proof. Admitted.
Proof. Admitted.
Exercise: prove
Lemma exm2 A B C : A ×m B ×m C = A ×m (B ×m C).
Proof. Admitted.
Proof. Admitted.
Prove that:
- (a - bX) has a size of 2
Lemma P1_size (a b : R) : size (a%:P - b*:'X) = 2%nat.
Proof. Admitted.
Proof. Admitted.
Prove that:
- the lead_coef of (a - bX) is -b.
Lemma P1_lead_coef (a b : R) : lead_coef (a%:P - b*:'X) = -b.
Proof. Admitted.
Proof. Admitted.
Prove that:
- the size of (a-X)^n is n.+1
Lemma P_size (a b : R) : size ((a%:P - b*:'X)^+n) = n.+1.
Proof. Admitted.
Proof. Admitted.