-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathother_stuff.v
187 lines (171 loc) · 8.1 KB
/
other_stuff.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
From mathcomp Require Import all_ssreflect all_algebra all_field all_real_closed.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope ring_scope.
Import GRing.Theory.
(* swiped from an earlier version of SSReflect *)
Definition seq2matrix (T: ringType) m n (l: seq (seq T)) :=
\matrix_(i<m,j<n) nth 1 (nth [::] l i) j.
Notation "''M{' l } " := (seq2matrix _ _ l).
Lemma sum_add_dist: forall (T: ringType) m (F: 'I_m -> T) (G: 'I_m -> T),
(\sum_(i < m) F i) + (\sum_(i < m) G i) =
\sum_(i < m) (F i + G i).
Proof.
intros. induction m;
[ rewrite !big_ord0; apply add0r
| rewrite !big_ord_recl
].
rewrite (addrC (F ord0)). rewrite -(addrA _ (F ord0)). rewrite (addrA (F ord0)).
rewrite (addrC (F ord0 + G ord0)). rewrite (addrA _ _ (F ord0 + G ord0)). rewrite addrC.
rewrite IHm //.
Qed.
Lemma sum_mul_dist: forall (T: ringType) m n (F: 'I_m -> T) (G: 'I_n -> T),
(\sum_(i < m) F i) * (\sum_(j < n) G j) =
\sum_(i < m) F i * \sum_(j < n) G j.
Proof.
intros. induction m;
[ rewrite !big_ord0; apply mul0r
| rewrite !big_ord_recl; rewrite mulrDl; rewrite IHm //
].
Qed.
Lemma sum_cast: forall (R: ringType) m n (Heq: m = n) (P1: pred 'I_m) (P2: pred 'I_n)
(F1: 'I_m -> R) (F2: 'I_n -> R),
(forall x, P1 x = P2 (cast_ord Heq x)) ->
(forall x, F1 x = F2 (cast_ord Heq x)) ->
\sum_(i < m | P1 i) F1 i =
\sum_(i < n | P2 i) F2 i.
Proof.
intros.
replace (\sum_(i < m | P1 i) F1 i) with (\sum_(i < m) (if P1 i then F1 i else 0)).
replace (\sum_(i < n | P2 i) F2 i) with (\sum_(i < n) (if P2 i then F2 i else 0)).
generalize P1 P2 F1 F2 Heq H H0. clear P1 P2 F1 F2 H H0 Heq. generalize m n. clear m n.
induction m; induction n.
intros; rewrite !big_ord0 //.
intros; inversion Heq.
intros; inversion Heq.
intros. (*clear H n0 m.*)
rewrite !big_ord_recl. inversion Heq.
rewrite (IHm n _ (fun x => P2 (fintype.lift ord0 x)) _ (fun x => F2 (fintype.lift ord0 x))).
rewrite H. rewrite H0. replace (F2 (cast_ord Heq ord0)) with (F2 ord0).
replace (P2 (cast_ord Heq ord0)) with (P2 ord0). reflexivity.
compute. rewrite (eq_irrelevance (ltn0Sn n) (cast_ord_proof (Ordinal (ltn0Sn m)) Heq)). reflexivity.
compute. rewrite (eq_irrelevance (ltn0Sn n) (cast_ord_proof (Ordinal (ltn0Sn m)) Heq)). reflexivity.
intros; rewrite H. compute. rewrite (eq_irrelevance (@cast_ord_proof (S m) (S n) (@Ordinal (S m) _ (@lift_subproof (S m) 0 x)) Heq)
(@lift_subproof (S n) 0 (@Ordinal n _ (@cast_ord_proof m n x H2)))
). reflexivity.
intros; rewrite H0. compute. rewrite (eq_irrelevance (@cast_ord_proof (S m) (S n) (@Ordinal (S m) _ (@lift_subproof (S m) 0 x)) Heq)
(@lift_subproof (S n) 0 (@Ordinal n _ (@cast_ord_proof m n x H2)))
). reflexivity.
rewrite -big_mkcond. reflexivity. rewrite -big_mkcond. reflexivity.
Qed.
Lemma sum_if_not: forall (R: ringType) m P (F: 'I_m -> R),
\sum_(i < m | ~~P i) F i + \sum_(i < m | P i) F i = \sum_(i < m) F i.
Proof.
intros. rewrite (big_mkcond (fun i => ~~P i)). rewrite (big_mkcond (fun i => P i)).
rewrite sum_add_dist. induction m;
[ rewrite !big_ord0 //
| rewrite !big_ord_recl; destruct (P ord0); [ rewrite add0r | rewrite addr0 ]; rewrite IHm //
].
Qed.
Lemma behead_tupleE: forall T k h (l: k.-tuple T), behead_tuple ([tuple of h :: l]) = [tuple of l].
Proof.
intros. apply eq_from_tnth. intro.
rewrite !(tnth_nth h). simpl.
reflexivity.
Qed.
Lemma ordinal_eq: forall m i j Hi Hj, i = j -> (@Ordinal m i Hi) = (@Ordinal m j Hj).
Proof.
intros. generalize Hi. clear Hi. rewrite H. intros Hi. rewrite (eq_irrelevance Hi Hj) //.
Qed.
Lemma leq_lt: forall a b: nat, (a >= b)%N -> ~(b > a)%N.
Proof.
intros. apply/elimF. Focus 2. rewrite leqNgt in H. apply negbTE. apply H.
destruct (a < b)%N; [ apply ReflectT | apply ReflectF ]; auto.
Qed.
Lemma blerp: forall a b c d x,
(a * x + b = c * x + d -> b < x -> d < x -> a = c /\ b = d)%N.
Proof.
intros. generalize a c H. clear a c H. induction a; induction c.
split. reflexivity. rewrite !mul0n in H. rewrite !add0n in H. exact H.
rewrite !mul0n. rewrite !add0n. intros.
absurd (b < x)%N. rewrite H. apply leq_lt. apply leq_trans with (c.+1 * x)%N.
apply leq_pmull. auto. apply leq_addr.
apply H0.
rewrite !mul0n. rewrite !add0n. intros.
absurd (d < x)%N. rewrite -H. apply leq_lt. apply leq_trans with (a.+1 * x)%N.
apply leq_pmull. auto. apply leq_addr.
apply H1.
intros. assert (a * x + b = c * x + d)%N.
rewrite !mulSnr in H. rewrite addnAC in H. rewrite (addnAC (c*x)%N x d) in H.
apply/eqP. rewrite -(eqn_add2r x). apply/eqP. apply H. split.
f_equal. apply (proj1 (IHa c H2)).
apply (proj2 (IHa c H2)).
Qed.
Lemma implP: forall A B,
is_true (A ==> B) -> is_true A -> is_true B.
Proof.
intros. destruct A. apply H.
inversion H0.
Qed.
Lemma andP: forall A B,
is_true (A && B) <-> is_true A /\ is_true B.
Proof.
split.
intros. destruct A. destruct B.
auto.
inversion H.
inversion H.
intros. destruct A. destruct B.
auto.
destruct H. inversion H0.
destruct H. inversion H.
Qed.
Lemma orP: forall A B,
is_true (A || B) <-> is_true A \/ is_true B.
Proof.
split. intros. destruct A. left; auto.
destruct B. right; auto.
inversion H.
intros. destruct H as [Ha | Hb].
destruct A. auto.
inversion Ha.
destruct B. apply orbT.
inversion Hb.
Qed.
Lemma modn: forall x y z,
(0 < y)%N -> x %% (z * y) = x %[mod y]%N.
Proof.
intros. rewrite !modn_def.
case:edivnP. intros q r. case:edivnP. intros q' r'. case:edivnP. intros q'' r''. intros. simpl.
simpl in e1. rewrite e1 in e0. clear e1. rewrite e in e0. clear e. rewrite mulnA in e0. rewrite addnA in e0.
rewrite -mulnDl in e0. symmetry. apply (blerp e0).
apply (implP i). apply H.
apply (implP i1). apply H.
Qed.
Lemma mxtensA: forall (R: ringType) ma na mb nb mc nc (Hma: (0 < ma)%N) (Hna: (0 < na)%N) (Hmb: (0 < mb)%N)
(Hnb: (0 < nb)%N) (Hmc: (0 < mc)%N) (Hnc: (0 < nc)%N) (a: 'M[R]_(ma, na)) (b: 'M[R]_(mb, nb)) (c: 'M[R]_(mc, nc)),
castmx (mulnA ma mb mc, mulnA na nb nc) (a *t (b *t c)) = a *t b *t c.
Proof.
intros; apply/matrixP; intros i j. rewrite castmxE. unfold cast_ord. unfold tensmx. rewrite !mxE. simpl. rewrite mulrA. f_equal. f_equal.
rewrite (ordinal_eq (mxtens_index_proof1 (Ordinal (cast_ord_proof i (esym (mulnA ma mb mc))))) (mxtens_index_proof1 (Ordinal (mxtens_index_proof1 i)))).
rewrite (ordinal_eq (mxtens_index_proof1 (Ordinal (cast_ord_proof j (esym (mulnA na nb nc))))) (mxtens_index_proof1 (Ordinal (mxtens_index_proof1 j)))).
reflexivity. rewrite -divnMA. rewrite (mulnC nc nb). auto.
rewrite -divnMA. rewrite (mulnC mc mb). auto.
rewrite (ordinal_eq (mxtens_index_proof1 (Ordinal (mxtens_index_proof2 (Ordinal (cast_ord_proof i (esym (mulnA ma mb mc))))))) (mxtens_index_proof2 (Ordinal (mxtens_index_proof1 i)))).
rewrite (ordinal_eq (mxtens_index_proof1 (Ordinal (mxtens_index_proof2 (Ordinal (cast_ord_proof j (esym (mulnA na nb nc))))))) (mxtens_index_proof2 (Ordinal (mxtens_index_proof1 j)))).
reflexivity.
simpl. rewrite !modn_def. case: edivnP => q r. case: edivnP => q' r'. simpl. intros. rewrite e0 in e. rewrite mulnA in e.
rewrite divnMDl in e.
apply (blerp e). rewrite ltn_divLR. apply (implP i1). rewrite muln_gt0. apply <- andP. split. apply Hnb. apply Hnc. apply Hnc.
apply (implP i0). apply Hnb. apply Hnc.
simpl. rewrite !modn_def. case: edivnP => q r. case: edivnP => q' r'. simpl. intros. rewrite e0 in e. rewrite mulnA in e.
rewrite divnMDl in e.
apply (blerp e). rewrite ltn_divLR. apply (implP i1). rewrite muln_gt0. apply <- andP. split. apply Hmb. apply Hmc. apply Hmc.
apply (implP i0). apply Hmb. apply Hmc.
rewrite (ordinal_eq (mxtens_index_proof2 (Ordinal (mxtens_index_proof2 (Ordinal (cast_ord_proof i (esym (mulnA ma mb mc))))))) (mxtens_index_proof2 i)).
rewrite (ordinal_eq (mxtens_index_proof2 (Ordinal (mxtens_index_proof2 (Ordinal (cast_ord_proof j (esym (mulnA na nb nc))))))) (mxtens_index_proof2 j)).
reflexivity.
simpl. apply modn. apply Hnc.
simpl. apply modn. apply Hmc.
Qed.