michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/data/real,library/theories/group_theory): group theory and real/basic

Browse source
This commit is contained in:
Jeremy Avigad 2015-10-12 18:00:27 -04:00 • committed by Leonardo de Moura
parent ffbb2be6ac
commit 7f88e9ad33
3 changed files with 147 additions and 106 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
library/data/fin.lean
View file

@ -92,9 +92,14 @@ mk 0 !zero_lt_succ
definition fin_has_zero [instance] [reducible] (n : nat) : has_zero (fin (succ n)) := definition fin_has_zero [instance] [reducible] (n : nat) : has_zero (fin (succ n)) :=
has_zero.mk (fin.zero n) has_zero.mk (fin.zero n)
theorem val_zero (n : nat) : val (0 : fin (succ n)) = 0 := rfl
definition mk_mod [reducible] (n i : nat) : fin (succ n) := definition mk_mod [reducible] (n i : nat) : fin (succ n) :=
mk (i mod (succ n)) (mod_lt _ !zero_lt_succ) mk (i mod (succ n)) (mod_lt _ !zero_lt_succ)
theorem mk_mod_zero_eq (n : nat) : mk_mod n 0 = 0 :=
rfl
variable {n : nat} variable {n : nat}
theorem val_lt : ∀ i : fin n, val i < n theorem val_lt : ∀ i : fin n, val i < n
@ -116,7 +121,7 @@ mk n !lt_succ_self
theorem val_lift : ∀ (i : fin n) (m : nat), val i = val (lift i m) theorem val_lift : ∀ (i : fin n) (m : nat), val i = val (lift i m)
| (mk v h) m := rfl | (mk v h) m := rfl
lemma mk_succ_ne_zero {i : nat} : ∀ {P}, mk (succ i) P ≠ fin.zero n := lemma mk_succ_ne_zero {i : nat} : ∀ {P}, mk (succ i) P ≠ (0 : fin (succ n)) :=
assume P Pe, absurd (veq_of_eq Pe) !succ_ne_zero assume P Pe, absurd (veq_of_eq Pe) !succ_ne_zero
lemma mk_mod_eq {i : fin (succ n)} : i = mk_mod n i := lemma mk_mod_eq {i : fin (succ n)} : i = mk_mod n i :=
@ -127,7 +132,7 @@ begin esimp [mk_mod], congruence, exact mod_eq_of_lt Plt end
section lift_lower section lift_lower
lemma lift_zero : lift_succ (fin.zero n) = fin.zero (succ n) := rfl lemma lift_zero : lift_succ (0 : fin (succ n)) = (0 : fin (succ (succ n))) := rfl
lemma ne_max_of_lt_max {i : fin (succ n)} : i < n → i ≠ maxi := lemma ne_max_of_lt_max {i : fin (succ n)} : i < n → i ≠ maxi :=
by intro hlt he; substvars; exact absurd hlt (lt.irrefl n) by intro hlt he; substvars; exact absurd hlt (lt.irrefl n)
@ -239,8 +244,10 @@ lemma val_mod : ∀ i : fin (succ n), (val i) mod (succ n) = val i
lemma madd_comm (i j : fin (succ n)) : madd i j = madd j i := lemma madd_comm (i j : fin (succ n)) : madd i j = madd j i :=
by apply eq_of_veq; rewrite [*val_madd, add.comm (val i)] by apply eq_of_veq; rewrite [*val_madd, add.comm (val i)]
lemma zero_madd (i : fin (succ n)) : madd (fin.zero n) i = i := lemma zero_madd (i : fin (succ n)) : madd 0 i = i :=
by apply eq_of_veq; rewrite [val_madd, ↑fin.zero, nat.zero_add, mod_eq_of_lt (is_lt i)] have H : madd (fin.zero n) i = i,
by apply eq_of_veq; rewrite [val_madd, ↑fin.zero, nat.zero_add, mod_eq_of_lt (is_lt i)],
H
lemma madd_zero (i : fin (succ n)) : madd i (fin.zero n) = i := lemma madd_zero (i : fin (succ n)) : madd i (fin.zero n) = i :=
!madd_comm ▸ zero_madd i !madd_comm ▸ zero_madd i
@ -368,10 +375,10 @@ begin
apply dmap_map_lift, apply @list.lt_of_mem_upto apply dmap_map_lift, apply @list.lt_of_mem_upto
end end
definition upto_step : ∀ {n : nat}, fin.upto (n +1) = (map succ (upto n))++[fin.zero n] definition upto_step : ∀ {n : nat}, fin.upto (n +1) = (map succ (upto n))++[0]
| 0 := rfl | 0 := rfl
| (i +1) := begin rewrite [upto_succ i, map_cons, append_cons, succ_max, upto_succ, -lift_zero], | (i +1) := begin rewrite [upto_succ i, map_cons, append_cons, succ_max, upto_succ, -lift_zero],
congruence, rewrite [map_map, -lift_succ.comm, -map_map, -(map_singleton _ (fin.zero i)), -map_append, -upto_step] end congruence, rewrite [map_map, -lift_succ.comm, -map_map, -(map_singleton _ 0), -map_append, -upto_step] end
end end
open sum equiv decidable open sum equiv decidable

213
library/data/real/basic.lean
View file

