From 95fa4cfb0a8774570d67bb231c1ab088a94e12bb Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 11 Jan 2019 17:42:54 +0100 Subject: [PATCH] refactor(library/init/meta/transfer): remove transfer and relators --- library/data/dlist.lean | 53 ---- library/init/data/int/basic.lean | 406 ++++++++++++++++++++----------- library/init/data/int/order.lean | 2 +- library/init/meta/transfer.lean | 187 -------------- library/init/relator.lean | 84 ------- 5 files changed, 270 insertions(+), 462 deletions(-) delete mode 100644 library/init/meta/transfer.lean delete mode 100644 library/init/relator.lean diff --git a/library/data/dlist.lean b/library/data/dlist.lean index 616b2c54d6..e554844c25 100644 --- a/library/data/dlist.lean +++ b/library/data/dlist.lean @@ -89,57 +89,4 @@ by cases l; simp lemma to_list_concat (x : α) (l : dlist α) : to_list (concat x l) = to_list l ++ [x] := by cases l; simp; rw [l_invariant] -section transfer - -protected def rel_dlist_list (d : dlist α) (l : list α) : Prop := -to_list d = l - -instance bi_total_rel_dlist_list : @relator.bi_total (dlist α) (list α) dlist.rel_dlist_list := -⟨assume d, ⟨to_list d, rfl⟩, assume l, ⟨of_list l, to_list_of_list l⟩⟩ - -protected lemma rel_eq : - (dlist.rel_dlist_list ⇒ dlist.rel_dlist_list ⇒ iff) (@eq (dlist α)) eq -| l₁ ._ rfl l₂ ._ rfl := ⟨congr_arg to_list, - assume : to_list l₁ = to_list l₂, - have of_list (to_list l₁) = of_list (to_list l₂), from congr_arg of_list this, - by simp [of_list_to_list] at this; assumption⟩ - -protected lemma rel_empty : dlist.rel_dlist_list (@empty α) [] := -to_list_empty - -protected lemma rel_singleton : (@eq α ⇒ dlist.rel_dlist_list) (λx, singleton x) (λx, [x]) -| ._ x rfl := to_list_singleton x - -protected lemma rel_append : - (dlist.rel_dlist_list ⇒ dlist.rel_dlist_list ⇒ dlist.rel_dlist_list) (λ(x y : dlist α), x ++ y) (λx y, x ++ y) -| l₁ ._ rfl l₂ ._ rfl := to_list_append l₁ l₂ - -protected lemma rel_cons : - (@eq α ⇒ dlist.rel_dlist_list ⇒ dlist.rel_dlist_list) cons (λx y, x :: y) -| x ._ rfl l ._ rfl := to_list_cons x l - -protected lemma rel_concat : - (@eq α ⇒ dlist.rel_dlist_list ⇒ dlist.rel_dlist_list) concat (λx y, y ++ [x]) -| x ._ rfl l ._ rfl := to_list_concat x l - -protected meta def transfer : tactic unit := do - _root_.transfer.transfer [`relator.rel_forall_of_total, `dlist.rel_eq, `dlist.rel_empty, - `dlist.rel_singleton, `dlist.rel_append, `dlist.rel_cons, `dlist.rel_concat] - -example : ∀(a b c : dlist α), a ++ (b ++ c) = (a ++ b) ++ c := -begin - dlist.transfer, - intros, - simp -end - -example : ∀(a : α), singleton a ++ empty = singleton a := -begin - dlist.transfer, - intros, - simp -end - -end transfer - end dlist diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean index adb45481e7..4c10c0217f 100644 --- a/library/init/data/int/basic.lean +++ b/library/init/data/int/basic.lean @@ -6,7 +6,7 @@ Authors: Jeremy Avigad The integers, with addition, multiplication, and subtraction. -/ prelude -import init.data.nat.lemmas init.data.nat.gcd init.meta.transfer init.data.list +import init.data.nat.lemmas init.data.nat.gcd open nat /- the type, coercions, and notation -/ @@ -58,6 +58,14 @@ match (n - m : nat) with | (succ k) := -[1+ k] -- m < n, and n - m = succ k end +private lemma sub_nat_nat_of_sub_eq_zero {m n : ℕ} (h : n - m = 0) : + sub_nat_nat m n = of_nat (m - n) := +begin unfold sub_nat_nat, rw h, unfold sub_nat_nat._match_1 end + +private lemma sub_nat_nat_of_sub_eq_succ {m n k : ℕ} (h : n - m = succ k) : + sub_nat_nat m n = -[1+ k] := +begin unfold sub_nat_nat, rw h, unfold sub_nat_nat._match_1 end + protected def neg : ℤ → ℤ | (of_nat n) := neg_of_nat n | -[1+ n] := succ n @@ -99,7 +107,30 @@ protected lemma coe_nat_add_out (m n : ℕ) : ↑m + ↑n = (m + n : ℤ) := rfl protected lemma coe_nat_mul_out (m n : ℕ) : ↑m * ↑n = (↑(m * n) : ℤ) := rfl protected lemma coe_nat_add_one_out (n : ℕ) : ↑n + (1 : ℤ) = ↑(succ n) := rfl -/- injectivity of the constructor functions -/ +/- these are only for internal use -/ + +private lemma of_nat_add_of_nat (m n : nat) : of_nat m + of_nat n = of_nat (m + n) := rfl +private lemma of_nat_add_neg_succ_of_nat (m n : nat) : + of_nat m + -[1+ n] = sub_nat_nat m (succ n) := rfl +private lemma neg_succ_of_nat_add_of_nat (m n : nat) : + -[1+ m] + of_nat n = sub_nat_nat n (succ m) := rfl +private lemma neg_succ_of_nat_add_neg_succ_of_nat (m n : nat) : + -[1+ m] + -[1+ n] = -[1+ succ (m + n)] := rfl + +private lemma of_nat_mul_of_nat (m n : nat) : of_nat m * of_nat n = of_nat (m * n) := rfl +private lemma of_nat_mul_neg_succ_of_nat (m n : nat) : + of_nat m * -[1+ n] = neg_of_nat (m * succ n) := rfl +private lemma neg_succ_of_nat_of_nat (m n : nat) : + -[1+ m] * of_nat n = neg_of_nat (succ m * n) := rfl +private lemma mul_neg_succ_of_nat_neg_succ_of_nat (m n : nat) : + -[1+ m] * -[1+ n] = of_nat (succ m * succ n) := rfl + +local attribute [simp] of_nat_add_of_nat of_nat_mul_of_nat neg_of_nat_zero neg_of_nat_of_succ + neg_neg_of_nat_succ of_nat_add_neg_succ_of_nat neg_succ_of_nat_add_of_nat + neg_succ_of_nat_add_neg_succ_of_nat of_nat_mul_neg_succ_of_nat neg_succ_of_nat_of_nat + mul_neg_succ_of_nat_neg_succ_of_nat + +/- some basic functions and properties -/ protected lemma of_nat_inj {m n : ℕ} (h : of_nat m = of_nat n) : m = n := int.no_confusion h id @@ -168,6 +199,13 @@ sub_nat_nat_elim m n (λm n i, sub_nat_nat (m + k) (n + k) = i) (assume i m, have m + i + 1 + k = (m + k) + i + 1, by simp, begin rw [this], exact sub_nat_nat_add_right end) +private lemma sub_nat_nat_of_ge {m n : ℕ} (h : m ≥ n) : sub_nat_nat m n = of_nat (m - n) := +sub_nat_nat_of_sub_eq_zero (sub_eq_zero_of_le h) + +private lemma sub_nat_nat_of_lt {m n : ℕ} (h : m < n) : sub_nat_nat m n = -[1+ pred (n - m)] := +have n - m = succ (pred (n - m)), from eq.symm (succ_pred_eq_of_pos (nat.sub_pos_of_lt h)), +by rewrite sub_nat_nat_of_sub_eq_succ this + /- nat_abs -/ @[simp] def nat_abs : ℤ → ℕ @@ -266,153 +304,244 @@ instance : has_mod ℤ := ⟨int.mod⟩ def gcd (m n : ℤ) : ℕ := gcd (nat_abs m) (nat_abs n) -/-- Relator between integers and pairs of natural numbers -/ - -inductive rel_int_nat_nat : ℤ → ℕ × ℕ → Prop -| pos : ∀{m p}, rel_int_nat_nat (of_nat p) (m + p, m) -| neg : ∀{m n}, rel_int_nat_nat (neg_succ_of_nat n) (m, m + n + 1) - -protected lemma rel_sub_nat_nat {a b : ℕ} : rel_int_nat_nat (sub_nat_nat a b) (a, b) := -sub_nat_nat_elim a b (λa b i, rel_int_nat_nat i (a, b)) - (assume i n, rel_int_nat_nat.pos) (assume i n, rel_int_nat_nat.neg) - -instance right_total_rel_int_nat_nat : relator.right_total rel_int_nat_nat -| (n, m) := ⟨_, int.rel_sub_nat_nat⟩ - -instance left_total_rel_int_nat_nat : relator.left_total rel_int_nat_nat -| (of_nat n) := ⟨(0 + n, 0), rel_int_nat_nat.pos⟩ -| (neg_succ_of_nat n) := ⟨(0, 0 + n + 1), rel_int_nat_nat.neg⟩ - -instance bi_total_rel_int_nat_nat : relator.bi_total rel_int_nat_nat := -⟨int.left_total_rel_int_nat_nat, int.right_total_rel_int_nat_nat⟩ - -protected lemma rel_neg_of_nat {m} : ∀{n}, rel_int_nat_nat (neg_of_nat n) (m, m + n) -| 0 := rel_int_nat_nat.pos -| (nat.succ n) := rel_int_nat_nat.neg - -protected lemma rel_eq : (rel_int_nat_nat ⇒ (rel_int_nat_nat ⇒ iff)) - eq (λa b, a.1 + b.2 = b.1 + a.2) -| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.pos m' p') := - calc of_nat p = of_nat p' - ↔ (m + m') + p = (m + m') + p' : by rw [of_nat_eq_of_nat_iff, add_left_cancel_iff] - ... ↔ (m + p) + m' = (m' + p') + m : by simp -| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.neg m' n') := - calc of_nat p = -[1+ n'] ↔ (m' + m) + (n' + p + 1) = (m' + m) + 0 : - begin rw [add_left_cancel_iff], apply iff.intro; intro; contradiction end - ... ↔ (m + p) + (m' + n' + 1) = m' + m : by simp -| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.pos m' p') := - calc -[1+ n] = of_nat p' ↔ (m + m') + 0 = (m + m') + (n + p' + 1) : - begin rw [add_left_cancel_iff], apply iff.intro; intro; contradiction end - ... ↔ m + m' = m' + p' + (m + n + 1) : by simp -| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.neg m' n') := - calc -[1+ n] = -[1+ n'] ↔ (m + m' + 1) + n' = (m + m' + 1) + n : - by rw [neg_succ_of_nat_inj_iff, add_left_cancel_iff, eq_comm] - ... ↔ m + (m' + n' + 1) = m' + (m + n + 1) : by simp - -/- should this be more general, i.e. ∀{n}, rel_int_nat_nat 0 (n, n) ? -/ -protected lemma rel_zero : rel_int_nat_nat 0 (0, 0) := -rel_int_nat_nat.pos - -protected lemma rel_one : rel_int_nat_nat 1 (1, 0) := -rel_int_nat_nat.pos - -protected lemma rel_neg : (rel_int_nat_nat ⇒ rel_int_nat_nat) has_neg.neg (λa, (a.2, a.1)) -| ._ ._ (@rel_int_nat_nat.pos m p) := int.rel_neg_of_nat -| ._ ._ (@rel_int_nat_nat.neg m n) := rel_int_nat_nat.pos - -protected lemma rel_add : (rel_int_nat_nat ⇒ (rel_int_nat_nat ⇒ rel_int_nat_nat)) - has_add.add (λa b, (a.1 + b.1, a.2 + b.2)) -| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.pos m' p') := - have eq : m + p + (m' + p') = m + m' + (p + p'), - by simp, - show rel_int_nat_nat (of_nat (p + p')) (m + p + (m' + p'), m + m'), - begin rw [eq], apply rel_int_nat_nat.pos end -| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.neg m' n') := - have eq1 : m + p + m' = p + (m + m'), - by simp, - have eq2 : m + (m' + n' + 1) = (n' + 1) + (m + m'), - by simp, - show rel_int_nat_nat (sub_nat_nat p (n' + 1)) (m + p + m', m + (m' + n' + 1)), - begin - rw [eq1, eq2, (sub_nat_nat_add_add _ _ (m + m')).symm], - apply int.rel_sub_nat_nat - end -| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.pos m' p') := - have eq1 : m + (m' + p') = p' + (m + m'), - by simp, - have eq2 : (m + n + 1) + m' = (n + 1) + (m + m'), - by simp, - show rel_int_nat_nat (sub_nat_nat p' (n + 1)) (m + (m' + p'), (m + n + 1) + m'), - begin - rw [eq1, eq2, (sub_nat_nat_add_add _ _ (m + m')).symm], - apply int.rel_sub_nat_nat - end -| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.neg m' n') := - have eq : (m + n + 1) + (m' + n' + 1) = (m + m') + (n + n' + 1) + 1, - by simp, - show rel_int_nat_nat -[1+ (n + n' + 1)] (m + m', (m + n + 1) + (m' + n' + 1)), - begin rw [eq], apply rel_int_nat_nat.neg end - -protected lemma rel_mul : (rel_int_nat_nat ⇒ (rel_int_nat_nat ⇒ rel_int_nat_nat)) - has_mul.mul (λa b, (a.1 * b.1 + a.2 * b.2, a.1 * b.2 + a.2 * b.1)) -| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.pos m' p') := - have e : (m + p) * (m' + p') + m * m' = (m + p) * m' + m * (m' + p') + p * p', - by simp [mul_add, add_mul], - show rel_int_nat_nat (of_nat (p * p')) - ((m + p) * (m' + p') + m * m', (m + p) * m' + m * (m' + p')), - begin rw [e], exact rel_int_nat_nat.pos end -| ._ ._ (@rel_int_nat_nat.pos m p) ._ ._ (@rel_int_nat_nat.neg m' n') := - have e : (m + p) * (m' + n' + 1) + m * m' = (m + p) * m' + m * (m' + n' + 1) + (p * (n' + 1)), - by simp [mul_add, add_mul], - show rel_int_nat_nat (of_nat p * -[1+ n']) - ((m + p) * m' + m * (m' + n' + 1), (m + p) * (m' + n' + 1) + m * m'), - begin rw [e], exact int.rel_neg_of_nat end -| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.pos m' p') := - have e : m * m' + (m + n + 1) * (m' + p') = m * (m' + p') + (m + n + 1) * m' + ((n + 1) * p'), - by simp [mul_add, add_mul], - show rel_int_nat_nat (-[1+ n] * of_nat p') - (m * (m' + p') + (m + n + 1) * m', m * m' + (m + n + 1) * (m' + p')), - begin rw [e], exact int.rel_neg_of_nat end -| ._ ._ (@rel_int_nat_nat.neg m n) ._ ._ (@rel_int_nat_nat.neg m' n') := - have e : m * m' + (m + n + 1) * (m' + n' + 1) = - m * (m' + n' + 1) + (m + n + 1) * m' + ((n + 1) * (n' + 1)), - by simp [mul_add, add_mul], - show rel_int_nat_nat (-[1+ n] * -[1+ n']) - (m * m' + (m + n + 1) * (m' + n' + 1), m * (m' + n' + 1) + (m + n + 1) * m'), - begin rw [e], exact rel_int_nat_nat.pos end - /- int is a ring -/ -protected meta def transfer_core : tactic unit := do - transfer.transfer [`relator.rel_forall_of_total, `relator.rel_not, - `int.rel_eq, `int.rel_zero, `int.rel_one, - `int.rel_add, `int.rel_neg, `int.rel_mul] +/- addition -/ + +protected lemma add_comm : ∀ a b : ℤ, a + b = b + a +| (of_nat n) (of_nat m) := by simp +| (of_nat n) -[1+ m] := rfl +| -[1+ n] (of_nat m) := rfl +| -[1+ n] -[1+m] := by simp + +protected lemma add_zero : ∀ a : ℤ, a + 0 = a +| (of_nat n) := rfl +| -[1+ n] := rfl + +protected lemma zero_add (a : ℤ) : 0 + a = a := +int.add_comm a 0 ▸ int.add_zero a + +private lemma sub_nat_nat_sub {m n : ℕ} (h : m ≥ n) (k : ℕ) : + sub_nat_nat (m - n) k = sub_nat_nat m (k + n) := +calc + sub_nat_nat (m - n) k = sub_nat_nat (m - n + n) (k + n) : by rewrite [sub_nat_nat_add_add] + ... = sub_nat_nat m (k + n) : by rewrite [nat.sub_add_cancel h] + +private lemma sub_nat_nat_add (m n k : ℕ) : sub_nat_nat (m + n) k = of_nat m + sub_nat_nat n k := +begin + have h := le_or_gt k n, + cases h with h' h', + { rw [sub_nat_nat_of_ge h'], + have h₂ : k ≤ m + n, exact (le_trans h' (le_add_left _ _)), + rw [sub_nat_nat_of_ge h₂], simp, + rw nat.add_sub_assoc h' }, + rw [sub_nat_nat_of_lt h'], simp, rw [succ_pred_eq_of_pos (nat.sub_pos_of_lt h')], + transitivity, rw [← nat.sub_add_cancel (le_of_lt h')], + apply sub_nat_nat_add_add +end + +private lemma sub_nat_nat_add_neg_succ_of_nat (m n k : ℕ) : + sub_nat_nat m n + -[1+ k] = sub_nat_nat m (n + succ k) := +begin + have h := le_or_gt n m, + cases h with h' h', + { rw [sub_nat_nat_of_ge h'], simp, rw [sub_nat_nat_sub h', add_comm] }, + have h₂ : m < n + succ k, exact nat.lt_of_lt_of_le h' (le_add_right _ _), + have h₃ : m ≤ n + k, exact le_of_succ_le_succ h₂, + rw [sub_nat_nat_of_lt h', sub_nat_nat_of_lt h₂], simp, + rw [← add_succ, succ_pred_eq_of_pos (nat.sub_pos_of_lt h'), add_succ, succ_sub h₃, pred_succ], + rw [add_comm n, nat.add_sub_assoc (le_of_lt h')] +end + +private lemma add_assoc_aux1 (m n : ℕ) : + ∀ c : ℤ, of_nat m + of_nat n + c = of_nat m + (of_nat n + c) +| (of_nat k) := by simp +| -[1+ k] := by simp [sub_nat_nat_add] + +private lemma add_assoc_aux2 (m n k : ℕ) : + -[1+ m] + -[1+ n] + of_nat k = -[1+ m] + (-[1+ n] + of_nat k) := +begin + simp [add_succ], rw [int.add_comm, sub_nat_nat_add_neg_succ_of_nat], simp [add_succ, succ_add] +end + +protected lemma add_assoc : ∀ a b c : ℤ, a + b + c = a + (b + c) +| (of_nat m) (of_nat n) c := add_assoc_aux1 _ _ _ +| (of_nat m) b (of_nat k) := by rw [int.add_comm, ← add_assoc_aux1, int.add_comm (of_nat k), + add_assoc_aux1, int.add_comm b] +| a (of_nat n) (of_nat k) := by rw [int.add_comm, int.add_comm a, ← add_assoc_aux1, + int.add_comm a, int.add_comm (of_nat k)] +| -[1+ m] -[1+ n] (of_nat k) := add_assoc_aux2 _ _ _ +| -[1+ m] (of_nat n) -[1+ k] := by rw [int.add_comm, ← add_assoc_aux2, int.add_comm (of_nat n), + ← add_assoc_aux2, int.add_comm -[1+ m] ] +| (of_nat m) -[1+ n] -[1+ k] := by rw [int.add_comm, int.add_comm (of_nat m), + int.add_comm (of_nat m), ← add_assoc_aux2, + int.add_comm -[1+ k] ] +| -[1+ m] -[1+ n] -[1+ k] := by simp [add_succ, neg_of_nat_of_succ] + +/- negation -/ + +private lemma sub_nat_self : ∀ n, sub_nat_nat n n = 0 +| 0 := rfl +| (succ m) := begin rw [sub_nat_nat_of_sub_eq_zero, nat.sub_self, of_nat_zero], rw nat.sub_self end + +local attribute [simp] sub_nat_self + +protected lemma add_left_neg : ∀ a : ℤ, -a + a = 0 +| (of_nat 0) := rfl +| (of_nat (succ m)) := by simp +| -[1+ m] := by simp + +/- multiplication -/ + +protected lemma mul_comm : ∀ a b : ℤ, a * b = b * a +| (of_nat m) (of_nat n) := by simp [nat.mul_comm] +| (of_nat m) -[1+ n] := by simp [nat.mul_comm] +| -[1+ m] (of_nat n) := by simp [nat.mul_comm] +| -[1+ m] -[1+ n] := by simp [nat.mul_comm] + +private lemma of_nat_mul_neg_of_nat (m : ℕ) : + ∀ n, of_nat m * neg_of_nat n = neg_of_nat (m * n) +| 0 := rfl +| (succ n) := begin unfold neg_of_nat, simp end + +private lemma neg_of_nat_mul_of_nat (m n : ℕ) : + neg_of_nat m * of_nat n = neg_of_nat (m * n) := +begin rw int.mul_comm, simp [of_nat_mul_neg_of_nat, nat.mul_comm] end + +private lemma neg_succ_of_nat_mul_neg_of_nat (m : ℕ) : + ∀ n, -[1+ m] * neg_of_nat n = of_nat (succ m * n) +| 0 := rfl +| (succ n) := begin unfold neg_of_nat, simp end + +private lemma neg_of_nat_mul_neg_succ_of_nat (m n : ℕ) : + neg_of_nat n * -[1+ m] = of_nat (n * succ m) := +begin rw int.mul_comm, simp [neg_succ_of_nat_mul_neg_of_nat, nat.mul_comm] end + +local attribute [simp] of_nat_mul_neg_of_nat neg_of_nat_mul_of_nat + neg_succ_of_nat_mul_neg_of_nat neg_of_nat_mul_neg_succ_of_nat + +protected lemma mul_assoc : ∀ a b c : ℤ, a * b * c = a * (b * c) +| (of_nat m) (of_nat n) (of_nat k) := by simp [nat.mul_assoc] +| (of_nat m) (of_nat n) -[1+ k] := by simp [nat.mul_assoc] +| (of_nat m) -[1+ n] (of_nat k) := by simp [nat.mul_assoc] +| (of_nat m) -[1+ n] -[1+ k] := by simp [nat.mul_assoc] +| -[1+ m] (of_nat n) (of_nat k) := by simp [nat.mul_assoc] +| -[1+ m] (of_nat n) -[1+ k] := by simp [nat.mul_assoc] +| -[1+ m] -[1+ n] (of_nat k) := by simp [nat.mul_assoc] +| -[1+ m] -[1+ n] -[1+ k] := by simp [nat.mul_assoc] + +protected lemma mul_one : ∀ (a : ℤ), a * 1 = a +| (of_nat m) := show of_nat m * of_nat 1 = of_nat m, by simp +| -[1+ m] := show -[1+ m] * of_nat 1 = -[1+ m], begin simp, reflexivity end + +protected lemma one_mul (a : ℤ) : 1 * a = a := +int.mul_comm a 1 ▸ int.mul_one a + +protected lemma mul_zero : ∀ (a : ℤ), a * 0 = 0 +| (of_nat m) := rfl +| -[1+ m] := rfl + +protected lemma zero_mul (a : ℤ) : 0 * a = 0 := +int.mul_comm a 0 ▸ int.mul_zero a + +private lemma neg_of_nat_eq_sub_nat_nat_zero : ∀ n, neg_of_nat n = sub_nat_nat 0 n +| 0 := rfl +| (succ n) := rfl -protected meta def transfer (distrib := tt) : tactic unit := -if distrib then `[int.transfer_core, simp [add_mul, mul_add]] -else `[int.transfer_core, simp] +private lemma of_nat_mul_sub_nat_nat (m n k : ℕ) : + of_nat m * sub_nat_nat n k = sub_nat_nat (m * n) (m * k) := +begin + have h₀ : m > 0 ∨ 0 = m, + exact lt_or_eq_of_le (zero_le _), + cases h₀ with h₀ h₀, + { have h := nat.lt_or_ge n k, + cases h with h h, + { have h' : m * n < m * k, + exact nat.mul_lt_mul_of_pos_left h h₀, + rw [sub_nat_nat_of_lt h, sub_nat_nat_of_lt h'], + simp, rw [succ_pred_eq_of_pos (nat.sub_pos_of_lt h)], + rw [← neg_of_nat_of_succ, nat.mul_sub_left_distrib], + rw [← succ_pred_eq_of_pos (nat.sub_pos_of_lt h')], reflexivity }, + have h' : m * k ≤ m * n, + exact mul_le_mul_left _ h, + rw [sub_nat_nat_of_ge h, sub_nat_nat_of_ge h'], simp, + rw [nat.mul_sub_left_distrib] + }, + have h₂ : of_nat 0 = 0, exact rfl, + subst h₀, simp [h₂, int.zero_mul] +end -local attribute [simp] mul_assoc mul_comm mul_left_comm +private lemma neg_of_nat_add (m n : ℕ) : + neg_of_nat m + neg_of_nat n = neg_of_nat (m + n) := +begin + cases m, + { cases n, + { simp, reflexivity }, + simp, reflexivity }, + cases n, + { simp, reflexivity }, + simp [nat.succ_add], reflexivity +end + +private lemma neg_succ_of_nat_mul_sub_nat_nat (m n k : ℕ) : + -[1+ m] * sub_nat_nat n k = sub_nat_nat (succ m * k) (succ m * n) := +begin + have h := nat.lt_or_ge n k, + cases h with h h, + { have h' : succ m * n < succ m * k, + exact nat.mul_lt_mul_of_pos_left h (nat.succ_pos m), + rw [sub_nat_nat_of_lt h, sub_nat_nat_of_ge (le_of_lt h')], + simp [succ_pred_eq_of_pos (nat.sub_pos_of_lt h), nat.mul_sub_left_distrib]}, + have h' : n > k ∨ k = n, + exact lt_or_eq_of_le h, + cases h' with h' h', + { have h₁ : succ m * n > succ m * k, + exact nat.mul_lt_mul_of_pos_left h' (nat.succ_pos m), + rw [sub_nat_nat_of_ge h, sub_nat_nat_of_lt h₁], simp [nat.mul_sub_left_distrib, nat.mul_comm], + rw [nat.mul_comm k, nat.mul_comm n, ← succ_pred_eq_of_pos (nat.sub_pos_of_lt h₁), + ← neg_of_nat_of_succ], + reflexivity }, + subst h', simp, reflexivity +end + +local attribute [simp] of_nat_mul_sub_nat_nat neg_of_nat_add neg_succ_of_nat_mul_sub_nat_nat + +protected lemma distrib_left : ∀ a b c : ℤ, a * (b + c) = a * b + a * c +| (of_nat m) (of_nat n) (of_nat k) := by simp [nat.left_distrib] +| (of_nat m) (of_nat n) -[1+ k] := begin simp [neg_of_nat_eq_sub_nat_nat_zero], + rw ← sub_nat_nat_add, reflexivity end +| (of_nat m) -[1+ n] (of_nat k) := begin simp [neg_of_nat_eq_sub_nat_nat_zero], + rw [int.add_comm, ← sub_nat_nat_add], reflexivity end +| (of_nat m) -[1+ n] -[1+ k] := begin simp, rw [← nat.left_distrib, succ_add] end +| -[1+ m] (of_nat n) (of_nat k) := begin simp [mul_comm], rw [← nat.right_distrib, mul_comm] end +| -[1+ m] (of_nat n) -[1+ k] := begin simp [neg_of_nat_eq_sub_nat_nat_zero], + rw [int.add_comm, ← sub_nat_nat_add], reflexivity end +| -[1+ m] -[1+ n] (of_nat k) := begin simp [neg_of_nat_eq_sub_nat_nat_zero], + rw [← sub_nat_nat_add], reflexivity end +| -[1+ m] -[1+ n] -[1+ k] := begin simp, rw [← nat.left_distrib, succ_add] end + +protected lemma distrib_right (a b c : ℤ) : (a + b) * c = a * c + b * c := +begin rw [int.mul_comm, int.distrib_left], simp [int.mul_comm] end instance : comm_ring int := { add := int.add, - add_assoc := by int.transfer, + add_assoc := int.add_assoc, zero := int.zero, - zero_add := by int.transfer, - add_zero := by int.transfer, + zero_add := int.zero_add, + add_zero := int.add_zero, neg := int.neg, - add_left_neg := by int.transfer, - add_comm := by int.transfer, + add_left_neg := int.add_left_neg, + add_comm := int.add_comm, mul := int.mul, - mul_assoc := by int.transfer tt, + mul_assoc := int.mul_assoc, one := int.one, - one_mul := by int.transfer, - mul_one := by int.transfer, - left_distrib := by int.transfer tt, - right_distrib := by int.transfer tt, - mul_comm := by int.transfer} + one_mul := int.one_mul, + mul_one := int.mul_one, + left_distrib := int.distrib_left, + right_distrib := int.distrib_right, + mul_comm := int.mul_comm } /- Extra instances to short-circuit type class resolution -/ instance : has_sub int := by apply_instance @@ -429,8 +558,11 @@ instance : semiring int := by apply_instance instance : ring int := by apply_instance instance : distrib int := by apply_instance +protected lemma zero_ne_one : (0 : int) ≠ 1 := +assume h : 0 = 1, succ_ne_zero _ (int.of_nat_inj h).symm + instance : zero_ne_one_class ℤ := -{ zero := 0, one := 1, zero_ne_one := by int.transfer } +{ zero := 0, one := 1, zero_ne_one := int.zero_ne_one } lemma of_nat_sub {n m : ℕ} (h : m ≤ n) : of_nat (n - m) = of_nat n - of_nat m := show of_nat (n - m) = of_nat n + neg_of_nat m, from match m, h with diff --git a/library/init/data/int/order.lean b/library/init/data/int/order.lean index 115813b37e..b3f566eff3 100644 --- a/library/init/data/int/order.lean +++ b/library/init/data/int/order.lean @@ -193,7 +193,7 @@ instance : decidable_linear_ordered_comm_ring int := lt_iff_le_not_le := @int.lt_iff_le_not_le, add_le_add_left := @int.add_le_add_left, add_lt_add_left := @int.add_lt_add_left, - zero_ne_one := zero_ne_one, + zero_ne_one := int.zero_ne_one, mul_nonneg := @int.mul_nonneg, mul_pos := @int.mul_pos, le_total := int.le_total, diff --git a/library/init/meta/transfer.lean b/library/init/meta/transfer.lean deleted file mode 100644 index 6fb88fe218..0000000000 --- a/library/init/meta/transfer.lean +++ /dev/null @@ -1,187 +0,0 @@ -/- -Copyright (c) 2017 Johannes Hölzl. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Johannes Hölzl (CMU) --/ -prelude -import init.meta.tactic init.meta.match_tactic init.relator init.meta.mk_dec_eq_instance -import init.data.list.instances - -namespace transfer -open tactic expr list monad - -/- Transfer rules are of the shape: - - rel_t : {u} Πx, R t₁ t₂ - -where `u` is a list of universe parameters, `x` is a list of dependent variables, and `R` is a -relation. Then this rule will translate `t₁` (depending on `u` and `x`) into `t₂`. `u` and `x` -will be called parameters. When `R` is a relation on functions lifted from `S` and `R` the variables -bound by `S` are called arguments. `R` is generally constructed using `⇒` (i.e. `relator.lift_fun`). - -As example: - - rel_eq : (R ⇒ R ⇒ iff) eq t - -transfer will match this rule when it sees: - - (@eq α a b) and transfer it to (t a b) - -Here `α` is a parameter and `a` and `b` are arguments. - - -TODO: add trace statements - -TODO: currently the used relation must be fixed by the matched rule or through type class - inference. Maybe we want to replace this by type inference similar to Isabelle's transfer. - --/ - - -private meta structure rel_data := -(in_type : expr) -(out_type : expr) -(relation : expr) - -meta instance has_to_tactic_format_rel_data : has_to_tactic_format rel_data := -⟨λr, do - R ← pp r.relation, - α ← pp r.in_type, - β ← pp r.out_type, - return format!"({R}: rel ({α}) ({β}))" ⟩ - -private meta structure rule_data := -(pr : expr) -(uparams : list name) -- levels not in pat -(params : list (expr × bool)) -- fst : local constant, snd = tt → param appears in pattern -(uargs : list name) -- levels not in pat -(args : list (expr × rel_data)) -- fst : local constant -(pat : pattern) -- `R c` -(output : expr) -- right-hand side `d` of rel equation `R c d` - -meta instance has_to_tactic_format_rule_data : has_to_tactic_format rule_data := -⟨λr, do - pr ← pp r.pr, - up ← pp r.uparams, - mp ← pp r.params, - ua ← pp r.uargs, - ma ← pp r.args, - pat ← pp r.pat.target, - output ← pp r.output, - return format!"{{ ⟨{pat}⟩ pr: {pr} → {output}, {up} {mp} {ua} {ma} }" ⟩ - -private meta def get_lift_fun : expr → tactic (list rel_data × expr) -| e := - do { - guardb (is_constant_of (get_app_fn e) ``relator.lift_fun), - [α, β, γ, δ, R, S] ← return $ get_app_args e, - (ps, r) ← get_lift_fun S, - return (rel_data.mk α β R :: ps, r)} <|> - return ([], e) - -private meta def mark_occurences (e : expr) : list expr → list (expr × bool) -| [] := [] -| (h :: t) := let xs := mark_occurences t in - (h, occurs h e || any xs (λ⟨e, oc⟩, oc && occurs h e)) :: xs - -private meta def analyse_rule (u' : list name) (pr : expr) : tactic rule_data := do - t ← infer_type pr, - (params, app (app r f) g) ← mk_local_pis t, - (arg_rels, R) ← get_lift_fun r, - args ← (enum arg_rels).mmap $ λ⟨n, a⟩, - prod.mk <$> mk_local_def (mk_simple_name ("a_" ++ repr n)) a.in_type <*> pure a, - a_vars ← return $ prod.fst <$> args, - p ← head_beta (app_of_list f a_vars), - p_data ← return $ mark_occurences (app R p) params, - p_vars ← return $ list.map prod.fst (p_data.filter (λx, ↑x.2)), - u ← return $ collect_univ_params (app R p) ∩ u', - pat ← mk_pattern (level.param <$> u) (p_vars ++ a_vars) (app R p) (level.param <$> u) (p_vars ++ a_vars), - return $ rule_data.mk pr (u'.remove_all u) p_data u args pat g - -private meta def analyse_decls : list name → tactic (list rule_data) := -mmap (λn, do - d ← get_decl n, - c ← return d.univ_params.length, - ls ← (repeat () c).mmap (λ_, mk_fresh_name), - analyse_rule ls (const n (ls.map level.param))) - -private meta def split_params_args : list (expr × bool) → list expr → list (expr × option expr) × list expr -| ((lc, tt) :: ps) (e :: es) := let (ps', es') := split_params_args ps es in ((lc, some e) :: ps', es') -| ((lc, ff) :: ps) es := let (ps', es') := split_params_args ps es in ((lc, none) :: ps', es') -| _ es := ([], es) - -private meta def param_substitutions (ctxt : list expr) : - list (expr × option expr) → tactic (list (name × expr) × list expr) -| (((local_const n _ bi t), s) :: ps) := do - (e, m) ← match s with - | (some e) := return (e, []) - | none := - let ctxt' := list.filter (λv, occurs v t) ctxt in - let ty := pis ctxt' t in - if bi = binder_info.inst_implicit then do - guard (bi = binder_info.inst_implicit), - e ← instantiate_mvars ty >>= mk_instance, - return (e, []) - else do - mv ← mk_meta_var ty, - return (app_of_list mv ctxt', [mv]) - end, - sb ← return $ instantiate_local n e, - ps ← return $ prod.map sb ((<$>) sb) <$> ps, - (ms, vs) ← param_substitutions ps, - return ((n, e) :: ms, m ++ vs) -| _ := return ([], []) - -/- input expression a type `R a`, it finds a type `b`, s.t. there is a proof of the type `R a b`. -It return (`a`, pr : `R a b`) -/ -meta def compute_transfer : list rule_data → list expr → expr → tactic (expr × expr × list expr) -| rds ctxt e := do - -- Select matching rule - (i, ps, args, ms, rd) ← first (rds.map (λrd, do - (l, m) ← match_pattern rd.pat e semireducible, - level_map ← rd.uparams.mmap $ λl, prod.mk l <$> mk_meta_univ, - inst_univ ← return $ λe, instantiate_univ_params e (level_map ++ zip rd.uargs l), - (ps, args) ← return $ split_params_args (rd.params.map (prod.map inst_univ id)) m, - (ps, ms) ← param_substitutions ctxt ps, /- this checks type class parameters -/ - return (instantiate_locals ps ∘ inst_univ, ps, args, ms, rd))) <|> - (do trace e, fail "no matching rule"), - - (bs, hs, mss) ← (zip rd.args args).mmap (λ⟨⟨_, d⟩, e⟩, do - -- Argument has function type - (args, r) ← get_lift_fun (i d.relation), - ((a_vars, b_vars), (R_vars, bnds)) ← (enum args).mmap (λ⟨n, arg⟩, do - a ← mk_local_def sformat!"a{n}" arg.in_type, - b ← mk_local_def sformat!"b{n}" arg.out_type, - R ← mk_local_def sformat!"R{n}" (arg.relation a b), - return ((a, b), (R, [a, b, R]))) >>= (return ∘ prod.map unzip unzip ∘ unzip), - rds' ← R_vars.mmap (analyse_rule []), - - -- Transfer argument - a ← return $ i e, - a' ← head_beta (app_of_list a a_vars), - (b, pr, ms) ← compute_transfer (rds ++ rds') (ctxt ++ a_vars) (app r a'), - b' ← head_eta (lambdas b_vars b), - return (b', [a, b', lambdas (list.join bnds) pr], ms)) >>= (return ∘ prod.map id unzip ∘ unzip), - - -- Combine - b ← head_beta (app_of_list (i rd.output) bs), - pr ← return $ app_of_list (i rd.pr) (prod.snd <$> ps ++ list.join hs), - return (b, pr, ms ++ mss.join) - -meta def transfer (ds : list name) : tactic unit := do - rds ← analyse_decls ds, - tgt ← target, - - (guard (¬ tgt.has_meta_var) <|> - fail "Target contains (universe) meta variables. This is not supported by transfer."), - - (new_tgt, pr, ms) ← compute_transfer rds [] ((const `iff [] : expr) tgt), - new_pr ← mk_meta_var new_tgt, - - /- Setup final tactic state -/ - exact ((const `iff.mpr [] : expr) tgt new_tgt pr new_pr), - ms ← ms.mmap (λm, (get_assignment m >> return []) <|> return [m]), - gs ← get_goals, - set_goals (ms.join ++ new_pr :: gs) - -end transfer diff --git a/library/init/relator.lean b/library/init/relator.lean deleted file mode 100644 index b6d67f0429..0000000000 --- a/library/init/relator.lean +++ /dev/null @@ -1,84 +0,0 @@ -/- -Copyright (c) 2017 Johannes Hölzl. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Johannes Hölzl - -Relator for functions, pairs, sums, and lists. --/ - -prelude -import init.core init.data.basic - -namespace relator -universe variables u₁ u₂ v₁ v₂ - -reserve infixr ` ⇒ `:40 - -/- TODO(johoelzl): - * should we introduce relators of datatypes as recursive function or as inductive -predicate? For now we stick to the recursor approach. - * relation lift for datatypes, Π, Σ, set, and subtype types - * proof composition and identity laws - * implement method to derive relators from datatype --/ - -section -variables {α : Type u₁} {β : Type u₂} {γ : Type v₁} {δ : Type v₂} -variables (R : α → β → Prop) (S : γ → δ → Prop) - -def lift_fun (f : α → γ) (g : β → δ) : Prop := -∀{a b}, R a b → S (f a) (g b) - -infixr ⇒ := lift_fun - -end - -section -variables {α : Type u₁} {β : out_param $ Type u₂} (R : out_param $ α → β → Prop) - -@[class] def right_total := ∀b, ∃a, R a b -@[class] def left_total := ∀a, ∃b, R a b -@[class] def bi_total := left_total R ∧ right_total R - -end - -section -variables {α : Type u₁} {β : Type u₂} (R : α → β → Prop) - -@[class] def left_unique := ∀{a b c}, R a b → R c b → a = c -@[class] def right_unique := ∀{a b c}, R a b → R a c → b = c - -lemma rel_forall_of_right_total [t : right_total R] : ((R ⇒ implies) ⇒ implies) (λp, ∀i, p i) (λq, ∀i, q i) := -assume p q Hrel H b, exists.elim (t b) (assume a Rab, Hrel Rab (H _)) - -lemma rel_exists_of_left_total [t : left_total R] : ((R ⇒ implies) ⇒ implies) (λp, ∃i, p i) (λq, ∃i, q i) := -assume p q Hrel ⟨a, pa⟩, let ⟨b, Rab⟩ := t a in ⟨b, Hrel Rab pa⟩ - -lemma rel_forall_of_total [t : bi_total R] : ((R ⇒ iff) ⇒ iff) (λp, ∀i, p i) (λq, ∀i, q i) := -assume p q Hrel, - ⟨assume H b, exists.elim (t.right b) (assume a Rab, (Hrel Rab).mp (H _)), - assume H a, exists.elim (t.left a) (assume b Rab, (Hrel Rab).mpr (H _))⟩ - -lemma rel_exists_of_total [t : bi_total R] : ((R ⇒ iff) ⇒ iff) (λp, ∃i, p i) (λq, ∃i, q i) := -assume p q Hrel, - ⟨assume ⟨a, pa⟩, let ⟨b, Rab⟩ := t.left a in ⟨b, (Hrel Rab).1 pa⟩, - assume ⟨b, qb⟩, let ⟨a, Rab⟩ := t.right b in ⟨a, (Hrel Rab).2 qb⟩⟩ - -lemma left_unique_of_rel_eq {eq' : β → β → Prop} (he : (R ⇒ (R ⇒ iff)) eq eq') : left_unique R -| a b c (ab : R a b) (cb : R c b) := -have eq' b b, - from iff.mp (he ab ab) rfl, -iff.mpr (he ab cb) this - -end - -lemma rel_imp : (iff ⇒ (iff ⇒ iff)) implies implies := -assume p q h r s l, imp_congr h l - -lemma rel_not : (iff ⇒ iff) not not := -assume p q h, not_congr h - -instance bi_total_eq {α : Type u₁} : relator.bi_total (@eq α) := -⟨assume a, ⟨a, rfl⟩, assume a, ⟨a, rfl⟩⟩ - -end relator