-
Notifications
You must be signed in to change notification settings - Fork 0
/
mathcomp_extra.v
119 lines (96 loc) · 3.54 KB
/
mathcomp_extra.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
From mathcomp Require Import all_ssreflect all_algebra.
From HB Require Import structures.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
(* Utility lemmas *)
Lemma addnLR m n p : m + n = p -> n = p - m.
Proof. move/(f_equal (subn^~ m)); by rewrite addKn. Qed.
Lemma ltn_ordK q (i : 'I_q) : Ordinal (ltn_ord i) = i.
Proof. by apply val_inj. Qed.
Lemma disjointP (T : finType) (a1 a2 : pred T) :
reflect (forall i, i \in a1 -> ~ i \in a2) [disjoint a1 & a2].
Proof.
case/boolP: [disjoint a1 & a2] => /pred0P Hdisj; constructor.
move=> i H1 H2. move: (Hdisj i). by rewrite /= H1 H2.
move=> H; elim: Hdisj => i /=.
case H1: (i \in a1) => //.
by apply/negbTE/negP/H.
Qed.
Lemma enum_filterP (T : finType) (P : pred T) :
[seq x <- enum T | P x] = enum P.
Proof. by rewrite {2}/enum_mem -enumT. Qed.
Section tnth.
Variables (T : Type) (m n : nat) (vl : m.-tuple T) (vr : n.-tuple T).
Lemma cast_tuple_proof (H : m = n) (v : m.-tuple T) : size v == n.
Proof. by rewrite size_tuple H. Qed.
Definition cast_tuple H v : n.-tuple T := Tuple (cast_tuple_proof H v).
Lemma eq_ord_tuple (t1 t2 : n.-tuple 'I_m) :
(t1 == t2) = (map val t1 == map val t2).
Proof.
case: eqP => [-> | H]; apply/esym/eqP => // /inj_map H'.
by elim H; apply/val_inj/H'/val_inj.
Qed.
Lemma nth_tnth i x0 (H : i < n) : nth x0 vr i = tnth vr (Ordinal H).
Proof. by rewrite (tnth_nth x0). Qed.
Lemma tnth_lshift i : tnth [tuple of vl ++ vr] (lshift n i) = tnth vl i.
Proof.
by rewrite (tnth_nth (tnth vl i)) /= nth_cat size_tuple ltn_ord -tnth_nth.
Qed.
Lemma tnth_rshift i : tnth [tuple of vl ++ vr] (rshift m i) = tnth vr i.
Proof.
rewrite (tnth_nth (tnth vr i)) /= nth_cat size_tuple ltnNge leq_addr /=.
by rewrite addKn -tnth_nth.
Qed.
Lemma eq_from_nth' (s1 s2 : seq T) :
size s1 = size s2 -> (forall a i, i < size s1 -> nth a s1 i = nth a s2 i) ->
s1 = s2.
Proof.
case: s1 => [|a s1 Hsz Heq].
by move/esym/eqP/nilP ->.
exact (eq_from_nth Hsz (Heq a)).
Qed.
End tnth.
Lemma cast_tupleE n T (v : n.-tuple T) (H : n = n) : cast_tuple H v = v.
Proof. exact/val_inj. Qed.
Lemma cast_tuple_bij T m n H : bijective (@cast_tuple T m n H).
Proof. by exists (cast_tuple (esym H)); move => x; apply val_inj. Qed.
Section tnth_eq.
Variables (A : eqType) (n : nat).
Lemma tnth_inj (t : n.-tuple A) : reflect (injective (tnth t)) (uniq t).
Proof.
apply: (iffP idP).
- move=> /uniqP Hu i j.
rewrite (tnth_nth (tnth t i)) (tnth_nth (tnth t i) t j).
move/(Hu (tnth t i) i j)/val_inj => -> //; by rewrite inE size_tuple.
- case: t => -[|a t] // Hlen Hinj.
apply/(uniqP a) => i j.
rewrite !inE !size_tuple => Hi Hj.
by rewrite !nth_tnth => /Hinj [].
Qed.
Lemma index_tuple (t : n.-tuple A) i : (index i t < n) <-> (i \in t).
Proof. by rewrite -index_mem size_tuple. Qed.
End tnth_eq.
Section sorted.
Definition ord_ltn {r} : rel 'I_r := relpre val ltn.
Lemma sorted_enum r : sorted ord_ltn (enum 'I_r).
Proof.
rewrite /is_true -[RHS](iota_ltn_sorted 0 r) -val_enum_ord.
by elim: (enum 'I_r) => //= a [|b l] //= <-.
Qed.
Variables (A : Type) (le : rel A) (le_trans : transitive le).
Lemma sorted_tnth q (lq : q.-tuple A) (a b : 'I_q) :
sorted le lq -> ord_ltn a b -> le (tnth lq a) (tnth lq b).
Proof.
move=> Hsort ab.
have := @sorted_ltn_nth _ le le_trans (tnth lq a) lq Hsort a b.
rewrite !inE !size_tuple !ltn_ord -!tnth_nth; exact.
Qed.
Lemma sorted_comp q (lq : q.-tuple A) (lr : seq 'I_q) :
sorted le lq -> sorted ord_ltn lr -> sorted le (map (tnth lq) lr).
Proof.
move=> Hlq /=.
elim: lr => // a [|b lr] IH //= /andP[ab] Hsort.
rewrite sorted_tnth //=; exact: IH.
Qed.
End sorted.