From a2cbf3dbca4bfc66f957b9e0457a4c1eb7932bb6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Jun 2015 16:52:00 -0700 Subject: [PATCH] refactor(library/data/fin): adjust proofs to support new approach for projections --- library/data/fin.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/data/fin.lean b/library/data/fin.lean index abd59499a..34e3c4a7c 100644 --- a/library/data/fin.lean +++ b/library/data/fin.lean @@ -159,7 +159,7 @@ lemma lift_fun_eq {f : fin n → fin n} {i : fin n} : lift_fun f (lift_succ i) = lift_succ (f i) := begin rewrite [lift_fun_of_ne_max lift_succ_ne_max], congruence, congruence, -rewrite [-eq_iff_veq, val_mk, ↑lift_succ, -val_lift] +rewrite [-eq_iff_veq], esimp, rewrite [↑lift_succ, -val_lift] end lemma lift_fun_of_inj {f : fin n → fin n} : injective f → injective (lift_fun f) := @@ -196,7 +196,7 @@ definition madd (i j : fin (succ n)) : fin (succ n) := mk ((i + j) mod (succ n)) (mod_lt _ !zero_lt_succ) lemma val_madd : ∀ i j : fin (succ n), val (madd i j) = (i + j) mod (succ n) -| (mk iv ilt) (mk jv jlt) := by rewrite [val_mk] +| (mk iv ilt) (mk jv jlt) := by esimp lemma madd_inj : ∀ {i : fin (succ n)}, injective (madd i) | (mk iv ilt) := @@ -208,7 +208,7 @@ take j₁ j₂, fin.destruct j₁ (fin.destruct j₂ (λ jv₁ jlt₁ jv₂ jlt end)) lemma val_mod : ∀ i : fin (succ n), (val i) mod (succ n) = val i -| (mk iv ilt) := by rewrite [*val_mk, mod_eq_of_lt ilt] +| (mk iv ilt) := by esimp; rewrite [(mod_eq_of_lt ilt)] definition minv : ∀ i : fin (succ n), fin (succ n) | (mk iv ilt) := mk ((succ n - iv) mod succ n) (mod_lt _ !zero_lt_succ)