@ -189,29 +189,29 @@ theorem eq_of_bdd {s t : seq} (Hs : regular s) (Ht : regular t)
have Hj : (∀ j : ℕ+, abs (s n - t n) ≤ n⁻¹ + n⁻¹ + j⁻¹ + j⁻¹ + j⁻¹), begin have Hj : (∀ j : ℕ+, abs (s n - t n) ≤ n⁻¹ + n⁻¹ + j⁻¹ + j⁻¹ + j⁻¹), begin
intros, intros,
cases H j with [Nj, HNj], cases H j with [Nj, HNj],
rewrite [-(rat.sub_add_cancel (s n) (s (max j Nj))), rat.add.assoc (s n + -s (max j Nj)), rewrite [-(sub_add_cancel (s n) (s (max j Nj))), +sub_eq_add_neg, algebra.add.assoc (s n + -s (max j Nj)),
↑regular at *], ↑regular at *],
apply rat.le.trans, apply rat.le.trans,
apply abs_add_le_abs_add_abs, apply abs_add_le_abs_add_abs,
apply rat.le.trans, apply rat.le.trans,
apply rat.add_le_add, apply add_le_add,
apply Hs, apply Hs,
rewrite [-(rat.sub_add_cancel (s (max j Nj)) (t (max j Nj))), rat.add.assoc], rewrite [-(sub_add_cancel (s (max j Nj)) (t (max j Nj))), rat.add.assoc],
apply abs_add_le_abs_add_abs, apply abs_add_le_abs_add_abs,
apply rat.le.trans, apply rat.le.trans,
apply rat.add_le_add_left, apply rat.add_le_add_left,
apply rat.add_le_add, apply add_le_add,
apply HNj (max j Nj) (max_right j Nj), apply HNj (max j Nj) (max_right j Nj),
apply Ht, apply Ht,
have hsimp : ∀ m : ℕ+, n⁻¹ + m⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) = n⁻¹ + n⁻¹ + j⁻¹ + (m⁻¹ + m⁻¹), have hsimp : ∀ m : ℕ+, n⁻¹ + m⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) = n⁻¹ + n⁻¹ + j⁻¹ + (m⁻¹ + m⁻¹),
from λm, calc from λm, calc
n⁻¹ + m⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) = n⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) + m⁻¹ : rat.add.right_comm n⁻¹ + m⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) = n⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) + m⁻¹ : algebra.add.right_comm
... = n⁻¹ + (j⁻¹ + m⁻¹ + n⁻¹) + m⁻¹ : rat.add.assoc ... = n⁻¹ + (j⁻¹ + m⁻¹ + n⁻¹) + m⁻¹ : rat.add.assoc
... = n⁻¹ + (n⁻¹ + (j⁻¹ + m⁻¹)) + m⁻¹ : rat.add.comm ... = n⁻¹ + (n⁻¹ + (j⁻¹ + m⁻¹)) + m⁻¹ : rat.add.comm
... = n⁻¹ + n⁻¹ + j⁻¹ + (m⁻¹ + m⁻¹) : by rewrite[-*rat.add.assoc], ... = n⁻¹ + n⁻¹ + j⁻¹ + (m⁻¹ + m⁻¹) : by rewrite[-*rat.add.assoc],
rewrite hsimp, rewrite hsimp,
have Hms : (max j Nj)⁻¹ + (max j Nj)⁻¹ ≤ j⁻¹ + j⁻¹, begin have Hms : (max j Nj)⁻¹ + (max j Nj)⁻¹ ≤ j⁻¹ + j⁻¹, begin
apply rat.add_le_add, apply add_le_add,
apply inv_ge_of_le (max_left j Nj), apply inv_ge_of_le (max_left j Nj),
apply inv_ge_of_le (max_left j Nj), apply inv_ge_of_le (max_left j Nj),
end, end,
@ -242,7 +242,7 @@ theorem bdd_of_eq_var {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡
intro n Hn, intro n Hn,
apply rat.le.trans, apply rat.le.trans,
apply bdd_of_eq Heq N n Hn, apply bdd_of_eq Heq N n Hn,
assumption exact HN -- assumption -- TODO: something funny here; what is 11.source.to_has_le_2?
end end
theorem equiv.trans (s t u : seq) (Hs : regular s) (Ht : regular t) (Hu : regular u) theorem equiv.trans (s t u : seq) (Hs : regular s) (Ht : regular t) (Hu : regular u)
@ -252,14 +252,14 @@ theorem equiv.trans (s t u : seq) (Hs : regular s) (Ht : regular t) (Hu : regula
intros, intros,
existsi 2 * (2 * j), existsi 2 * (2 * j),
intro n Hn, intro n Hn,
rewrite [-rat.sub_add_cancel (s n) (t n), rat.add.assoc], rewrite [-sub_add_cancel (s n) (t n), *sub_eq_add_neg, algebra.add.assoc],
apply rat.le.trans, apply rat.le.trans,
apply abs_add_le_abs_add_abs, apply abs_add_le_abs_add_abs,
have Hst : abs (s n - t n) ≤ (2 * j)⁻¹, from bdd_of_eq H _ _ Hn, have Hst : abs (s n - t n) ≤ (2 * j)⁻¹, from bdd_of_eq H _ _ Hn,
have Htu : abs (t n - u n) ≤ (2 * j)⁻¹, from bdd_of_eq H2 _ _ Hn, have Htu : abs (t n - u n) ≤ (2 * j)⁻¹, from bdd_of_eq H2 _ _ Hn,
rewrite -(add_halves j), rewrite -(add_halves j),
apply rat.add_le_add, apply add_le_add,
repeat assumption exact Hst, exact Htu
end end
----------------------------------- -----------------------------------
@ -269,14 +269,14 @@ private definition K (s : seq) : ℕ+ := pnat.pos (ubound (abs (s pone)) + 1 + 1
private theorem canon_bound {s : seq} (Hs : regular s) (n : ℕ+) : abs (s n) ≤ rat_of_pnat (K s) := private theorem canon_bound {s : seq} (Hs : regular s) (n : ℕ+) : abs (s n) ≤ rat_of_pnat (K s) :=
calc calc
abs (s n) = abs (s n - s pone + s pone) : by rewrite rat.sub_add_cancel abs (s n) = abs (s n - s pone + s pone) : by rewrite algebra.sub_add_cancel
... ≤ abs (s n - s pone) + abs (s pone) : abs_add_le_abs_add_abs ... ≤ abs (s n - s pone) + abs (s pone) : abs_add_le_abs_add_abs
... ≤ n⁻¹ + pone⁻¹ + abs (s pone) : rat.add_le_add_right !Hs ... ≤ n⁻¹ + pone⁻¹ + abs (s pone) : algebra.add_le_add_right !Hs
... = n⁻¹ + (1 + abs (s pone)) : by rewrite [pone_inv, rat.add.assoc] ... = n⁻¹ + (1 + abs (s pone)) : by rewrite [pone_inv, rat.add.assoc]
... ≤ 1 + (1 + abs (s pone)) : rat.add_le_add_right (inv_le_one n) ... ≤ 1 + (1 + abs (s pone)) : algebra.add_le_add_right (inv_le_one n)
... = abs (s pone) + (1 + 1) : ... = abs (s pone) + (1 + 1) :
by rewrite [add.comm 1 (abs (s pone)), rat.add.comm 1, rat.add.assoc] by rewrite [add.comm 1 (abs (s pone)), rat.add.comm 1, rat.add.assoc]
... ≤ of_nat (ubound (abs (s pone))) + (1 + 1) : rat.add_le_add_right (!ubound_ge) ... ≤ of_nat (ubound (abs (s pone))) + (1 + 1) : algebra.add_le_add_right (!ubound_ge)
... = of_nat (ubound (abs (s pone)) + (1 + 1)) : of_nat_add ... = of_nat (ubound (abs (s pone)) + (1 + 1)) : of_nat_add
... = of_nat (ubound (abs (s pone)) + 1 + 1) : nat.add.assoc ... = of_nat (ubound (abs (s pone)) + 1 + 1) : nat.add.assoc
... = rat_of_pnat (K s) : by esimp ... = rat_of_pnat (K s) : by esimp
@ -297,8 +297,8 @@ theorem bdd_of_regular_strict {s : seq} (H : regular s) : ∃ b : ℚ, ∀ n :
intro n, intro n,
apply rat.lt_of_le_of_lt, apply rat.lt_of_le_of_lt,
apply Hb, apply Hb,
apply rat.lt_add_of_pos_right, apply algebra.lt_add_of_pos_right,
apply rat.zero_lt_one apply zero_lt_one
end end
definition K₂ (s t : seq) := max (K s) (K t) definition K₂ (s t : seq) := max (K s) (K t)
@ -339,7 +339,7 @@ theorem reg_add_reg {s t : seq} (Hs : regular s) (Ht : regular t) : regular (sad
apply rat.le.trans, apply rat.le.trans,
apply abs_add_le_abs_add_abs, apply abs_add_le_abs_add_abs,
rewrite add_halves_double, rewrite add_halves_double,
apply rat.add_le_add, apply add_le_add,
apply Hs, apply Hs,
apply Ht apply Ht
end end
@ -354,13 +354,13 @@ theorem reg_mul_reg {s t : seq} (Hs : regular s) (Ht : regular t) : regular (smu
apply rat.le.trans, apply rat.le.trans,
apply abs_add_le_abs_add_abs, apply abs_add_le_abs_add_abs,
apply rat.le.trans, apply rat.le.trans,
apply rat.add_le_add, apply add_le_add,
rewrite abs_mul, rewrite abs_mul,
apply rat.mul_le_mul_of_nonneg_right, apply mul_le_mul_of_nonneg_right,
apply canon_2_bound_left s t Hs, apply canon_2_bound_left s t Hs,
apply abs_nonneg, apply abs_nonneg,
rewrite abs_mul, rewrite abs_mul,
apply rat.mul_le_mul_of_nonneg_left, apply mul_le_mul_of_nonneg_left,
apply canon_2_bound_right s t Ht, apply canon_2_bound_right s t Ht,
apply abs_nonneg, apply abs_nonneg,
apply ineq_helper, apply ineq_helper,
@ -389,7 +389,7 @@ theorem s_add_comm (s t : seq) : sadd s t ≡ sadd t s :=
begin begin
esimp [sadd], esimp [sadd],
intro n, intro n,
rewrite [sub_add_eq_sub_sub, rat.add_sub_cancel, rat.sub_self, abs_zero], rewrite [sub_add_eq_sub_sub, algebra.add_sub_cancel, algebra.sub_self, abs_zero],
apply add_invs_nonneg apply add_invs_nonneg
end end
@ -403,10 +403,10 @@ theorem s_add_assoc (s t u : seq) (Hs : regular s) (Hu : regular u) :
apply abs_add_le_abs_add_abs, apply abs_add_le_abs_add_abs,
apply rat.le.trans, apply rat.le.trans,
rotate 1, rotate 1,
apply rat.add_le_add_right, apply algebra.add_le_add_right,
apply inv_two_mul_le_inv, apply inv_two_mul_le_inv,
rewrite [-(add_halves (2 * n)), -(add_halves n), factor_lemma_2], rewrite [-(add_halves (2 * n)), -(add_halves n), factor_lemma_2],
apply rat.add_le_add, apply add_le_add,
apply Hs, apply Hs,
apply Hu apply Hu
end end
@ -415,7 +415,7 @@ theorem s_mul_comm (s t : seq) : smul s t ≡ smul t s :=
begin begin
rewrite ↑smul, rewrite ↑smul,
intros n, intros n,
rewrite [*(K₂_symm s t), rat.mul.comm, rat.sub_self, abs_zero], rewrite [*(K₂_symm s t), rat.mul.comm, algebra.sub_self, abs_zero],
apply add_invs_nonneg apply add_invs_nonneg
end end
@ -435,15 +435,15 @@ private theorem s_mul_assoc_lemma (s t u : seq) (a b c d : ℕ+) :
apply rat.le.trans, apply rat.le.trans,
apply abs_add_le_abs_add_abs, apply abs_add_le_abs_add_abs,
rewrite rat.add.assoc, rewrite rat.add.assoc,
apply rat.add_le_add, apply add_le_add,
rewrite 2 abs_mul, rewrite 2 abs_mul,
apply rat.le.refl, apply rat.le.refl,
rewrite [*rat.mul.assoc, -rat.mul_sub_left_distrib, -rat.left_distrib, abs_mul], rewrite [*rat.mul.assoc, -algebra.mul_sub_left_distrib, -left_distrib, abs_mul],
apply rat.mul_le_mul_of_nonneg_left, apply mul_le_mul_of_nonneg_left,
rewrite rewrite_helper, rewrite rewrite_helper,
apply rat.le.trans, apply rat.le.trans,
apply abs_add_le_abs_add_abs, apply abs_add_le_abs_add_abs,
apply rat.add_le_add, apply add_le_add,
rewrite abs_mul, apply rat.le.refl, rewrite abs_mul, apply rat.le.refl,
rewrite [abs_mul, rat.mul.comm], apply rat.le.refl, rewrite [abs_mul, rat.mul.comm], apply rat.le.refl,
apply abs_nonneg apply abs_nonneg
@ -456,7 +456,7 @@ private theorem Kq_bound {s : seq} (H : regular s) : ∀ n, abs (s n) ≤ Kq s :
apply rat.le_of_lt, apply rat.le_of_lt,
apply rat.lt_of_le_of_lt, apply rat.lt_of_le_of_lt,
apply canon_bound H, apply canon_bound H,
apply rat.lt_add_of_pos_right, apply algebra.lt_add_of_pos_right,
apply rat.zero_lt_one apply rat.zero_lt_one
end end
@ -470,7 +470,7 @@ private theorem Kq_bound_pos {s : seq} (H : regular s) : 0 < Kq s :=
private theorem s_mul_assoc_lemma_5 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) private theorem s_mul_assoc_lemma_5 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
(a b c : ℕ+) : abs (t a) * abs (u b) * abs (s a - s c) ≤ (Kq t) * (Kq u) * (a⁻¹ + c⁻¹) := (a b c : ℕ+) : abs (t a) * abs (u b) * abs (s a - s c) ≤ (Kq t) * (Kq u) * (a⁻¹ + c⁻¹) :=
begin begin
repeat apply rat.mul_le_mul, repeat apply algebra.mul_le_mul,
apply Kq_bound Ht, apply Kq_bound Ht,
apply Kq_bound Hu, apply Kq_bound Hu,
apply abs_nonneg, apply abs_nonneg,
@ -489,17 +489,17 @@ private theorem s_mul_assoc_lemma_2 {s t u : seq} (Hs : regular s) (Ht : regular
(Kq t) * (Kq u) * (a⁻¹ + c⁻¹) + (Kq s) * (Kq t) * (b⁻¹ + d⁻¹) + (Kq s) * (Kq u) * (a⁻¹ + d⁻¹) := (Kq t) * (Kq u) * (a⁻¹ + c⁻¹) + (Kq s) * (Kq t) * (b⁻¹ + d⁻¹) + (Kq s) * (Kq u) * (a⁻¹ + d⁻¹) :=
begin begin
apply add_le_add_three, apply add_le_add_three,
repeat (assumption | apply rat.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg | repeat (assumption | apply algebra.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg |
apply abs_nonneg), apply abs_nonneg),
apply Hs, apply Hs,
apply abs_nonneg, apply abs_nonneg,
apply rat.mul_nonneg, apply rat.mul_nonneg,
repeat (assumption | apply rat.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg | repeat (assumption | apply algebra.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg |
apply abs_nonneg), apply abs_nonneg),
apply Hu, apply Hu,
apply abs_nonneg, apply abs_nonneg,
apply rat.mul_nonneg, apply rat.mul_nonneg,
repeat (assumption | apply rat.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg | repeat (assumption | apply algebra.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg |
apply abs_nonneg), apply abs_nonneg),
apply Ht, apply Ht,
apply abs_nonneg, apply abs_nonneg,
@ -528,24 +528,24 @@ theorem s_mul_assoc {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regula
apply Hs, apply Hs,
apply Ht, apply Ht,
apply Hu, apply Hu,
rewrite [*s_mul_assoc_lemma_3, -rat.distrib_three_right], rewrite [*s_mul_assoc_lemma_3, -distrib_three_right],
apply s_mul_assoc_lemma_4, apply s_mul_assoc_lemma_4,
apply a, apply a,
repeat apply rat.add_pos, repeat apply add_pos,
repeat apply rat.mul_pos, repeat apply mul_pos,
apply Kq_bound_pos Ht, apply Kq_bound_pos Ht,
apply Kq_bound_pos Hu, apply Kq_bound_pos Hu,
apply rat.add_pos, apply add_pos,
repeat apply inv_pos, repeat apply inv_pos,
repeat apply rat.mul_pos, repeat apply rat.mul_pos,
apply Kq_bound_pos Hs, apply Kq_bound_pos Hs,
apply Kq_bound_pos Ht, apply Kq_bound_pos Ht,
apply rat.add_pos, apply add_pos,
repeat apply inv_pos, repeat apply inv_pos,
repeat apply rat.mul_pos, repeat apply rat.mul_pos,
apply Kq_bound_pos Hs, apply Kq_bound_pos Hs,
apply Kq_bound_pos Hu, apply Kq_bound_pos Hu,
apply rat.add_pos, apply add_pos,
repeat apply inv_pos, repeat apply inv_pos,
apply a_1 apply a_1
end end
@ -554,7 +554,7 @@ theorem zero_is_reg : regular zero :=
begin begin
rewrite [↑regular, ↑zero], rewrite [↑regular, ↑zero],
intros, intros,
rewrite [rat.sub_zero, abs_zero], rewrite [algebra.sub_zero, abs_zero],
apply add_invs_nonneg apply add_invs_nonneg
end end
@ -565,7 +565,7 @@ theorem s_zero_add (s : seq) (H : regular s) : sadd zero s ≡ s :=
rewrite [rat.zero_add], rewrite [rat.zero_add],
apply rat.le.trans, apply rat.le.trans,
apply H, apply H,
apply rat.add_le_add, apply add_le_add,
apply inv_two_mul_le_inv, apply inv_two_mul_le_inv,
apply rat.le.refl apply rat.le.refl
end end
@ -577,7 +577,7 @@ theorem s_add_zero (s : seq) (H : regular s) : sadd s zero ≡ s :=
rewrite [rat.add_zero], rewrite [rat.add_zero],
apply rat.le.trans, apply rat.le.trans,
apply H, apply H,
apply rat.add_le_add, apply add_le_add,
apply inv_two_mul_le_inv, apply inv_two_mul_le_inv,
apply rat.le.refl apply rat.le.refl
end end
@ -586,7 +586,7 @@ theorem s_neg_cancel (s : seq) (H : regular s) : sadd (sneg s) s ≡ zero :=
begin begin
rewrite [↑sadd, ↑sneg, ↑regular at H, ↑zero, ↑equiv], rewrite [↑sadd, ↑sneg, ↑regular at H, ↑zero, ↑equiv],
intros, intros,
rewrite [neg_add_eq_sub, rat.sub_self, rat.sub_zero, abs_zero], rewrite [neg_add_eq_sub, algebra.sub_self, algebra.sub_zero, abs_zero],
apply add_invs_nonneg apply add_invs_nonneg
end end
@ -608,7 +608,7 @@ theorem add_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu :
rewrite [add_sub_comm, add_halves_double], rewrite [add_sub_comm, add_halves_double],
apply rat.le.trans, apply rat.le.trans,
apply abs_add_le_abs_add_abs, apply abs_add_le_abs_add_abs,
apply rat.add_le_add, apply add_le_add,
apply Esu, apply Esu,
apply Etv apply Etv
end end
@ -627,57 +627,60 @@ private theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (
rotate 1, rotate 1,
show n⁻¹ * ((rat_of_pnat (K s)) * (b⁻¹ + c⁻¹)) + show n⁻¹ * ((rat_of_pnat (K s)) * (b⁻¹ + c⁻¹)) +
n⁻¹ * ((a⁻¹ + c⁻¹) * (rat_of_pnat (K t))) ≤ j⁻¹, begin n⁻¹ * ((a⁻¹ + c⁻¹) * (rat_of_pnat (K t))) ≤ j⁻¹, begin
rewrite -rat.left_distrib, rewrite -left_distrib,
apply rat.le.trans, apply rat.le.trans,
apply rat.mul_le_mul_of_nonneg_right, apply mul_le_mul_of_nonneg_right,
apply pceil_helper Hn, apply pceil_helper Hn,
repeat (apply rat.mul_pos | apply rat.add_pos | apply inv_pos | apply rat_of_pnat_is_pos), { repeat (apply algebra.mul_pos | apply algebra.add_pos | apply rat_of_pnat_is_pos |
apply pnat.inv_pos) },
apply rat.le_of_lt, apply rat.le_of_lt,
apply rat.add_pos, apply add_pos,
apply rat.mul_pos, apply rat.mul_pos,
apply rat_of_pnat_is_pos, apply rat_of_pnat_is_pos,
apply rat.add_pos, apply add_pos,
repeat apply inv_pos, apply pnat.inv_pos,
apply pnat.inv_pos,
apply rat.mul_pos, apply rat.mul_pos,
apply rat.add_pos, apply add_pos,
repeat apply inv_pos, apply pnat.inv_pos,
apply pnat.inv_pos,
apply rat_of_pnat_is_pos, apply rat_of_pnat_is_pos,
have H : (rat_of_pnat (K s) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) * rat_of_pnat (K t)) ≠ 0, begin have H : (rat_of_pnat (K s) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) * rat_of_pnat (K t)) ≠ 0, begin
apply rat.ne_of_gt, apply ne_of_gt,
repeat (apply rat.mul_pos | apply rat.add_pos | apply rat_of_pnat_is_pos | apply inv_pos), repeat (apply algebra.mul_pos | apply algebra.add_pos | apply rat_of_pnat_is_pos | apply pnat.inv_pos),
end, end,
rewrite (!rat.div_helper H), rewrite (!div_helper H),
apply rat.le.refl apply rat.le.refl
end, end,
apply rat.add_le_add, apply add_le_add,
rewrite [-rat.mul_sub_left_distrib, abs_mul], rewrite [-algebra.mul_sub_left_distrib, abs_mul],
apply rat.le.trans, apply rat.le.trans,
apply rat.mul_le_mul, apply algebra.mul_le_mul,
apply canon_bound, apply canon_bound,
apply Hs, apply Hs,
apply Ht, apply Ht,
apply abs_nonneg, apply abs_nonneg,
apply rat.le_of_lt, apply rat.le_of_lt,
apply rat_of_pnat_is_pos, apply rat_of_pnat_is_pos,
rewrite [*inv_mul_eq_mul_inv, -rat.right_distrib, -rat.mul.assoc, rat.mul.comm], rewrite [*inv_mul_eq_mul_inv, -right_distrib, -rat.mul.assoc, rat.mul.comm],
apply rat.mul_le_mul_of_nonneg_left, apply mul_le_mul_of_nonneg_left,
apply rat.le.refl, apply rat.le.refl,
apply rat.le_of_lt, apply rat.le_of_lt,
apply inv_pos, apply inv_pos,
rewrite [-rat.mul_sub_right_distrib, abs_mul], rewrite [-algebra.mul_sub_right_distrib, abs_mul],
apply rat.le.trans, apply rat.le.trans,
apply rat.mul_le_mul, apply algebra.mul_le_mul,
apply Hs, apply Hs,
apply canon_bound, apply canon_bound,
apply Ht, apply Ht,
apply abs_nonneg, apply abs_nonneg,
apply add_invs_nonneg, apply add_invs_nonneg,
rewrite [*inv_mul_eq_mul_inv, -rat.right_distrib, mul.comm _ n⁻¹, rat.mul.assoc], rewrite [*inv_mul_eq_mul_inv, -right_distrib, mul.comm _ n⁻¹, rat.mul.assoc],
apply rat.mul_le_mul, apply algebra.mul_le_mul,
repeat apply rat.le.refl, repeat apply rat.le.refl,
apply rat.le_of_lt, apply rat.le_of_lt,
apply rat.mul_pos, apply rat.mul_pos,
apply rat.add_pos, apply add_pos,
repeat apply inv_pos, repeat apply inv_pos,
apply rat_of_pnat_is_pos, apply rat_of_pnat_is_pos,
apply rat.le_of_lt, apply rat.le_of_lt,
@ -705,13 +708,13 @@ theorem s_distrib {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular
rewrite [↑sadd at *, ↑smul, rewrite_helper3, -add_halves j, -*pnat.mul.assoc at *], rewrite [↑sadd at *, ↑smul, rewrite_helper3, -add_halves j, -*pnat.mul.assoc at *],
apply rat.le.trans, apply rat.le.trans,
apply abs_add_le_abs_add_abs, apply abs_add_le_abs_add_abs,
apply rat.add_le_add, apply add_le_add,
apply HN1, apply HN1,
apply le.trans, apply pnat.le.trans,
apply max_left N1 N2, apply max_left N1 N2,
apply Hn, apply Hn,
apply HN2, apply HN2,
apply le.trans, apply pnat.le.trans,
apply max_right N1 N2, apply max_right N1 N2,
apply Hn apply Hn
end end
@ -728,17 +731,18 @@ theorem mul_zero_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t) (Htz :
cases Bd with [N, HN], cases Bd with [N, HN],
existsi N, existsi N,
intro n Hn, intro n Hn,
rewrite [↑equiv at Htz, ↑zero at *, rat.sub_zero, ↑smul, abs_mul], rewrite [↑equiv at Htz, ↑zero at *, algebra.sub_zero, ↑smul, abs_mul],
apply rat.le.trans, apply rat.le.trans,
apply rat.mul_le_mul, apply algebra.mul_le_mul,
apply Kq_bound Hs, apply Kq_bound Hs,
let HN' := λ n, (!rat.sub_zero ▸ HN n), have HN' : ∀ (n : ℕ+), N ≤ n → abs (t n) ≤ ε / Kq s,
from λ n, (eq.subst (sub_zero (t n)) (HN n)),
apply HN', apply HN',
apply le.trans Hn, apply le.trans Hn,
apply pnat.mul_le_mul_left, apply pnat.mul_le_mul_left,
apply abs_nonneg, apply abs_nonneg,
apply rat.le_of_lt (Kq_bound_pos Hs), apply rat.le_of_lt (Kq_bound_pos Hs),
rewrite (rat.mul_div_cancel' (ne.symm (rat.ne_of_lt (Kq_bound_pos Hs)))), rewrite (mul_div_cancel' (ne.symm (ne_of_lt (Kq_bound_pos Hs)))),
apply rat.le.refl apply rat.le.refl
end end
@ -755,7 +759,7 @@ theorem mul_neg_equiv_neg_mul {s t : seq} : smul s (sneg t) ≡ sneg (smul s t)
rewrite [↑equiv, ↑smul], rewrite [↑equiv, ↑smul],
intros, intros,
rewrite [↑sneg, *sub_neg_eq_add, -neg_mul_eq_mul_neg, rat.add.comm, *sneg_def, rewrite [↑sneg, *sub_neg_eq_add, -neg_mul_eq_mul_neg, rat.add.comm, *sneg_def,
*neg_bound2_eq_bound2, rat.sub_self, abs_zero], *neg_bound2_eq_bound2, algebra.add.right_inv, abs_zero],
apply add_invs_nonneg apply add_invs_nonneg
end end
@ -764,7 +768,7 @@ theorem equiv_of_diff_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t)
begin begin
have hsimp : ∀ a b c d e : ℚ, a + b + c + (d + e) = b + d + a + e + c, from have hsimp : ∀ a b c d e : ℚ, a + b + c + (d + e) = b + d + a + e + c, from
λ a b c d e, calc λ a b c d e, calc
a + b + c + (d + e) = a + b + (d + e) + c : rat.add.right_comm a + b + c + (d + e) = a + b + (d + e) + c : algebra.add.right_comm
... = a + (b + d) + e + c : by rewrite[-*rat.add.assoc] ... = a + (b + d) + e + c : by rewrite[-*rat.add.assoc]
... = b + d + a + e + c : rat.add.comm, ... = b + d + a + e + c : rat.add.comm,
apply eq_of_bdd Hs Ht, apply eq_of_bdd Hs Ht,
@ -779,11 +783,11 @@ theorem equiv_of_diff_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t)
apply add_le_add_three, apply add_le_add_three,
apply Hs, apply Hs,
rewrite [↑sadd at He, ↑sneg at He, ↑zero at He], rewrite [↑sadd at He, ↑sneg at He, ↑zero at He],
let He' := λ a b c, !rat.sub_zero ▸ (He a b c), let He' := λ a b c, eq.subst !algebra.sub_zero (He a b c),
apply (He' _ _ Hn), apply (He' _ _ Hn),
apply Ht, apply Ht,
rewrite [hsimp, add_halves, -(add_halves j), -(add_halves (2 * j)), -*rat.add.assoc], rewrite [hsimp, add_halves, -(add_halves j), -(add_halves (2 * j)), -*rat.add.assoc],
apply rat.add_le_add_right, apply algebra.add_le_add_right,
apply add_le_add_three, apply add_le_add_three,
repeat (apply rat.le.trans; apply inv_ge_of_le Hn; apply inv_two_mul_le_inv) repeat (apply rat.le.trans; apply inv_ge_of_le Hn; apply inv_two_mul_le_inv)
end end
@ -792,7 +796,7 @@ theorem s_sub_cancel (s : seq) : sadd s (sneg s) ≡ zero :=
begin begin
rewrite [↑equiv, ↑sadd, ↑sneg, ↑zero], rewrite [↑equiv, ↑sadd, ↑sneg, ↑zero],
intros, intros,
rewrite [rat.sub_zero, rat.sub_self, abs_zero], rewrite [algebra.sub_zero, algebra.add.right_inv, abs_zero],
apply add_invs_nonneg apply add_invs_nonneg
end end
@ -875,7 +879,7 @@ theorem one_is_reg : regular one :=
begin begin
rewrite [↑regular, ↑one], rewrite [↑regular, ↑one],
intros, intros,
rewrite [rat.sub_self, abs_zero], rewrite [algebra.sub_self, abs_zero],
apply add_invs_nonneg apply add_invs_nonneg
end end
@ -885,7 +889,7 @@ theorem s_one_mul {s : seq} (H : regular s) : smul one s ≡ s :=
rewrite [↑smul, ↑one, rat.one_mul], rewrite [↑smul, ↑one, rat.one_mul],
apply rat.le.trans, apply rat.le.trans,
apply H, apply H,
apply rat.add_le_add_right, apply algebra.add_le_add_right,
apply inv_mul_le_inv apply inv_mul_le_inv
end end
@ -905,7 +909,7 @@ theorem zero_nequiv_one : ¬ zero ≡ one :=
intro Hz, intro Hz,
rewrite [↑equiv at Hz, ↑zero at Hz, ↑one at Hz], rewrite [↑equiv at Hz, ↑zero at Hz, ↑one at Hz],
let H := Hz (2 * 2), let H := Hz (2 * 2),
rewrite [rat.zero_sub at H, abs_neg at H, add_halves at H], rewrite [algebra.zero_sub at H, abs_neg at H, add_halves at H],
have H' : pone⁻¹ ≤ 2⁻¹, from calc have H' : pone⁻¹ ≤ 2⁻¹, from calc
pone⁻¹ = 1 : by rewrite -pone_inv pone⁻¹ = 1 : by rewrite -pone_inv
... = abs 1 : abs_of_pos zero_lt_one ... = abs 1 : abs_of_pos zero_lt_one
@ -922,7 +926,7 @@ definition const (a : ℚ) : seq := λ n, a
theorem const_reg (a : ℚ) : regular (const a) := theorem const_reg (a : ℚ) : regular (const a) :=
begin begin
intros, intros,
rewrite [↑const, rat.sub_self, abs_zero], rewrite [↑const, algebra.sub_self, abs_zero],
apply add_invs_nonneg apply add_invs_nonneg
end end
@ -948,7 +952,7 @@ section
show abs (a - b) ≤ ε, from calc show abs (a - b) ≤ ε, from calc
abs (a - b) ≤ n⁻¹ + n⁻¹ : H₁ n abs (a - b) ≤ n⁻¹ + n⁻¹ : H₁ n
... ≤ ε / 2 + ε / 2 : add_le_add Hn Hn ... ≤ ε / 2 + ε / 2 : add_le_add Hn Hn
... = ε : rat.add_halves) ... = ε : algebra.add_halves)
end end
--------------------------------------------- ---------------------------------------------
@ -1051,11 +1055,13 @@ definition real := quot reg_seq.to_setoid
namespace real namespace real
notation `ℝ` := real notation `ℝ` := real
protected definition prio := num.pred rat.prio
definition add (x y : ℝ) : ℝ := definition add (x y : ℝ) : ℝ :=
(quot.lift_on₂ x y (λ a b, quot.mk (a + b)) (quot.lift_on₂ x y (λ a b, quot.mk (a + b))
(take a b c d : reg_seq, take Hab : requiv a c, take Hcd : requiv b d, (take a b c d : reg_seq, take Hab : requiv a c, take Hcd : requiv b d,
quot.sound (radd_well_defined Hab Hcd))) quot.sound (radd_well_defined Hab Hcd)))
protected definition prio := num.pred rat.prio
infix [priority real.prio] + := add infix [priority real.prio] + := add
definition mul (x y : ℝ) : ℝ := definition mul (x y : ℝ) : ℝ :=
@ -1069,6 +1075,20 @@ definition neg (x : ℝ) : ℝ :=
quot.sound (rneg_well_defined Hab))) quot.sound (rneg_well_defined Hab)))
prefix [priority real.prio] `-` := neg prefix [priority real.prio] `-` := neg
definition real_has_add [reducible] [instance] [priority real.prio] : has_add real :=
has_add.mk real.add
definition real_has_mul [reducible] [instance] [priority real.prio] : has_mul real :=
has_mul.mk real.mul
definition real_has_neg [reducible] [instance] [priority real.prio] : has_neg real :=
has_neg.mk real.neg
protected definition sub [reducible] (a b : ℝ) : real := a + (-b)
definition real_has_sub [reducible] [instance] [priority real.prio] : has_sub real :=
has_sub.mk real.sub
open rat -- no coercions before open rat -- no coercions before
definition of_rat [coercion] (a : ℚ) : ℝ := quot.mk (r_const a) definition of_rat [coercion] (a : ℚ) : ℝ := quot.mk (r_const a)
@ -1076,6 +1096,18 @@ definition of_int [coercion] (i : ℤ) : ℝ := int.to.real i
definition of_nat [coercion] (n : ℕ) : ℝ := nat.to.real n definition of_nat [coercion] (n : ℕ) : ℝ := nat.to.real n
definition of_num [coercion] [reducible] (n : num) : ℝ := of_rat (rat.of_num n) definition of_num [coercion] [reducible] (n : num) : ℝ := of_rat (rat.of_num n)
definition real_has_zero [reducible] [instance] [priority rat.prio] : has_zero real :=
has_zero.mk (0:rat)
definition real_has_one [reducible] [instance] [priority rat.prio] : has_one real :=
has_one.mk (1:rat)
theorem real_zero_eq_rat_zero : (0:real) = of_rat (0:rat) :=
rfl
theorem real_one_eq_rat_one : (1:real) = of_rat (1:rat) :=
rfl
theorem add_comm (x y : ℝ) : x + y = y + x := theorem add_comm (x y : ℝ) : x + y = y + x :=
quot.induction_on₂ x y (λ s t, quot.sound (r_add_comm s t)) quot.induction_on₂ x y (λ s t, quot.sound (r_add_comm s t))
@ -1174,25 +1206,26 @@ theorem of_rat_neg (a : ℚ) : of_rat (-a) = -of_rat a :=
theorem of_rat_mul (a b : ℚ) : of_rat (a * b) = of_rat a * of_rat b := theorem of_rat_mul (a b : ℚ) : of_rat (a * b) = of_rat a * of_rat b :=
quot.sound (r_mul_consts a b) quot.sound (r_mul_consts a b)
theorem of_int_add (a b : ℤ) : of_int (#int a + b) = of_int a + of_int b := open int
theorem of_int_add (a b : ℤ) : of_int (a + b) = of_int a + of_int b :=
by rewrite [of_int_eq, rat.of_int_add, of_rat_add] by rewrite [of_int_eq, rat.of_int_add, of_rat_add]
theorem of_int_neg (a : ℤ) : of_int (#int -a) = -of_int a := theorem of_int_neg (a : ℤ) : of_int (-a) = -of_int a :=
by rewrite [of_int_eq, rat.of_int_neg, of_rat_neg] by rewrite [of_int_eq, rat.of_int_neg, of_rat_neg]
theorem of_int_mul (a b : ℤ) : of_int (#int a * b) = of_int a * of_int b := theorem of_int_mul (a b : ℤ) : of_int (a * b) = of_int a * of_int b :=
by rewrite [of_int_eq, rat.of_int_mul, of_rat_mul] by rewrite [of_int_eq, rat.of_int_mul, of_rat_mul]
theorem of_nat_add (a b : ℕ) : of_nat (#nat a + b) = of_nat a + of_nat b := theorem of_nat_add (a b : ℕ) : of_nat (a + b) = of_nat a + of_nat b :=
by rewrite [of_nat_eq, rat.of_nat_add, of_rat_add] by rewrite [of_nat_eq, rat.of_nat_add, of_rat_add]
theorem of_nat_mul (a b : ℕ) : of_nat (#nat a * b) = of_nat a * of_nat b := theorem of_nat_mul (a b : ℕ) : of_nat (a * b) = of_nat a * of_nat b :=
by rewrite [of_nat_eq, rat.of_nat_mul, of_rat_mul] by rewrite [of_nat_eq, rat.of_nat_mul, of_rat_mul]
theorem add_half_of_rat (n : ℕ+) : of_rat (2 * n)⁻¹ + of_rat (2 * n)⁻¹ = of_rat (n⁻¹) := theorem add_half_of_rat (n : ℕ+) : of_rat (2 * n)⁻¹ + of_rat (2 * n)⁻¹ = of_rat (n⁻¹) :=
by rewrite [-of_rat_add, pnat.add_halves] by rewrite [-of_rat_add, pnat.add_halves]
theorem one_add_one : 1 + 1 = (2 : ℝ) := theorem one_add_one : 1 + 1 = (2 : ℝ) := rfl
by rewrite -of_rat_add
end real end real

21
library/theories/group_theory/cyclic.lean
View file

@ -229,7 +229,8 @@ end
definition pow_fin_is_iso (a : A) : is_iso_class (pow_fin' a) := definition pow_fin_is_iso (a : A) : is_iso_class (pow_fin' a) :=
is_iso_class.mk (pow_fin_hom a) is_iso_class.mk (pow_fin_hom a)
(begin rewrite [↑pow_fin', succ_pred_of_pos !order_pos], exact pow_fin_inj a 0 end) (have H : injective (λ (i : fin (order a)), a ^ (val i + 0)), from pow_fin_inj a 0,
begin+ rewrite [↑pow_fin', succ_pred_of_pos !order_pos]; exact H end)
end cyclic end cyclic
@ -262,16 +263,16 @@ lemma rotl_succ' {n m : nat} : rotl m = madd (mk_mod n (n*m)) := rfl
lemma rotl_zero : ∀ {n : nat}, @rotl n 0 = id lemma rotl_zero : ∀ {n : nat}, @rotl n 0 = id
| 0 := funext take i, elim0 i | 0 := funext take i, elim0 i
| (succ n) := funext take i, zero_add i | (nat.succ n) := funext take i, begin rewrite [↑rotl, mul_zero, mk_mod_zero_eq, zero_madd] end
lemma rotl_id : ∀ {n : nat}, @rotl n n = id lemma rotl_id : ∀ {n : nat}, @rotl n n = id
| 0 := funext take i, elim0 i | 0 := funext take i, elim0 i
| (succ n) := | (nat.succ n) :=
assert P : mk_mod n (n * succ n) = mk_mod n 0, assert P : mk_mod n (n * succ n) = mk_mod n 0,
from eq_of_veq !mul_mod_left, from eq_of_veq (by rewrite [↑mk_mod, mul_mod_left]),
begin rewrite [rotl_succ', P], apply rotl_zero end begin rewrite [rotl_succ', P], apply rotl_zero end
lemma rotl_to_zero {n i : nat} : rotl i (mk_mod n i) = zero n := lemma rotl_to_zero {n i : nat} : rotl i (mk_mod n i) = 0 :=
eq_of_veq begin rewrite [↑rotl, val_madd], esimp [mk_mod], rewrite [ mod_add_mod, add_mod_mod, -succ_mul, mul_mod_right] end eq_of_veq begin rewrite [↑rotl, val_madd], esimp [mk_mod], rewrite [ mod_add_mod, add_mod_mod, -succ_mul, mul_mod_right] end
lemma rotl_compose : ∀ {n : nat} {j k : nat}, (@rotl n j) ∘ (rotl k) = rotl (j + k) lemma rotl_compose : ∀ {n : nat} {j k : nat}, (@rotl n j) ∘ (rotl k) = rotl (j + k)
@ -307,8 +308,8 @@ lemma rotl_eq_rotl : ∀ {n : nat}, map (rotl 1) (upto n) = list.rotl (upto n)
rewrite [upto_step at {1}, upto_succ, rotl_cons, map_append], rewrite [upto_step at {1}, upto_succ, rotl_cons, map_append],
congruence, congruence,
rewrite [map_map], congruence, exact rotl_succ, rewrite [map_map], congruence, exact rotl_succ,
rewrite [map_singleton], congruence, rewrite [↑rotl, mul_one n, ↑mk_mod, ↑zero, ↑maxi, ↑madd], rewrite [map_singleton], congruence, rewrite [↑rotl, mul_one n, ↑mk_mod, ↑maxi, ↑madd],
congruence, rewrite [ mod_add_mod, nat.add_zero, mod_eq_of_lt !lt_succ_self ] congruence, rewrite [ mod_add_mod, val_zero, add_zero, mod_eq_of_lt !lt_succ_self ]
end end
definition seq [reducible] (A : Type) (n : nat) := fin n → A definition seq [reducible] (A : Type) (n : nat) := fin n → A
@ -322,9 +323,9 @@ lemma rotl_seq_zero {n : nat} : rotl_fun 0 = @id (seq A n) :=
funext take f, begin rewrite [↑rotl_fun, rotl_zero] end funext take f, begin rewrite [↑rotl_fun, rotl_zero] end
lemma rotl_seq_ne_id : ∀ {n : nat}, (∃ a b : A, a ≠ b) → ∀ i, i < n → rotl_fun (succ i) ≠ (@id (seq A (succ n))) lemma rotl_seq_ne_id : ∀ {n : nat}, (∃ a b : A, a ≠ b) → ∀ i, i < n → rotl_fun (succ i) ≠ (@id (seq A (succ n)))
| 0 := assume Pex, take i, assume Piltn, absurd Piltn !not_lt_zero | 0 := assume Pex, take i, assume Piltn, absurd Piltn !not_lt_zero
| (succ n) := assume Pex, obtain a b Pne, from Pex, take i, assume Pilt, | (nat.succ n) := assume Pex, obtain a b Pne, from Pex, take i, assume Pilt,
let f := (λ j : fin (succ (succ n)), if j = zero (succ n) then a else b), let f := (λ j : fin (succ (succ n)), if j = 0 then a else b),
fi := mk_mod (succ n) (succ i) in fi := mk_mod (succ n) (succ i) in
have Pfne : rotl_fun (succ i) f fi ≠ f fi, have Pfne : rotl_fun (succ i) f fi ≠ f fi,
from begin rewrite [↑rotl_fun, rotl_to_zero, mk_mod_of_lt (succ_lt_succ Pilt), if_pos rfl, if_neg mk_succ_ne_zero], assumption end, from begin rewrite [↑rotl_fun, rotl_to_zero, mk_mod_of_lt (succ_lt_succ Pilt), if_pos rfl, if_neg mk_succ_ne_zero], assumption end,