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

refactor(library/data/fin): adjust proofs to support new approach for projections

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-25 16:52:00 -07:00
parent 0b7859f387
commit a2cbf3dbca
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/data/fin.lean
View file

@ -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)