max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(frontends/lean): remove calc_proof_elaborator

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-03 17:22:45 -08:00
parent 227b548341
commit 9d0dfb8404
49 changed files with 318 additions and 1717 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
library/algebra/binary.lean
View file

@ -46,23 +46,24 @@ namespace binary
variable H_comm : commutative f
variable H_assoc : associative f
local infixl `*` := f
include H_comm
theorem left_comm : left_commutative f :=
take a b c, calc
a*(b*c) = (a*b)*c : H_assoc
... = (b*a)*c : H_comm
... = b*(a*c) : H_assoc
a*(b*c) = (a*b)*c : eq.symm !H_assoc
... = (b*a)*c : by rewrite (H_comm a b)
... = b*(a*c) : !H_assoc
theorem right_comm : right_commutative f :=
take a b c, calc
(a*b)*c = a*(b*c) : H_assoc
... = a*(c*b) : H_comm
... = (a*c)*b : H_assoc
(a*b)*c = a*(b*c) : !H_assoc
... = a*(c*b) : by rewrite (H_comm b c)
... = (a*c)*b : eq.symm !H_assoc
theorem comm4 (a b c d : A) : a*b*(c*d) = a*c*(b*d) :=
calc
a*b*(c*d) = a*b*c*d : H_assoc
... = a*c*b*d : right_comm H_comm H_assoc
... = a*c*(b*d) : H_assoc
a*b*(c*d) = a*b*c*d : eq.symm !H_assoc
... = a*c*b*d : by rewrite (right_comm H_comm H_assoc a b c)
... = a*c*(b*d) : !H_assoc
end
section
@ -72,8 +73,8 @@ namespace binary
local infixl `*` := f
theorem assoc4helper (a b c d) : (a*b)*(c*d) = a*((b*c)*d) :=
calc
(a*b)*(c*d) = a*(b*(c*d)) : H_assoc
... = a*((b*c)*d) : H_assoc
(a*b)*(c*d) = a*(b*(c*d)) : !H_assoc
... = a*((b*c)*d) : by rewrite (H_assoc b c d)
end
definition right_commutative_comp_right [reducible]

34
library/algebra/field.lean
View file

@ -104,23 +104,23 @@ section division_ring
symm (eq_one_div_of_mul_eq_one this)
theorem division_ring.one_div_neg_eq_neg_one_div (H : a ≠ 0) : 1 / (- a) = - (1 / a) :=
have -1 ≠ 0, from
have -1 ≠ (0:A), from
(suppose -1 = 0, absurd (symm (calc
1 = -(-1) : neg_neg
... = -0 : this
... = (0:A) : neg_zero)) zero_ne_one),
1 = -(-1) : eq.symm !neg_neg
... = -0 : by rewrite this
... = (0:A) : !neg_zero)) zero_ne_one),
calc
1 / (- a) = 1 / ((-1) * a) : neg_eq_neg_one_mul
... = (1 / a) * (1 / (- 1)) : division_ring.one_div_mul_one_div H this
... = (1 / a) * (-1) : one_div_neg_one_eq_neg_one
... = - (1 / a) : mul_neg_one_eq_neg
1 / (- a) = 1 / ((-1) * a) : by rewrite neg_eq_neg_one_mul
... = (1 / a) * (1 / (- 1)) : by rewrite (division_ring.one_div_mul_one_div H this)
... = (1 / a) * (-1) : by rewrite one_div_neg_one_eq_neg_one
... = - (1 / a) : by rewrite mul_neg_one_eq_neg
theorem div_neg_eq_neg_div (b : A) (Ha : a ≠ 0) : b / (- a) = - (b / a) :=
calc
b / (- a) = b * (1 / (- a)) : by rewrite -inv_eq_one_div
... = b * -(1 / a) : division_ring.one_div_neg_eq_neg_one_div Ha
... = -(b * (1 / a)) : neg_mul_eq_mul_neg
... = - (b * a⁻¹) : inv_eq_one_div
... = b * -(1 / a) : by rewrite (division_ring.one_div_neg_eq_neg_one_div Ha)
... = -(b * (1 / a)) : by rewrite neg_mul_eq_mul_neg
... = - (b * a⁻¹) : by rewrite inv_eq_one_div
theorem neg_div (a b : A) : (-b) / a = - (b / a) :=
by rewrite [neg_eq_neg_one_mul, mul_div_assoc, -neg_eq_neg_one_mul]
@ -166,7 +166,7 @@ section division_ring
iff.intro
(suppose a / b = 1, calc
a = a / b * b : by inst_simp
... = 1 * b : this
... = 1 * b : by rewrite this
... = b : by simp)
(suppose a = b, by simp)
@ -208,7 +208,7 @@ section field
have a ≠ 0, from and.left (ne_zero_and_ne_zero_of_mul_ne_zero H),
symm (calc
1 / b = a * ((1 / a) * (1 / b)) : by inst_simp
... = a * (1 / (b * a)) : division_ring.one_div_mul_one_div this Hb
... = a * (1 / (b * a)) : by rewrite (division_ring.one_div_mul_one_div this Hb)
... = a * (a * b)⁻¹ : by inst_simp)
theorem field.div_mul_left (Ha : a ≠ 0) (H : a * b ≠ 0) : b / (a * b) = 1 / a :=
@ -263,7 +263,7 @@ section field
theorem field.one_div_div (Ha : a ≠ 0) (Hb : b ≠ 0) : 1 / (a / b) = b / a :=
have (a / b) * (b / a) = 1, from calc
(a / b) * (b / a) = (a * b) / (b * a) : !field.div_mul_div Hb Ha
... = (a * b) / (a * b) : mul.comm
... = (a * b) / (a * b) : by rewrite mul.comm
... = 1 : div_self (division_ring.mul_ne_zero Ha Hb),
symm (eq_one_div_of_mul_eq_one this)
@ -322,9 +322,9 @@ section discrete_field
theorem one_div_zero : 1 / 0 = (0:A) :=
calc
1 / 0 = 1 * 0⁻¹ : refl
... = 1 * 0 : inv_zero
... = 0 : mul_zero
1 / 0 = 1 * 0⁻¹ : rfl
... = 1 * 0 : by rewrite inv_zero
... = 0 : by rewrite mul_zero
theorem div_zero (a : A) : a / 0 = 0 := by rewrite [div_eq_mul_one_div, one_div_zero, mul_zero]

4
library/algebra/group.lean
View file

@ -508,8 +508,8 @@ section add_group
theorem eq_iff_eq_of_sub_eq_sub {a b c d : A} (H : a - b = c - d) : a = b ↔ c = d :=
calc
a = b ↔ a - b = 0 : eq_iff_sub_eq_zero
... = (c - d = 0) : H
a = b ↔ a - b = 0 : !eq_iff_sub_eq_zero
... = (c - d = 0) : by rewrite H
... ↔ c = d : iff.symm (eq_iff_sub_eq_zero c d)
theorem eq_sub_of_add_eq {a b c : A} (H : a + c = b) : a = b - c :=

80
library/algebra/ordered_field.lean
View file

@ -17,17 +17,17 @@ section linear_ordered_field
-- helpers for following
theorem mul_zero_lt_mul_inv_of_pos (H : 0 < a) : a * 0 < a * (1 / a) :=
calc
a * 0 = 0 : mul_zero
... < 1 : zero_lt_one
... = a * a⁻¹ : mul_inv_cancel (ne.symm (ne_of_lt H))
... = a * (1 / a) : inv_eq_one_div
a * 0 = 0 : by rewrite mul_zero
... < 1 : !zero_lt_one
... = a * a⁻¹ : eq.symm (mul_inv_cancel (ne.symm (ne_of_lt H)))
... = a * (1 / a) : by rewrite inv_eq_one_div
theorem mul_zero_lt_mul_inv_of_neg (H : a < 0) : a * 0 < a * (1 / a) :=
calc
a * 0 = 0 : mul_zero
... < 1 : zero_lt_one
... = a * a⁻¹ : mul_inv_cancel (ne_of_lt H)
... = a * (1 / a) : inv_eq_one_div
a * 0 = 0 : by rewrite mul_zero
... < 1 : !zero_lt_one
... = a * a⁻¹ : eq.symm (mul_inv_cancel (ne_of_lt H))
... = a * (1 / a) : by rewrite inv_eq_one_div
theorem one_div_pos_of_pos (H : 0 < a) : 0 < 1 / a :=
lt_of_mul_lt_mul_left (mul_zero_lt_mul_inv_of_pos H) (le_of_lt H)
@ -47,14 +47,14 @@ section linear_ordered_field
iff.intro
(assume H : 1 ≤ a / b,
calc
b = b : refl
b = b : rfl
... ≤ b * (a / b) : le_mul_of_ge_one_right (le_of_lt Hb) H
... = a : mul_div_cancel' Hb')
(assume H : b ≤ a,
have Hbinv : 1 / b > 0, from one_div_pos_of_pos Hb, calc
1 = b * (1 / b) : mul_one_div_cancel Hb'
1 = b * (1 / b) : eq.symm (mul_one_div_cancel Hb')
... ≤ a * (1 / b) : mul_le_mul_of_nonneg_right H (le_of_lt Hbinv)
... = a / b : div_eq_mul_one_div)
... = a / b : eq.symm !div_eq_mul_one_div)
theorem le_of_one_le_div (Hb : b > 0) (H : 1 ≤ a / b) : b ≤ a :=
(iff.mp (!one_le_div_iff_le Hb)) H
@ -71,9 +71,9 @@ section linear_ordered_field
... = a : mul_div_cancel' Hb')
(assume H : b < a,
have Hbinv : 1 / b > 0, from one_div_pos_of_pos Hb, calc
1 = b * (1 / b) : mul_one_div_cancel Hb'
1 = b * (1 / b) : eq.symm (mul_one_div_cancel Hb')
... < a * (1 / b) : mul_lt_mul_of_pos_right H Hbinv
... = a / b : div_eq_mul_one_div)
... = a / b : eq.symm !div_eq_mul_one_div)
theorem lt_of_one_lt_div (Hb : b > 0) (H : 1 < a / b) : b < a :=
(iff.mp (!one_lt_div_iff_lt Hb)) H
@ -98,7 +98,7 @@ section linear_ordered_field
calc
a = a * c * (1 / c) : !mul_mul_div (ne.symm (ne_of_lt Hc))
... ≤ b * (1 / c) : mul_le_mul_of_nonneg_right H (le_of_lt (one_div_pos_of_pos Hc))
... = b / c : div_eq_mul_one_div
... = b / c : eq.symm !div_eq_mul_one_div
theorem mul_lt_of_lt_div (Hc : 0 < c) (H : a < b / c) : a * c < b :=
!div_mul_cancel (ne.symm (ne_of_lt Hc)) ▸ mul_lt_mul_of_pos_right H Hc
@ -107,7 +107,7 @@ section linear_ordered_field
calc
a = a * c * (1 / c) : !mul_mul_div (ne.symm (ne_of_lt Hc))
... < b * (1 / c) : mul_lt_mul_of_pos_right H (one_div_pos_of_pos Hc)
... = b / c : div_eq_mul_one_div
... = b / c : eq.symm !div_eq_mul_one_div
theorem mul_le_of_div_le_of_neg (Hc : c < 0) (H : b / c ≤ a) : a * c ≤ b :=
!div_mul_cancel (ne_of_lt Hc) ▸ mul_le_mul_of_nonpos_right H (le_of_lt Hc)
@ -116,7 +116,7 @@ section linear_ordered_field
calc
a = a * c * (1 / c) : !mul_mul_div (ne_of_lt Hc)
... ≥ b * (1 / c) : mul_le_mul_of_nonpos_right H (le_of_lt (one_div_neg_of_neg Hc))
... = b / c : div_eq_mul_one_div
... = b / c : eq.symm !div_eq_mul_one_div
theorem mul_lt_of_gt_div_of_neg (Hc : c < 0) (H : a > b / c) : a * c < b :=
!div_mul_cancel (ne_of_lt Hc) ▸ mul_lt_mul_of_neg_right H Hc
@ -125,24 +125,24 @@ section linear_ordered_field
calc
a = a * c * (1 / c) : !mul_mul_div (ne_of_gt Hc)
... > b * (1 / c) : mul_lt_mul_of_pos_right H (one_div_pos_of_pos Hc)
... = b / c : div_eq_mul_one_div
... = b / c : eq.symm !div_eq_mul_one_div
theorem div_lt_of_mul_gt_of_neg (Hc : c < 0) (H : a * c < b) : b / c < a :=
calc
a = a * c * (1 / c) : !mul_mul_div (ne_of_lt Hc)
... > b * (1 / c) : mul_lt_mul_of_neg_right H (one_div_neg_of_neg Hc)
... = b / c : div_eq_mul_one_div
... = b / c : eq.symm !div_eq_mul_one_div
theorem div_le_of_le_mul (Hb : b > 0) (H : a ≤ b * c) : a / b ≤ c :=
calc
a / b = a * (1 / b) : div_eq_mul_one_div
a / b = a * (1 / b) : !div_eq_mul_one_div
... ≤ (b * c) * (1 / b) : mul_le_mul_of_nonneg_right H (le_of_lt (one_div_pos_of_pos Hb))
... = (b * c) / b : div_eq_mul_one_div
... = (b * c) / b : eq.symm !div_eq_mul_one_div
... = c : mul_div_cancel_left (ne.symm (ne_of_lt Hb))
theorem le_mul_of_div_le (Hc : c > 0) (H : a / c ≤ b) : a ≤ b * c :=
calc
a = a / c * c : !div_mul_cancel (ne.symm (ne_of_lt Hc))
a = a / c * c : by rewrite (!div_mul_cancel (ne.symm (ne_of_lt Hc)))
... ≤ b * c : mul_le_mul_of_nonneg_right H (le_of_lt Hc)
-- following these in the isabelle file, there are 8 biconditionals for the above with - signs
@ -151,22 +151,22 @@ section linear_ordered_field
theorem mul_sub_mul_div_mul_neg (Hc : c ≠ 0) (Hd : d ≠ 0) (H : a / c < b / d) :
(a * d - b * c) / (c * d) < 0 :=
have H1 : a / c - b / d < 0, from calc
a / c - b / d < b / d - b / d : sub_lt_sub_right H
... = 0 : sub_self,
a / c - b / d < b / d - b / d : sub_lt_sub_right H _
... = 0 : !sub_self,
calc
0 > a / c - b / d : H1
... = (a * d - c * b) / (c * d) : !div_sub_div Hc Hd
... = (a * d - b * c) / (c * d) : mul.comm
... = (a * d - b * c) / (c * d) : by rewrite (mul.comm b c)
theorem mul_sub_mul_div_mul_nonpos (Hc : c ≠ 0) (Hd : d ≠ 0) (H : a / c ≤ b / d) :
(a * d - b * c) / (c * d) ≤ 0 :=
have H1 : a / c - b / d ≤ 0, from calc
a / c - b / d ≤ b / d - b / d : sub_le_sub_right H
... = 0 : sub_self,
a / c - b / d ≤ b / d - b / d : sub_le_sub_right H _
... = 0 : !sub_self,
calc
0 ≥ a / c - b / d : H1
... = (a * d - c * b) / (c * d) : !div_sub_div Hc Hd
... = (a * d - b * c) / (c * d) : mul.comm
... = (a * d - b * c) / (c * d) : by rewrite (mul.comm b c)
theorem div_lt_div_of_mul_sub_mul_div_neg (Hc : c ≠ 0) (Hd : d ≠ 0)
(H : (a * d - b * c) / (c * d) < 0) : a / c < b / d :=
@ -319,8 +319,8 @@ section linear_ordered_field
theorem two_gt_one : (2:A) > 1 :=
calc (2:A) = 1+1 : one_add_one_eq_two
... > 1+0 : add_lt_add_left zero_lt_one
... = 1 : add_zero
... > 1+0 : add_lt_add_left zero_lt_one _
... = 1 : !add_zero
theorem two_ge_one : (2:A) ≥ 1 :=
le_of_lt two_gt_one
@ -337,7 +337,7 @@ section linear_ordered_field
have Ha : a / (1 + 1) > 0, from div_pos_of_pos_of_pos H (add_pos zero_lt_one zero_lt_one),
calc
a / (1 + 1) < a / (1 + 1) + a / (1 + 1) : lt_add_of_pos_left Ha
... = a : add_halves
... = a : !add_halves
theorem div_mul_le_div_mul_of_div_le_div_pos {e : A} (Hb : b ≠ 0) (Hd : d ≠ 0) (H : a / b ≤ c / d)
(He : e > 0) : a / (b * e) ≤ c / (d * e) :=
@ -352,10 +352,10 @@ section linear_ordered_field
theorem exists_add_lt_and_pos_of_lt (H : b < a) : ∃ c : A, b + c < a ∧ c > 0 :=
exists.intro ((a - b) / (1 + 1))
(and.intro (have H2 : a + a > (b + b) + (a - b), from calc
a + a > b + a : add_lt_add_right H
... = b + a + b - b : add_sub_cancel
... = b + b + a - b : add.right_comm
... = (b + b) + (a - b) : add_sub,
a + a > b + a : add_lt_add_right H _
... = b + a + b - b : by rewrite add_sub_cancel
... = b + b + a - b : by rewrite add.right_comm
... = (b + b) + (a - b) : by rewrite add_sub,
have H3 : (a + a) / 2 > ((b + b) + (a - b)) / 2,
from div_lt_div_of_lt_of_pos H2 two_pos,
by rewrite [one_add_one_eq_two, sub_eq_add_neg, add_self_div_two at H3, -div_add_div_same at H3, add_self_div_two at H3];
@ -416,10 +416,10 @@ section discrete_linear_ordered_field
0 < 1 / a : one_div_pos_of_pos H
... ≤ 1 / b : Hl),
have H' : 1 ≤ a / b, from (calc
1 = a / a : div_self (ne.symm (ne_of_lt H))
... = a * (1 / a) : div_eq_mul_one_div
1 = a / a : eq.symm (div_self (ne.symm (ne_of_lt H)))
... = a * (1 / a) : !div_eq_mul_one_div
... ≤ a * (1 / b) : mul_le_mul_of_nonneg_left Hl (le_of_lt H)
... = a / b : div_eq_mul_one_div
... = a / b : eq.symm !div_eq_mul_one_div
), le_of_one_le_div Hb H'
theorem le_of_one_div_le_one_div_of_neg (H : b < 0) (Hl : 1 / a ≤ 1 / b) : b ≤ a :=
@ -439,10 +439,10 @@ section discrete_linear_ordered_field
0 < 1 / a : one_div_pos_of_pos H
... < 1 / b : Hl),
have H : 1 < a / b, from (calc
1 = a / a : div_self (ne.symm (ne_of_lt H))
... = a * (1 / a) : div_eq_mul_one_div
1 = a / a : eq.symm (div_self (ne.symm (ne_of_lt H)))
... = a * (1 / a) : !div_eq_mul_one_div
... < a * (1 / b) : mul_lt_mul_of_pos_left Hl H
... = a / b : div_eq_mul_one_div),
... = a / b : eq.symm !div_eq_mul_one_div),
lt_of_one_lt_div Hb H
theorem lt_of_one_div_lt_one_div_of_neg (H : b < 0) (Hl : 1 / a < 1 / b) : b < a :=

20
library/algebra/ordered_group.lean
View file

@ -128,7 +128,7 @@ section
have Ha' : a ≤ 0, from
calc
a = a + 0 : by rewrite add_zero
... ≤ a + b : add_le_add_left Hb
... ≤ a + b : add_le_add_left Hb _
... = 0 : Hab,
have Haz : a = 0, from le.antisymm Ha' Ha,
have Hb' : b ≤ 0, from
@ -592,13 +592,13 @@ section
theorem sub_le_self (a : A) {b : A} (H : b ≥ 0) : a - b ≤ a :=
calc
a - b = a + -b : rfl
... ≤ a + 0 : add_le_add_left (neg_nonpos_of_nonneg H)
... ≤ a + 0 : add_le_add_left (neg_nonpos_of_nonneg H) _
... = a : by rewrite add_zero
theorem sub_lt_self (a : A) {b : A} (H : b > 0) : a - b < a :=
calc
a - b = a + -b : rfl
... < a + 0 : add_lt_add_left (neg_neg_of_pos H)
... < a + 0 : add_lt_add_left (neg_neg_of_pos H) _
... = a : by rewrite add_zero
theorem add_le_add_three {a b c d e f : A} (H1 : a ≤ d) (H2 : b ≤ e) (H3 : c ≤ f) :
@ -834,7 +834,7 @@ section
(assume H : a ≤ 0,
calc
0 ≤ -a : neg_nonneg_of_nonpos H
... = abs a : abs_of_nonpos H)
... = abs a : eq.symm (abs_of_nonpos H))
theorem abs_abs (a : A) : abs (abs a) = abs a := abs_of_nonneg !abs_nonneg
@ -878,7 +878,7 @@ section
decidable.by_cases
(assume H3 : b ≥ 0,
calc
abs (a + b) ≤ abs (a + b) : le.refl
abs (a + b) ≤ abs (a + b) : !le.refl
... = a + b : by rewrite (abs_of_nonneg H1)
... = abs a + b : by rewrite (abs_of_nonneg H2)
... = abs a + abs b : by rewrite (abs_of_nonneg H3))
@ -887,8 +887,8 @@ section
calc
abs (a + b) = a + b : by rewrite (abs_of_nonneg H1)
... = abs a + b : by rewrite (abs_of_nonneg H2)
... ≤ abs a + 0 : add_le_add_left H4
... ≤ abs a + -b : add_le_add_left (neg_nonneg_of_nonpos H4)
... ≤ abs a + 0 : add_le_add_left H4 _
... ≤ abs a + -b : add_le_add_left (neg_nonneg_of_nonpos H4) _
... = abs a + abs b : by rewrite (abs_of_nonpos H4))
private lemma aux2 {a b : A} (H1 : a + b ≥ 0) : abs (a + b) ≤ abs a + abs b :=
@ -927,13 +927,13 @@ section
calc
abs a - abs b + abs b = abs a : by rewrite sub_add_cancel
... = abs (a - b + b) : by rewrite sub_add_cancel
... ≤ abs (a - b) + abs b : abs_add_le_abs_add_abs,
... ≤ abs (a - b) + abs b : !abs_add_le_abs_add_abs,
le_of_add_le_add_right H1
theorem abs_sub_le (a b c : A) : abs (a - c) ≤ abs (a - b) + abs (b - c) :=
calc
abs (a - c) = abs (a - b + (b - c)) : by rewrite [*sub_eq_add_neg, add.assoc, neg_add_cancel_left]
... ≤ abs (a - b) + abs (b - c) : abs_add_le_abs_add_abs
abs (a - c) = abs (a - b + (b - c)) : by rewrite [*sub_eq_add_neg, add.assoc, neg_add_cancel_left]
... ≤ abs (a - b) + abs (b - c) : !abs_add_le_abs_add_abs
theorem abs_add_three (a b c : A) : abs (a + b + c) ≤ abs a + abs b + abs c :=
begin

10
library/algebra/ordered_ring.lean
View file

@ -429,9 +429,9 @@ section
have nhc : -c ≥ 0, from neg_nonneg_of_nonpos Hc,
have H2 : -(c * b) < -(c * a), from iff.mpr (neg_lt_neg_iff_lt _ _) H,
have H3 : (-c) * b < (-c) * a, from calc
(-c) * b = - (c * b) : neg_mul_eq_neg_mul
(-c) * b = - (c * b) : by rewrite neg_mul_eq_neg_mul
... < -(c * a) : H2
... = (-c) * a : neg_mul_eq_neg_mul,
... = (-c) * a : by rewrite neg_mul_eq_neg_mul,
lt_of_mul_lt_mul_left H3 nhc
theorem zero_gt_neg_one : -1 < (0:A) :=
@ -440,7 +440,7 @@ section
theorem le_of_mul_le_of_ge_one {a b c : A} (H : a * c ≤ b) (Hb : b ≥ 0) (Hc : c ≥ 1) : a ≤ b :=
have H' : a * c ≤ b * c, from calc
a * c ≤ b : H
... = b * 1 : mul_one
... = b * 1 : by rewrite mul_one
... ≤ b * c : mul_le_mul_of_nonneg_left Hc Hb,
le_of_mul_le_mul_right H' (lt_of_lt_of_le zero_lt_one Hc)
@ -558,7 +558,7 @@ section
calc
sign (-a) = 1 : sign_of_pos (neg_pos_of_neg H1)
... = -(-1) : by rewrite neg_neg
... = -(sign a) : sign_of_neg H1)
... = -(sign a) : by rewrite (sign_of_neg H1))
theorem sign_mul (a b : A) : sign (a * b) = sign a * sign b :=
lt.by_cases
@ -607,7 +607,7 @@ section
lt.by_cases
(assume H1 : 0 < a,
calc
a = abs a : abs_of_pos H1
a = abs a : by rewrite (abs_of_pos H1)
... = 1 * abs a : by rewrite one_mul
... = sign a * abs a : by rewrite (sign_of_pos H1))
(assume H1 : 0 = a,

6
library/algebra/ring.lean
View file

@ -209,12 +209,12 @@ section
theorem mul_sub_left_distrib : a * (b - c) = a * b - a * c :=
calc
a * (b - c) = a * b + a * -c : left_distrib
a * (b - c) = a * b + a * -c : !left_distrib
... = a * b - a * c : by simp
theorem mul_sub_right_distrib : (a - b) * c = a * c - b * c :=
calc
(a - b) * c = a * c + -b * c : right_distrib
(a - b) * c = a * c + -b * c : !right_distrib
... = a * c - b * c : by simp
-- TODO: can calc mode be improved to make this easier?
@ -237,7 +237,7 @@ section
theorem mul_neg_one_eq_neg : a * (-1) = -a :=
have a + a * -1 = 0, from calc
a + a * -1 = a * 1 + a * -1 : by simp
... = a * (1 + -1) : left_distrib
... = a * (1 + -1) : eq.symm !left_distrib
... = 0 : by simp,
symm (neg_eq_of_add_eq_zero this)

6
library/data/list/basic.lean
View file

@ -648,12 +648,12 @@ theorem length_dropn
: ∀ (i : ℕ) (l : list A), length (dropn i l) = length l - i
| 0 l := rfl
| (succ i) [] := calc
length (dropn (succ i) []) = 0 - succ i : nat.zero_sub (succ i)
length (dropn (succ i) []) = 0 - succ i : by rewrite (nat.zero_sub (succ i))
| (succ i) (x::l) := calc
length (dropn (succ i) (x::l))
= length (dropn i l) : rfl
... = length l - i : length_dropn i l
... = succ (length l) - succ i : succ_sub_succ (length l) i
... = succ (length l) - succ i : by rewrite (succ_sub_succ (length l) i)
end dropn
section count
@ -708,7 +708,7 @@ lemma count_gt_zero_of_mem : ∀ {a : A} {l : list A}, a ∈ l → count a l > 0
| a (b::l) h := or.elim h
(suppose a = b, begin subst b, rewrite count_cons_eq, apply zero_lt_succ end)
(suppose a ∈ l, calc
count a (b::l) ≥ count a l : count_cons_ge_count
count a (b::l) ≥ count a l : !count_cons_ge_count
... > 0 : count_gt_zero_of_mem this)
lemma count_eq_zero_of_not_mem {a : A} {l : list A} (h : a ∉ l) : count a l = 0 :=

20
library/data/list/comb.lean
View file

@ -23,7 +23,7 @@ theorem length_replicate : ∀ (i : ℕ) (a : A), length (replicate i a) = i
| 0 a := rfl
| (succ i) a := calc
length (replicate (succ i) a) = length (replicate i a) + 1 : rfl
... = i + 1 : length_replicate
... = i + 1 : by rewrite length_replicate
end replicate
/- map -/
@ -73,7 +73,7 @@ theorem map_ne_nil_of_ne_nil (f : A → B) {l : list A} (H : l ≠ nil) : map f
suppose h₁ : map f l = nil,
have length (map f l) = length l, from !length_map,
have 0 = length l, from calc
0 = length (@nil B) : length_nil
0 = length (@nil B) : by rewrite length_nil
... = length (map f l) : by rewrite h₁
... = length l : this,
have l = nil, from eq_nil_of_length_eq_zero (eq.symm this),
@ -121,9 +121,10 @@ theorem length_map₂ : ∀(f : A → B → C) x y, length (map₂ f x y) = min
| f [] (yh::yr) := rfl
| f (xh::xr) (yh::yr) := calc
length (map₂ f (xh::xr) (yh::yr))
= length (map₂ f xr yr) + 1 : rfl
... = min (length xr) (length yr) + 1 : length_map₂
... = min (length (xh::xr)) (length (yh::yr)) : min_succ_succ
= length (map₂ f xr yr) + 1 : rfl
... = min (length xr) (length yr) + 1 : by rewrite length_map₂
... = min (succ (length xr)) (succ (length yr)) : by rewrite min_succ_succ
... = min (length (xh::xr)) (length (yh::yr)) : rfl
/- filter -/
definition filter (p : A → Prop) [h : decidable_pred p] : list A → list A
@ -371,9 +372,7 @@ theorem length_mapAccumR
length (pr₂ (mapAccumR f (a::x) s))
= length x + 1 : by rewrite -(length_mapAccumR f x s)
... = length (a::x) : rfl
| f [] s := calc
length (pr₂ (mapAccumR f [] s))
= 0 : rfl
| f [] s := calc length (pr₂ (mapAccumR f [] s)) = 0 : by esimp
end mapAccumR
section mapAccumR₂
@ -395,8 +394,9 @@ theorem length_mapAccumR₂
| f (a::x) (b::y) c := calc
length (pr₂ (mapAccumR₂ f (a::x) (b::y) c))
= length (pr₂ (mapAccumR₂ f x y c)) + 1 : rfl
... = min (length x) (length y) + 1 : length_mapAccumR₂ f x y c
... = min (length (a::x)) (length (b::y)) : min_succ_succ
... = min (length x) (length y) + 1 : by rewrite (length_mapAccumR₂ f x y c)
... = min (succ (length x)) (succ (length y)) : by rewrite min_succ_succ
... = min (length (a::x)) (length (b::y)) : rfl
| f (a::x) [] c := rfl
| f [] (b::y) c := rfl
| f [] [] c := rfl

48
library/data/list/perm.lean
View file

@ -108,8 +108,8 @@ list.induction_on l₁
(by rewrite [append_nil_right, append_nil_left])
(λ a t r, calc
a::(t++l₂) ~ a::(l₂++t) : skip a r
... ~ l₂++t++[a] : perm_cons_app
... = l₂++(t++[a]) : append.assoc
... ~ l₂++t++[a] : !perm_cons_app
... = l₂++(t++[a]) : !append.assoc
... ~ l₂++(a::t) : perm_app_right l₂ (perm.symm (perm_cons_app a t)))
theorem length_eq_length_of_perm {l₁ l₂ : list A} : l₁ ~ l₂ → length l₁ = length l₂ :=
@ -154,8 +154,8 @@ take l, perm.symm (perm_rev l)
theorem perm_middle (a : A) (l₁ l₂ : list A) : (a::l₁)++l₂ ~ l₁++(a::l₂) :=
calc
(a::l₁) ++ l₂ = a::(l₁++l₂) : rfl
... ~ l₁++l₂++[a] : perm_cons_app
... = l₁++(l₂++[a]) : append.assoc
... ~ l₁++l₂++[a] : !perm_cons_app
... = l₁++(l₂++[a]) : !append.assoc
... ~ l₁++(a::l₂) : perm_app_right l₁ (perm.symm (perm_cons_app a l₂))
theorem perm_middle_simp [simp] (a : A) (l₁ l₂ : list A) : l₁++(a::l₂) ~ (a::l₁)++l₂ :=
@ -163,9 +163,9 @@ perm.symm !perm_middle
theorem perm_cons_app_cons {l l₁ l₂ : list A} (a : A) : l ~ l₁++l₂ → a::l ~ l₁++(a::l₂) :=
assume p, calc
a::l ~ l++[a] : perm_cons_app
a::l ~ l++[a] : !perm_cons_app
... ~ l₁++l₂++[a] : perm_app_left [a] p
... = l₁++(l₂++[a]) : append.assoc
... = l₁++(l₂++[a]) : !append.assoc
... ~ l₁++(a::l₂) : perm_app_right l₁ (perm.symm (perm_cons_app a l₂))
open decidable
@ -178,7 +178,7 @@ theorem perm_erase [decidable_eq A] {a : A} : ∀ {l : list A}, a ∈ l → l ~
have aint : a ∈ t, from mem_of_ne_of_mem naeqx h,
have aux : t ~ a :: erase a t, from perm_erase aint,
calc x::t ~ x::a::(erase a t) : skip x aux
... ~ a::x::(erase a t) : swap
... ~ a::x::(erase a t) : !swap
... = a::(erase a (x::t)) : by rewrite [!erase_cons_tail naeqx])
theorem erase_perm_erase_of_perm [congr] [decidable_eq A] (a : A) {l₁ l₂ : list A} : l₁ ~ l₂ → erase a l₁ ~ erase a l₂ :=
@ -214,7 +214,7 @@ perm.induction_on p h₁ h₂ (λ x y l, h₃ x y l l !perm.refl !P_refl) h₄
theorem xswap {l₁ l₂ : list A} (x y : A) : l₁ ~ l₂ → x::y::l₁ ~ y::x::l₂ :=
assume p, calc
x::y::l₁ ~ y::x::l₁ : swap
x::y::l₁ ~ y::x::l₁ : !swap
... ~ y::x::l₂ : skip y (skip x p)
theorem perm_map [congr] (f : A → B) {l₁ l₂ : list A} : l₁ ~ l₂ → map f l₁ ~ map f l₂ :=
@ -229,7 +229,7 @@ assume q, qeq.induction_on q
(λ h, !perm.refl)
(λ b t₁ t₂ q₁ r₁, calc
b::t₂ ~ b::a::t₁ : skip b r₁
... ~ a::b::t₁ : swap)
... ~ a::b::t₁ : !swap)
/- permutation is decidable if A has decidable equality -/
section dec
@ -252,7 +252,7 @@ definition decidable_perm_aux : ∀ (n : nat) (l₁ l₂ : list A), length l₁
match decidable_perm_aux n t₁ t₂ len_t₁ this with
| inl p := inl (calc
x::t₁ ~ x::(erase x l₂) : skip x p
... ~ l₂ : perm_erase xinl₂)
... ~ l₂ : perm.symm (perm_erase xinl₂))
| inr np := inr (λ p : x::t₁ ~ l₂,
have erase x (x::t₁) ~ erase x l₂, from erase_perm_erase_of_perm x p,
have t₁ ~ erase x l₂, by rewrite [erase_cons_head at this]; exact this,
@ -340,7 +340,7 @@ perm_induction_on p'
proof calc
s₁ ~ t₂ : s₁_p
... = ts₂₁++(a::s₂₂) : t₂_eq
... ~ (a::ts₂₁)++s₂₂ : !perm_middle
... ~ (a::ts₂₁)++s₂₂ : perm.symm !perm_middle
... = s₂₁ ++ s₂₂ : by rewrite [-x_eq_a, -s₂₁_eq]
... = s₂ : by rewrite C₂₁
qed))
@ -354,7 +354,7 @@ perm_induction_on p'
proof calc
s₁ = a::(ts₁₁++s₁₂) : by rewrite [s₁_eq, x_eq_a]
... ~ ts₁₁++(a::s₁₂) : !perm_middle
... = t₁ : t₁_eq
... = t₁ : eq.symm t₁_eq
... ~ t₂ : p
... = s₂ : by rewrite [t₂_eq, C₂₁, s₂₁_eq, append_nil_left]
qed)
@ -391,7 +391,7 @@ perm_induction_on p'
proof calc
s₁ ~ x::t₂ : s₁_p
... = x::(ts₂₁++(y::s₂₂)) : by rewrite [t₂_eq, -y_eq_a]
... ~ x::y::(ts₂₁++s₂₂) : skip x !perm_middle
... ~ x::y::(ts₂₁++s₂₂) : perm.symm (skip x (perm_middle _ _ _)) -- !perm_middle
... = s₂₁ ++ s₂₂ : by rewrite [s₂₁_eq, append_cons]
... = s₂ : by rewrite C₂₁
qed))
@ -416,8 +416,8 @@ perm_induction_on p'
proof calc
s₁ ~ y::t₂ : s₁_p
... = y::(ts₂₁++(x::s₂₂)) : by rewrite [t₂_eq, -x_eq_a]
... ~ y::x::(ts₂₁++s₂₂) : skip y !perm_middle
... ~ x::y::(ts₂₁++s₂₂) : swap
... ~ y::x::(ts₂₁++s₂₂) : perm.symm (skip y (perm_middle _ _ _))
... ~ x::y::(ts₂₁++s₂₂) : !swap
... = s₂₁ ++ s₂₂ : by rewrite [s₂₁_eq]
... = s₂ : by rewrite C₂₁
qed))
@ -436,9 +436,9 @@ perm_induction_on p'
(λ (s₂₁_eq : s₂₁ = [x]) (y_eq_a : y = a) (t₂_eq : t₂ = s₂₂),
proof calc
s₁ = y::x::(ts₁₁++s₁₂) : by rewrite s₁_eq
... ~ x::y::(ts₁₁++s₁₂) : swap
... ~ x::y::(ts₁₁++s₁₂) : !swap
... = x::a::(ts₁₁++s₁₂) : by rewrite y_eq_a
... ~ x::(ts₁₁++(a::s₁₂)) : skip x !perm_middle
... ~ x::(ts₁₁++(a::s₁₂)) : skip x (perm_middle _ _ _)
... = x::t₁ : by rewrite t₁_eq
... ~ x::t₂ : skip x p
... = s₂₁ ++ s₂₂ : by rewrite [t₂_eq, s₂₁_eq]
@ -451,7 +451,7 @@ perm_induction_on p'
proof calc
s₁ = y::x::(ts₁₁++s₁₂) : by rewrite s₁_eq
... ~ y::x::(ts₂₁++s₂₂) : skip y (skip x p_aux)
... ~ x::y::(ts₂₁++s₂₂) : swap
... ~ x::y::(ts₂₁++s₂₂) : !swap
... = s₂₁ ++ s₂₂ : by rewrite s₂₁_eq
... = s₂ : by rewrite C₂₁
qed)))
@ -471,7 +471,7 @@ assume p, perm_inv_core p (qeq.qhead a l₁) (qeq.qhead a l₂)
theorem perm_app_inv {a : A} {l₁ l₂ l₃ l₄ : list A} : l₁++(a::l₂) ~ l₃++(a::l₄) → l₁++l₂ ~ l₃++l₄ :=
assume p : l₁++(a::l₂) ~ l₃++(a::l₄),
have p' : a::(l₁++l₂) ~ a::(l₃++l₄), from calc
a::(l₁++l₂) ~ l₁++(a::l₂) : perm_middle
a::(l₁++l₂) ~ l₁++(a::l₂) : !perm_middle
... ~ l₃++(a::l₄) : p
... ~ a::(l₃++l₄) : perm.symm (!perm_middle),
perm_cons_inv p'
@ -485,9 +485,9 @@ section foldl
assume p, perm_induction_on p
(λ b, by rewrite *foldl_nil)
(λ x t₁ t₂ p r b, calc
foldl f b (x::t₁) = foldl f (f b x) t₁ : foldl_cons
... = foldl f (f b x) t₂ : r (f b x)
... = foldl f b (x::t₂) : foldl_cons)
foldl f b (x::t₁) = foldl f (f b x) t₁ : !foldl_cons
... = foldl f (f b x) t₂ : by rewrite (r (f b x))
... = foldl f b (x::t₂) : eq.symm !foldl_cons)
(λ x y t₁ t₂ p r b, calc
foldl f b (y :: x :: t₁) = foldl f (f (f b y) x) t₁ : by rewrite foldl_cons
... = foldl f (f (f b x) y) t₁ : by rewrite rcomm
@ -505,9 +505,9 @@ section foldr
assume p, perm_induction_on p
(λ b, by rewrite *foldl_nil)
(λ x t₁ t₂ p r b, calc
foldr f b (x::t₁) = f x (foldr f b t₁) : foldr_cons
foldr f b (x::t₁) = f x (foldr f b t₁) : !foldr_cons
... = f x (foldr f b t₂) : by rewrite [r b]
... = foldr f b (x::t₂) : foldr_cons)
... = foldr f b (x::t₂) : eq.symm !foldr_cons)
(λ x y t₁ t₂ p r b, calc
foldr f b (y :: x :: t₁) = f y (f x (foldr f b t₁)) : by rewrite foldr_cons
... = f x (f y (foldr f b t₁)) : by rewrite lcomm

6
library/data/list/set.lean
View file

@ -466,9 +466,9 @@ theorem upto_ne_nil_of_ne_zero {n : ℕ} (H : n ≠ 0) : upto n ≠ nil :=
suppose upto n = nil,
have upto n = upto 0, from upto_nil ▸ this,
have n = 0, from calc
n = length (upto n) : length_upto
... = length (upto 0) : this
... = 0 : length_upto,
n = length (upto n) : by rewrite length_upto
... = length (upto 0) : by rewrite this
... = 0 : by rewrite length_upto,
H this
theorem upto_less : ∀ n, all (upto n) (λ i, i < n)

6
library/data/list/sort.lean
View file

@ -157,7 +157,7 @@ lemma sort_aux_perm : ∀ {n : nat} {l : list A} (h : length l = n), sort_aux R
have leq : length (erase m l) = n, from sort_aux_lemma R h,
calc m :: sort_aux R n (erase m l) leq
~ m :: erase m l : perm.skip m (sort_aux_perm leq)
... ~ l : perm_erase (min_mem _ _ _)
... ~ l : perm.symm (perm_erase (min_mem _ _ _))
lemma sort_perm (l : list A) : sort R l ~ l :=
sort_aux_perm R rfl
@ -186,9 +186,9 @@ lemma sort_eq_of_perm_core {l₁ l₂ : list A} (to : total R) (tr : transitive
have s₁ : sorted R (sort R l₁), from sorted_of_strongly_sorted (strongly_sorted_sort_core to tr rf l₁),
have s₂ : sorted R (sort R l₂), from sorted_of_strongly_sorted (strongly_sorted_sort_core to tr rf l₂),
have p : sort R l₁ ~ sort R l₂, from calc
sort R l₁ ~ l₁ : sort_perm
sort R l₁ ~ l₁ : !sort_perm
... ~ l₂ : h
... ~ sort R l₂ : sort_perm,
... ~ sort R l₂ : perm.symm !sort_perm,
eq_of_sorted_of_perm tr asy p s₁ s₂
section

6
library/data/nat/basic.lean
View file

@ -21,7 +21,7 @@ nat.induction_on n
rfl
(λ n₁ ih, calc
succ n₁ ⊕ succ m = succ (n₁ ⊕ succ m) : rfl
... = succ (succ (n₁ ⊕ m)) : ih
... = succ (succ (n₁ ⊕ m)) : by rewrite ih
... = succ (succ n₁ ⊕ m) : rfl)
theorem add_eq_addl (x : ℕ) : ∀y, x + y = x ⊕ y :=
@ -40,7 +40,7 @@ nat.induction_on x
(λ y₁ ih₂, calc
succ x₁ + succ y₁ = succ (succ x₁ + y₁) : rfl
... = succ (succ x₁ ⊕ y₁) : by rewrite ih₂
... = succ x₁ ⊕ succ y₁ : addl_succ_right))
... = succ x₁ ⊕ succ y₁ : eq.symm !addl_succ_right))
/- successor and predecessor -/
@ -217,7 +217,7 @@ local attribute nat.mul_assoc [simp]
protected theorem mul_one (n : ℕ) : n * 1 = n :=
calc
n * 1 = n * 0 + n : mul_succ
n * 1 = n * 0 + n : !mul_succ
... = n : by simp
local attribute nat.mul_one [simp]

106
library/data/nat/div.lean
View file

@ -57,7 +57,7 @@ nat.induction_on y
assume IH : (x + y * z) / z = x / z + y, calc
(x + succ y * z) / z = (x + y * z + z) / z : by inst_simp
... = succ ((x + y * z) / z) : !add_div_self H
... = succ (x / z + y) : IH)
... = succ (x / z + y) : by rewrite IH)
theorem add_mul_div_self_left (x z : ℕ) {y : ℕ} (H : y > 0) : (x + y * z) / y = x / y + z :=
!mul.comm ▸ add_mul_div_self H
@ -103,9 +103,9 @@ by_cases_zero_pos z
(by rewrite add_zero)
(take z, assume H : z > 0,
calc
(x + z) % z = if 0 < z ∧ z ≤ x + z then (x + z - z) % z else _ : mod_def
(x + z) % z = if 0 < z ∧ z ≤ x + z then (x + z - z) % z else _ : !mod_def
... = (x + z - z) % z : if_pos (and.intro H (le_add_left z x))
... = x % z : nat.add_sub_cancel)
... = x % z : by rewrite nat.add_sub_cancel)
theorem add_mod_self_left [simp] (x z : ℕ) : (x + z) % x = z % x :=
!add.comm ▸ !add_mod_self
@ -154,9 +154,9 @@ begin
eapply by_cases_zero_pos y,
show x = x / 0 * 0 + x % 0, from
(calc
x / 0 * 0 + x % 0 = 0 + x % 0 : mul_zero
... = x % 0 : zero_add
... = x : mod_zero)⁻¹,
x / 0 * 0 + x % 0 = 0 + x % 0 : by rewrite mul_zero
... = x % 0 : by rewrite zero_add
... = x : by rewrite mod_zero)⁻¹,
intro y H,
show x = x / y * y + x % y,
begin
@ -179,7 +179,7 @@ begin
succ ((succ x - y) / y) * y + succ x % y : by rewrite H3
... = ((succ x - y) / y) * y + y + succ x % y : by rewrite succ_mul
... = ((succ x - y) / y) * y + y + (succ x - y) % y : by rewrite H4
... = ((succ x - y) / y) * y + (succ x - y) % y + y : add.right_comm
... = ((succ x - y) / y) * y + (succ x - y) % y + y : by rewrite add.right_comm
... = succ x - y + y : by rewrite -(IH _ H6)
... = succ x : nat.sub_add_cancel H2)⁻¹
end
@ -228,9 +228,9 @@ theorem mod_le {x y : ℕ} : x % y ≤ x :=
theorem eq_remainder {q1 r1 q2 r2 y : ℕ} (H1 : r1 < y) (H2 : r2 < y)
(H3 : q1 * y + r1 = q2 * y + r2) : r1 = r2 :=
calc
r1 = r1 % y : mod_eq_of_lt H1
r1 = r1 % y : eq.symm (mod_eq_of_lt H1)
... = (r1 + q1 * y) % y : !add_mul_mod_self⁻¹
... = (q1 * y + r1) % y : add.comm
... = (q1 * y + r1) % y : by rewrite add.comm
... = (r2 + q2 * y) % y : by rewrite [H3, add.comm]
... = r2 % y : !add_mul_mod_self
... = r2 : mod_eq_of_lt H2
@ -253,10 +253,10 @@ else
have H2 : z * (x % y) < z * y, from mul_lt_mul_of_pos_left (!mod_lt ypos) zpos,
eq_quotient H1 H2
(calc
((z * x) / (z * y)) * (z * y) + (z * x) % (z * y) = z * x : eq_div_mul_add_mod
... = z * (x / y * y + x % y) : eq_div_mul_add_mod
... = z * (x / y * y) + z * (x % y) : left_distrib
... = (x / y) * (z * y) + z * (x % y) : mul.left_comm)
((z * x) / (z * y)) * (z * y) + (z * x) % (z * y) = z * x : by rewrite -eq_div_mul_add_mod
... = z * (x / y * y + x % y) : by rewrite -eq_div_mul_add_mod
... = z * (x / y * y) + z * (x % y) : !left_distrib
... = (x / y) * (z * y) + z * (x % y) : by rewrite mul.left_comm)
protected theorem mul_div_mul_right {x z y : ℕ} (zpos : z > 0) : (x * z) / (y * z) = x / y :=
!mul.comm ▸ !mul.comm ▸ !nat.mul_div_mul_left zpos
@ -264,9 +264,9 @@ protected theorem mul_div_mul_right {x z y : ℕ} (zpos : z > 0) : (x * z) / (y
theorem mul_mod_mul_left (z x y : ℕ) : (z * x) % (z * y) = z * (x % y) :=
or.elim (eq_zero_or_pos z)
(assume H : z = 0, H⁻¹ ▸ calc
(0 * x) % (z * y) = 0 % (z * y) : zero_mul
... = 0 : zero_mod
... = 0 * (x % y) : zero_mul)
(0 * x) % (z * y) = 0 % (z * y) : by rewrite zero_mul
... = 0 : by rewrite zero_mod
... = 0 * (x % y) : by rewrite zero_mul)
(assume zpos : z > 0,
or.elim (eq_zero_or_pos y)
(assume H : y = 0, by rewrite [H, mul_zero, *mod_zero])
@ -276,10 +276,10 @@ or.elim (eq_zero_or_pos z)
have H2 : z * (x % y) < z * y, from mul_lt_mul_of_pos_left (!mod_lt ypos) zpos,
eq_remainder H1 H2
(calc
((z * x) / (z * y)) * (z * y) + (z * x) % (z * y) = z * x : eq_div_mul_add_mod
... = z * (x / y * y + x % y) : eq_div_mul_add_mod
... = z * (x / y * y) + z * (x % y) : left_distrib
... = (x / y) * (z * y) + z * (x % y) : mul.left_comm)))
((z * x) / (z * y)) * (z * y) + (z * x) % (z * y) = z * x : by rewrite -eq_div_mul_add_mod
... = z * (x / y * y + x % y) : by rewrite -eq_div_mul_add_mod
... = z * (x / y * y) + z * (x % y) : by rewrite left_distrib
... = (x / y) * (z * y) + z * (x % y) : by rewrite mul.left_comm)))
theorem mul_mod_mul_right (x z y : ℕ) : (x * z) % (y * z) = (x % y) * z :=
mul.comm z x ▸ mul.comm z y ▸ !mul.comm ▸ !mul_mod_mul_left
@ -290,7 +290,7 @@ nat.cases_on n (by rewrite zero_mod)
theorem mul_mod_eq_mod_mul_mod (m n k : nat) : (m * n) % k = ((m % k) * n) % k :=
calc
(m * n) % k = (((m / k) * k + m % k) * n) % k : eq_div_mul_add_mod
(m * n) % k = (((m / k) * k + m % k) * n) % k : by rewrite -eq_div_mul_add_mod
... = ((m % k) * n) % k :
by rewrite [right_distrib, mul.right_comm, add.comm, add_mul_mod_self]
@ -335,10 +335,10 @@ theorem dvd_of_dvd_add_left {m n₁ n₂ : ℕ} (H₁ : m ∣ n₁ + n₂) (H₂
obtain (c₁ : nat) (Hc₁ : n₁ + n₂ = m * c₁), from H₁,
obtain (c₂ : nat) (Hc₂ : n₁ = m * c₂), from H₂,
have aux : m * (c₁ - c₂) = n₂, from calc
m * (c₁ - c₂) = m * c₁ - m * c₂ : nat.mul_sub_left_distrib
... = n₁ + n₂ - m * c₂ : Hc₁
... = n₁ + n₂ - n₁ : Hc₂
... = n₂ : nat.add_sub_cancel_left,
m * (c₁ - c₂) = m * c₁ - m * c₂ : !nat.mul_sub_left_distrib
... = n₁ + n₂ - m * c₂ : by rewrite Hc₁
... = n₁ + n₂ - n₁ : by rewrite Hc₂
... = n₂ : !nat.add_sub_cancel_left,
dvd.intro aux
theorem dvd_of_dvd_add_right {m n₁ n₂ : ℕ} (H : m ∣ n₁ + n₂) : m ∣ n₂ → m ∣ n₁ :=
@ -371,16 +371,16 @@ protected theorem mul_div_assoc (m : ℕ) {n k : ℕ} (H : k ∣ n) : m * n / k
or.elim (eq_zero_or_pos k)
(assume H1 : k = 0,
calc
m * n / k = m * n / 0 : H1
... = 0 : nat.div_zero
m * n / k = m * n / 0 : by rewrite H1
... = 0 : by rewrite nat.div_zero
... = m * 0 : mul_zero m
... = m * (n / 0) : nat.div_zero
... = m * (n / k) : H1)
... = m * (n / 0) : by rewrite nat.div_zero
... = m * (n / k) : by rewrite H1)
(assume H1 : k > 0,
have H2 : n = n / k * k, from (nat.div_mul_cancel H)⁻¹,
calc
m * n / k = m * (n / k * k) / k : H2
... = m * (n / k) * k / k : mul.assoc
m * n / k = m * (n / k * k) / k : by rewrite -H2
... = m * (n / k) * k / k : by rewrite mul.assoc
... = m * (n / k) : nat.mul_div_cancel _ H1)
theorem dvd_of_mul_dvd_mul_left {m n k : ℕ} (kpos : k > 0) (H : k * m ∣ k * n) : m ∣ n :=
@ -419,14 +419,14 @@ protected theorem div_eq_iff_eq_mul_left {m n : ℕ} (k : ℕ) (H : n > 0) (H' :
protected theorem eq_mul_of_div_eq_right {m n k : ℕ} (H1 : n ∣ m) (H2 : m / n = k) :
m = n * k :=
calc
m = n * (m / n) : nat.mul_div_cancel' H1
... = n * k : H2
m = n * (m / n) : by rewrite (nat.mul_div_cancel' H1)
... = n * k : by rewrite H2
protected theorem div_eq_of_eq_mul_right {m n k : ℕ} (H1 : n > 0) (H2 : m = n * k) :
m / n = k :=
calc
m / n = n * k / n : H2
... = k : !nat.mul_div_cancel_left H1
m / n = n * k / n : by rewrite -H2
... = k : by rewrite (!nat.mul_div_cancel_left H1)
protected theorem eq_mul_of_div_eq_left {m n k : ℕ} (H1 : n ∣ m) (H2 : m / n = k) :
m = k * n :=
@ -460,42 +460,42 @@ by_contradiction
theorem div_mul_le (m n : ℕ) : m / n * n ≤ m :=
calc
m = m / n * n + m % n : eq_div_mul_add_mod
... ≥ m / n * n : le_add_right
m = m / n * n + m % n : by rewrite -eq_div_mul_add_mod
... ≥ m / n * n : !le_add_right
protected theorem div_le_of_le_mul {m n k : ℕ} (H : m ≤ n * k) : m / k ≤ n :=
or.elim (eq_zero_or_pos k)
(assume H1 : k = 0,
calc
m / k = m / 0 : H1
... = 0 : nat.div_zero
... ≤ n : zero_le)
m / k = m / 0 : by rewrite H1
... = 0 : by rewrite nat.div_zero
... ≤ n : !zero_le)
(assume H1 : k > 0,
le_of_mul_le_mul_right (calc
m / k * k ≤ m / k * k + m % k : le_add_right
... = m : eq_div_mul_add_mod
m / k * k ≤ m / k * k + m % k : !le_add_right
... = m : by rewrite -eq_div_mul_add_mod
... ≤ n * k : H) H1)
protected theorem div_le_self (m n : ℕ) : m / n ≤ m :=
nat.cases_on n (!nat.div_zero⁻¹ ▸ !zero_le)
take n,
have H : m ≤ m * succ n, from calc
m = m * 1 : mul_one
m = m * 1 : by rewrite mul_one
... ≤ m * succ n : !mul_le_mul_left (succ_le_succ !zero_le),
nat.div_le_of_le_mul H
protected theorem mul_le_of_le_div {m n k : ℕ} (H : m ≤ n / k) : m * k ≤ n :=
calc
m * k ≤ n / k * k : !mul_le_mul_right H
... ≤ n : div_mul_le
... ≤ n : !div_mul_le
protected theorem le_div_of_mul_le {m n k : ℕ} (H1 : k > 0) (H2 : m * k ≤ n) : m ≤ n / k :=
have H3 : m * k < (succ (n / k)) * k, from
calc
m * k ≤ n : H2
... = n / k * k + n % k : eq_div_mul_add_mod
... < n / k * k + k : add_lt_add_left (!mod_lt H1)
... = (succ (n / k)) * k : succ_mul,
... = n / k * k + n % k : by rewrite -eq_div_mul_add_mod
... < n / k * k + k : add_lt_add_left (!mod_lt H1) _
... = (succ (n / k)) * k : by rewrite succ_mul,
le_of_lt_succ (lt_of_mul_lt_mul_right H3)
protected theorem le_div_iff_mul_le {m n k : ℕ} (H : k > 0) : m ≤ n / k ↔ m * k ≤ n :=
@ -508,16 +508,16 @@ by_cases_zero_pos k
protected theorem div_lt_of_lt_mul {m n k : ℕ} (H : m < n * k) : m / k < n :=
lt_of_mul_lt_mul_right (calc
m / k * k ≤ m / k * k + m % k : le_add_right
... = m : eq_div_mul_add_mod
m / k * k ≤ m / k * k + m % k : !le_add_right
... = m : by rewrite -eq_div_mul_add_mod
... < n * k : H)
protected theorem lt_mul_of_div_lt {m n k : ℕ} (H1 : k > 0) (H2 : m / k < n) : m < n * k :=
have H3 : succ (m / k) * k ≤ n * k, from !mul_le_mul_right (succ_le_of_lt H2),
have H4 : m / k * k + k ≤ n * k, by rewrite [succ_mul at H3]; apply H3,
calc
m = m / k * k + m % k : eq_div_mul_add_mod
... < m / k * k + k : add_lt_add_left (!mod_lt H1)
m = m / k * k + m % k : by rewrite -eq_div_mul_add_mod
... < m / k * k + k : add_lt_add_left (!mod_lt H1) _
... ≤ n * k : H4
protected theorem div_lt_iff_lt_mul {m n k : ℕ} (H : k > 0) : m / k < n ↔ m < n * k :=
@ -538,14 +538,14 @@ begin
have H1 : k / m < n, from nat.div_lt_of_lt_mul (!mul.comm ▸ H),
have H2 : n - k / m ≥ 1, from
nat.le_sub_of_add_le (calc
1 + k / m = succ (k / m) : add.comm
1 + k / m = succ (k / m) : by rewrite add.comm
... ≤ n : succ_le_of_lt H1),
have H3 : n - k / m = n - k / m - 1 + 1, from (nat.sub_add_cancel H2)⁻¹,
have H4 : m > 0, from pos_of_ne_zero (assume H': m = 0, not_lt_zero k (begin rewrite [H' at H, zero_mul at H], exact H end)),
have H5 : k % m + 1 ≤ m, from succ_le_of_lt (!mod_lt H4),
have H6 : m - (k % m + 1) < m, from nat.sub_lt_self H4 !succ_pos,
calc
(m * n - (k + 1)) / m = (m * n - (k / m * m + k % m + 1)) / m : eq_div_mul_add_mod
(m * n - (k + 1)) / m = (m * n - (k / m * m + k % m + 1)) / m : by rewrite -eq_div_mul_add_mod
... = (m * n - k / m * m - (k % m + 1)) / m : by rewrite [*nat.sub_sub]
... = ((n - k / m) * m - (k % m + 1)) / m :
by rewrite [mul.comm m, nat.mul_sub_right_distrib]

10
library/data/nat/examples/partial_sum.lean
View file

@ -19,11 +19,11 @@ rfl
lemma two_mul_partial_sum_eq : ∀ n, 2 * partial_sum n = (succ n) * n
| 0 := by reflexivity
| (succ n) := calc
2 * (succ n + partial_sum n) = 2 * succ n + 2 * partial_sum n : left_distrib
... = 2 * succ n + succ n * n : two_mul_partial_sum_eq
... = 2 * succ n + n * succ n : mul.comm
... = (2 + n) * succ n : right_distrib
... = (n + 2) * succ n : add.comm
2 * (succ n + partial_sum n) = 2 * succ n + 2 * partial_sum n : by rewrite left_distrib
... = 2 * succ n + succ n * n : by rewrite two_mul_partial_sum_eq
... = 2 * succ n + n * succ n : by rewrite (mul.comm n (succ n))
... = (2 + n) * succ n : by rewrite right_distrib
... = (n + 2) * succ n : by rewrite add.comm
... = (succ (succ n)) * succ n : rfl
theorem partial_sum_eq : ∀ n, partial_sum n = ((n + 1) * n) / 2 :=

66
library/data/nat/gcd.lean
View file

@ -34,8 +34,8 @@ theorem gcd_succ [simp] (x y : nat) : gcd x (succ y) = gcd (succ y) (x % succ y)
well_founded.fix_eq gcd.F (x, succ y)
theorem gcd_one_right (n : ℕ) : gcd n 1 = 1 :=
calc gcd n 1 = gcd 1 (n % 1) : gcd_succ
... = gcd 1 0 : mod_one
calc gcd n 1 = gcd 1 (n % 1) : !gcd_succ
... = gcd 1 0 : by rewrite mod_one
theorem gcd_def (x : ℕ) : Π (y : ℕ), gcd x y = if y = 0 then x else gcd y (x % y)
| 0 := !gcd_zero_right
@ -45,14 +45,14 @@ theorem gcd_def (x : ℕ) : Π (y : ℕ), gcd x y = if y = 0 then x else gcd y (
theorem gcd_self : Π (n : ℕ), gcd n n = n
| 0 := rfl
| (succ n₁) := calc
gcd (succ n₁) (succ n₁) = gcd (succ n₁) (succ n₁ % succ n₁) : gcd_succ
... = gcd (succ n₁) 0 : mod_self
gcd (succ n₁) (succ n₁) = gcd (succ n₁) (succ n₁ % succ n₁) : !gcd_succ
... = gcd (succ n₁) 0 : by rewrite mod_self
theorem gcd_zero_left : Π (n : ℕ), gcd 0 n = n
| 0 := rfl
| (succ n₁) := calc
gcd 0 (succ n₁) = gcd (succ n₁) (0 % succ n₁) : gcd_succ
... = gcd (succ n₁) 0 : zero_mod
gcd 0 (succ n₁) = gcd (succ n₁) (0 % succ n₁) : !gcd_succ
... = gcd (succ n₁) 0 : by rewrite zero_mod
theorem gcd_of_pos (m : ℕ) {n : ℕ} (H : n > 0) : gcd m n = gcd n (m % n) :=
gcd_def m n ⬝ if_neg (ne_zero_of_pos H)
@ -60,8 +60,8 @@ gcd_def m n ⬝ if_neg (ne_zero_of_pos H)
theorem gcd_rec (m n : ℕ) : gcd m n = gcd n (m % n) :=
by_cases_zero_pos n
(calc
m = gcd 0 m : gcd_zero_left
... = gcd 0 (m % 0) : mod_zero)
m = gcd 0 m : by rewrite gcd_zero_left
... = gcd 0 (m % 0) : by rewrite mod_zero)
(take n, assume H : 0 < n, gcd_of_pos m H)
theorem gcd.induction {P : ℕ → ℕ → Prop}
@ -115,22 +115,22 @@ theorem gcd_one_left (m : ℕ) : gcd 1 m = 1 :=
theorem gcd_mul_left (m n k : ℕ) : gcd (m * n) (m * k) = m * gcd n k :=
gcd.induction n k
(take n, calc gcd (m * n) (m * 0) = gcd (m * n) 0 : mul_zero)
(take n, calc gcd (m * n) (m * 0) = gcd (m * n) 0 : by rewrite mul_zero)
(take n k,
assume H : 0 < k,
assume IH : gcd (m * k) (m * (n % k)) = m * gcd k (n % k),
calc
gcd (m * n) (m * k) = gcd (m * k) (m * n % (m * k)) : !gcd_rec
... = gcd (m * k) (m * (n % k)) : mul_mod_mul_left
... = m * gcd k (n % k) : IH
... = m * gcd n k : !gcd_rec)
... = gcd (m * k) (m * (n % k)) : by rewrite mul_mod_mul_left
... = m * gcd k (n % k) : by rewrite IH
... = m * gcd n k : by rewrite -gcd_rec)
theorem gcd_mul_right (m n k : ℕ) : gcd (m * n) (k * n) = gcd m k * n :=
calc
gcd (m * n) (k * n) = gcd (n * m) (k * n) : mul.comm
... = gcd (n * m) (n * k) : mul.comm
... = n * gcd m k : gcd_mul_left
... = gcd m k * n : mul.comm
gcd (m * n) (k * n) = gcd (n * m) (k * n) : by rewrite (mul.comm m n)
... = gcd (n * m) (n * k) : by rewrite (mul.comm n k)
... = n * gcd m k : by rewrite gcd_mul_left
... = gcd m k * n : by rewrite mul.comm
theorem gcd_pos_of_pos_left {m : ℕ} (n : ℕ) (mpos : m > 0) : gcd m n > 0 :=
pos_of_dvd_of_pos !gcd_dvd_left mpos
@ -151,9 +151,9 @@ theorem gcd_div {m n k : ℕ} (H1 : k ∣ m) (H2 : k ∣ n) :
or.elim (eq_zero_or_pos k)
(assume H3 : k = 0, by subst k; rewrite *nat.div_zero)
(assume H3 : k > 0, (nat.div_eq_of_eq_mul_left H3 (calc
gcd m n = gcd m (n / k * k) : nat.div_mul_cancel H2
... = gcd (m / k * k) (n / k * k) : nat.div_mul_cancel H1
... = gcd (m / k) (n / k) * k : gcd_mul_right))⁻¹)
gcd m n = gcd m (n / k * k) : by rewrite (nat.div_mul_cancel H2)
... = gcd (m / k * k) (n / k * k) : by rewrite (nat.div_mul_cancel H1)
... = gcd (m / k) (n / k) * k : by rewrite gcd_mul_right))⁻¹)
theorem gcd_dvd_gcd_mul_left (m n k : ℕ) : gcd m n ∣ gcd (k * m) n :=
dvd_gcd (dvd.trans !gcd_dvd_left !dvd_mul_left) !gcd_dvd_right
@ -174,24 +174,24 @@ definition lcm (m n : ℕ) : ℕ := m * n / (gcd m n)
theorem lcm.comm (m n : ℕ) : lcm m n = lcm n m :=
calc
lcm m n = m * n / gcd m n : rfl
... = n * m / gcd m n : mul.comm
... = n * m / gcd n m : gcd.comm
... = n * m / gcd m n : by rewrite mul.comm
... = n * m / gcd n m : by rewrite gcd.comm
... = lcm n m : rfl
theorem lcm_zero_left (m : ℕ) : lcm 0 m = 0 :=
calc
lcm 0 m = 0 * m / gcd 0 m : rfl
... = 0 / gcd 0 m : zero_mul
... = 0 : nat.zero_div
... = 0 / gcd 0 m : by rewrite zero_mul
... = 0 : by rewrite nat.zero_div
theorem lcm_zero_right (m : ℕ) : lcm m 0 = 0 := !lcm.comm ▸ !lcm_zero_left
theorem lcm_one_left (m : ℕ) : lcm 1 m = m :=
calc
lcm 1 m = 1 * m / gcd 1 m : rfl
... = m / gcd 1 m : one_mul
... = m / 1 : gcd_one_left
... = m : nat.div_one
... = m / gcd 1 m : by rewrite one_mul
... = m / 1 : by rewrite gcd_one_left
... = m : by rewrite nat.div_one
theorem lcm_one_right (m : ℕ) : lcm m 1 = m := !lcm.comm ▸ !lcm_one_left
@ -200,8 +200,8 @@ have H : m * m / m = m, from
by_cases_zero_pos m !nat.div_zero (take m, assume H1 : m > 0, !nat.mul_div_cancel H1),
calc
lcm m m = m * m / gcd m m : rfl
... = m * m / m : gcd_self
... = m : H
... = m * m / m : by rewrite gcd_self
... = m : H
theorem dvd_lcm_left (m n : ℕ) : m ∣ lcm m n :=
have H : lcm m n = m * (n / gcd m n), from nat.mul_div_assoc _ !gcd_dvd_right,
@ -265,9 +265,9 @@ theorem coprime_swap {m n : ℕ} (H : coprime n m) : coprime m n :=
theorem dvd_of_coprime_of_dvd_mul_right {m n k : ℕ} (H1 : coprime k n) (H2 : k ∣ m * n) : k ∣ m :=
have H3 : gcd (m * k) (m * n) = m, from
calc
gcd (m * k) (m * n) = m * gcd k n : gcd_mul_left
... = m * 1 : H1
... = m : mul_one,
gcd (m * k) (m * n) = m * gcd k n : by rewrite gcd_mul_left
... = m * 1 : begin unfold coprime at H1, rewrite H1 end
... = m : by rewrite mul_one,
have H4 : (k ∣ gcd (m * k) (m * n)), from dvd_gcd !dvd_mul_left H2,
H3 ▸ H4
@ -359,9 +359,9 @@ or.elim (eq_zero_or_pos (gcd k m))
have H3 : k / gcd k m ∣ (m * n) / gcd k m, from nat.div_dvd_div H2 H,
have H4 : (m * n) / gcd k m = (m / gcd k m) * n, from
calc
m * n / gcd k m = n * m / gcd k m : mul.comm
m * n / gcd k m = n * m / gcd k m : by rewrite mul.comm
... = n * (m / gcd k m) : !nat.mul_div_assoc !gcd_dvd_right
... = m / gcd k m * n : mul.comm,
... = m / gcd k m * n : by rewrite mul.comm,
have H5 : k / gcd k m ∣ (m / gcd k m) * n, from H4 ▸ H3,
have H6 : coprime (k / gcd k m) (m / gcd k m), from coprime_div_gcd_div_gcd H1,
have H7 : k / gcd k m ∣ n, from dvd_of_coprime_of_dvd_mul_left H6 H5,

6
library/data/nat/sqrt.lean
View file

@ -78,8 +78,8 @@ private theorem lt_squared : ∀ {n : nat}, n > 1 → n < n * n
by rewrite [mul_one at this]; exact this
theorem sqrt_le (n : nat) : sqrt n ≤ n :=
calc sqrt n ≤ sqrt n * sqrt n : le_squared
... ≤ n : sqrt_lower
calc sqrt n ≤ sqrt n * sqrt n : !le_squared
... ≤ n : !sqrt_lower
theorem eq_zero_of_sqrt_eq_zero {n : nat} : sqrt n = 0 → n = 0 :=
suppose sqrt n = 0,
@ -110,7 +110,7 @@ theorem sqrt_lt : ∀ {n : nat}, n > 1 → sqrt n < n
have n + 4 = 0, from eq_zero_of_sqrt_eq_zero this,
absurd this dec_trivial)),
calc sqrt (n+4) < sqrt (n+4) * sqrt (n+4) : lt_squared this
... ≤ n+4 : sqrt_lower
... ≤ n+4 : !sqrt_lower
theorem sqrt_pos_of_pos {n : nat} : n > 0 → sqrt n > 0 :=
suppose n > 0,

74
library/data/nat/sub.lean
View file

@ -96,9 +96,9 @@ sub_induction n m
assume IH : k ≤ l → succ l - k = succ (l - k),
take H : succ k ≤ succ l,
calc
succ (succ l) - succ k = succ l - k : succ_sub_succ
succ (succ l) - succ k = succ l - k : !succ_sub_succ
... = succ (l - k) : IH (le_of_succ_le_succ H)
... = succ (succ l - succ k) : succ_sub_succ)
... = succ (succ l - succ k) : by rewrite succ_sub_succ)
theorem sub_eq_zero_of_le {n m : ℕ} (H : n ≤ m) : n - m = 0 :=
obtain (k : ℕ) (Hk : n + k = m), from le.elim H, Hk ▸ !sub_self_add
@ -108,21 +108,21 @@ sub_induction n m
(take k,
assume H : 0 ≤ k,
calc
0 + (k - 0) = k - 0 : zero_add
... = k : nat.sub_zero)
0 + (k - 0) = k - 0 : by rewrite zero_add
... = k : by rewrite nat.sub_zero)
(take k, assume H : succ k ≤ 0, absurd H !not_succ_le_zero)
(take k l,
assume IH : k ≤ l → k + (l - k) = l,
take H : succ k ≤ succ l,
calc
succ k + (succ l - succ k) = succ k + (l - k) : succ_sub_succ
... = succ (k + (l - k)) : succ_add
... = succ l : IH (le_of_succ_le_succ H))
succ k + (succ l - succ k) = succ k + (l - k) : by rewrite succ_sub_succ
... = succ (k + (l - k)) : by rewrite succ_add
... = succ l : by rewrite (IH (le_of_succ_le_succ H)))
theorem add_sub_of_ge {n m : ℕ} (H : n ≥ m) : n + (m - n) = n :=
calc
n + (m - n) = n + 0 : sub_eq_zero_of_le H
... = n : add_zero
n + (m - n) = n + 0 : by rewrite (sub_eq_zero_of_le H)
... = n : by rewrite add_zero
protected theorem sub_add_cancel {n m : ℕ} : n ≥ m → n - m + m = n :=
!add.comm ▸ !add_sub_of_le
@ -141,7 +141,7 @@ obtain (k : ℕ) (Hk : n + k = m), from le.elim H,
exists.intro k
(calc
m - k = n + k - k : by rewrite Hk
... = n : nat.add_sub_cancel)
... = n : by rewrite nat.add_sub_cancel)
protected theorem add_sub_assoc {m k : ℕ} (H : k ≤ m) (n : ℕ) : n + m - k = n + (m - k) :=
have l1 : k ≤ m → n + m - k = n + (m - k), from
@ -152,10 +152,10 @@ have l1 : k ≤ m → n + m - k = n + (m - k), from
assume IH : k ≤ m → n + m - k = n + (m - k),
take H : succ k ≤ succ m,
calc
n + succ m - succ k = succ (n + m) - succ k : add_succ
... = n + m - k : succ_sub_succ
... = n + (m - k) : IH (le_of_succ_le_succ H)
... = n + (succ m - succ k) : succ_sub_succ),
n + succ m - succ k = succ (n + m) - succ k : by rewrite add_succ
... = n + m - k : by rewrite succ_sub_succ
... = n + (m - k) : by rewrite (IH (le_of_succ_le_succ H))
... = n + (succ m - succ k) : by rewrite succ_sub_succ),
l1 H
theorem le_of_sub_eq_zero {n m : ℕ} : n - m = 0 → n ≤ m :=
@ -197,7 +197,7 @@ or.elim !le.total
have H3 : n - k + l = m - k, from
calc
n - k + l = l + (n - k) : by simp
... = l + n - k : nat.add_sub_assoc H2 l
... = l + n - k : by rewrite (nat.add_sub_assoc H2 l)
... = m - k : by simp,
le.intro H3)
@ -249,36 +249,36 @@ sub.cases
have H : k + (mn + km) = n, from
calc
k + (mn + km) = k + km + mn : by simp
... = m + mn : Hkm
... = m + mn : by rewrite Hkm
... = n : Hmn,
have H2 : n - k = mn + km, from nat.sub_eq_of_add_eq H,
H2 ▸ !le.refl))
protected theorem sub_lt_self {m n : ℕ} (H1 : m > 0) (H2 : n > 0) : m - n < m :=
calc
m - n = succ (pred m) - n : succ_pred_of_pos H1
... = succ (pred m) - succ (pred n) : succ_pred_of_pos H2
... = pred m - pred n : succ_sub_succ
... ≤ pred m : sub_le
... < succ (pred m) : lt_succ_self
m - n = succ (pred m) - n : by rewrite (succ_pred_of_pos H1)
... = succ (pred m) - succ (pred n) : by rewrite (succ_pred_of_pos H2)
... = pred m - pred n : by rewrite succ_sub_succ
... ≤ pred m : !sub_le
... < succ (pred m) : !lt_succ_self
... = m : succ_pred_of_pos H1
protected theorem le_sub_of_add_le {m n k : ℕ} (H : m + k ≤ n) : m ≤ n - k :=
calc
m = m + k - k : nat.add_sub_cancel
m = m + k - k : by rewrite nat.add_sub_cancel
... ≤ n - k : nat.sub_le_sub_right H k
protected theorem lt_sub_of_add_lt {m n k : ℕ} (H : m + k < n) (H2 : k ≤ n) : m < n - k :=
lt_of_succ_le (nat.le_sub_of_add_le (calc
succ m + k = succ (m + k) : succ_add_eq_succ_add
succ m + k = succ (m + k) : by rewrite succ_add_eq_succ_add
... ≤ n : succ_le_of_lt H))
protected theorem sub_lt_of_lt_add {v n m : nat} (h₁ : v < n + m) (h₂ : n ≤ v) : v - n < m :=
have succ v ≤ n + m, from succ_le_of_lt h₁,
have succ (v - n) ≤ m, from
calc succ (v - n) = succ v - n : succ_sub h₂
calc succ (v - n) = succ v - n : by rewrite (succ_sub h₂)
... ≤ n + m - n : nat.sub_le_sub_right this n
... = m : nat.add_sub_cancel_left,
... = m : by rewrite nat.add_sub_cancel_left,
lt_of_succ_le this
/- distance -/
@ -304,7 +304,7 @@ by substvars; rewrite [↑dist, *nat.sub_self, add_zero]
theorem dist_eq_sub_of_le {n m : ℕ} (H : n ≤ m) : dist n m = m - n :=
calc
dist n m = 0 + (m - n) : by rewrite -(sub_eq_zero_of_le H)
... = m - n : zero_add
... = m - n : by rewrite zero_add
theorem dist_eq_sub_of_lt {n m : ℕ} (H : n < m) : dist n m = m - n :=
dist_eq_sub_of_le (le_of_lt H)
@ -329,8 +329,8 @@ calc
theorem dist_add_add_right (n k m : ℕ) : dist (n + k) (m + k) = dist n m :=
calc
dist (n + k) (m + k) = ((n+k) - (m+k)) + ((m+k)-(n+k)) : rfl
... = (n - m) + ((m + k) - (n + k)) : nat.add_sub_add_right
... = (n - m) + (m - n) : nat.add_sub_add_right
... = (n - m) + ((m + k) - (n + k)) : by rewrite nat.add_sub_add_right
... = (n - m) + (m - n) : by rewrite nat.add_sub_add_right
theorem dist_add_add_left (k n m : ℕ) : dist (k + n) (k + m) = dist n m :=
begin rewrite [add.comm k n, add.comm k m]; apply dist_add_add_right end
@ -342,16 +342,16 @@ calc
theorem dist_eq_intro {n m k l : ℕ} (H : n + m = k + l) : dist n k = dist l m :=
calc
dist n k = dist (n + m) (k + m) : dist_add_add_right
... = dist (k + l) (k + m) : H
... = dist l m : dist_add_add_left
dist n k = dist (n + m) (k + m) : by rewrite dist_add_add_right
... = dist (k + l) (k + m) : by rewrite H
... = dist l m : by rewrite dist_add_add_left
theorem dist_sub_eq_dist_add_left {n m : ℕ} (H : n ≥ m) (k : ℕ) :
dist (n - m) k = dist n (k + m) :=
have H2 : n - m + (k + m) = k + n, from
calc
n - m + (k + m) = n - m + m + k : by simp
... = n + k : nat.sub_add_cancel H
... = n + k : by rewrite (nat.sub_add_cancel H)
... = k + n : by simp,
dist_eq_intro H2
@ -382,12 +382,12 @@ have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l
have H2 : m * k ≥ m * l, from !mul_le_mul_left H,
have H3 : n * l + m * k ≥ m * l, from le.trans H2 !le_add_left,
calc
dist n m * dist k l = dist n m * (k - l) : dist_eq_sub_of_ge H
... = dist (n * (k - l)) (m * (k - l)) : dist_mul_right
dist n m * dist k l = dist n m * (k - l) : by rewrite (dist_eq_sub_of_ge H)
... = dist (n * (k - l)) (m * (k - l)) : by rewrite dist_mul_right
... = dist (n * k - n * l) (m * k - m * l) : by rewrite [*nat.mul_sub_left_distrib]
... = dist (n * k) (m * k - m * l + n * l) : dist_sub_eq_dist_add_left (!mul_le_mul_left H)
... = dist (n * k) (n * l + (m * k - m * l)) : add.comm
... = dist (n * k) (n * l + m * k - m * l) : nat.add_sub_assoc H2 (n * l)
... = dist (n * k) (m * k - m * l + n * l) : by rewrite (dist_sub_eq_dist_add_left (!mul_le_mul_left H))
... = dist (n * k) (n * l + (m * k - m * l)) : by rewrite (add.comm (n * l))
... = dist (n * k) (n * l + m * k - m * l) : by rewrite (nat.add_sub_assoc H2 (n * l))
... = dist (n * k + m * l) (n * l + m * k) : dist_sub_eq_dist_add_right H3 _,
or.elim !le.total
(assume H : k ≤ l, !dist.comm ▸ !dist.comm ▸ aux l k H)

10
library/data/num.lean
View file

@ -28,9 +28,9 @@ namespace pos_num
| (bit1 a) :=
calc
pred (succ (bit1 a)) = cond (is_one (succ a)) one (bit1 (pred (succ a))) : rfl
... = cond ff one (bit1 (pred (succ a))) : succ_not_is_one
... = cond ff one (bit1 (pred (succ a))) : by rewrite succ_not_is_one
... = bit1 (pred (succ a)) : rfl
... = bit1 a : pred_succ a
... = bit1 a : by rewrite pred_succ
section
variables (a b : pos_num)
@ -51,11 +51,11 @@ namespace pos_num
| one := rfl
| (bit1 n) :=
calc bit1 n * one = bit0 (n * one) + one : rfl
... = bit0 n + one : mul_one n
... = bit1 n : bit0_add_one
... = bit0 n + one : by rewrite mul_one
... = bit1 n : !bit0_add_one
| (bit0 n) :=
calc bit0 n * one = bit0 (n * one) : rfl
... = bit0 n : mul_one n
... = bit0 n : by rewrite mul_one
theorem decidable_eq [instance] : ∀ (a b : pos_num), decidable (a = b)
| one one := inl rfl

6
library/init/function.lean
View file

@ -113,7 +113,7 @@ definition has_right_inverse (f : A → B) : Prop := ∃ finv : B → A, right_i
theorem injective_of_left_inverse {g : B → A} {f : A → B} : left_inverse g f → injective f :=
assume h, take a b, assume faeqfb,
calc a = g (f a) : by rewrite h
... = g (f b) : faeqfb
... = g (f b) : by rewrite faeqfb
... = b : by rewrite h
theorem injective_of_has_left_inverse {f : A → B} : has_left_inverse f → injective f :=
@ -143,8 +143,8 @@ theorem left_inverse_of_surjective_of_right_inverse {f : A → B} {g : B → A}
take y,
obtain x (Hx : f x = y), from surjf y,
calc
f (g y) = f (g (f x)) : Hx
... = f x : rfg
f (g y) = f (g (f x)) : by rewrite Hx
... = f x : by rewrite (rfg x)
... = y : Hx
theorem injective_id : injective (@id A) := take a₁ a₂ H, H

22
library/init/logic.lean
View file

@ -230,7 +230,7 @@ of_eq_true (eq_of_heq H)
theorem eq_rec_compose : ∀ {A B C : Type} (p₁ : B = C) (p₂ : A = B) (a : A), p₁ ▹ (p₂ ▹ a : B) = (p₂ ⬝ p₁) ▹ a
| A A A (eq.refl A) (eq.refl A) a := calc
eq.refl A ▹ eq.refl A ▹ a = eq.refl A ▹ a : rfl
... = (eq.refl A ⬝ eq.refl A) ▹ a : by rewrite (proof_irrel (eq.refl A) (eq.refl A ⬝ eq.refl A))
... = (eq.refl A ⬝ eq.refl A) ▹ a : by rewrite (proof_irrel (eq.refl A) (eq.refl A ⬝ eq.refl A))
theorem eq_rec_eq_eq_rec {A₁ A₂ : Type} {p : A₁ = A₂} : ∀ {a₁ : A₁} {a₂ : A₂}, p ▹ a₁ = a₂ → a₁ = p⁻¹ ▹ a₂ :=
eq.drec_on p (λ a₁ a₂ h, eq.drec_on h rfl)
@ -836,11 +836,11 @@ decidable.rec_on dec_b
(λ hp : b, calc
ite b x y = x : if_pos hp
... = u : h_t (iff.mp h_c hp)
... = ite c u v : if_pos (iff.mp h_c hp))
... = ite c u v : by rewrite (if_pos (iff.mp h_c hp)))
(λ hn : ¬b, calc
ite b x y = y : if_neg hn
... = v : h_e (iff.mp (not_iff_not_of_iff h_c) hn)
... = ite c u v : if_neg (iff.mp (not_iff_not_of_iff h_c) hn))
... = ite c u v : by rewrite (if_neg (iff.mp (not_iff_not_of_iff h_c) hn)))
theorem if_congr [congr] {A : Type} {b c : Prop} [dec_b : decidable b] [dec_c : decidable c]
{x y u v : A}
@ -871,11 +871,11 @@ decidable.rec_on dec_b
(λ hp : b, calc
ite b x y ↔ x : iff.of_eq (if_pos hp)
... ↔ u : h_t (iff.mp h_c hp)
... ↔ ite c u v : iff.of_eq (if_pos (iff.mp h_c hp)))
... ↔ ite c u v : by rewrite (if_pos (iff.mp h_c hp)))
(λ hn : ¬b, calc
ite b x y ↔ y : iff.of_eq (if_neg hn)
... ↔ v : h_e (iff.mp (not_iff_not_of_iff h_c) hn)
... ↔ ite c u v : iff.of_eq (if_neg (iff.mp (not_iff_not_of_iff h_c) hn)))
... ↔ ite c u v : by rewrite (if_neg (iff.mp (not_iff_not_of_iff h_c) hn)))
theorem if_congr_prop [congr] {b c x y u v : Prop} [dec_b : decidable b] [dec_c : decidable c]
(h_c : b ↔ c) (h_t : x ↔ u) (h_e : y ↔ v) :
@ -913,14 +913,14 @@ theorem dif_ctx_congr {A : Type} {b c : Prop} [dec_b : decidable b] [dec_c : dec
decidable.rec_on dec_b
(λ hp : b, calc
dite b x y = x hp : dif_pos hp
... = x (iff.mpr h_c (iff.mp h_c hp)) : proof_irrel
... = u (iff.mp h_c hp) : h_t
... = dite c u v : dif_pos (iff.mp h_c hp))
... = x (iff.mpr h_c (iff.mp h_c hp)) : rfl
... = u (iff.mp h_c hp) : by rewrite h_t
... = dite c u v : by rewrite (dif_pos (iff.mp h_c hp)))
(λ hn : ¬b, let h_nc : ¬b ↔ ¬c := not_iff_not_of_iff h_c in calc
dite b x y = y hn : dif_neg hn
... = y (iff.mpr h_nc (iff.mp h_nc hn)) : proof_irrel
... = v (iff.mp h_nc hn) : h_e
... = dite c u v : dif_neg (iff.mp h_nc hn))
... = y (iff.mpr h_nc (iff.mp h_nc hn)) : rfl
... = v (iff.mp h_nc hn) : by rewrite h_e
... = dite c u v : by rewrite (dif_neg (iff.mp h_nc hn)))
theorem dif_ctx_simp_congr {A : Type} {b c : Prop} [dec_b : decidable b]
{x : b → A} {u : c → A} {y : ¬b → A} {v : ¬c → A}

6
library/init/quot.lean
View file

@ -79,7 +79,7 @@ namespace quot
(q : quot s) (f : Π a, B ⟦a⟧) (c : ∀ (a b : A) (p : a ≈ b), f a == f b) : B q :=
quot.rec_on q f
(λ a b p, eq_of_heq (calc
eq.rec (f a) (sound p) == f a : eq_rec_heq
eq.rec (f a) (sound p) == f a : !eq_rec_heq
... == f b : c a b p))
end
@ -161,9 +161,9 @@ namespace quot
(λ b,
have aux : f a₁ b == f a₂ b, from c _ _ _ _ p !setoid.refl,
calc quot.hrec_on ⟦b⟧ (λ (b : B), f a₁ b) _
== f a₁ b : eq_rec_heq
== f a₁ b : !eq_rec_heq
... == f a₂ b : aux
... == quot.hrec_on ⟦b⟧ (λ (b : B), f a₂ b) _ : eq_rec_heq))
... == quot.hrec_on ⟦b⟧ (λ (b : B), f a₂ b) _ : heq.symm !eq_rec_heq))
end
end quot

2
library/logic/identities.lean
View file

@ -71,7 +71,7 @@ theorem not_implies_iff_and_not (a b : Prop) [Da : decidable a] :
¬(a → b) ↔ a ∧ ¬b :=
calc
¬(a → b) ↔ ¬(¬a ∨ b) : by rewrite (imp_iff_not_or a b)
... ↔ ¬¬a ∧ ¬b : not_or_iff_not_and_not
... ↔ ¬¬a ∧ ¬b : !not_or_iff_not_and_not
... ↔ a ∧ ¬b : by rewrite (not_not_iff a)
theorem and_not_of_not_implies {a b : Prop} [Da : decidable a] (H : ¬ (a → b)) : a ∧ ¬ b :=

2
src/frontends/lean/CMakeLists.txt
View file

@ -6,7 +6,7 @@ inductive_cmd.cpp elaborator.cpp dependencies.cpp
begin_end_annotation.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.cpp
coercion_elaborator.cpp info_tactic.cpp
init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp
init_module.cpp elaborator_context.cpp
parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp
type_util.cpp elaborator_exception.cpp local_ref_info.cpp
obtain_expr.cpp decl_attributes.cpp nested_declaration.cpp

5
src/frontends/lean/calc.cpp
View file

@ -79,8 +79,9 @@ static expr mk_op_fn(parser & p, name const & op, unsigned num_placeholders, pos
static calc_step parse_calc_proof(parser & p, calc_pred const & pred) {
p.check_token_next(get_colon_tk(), "invalid 'calc' expression, ':' expected");
expr pr = p.parse_expr();
return calc_step(pred, mk_calc_annotation(pr));
auto pos = p.pos();
expr pr = p.parse_expr();
return calc_step(pred, p.save_pos(mk_calc_annotation(pr), pos));
}
static unsigned get_arity_of(parser & p, name const & op) {

285
src/frontends/lean/calc_proof_elaborator.cpp
View file

@ -1,285 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/sexpr/option_declarations.h"
#include "kernel/free_vars.h"
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "library/unifier.h"
#include "library/reducible.h"
#include "library/metavar_closure.h"
#include "library/old_local_context.h"
#include "library/relation_manager.h"
#include "frontends/lean/util.h"
#include "frontends/lean/info_manager.h"
#include "frontends/lean/calc.h"
#include "frontends/lean/calc_proof_elaborator.h"
#include "frontends/lean/elaborator_exception.h"
#ifndef LEAN_DEFAULT_CALC_ASSISTANT
#define LEAN_DEFAULT_CALC_ASSISTANT true
#endif
namespace lean {
static name * g_elaborator_calc_assistant = nullptr;
void initialize_calc_proof_elaborator() {
g_elaborator_calc_assistant = new name{"elaborator", "calc_assistant"};
register_bool_option(*g_elaborator_calc_assistant, LEAN_DEFAULT_CALC_ASSISTANT,
"(elaborator) when needed lean automatically adds symmetry, "
"inserts missing arguments, and applies substitutions");
}
void finalize_calc_proof_elaborator() {
delete g_elaborator_calc_assistant;
}
bool get_elaborator_calc_assistant(options const & o) {
return o.get_bool(*g_elaborator_calc_assistant, LEAN_DEFAULT_CALC_ASSISTANT);
}
static optional<pair<expr, expr>> mk_op(environment const & env, old_local_context & ctx, type_checker_ptr & tc,
name const & op, unsigned nunivs, unsigned nargs, std::initializer_list<expr> const & explicit_args,
constraint_seq & cs, tag g) {
levels lvls;
for (unsigned i = 0; i < nunivs; i++)
lvls = levels(mk_meta_univ(mk_fresh_name()), lvls);
expr c = mk_constant(op, lvls);
expr op_type = instantiate_type_univ_params(env.get(op), lvls);
buffer<expr> args;
for (unsigned i = 0; i < nargs; i++) {
if (!is_pi(op_type))
return optional<pair<expr, expr>>();
expr arg = ctx.mk_meta(some_expr(binding_domain(op_type)), g);
args.push_back(arg);
op_type = instantiate(binding_body(op_type), arg);
}
expr r = mk_app(c, args, g);
for (expr const & explicit_arg : explicit_args) {
if (!is_pi(op_type))
return optional<pair<expr, expr>>();
r = mk_app(r, explicit_arg);
expr type = tc->infer(explicit_arg, cs);
justification j = mk_app_justification(r, op_type, explicit_arg, type);
if (!tc->is_def_eq(binding_domain(op_type), type, j, cs))
return optional<pair<expr, expr>>();
op_type = instantiate(binding_body(op_type), explicit_arg);
}
return some(mk_pair(r, op_type));
}
static optional<pair<expr, expr>> apply_symmetry(environment const & env, old_local_context & ctx, type_checker_ptr & tc,
expr const & e, expr const & e_type, constraint_seq & cs, tag g) {
buffer<expr> args;
expr const & op = get_app_args(e_type, args);
if (is_constant(op)) {
if (auto info = get_symm_extra_info(env, const_name(op))) {
return mk_op(env, ctx, tc, info->m_name,
info->m_num_univs, info->m_num_args-1, {e}, cs, g);
}
}
return optional<pair<expr, expr>>();
}
static optional<pair<expr, expr>> apply_subst(environment const & env, old_local_context & ctx,
type_checker_ptr & tc, expr const & e, expr const & e_type,
expr const & pred, constraint_seq & cs, tag g) {
buffer<expr> pred_args;
get_app_args(pred, pred_args);
unsigned npargs = pred_args.size();
if (npargs < 2)
return optional<pair<expr, expr>>();
buffer<expr> args;
expr const & op = get_app_args(e_type, args);
if (is_constant(op) && args.size() >= 2) {
if (auto sinfo = get_subst_extra_info(env, const_name(op))) {
if (auto rinfo = get_refl_extra_info(env, const_name(op))) {
if (auto refl_pair = mk_op(env, ctx, tc, rinfo->m_name, rinfo->m_num_univs,
rinfo->m_num_args-1, { pred_args[npargs-2] }, cs, g)) {
return mk_op(env, ctx, tc, sinfo->m_name, sinfo->m_num_univs,
sinfo->m_num_args-2, {e, refl_pair->first}, cs, g);
}
}
}
}
return optional<pair<expr, expr>>();
}
// Return true if \c e is convertible to a term of the form (h ...).
// If the result is true, update \c e and \c cs.
bool try_normalize_to_head(environment const & env, name const & h, expr & e, constraint_seq & cs) {
type_checker_ptr tc = mk_type_checker(env, [=](name const & n) { return n == h; });
constraint_seq new_cs;
expr new_e = tc->whnf(e, new_cs);
expr const & fn = get_app_fn(new_e);
if (is_constant(fn) && const_name(fn) == h) {
e = new_e;
cs += new_cs;
return true;
} else {
return false;
}
}
/** \brief Create a "choice" constraint that postpones the resolution of a calc proof step.
By delaying it, we can perform quick fixes such as:
- adding symmetry
- adding !
- adding subst
*/
constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
old_local_context const & _ctx, expr const & m, expr const & _e,
constraint_seq const & cs, unifier_config const & cfg,
info_manager * im, update_type_info_fn const & fn) {
justification j = mk_failed_to_synthesize_jst(env, m);
auto choice_fn = [=](expr const & meta, expr const & _meta_type, substitution const & _s) {
old_local_context ctx = _ctx;
expr e = _e;
substitution s = _s;
expr meta_type = _meta_type;
type_checker_ptr tc = mk_type_checker(env);
constraint_seq new_cs = cs;
expr e_type = tc->infer(e, new_cs);
e_type = s.instantiate(e_type);
tag g = e.get_tag();
bool calc_assistant = get_elaborator_calc_assistant(opts);
if (calc_assistant) {
// add '!' is needed
while (is_norm_pi(*tc, e_type, new_cs)) {
binder_info bi = binding_info(e_type);
if (!bi.is_implicit() && !bi.is_inst_implicit()) {
if (!has_free_var(binding_body(e_type), 0)) {
// if the rest of the type does not reference argument,
// then we also stop consuming arguments
break;
}
}
expr imp_arg = ctx.mk_meta(some_expr(binding_domain(e_type)), g);
e = mk_app(e, imp_arg, g);
e_type = instantiate(binding_body(e_type), imp_arg);
}
if (im)
fn(e);
}
e_type = head_beta_reduce(e_type);
expr const & meta_type_fn = get_app_fn(meta_type);
expr const & e_type_fn = get_app_fn(e_type);
if (is_constant(meta_type_fn) && (!is_constant(e_type_fn) || const_name(e_type_fn) != const_name(meta_type_fn))) {
// try to make sure meta_type and e_type have the same head symbol
if (!try_normalize_to_head(env, const_name(meta_type_fn), e_type, new_cs) &&
is_constant(e_type_fn)) {
try_normalize_to_head(env, const_name(e_type_fn), meta_type, new_cs);
}
}
auto try_alternative = [&](expr const & e, expr const & e_type, constraint_seq fcs, bool conservative) {
justification new_j = mk_type_mismatch_jst(e, e_type, meta_type);
if (!tc->is_def_eq(e_type, meta_type, new_j, fcs))
throw unifier_exception(new_j, s);
buffer<constraint> cs_buffer;
fcs.linearize(cs_buffer);
metavar_closure cls(meta);
cls.add(meta_type);
cls.mk_constraints(s, j, cs_buffer);
unifier_config new_cfg(cfg);
new_cfg.m_discard = false;
new_cfg.m_kind = conservative ? unifier_kind::Conservative : unifier_kind::Liberal;
unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), substitution(), new_cfg);
auto p = seq.pull();
lean_assert(p);
substitution new_s = p->first.first;
constraints postponed = map(p->first.second,
[&](constraint const & c) {
// we erase internal justifications
return update_justification(c, j);
});
expr new_e = new_s.instantiate(e);
if (conservative && has_expr_metavar_relaxed(new_s.instantiate_all(e)))
throw_elaborator_exception("solution contains metavariables", e);
if (im)
im->instantiate(new_s);
constraints r = cls.mk_constraints(new_s, j);
buffer<expr> locals;
expr mvar = get_app_args(meta, locals);
expr val = Fun(locals, new_e);
r = cons(mk_eq_cnstr(mvar, val, j), r);
return append(r, postponed);
};
if (!get_elaborator_calc_assistant(opts)) {
bool conservative = false;
return try_alternative(e, e_type, new_cs, conservative);
} else {
// TODO(Leo): after we have the simplifier and rewriter tactic, we should revise
// this code. It is "abusing" the higher-order unifier.
{
// Try the following possible intrepretations using a "conservative" unification procedure.
// That is, we only unfold definitions marked as reducible.
// Assume pr is the proof provided.
// 1. pr
bool conservative = true;
try { return try_alternative(e, e_type, new_cs, conservative); } catch (exception & ex) {}
// 2. eq.symm pr
constraint_seq symm_cs = new_cs;
auto symm = apply_symmetry(env, ctx, tc, e, e_type, symm_cs, g);
if (symm) {
try { return try_alternative(symm->first, symm->second, symm_cs, conservative); } catch (exception &) {}
}
// 3. subst pr (eq.refl lhs)
constraint_seq subst_cs = new_cs;
if (auto subst = apply_subst(env, ctx, tc, e, e_type, meta_type, subst_cs, g)) {
try { return try_alternative(subst->first, subst->second, subst_cs, conservative); } catch (exception&) {}
}
// 4. subst (eq.symm pr) (eq.refl lhs)
if (symm) {
constraint_seq subst_cs = symm_cs;
if (auto subst = apply_subst(env, ctx, tc, symm->first, symm->second,
meta_type, subst_cs, g)) {
try { return try_alternative(subst->first, subst->second, subst_cs, conservative); }
catch (exception&) {}
}
}
}
{
// Try the following possible insterpretations using the default unification procedure.
// 1. pr
bool conservative = false;
std::unique_ptr<throwable> saved_ex;
try {
return try_alternative(e, e_type, new_cs, conservative);
} catch (exception & ex) {
saved_ex.reset(ex.clone());
}
// 2. eq.symm pr
constraint_seq symm_cs = new_cs;
auto symm = apply_symmetry(env, ctx, tc, e, e_type, symm_cs, g);
if (symm) {
try { return try_alternative(symm->first, symm->second, symm_cs, conservative); }
catch (exception &) {}
}
// We use the exception for the first alternative as the error message
saved_ex->rethrow();
lean_unreachable();
}
}
};
bool owner = false;
return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Epilogue), owner, j);
}
}

30
src/frontends/lean/calc_proof_elaborator.h
View file

@ -1,30 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <functional>
#include "library/unifier.h"
#include "library/old_local_context.h"
#include "frontends/lean/info_manager.h"
namespace lean {
typedef std::function<void(expr const &)> update_type_info_fn;
/** \brief Create a "choice" constraint that postpones the resolution of a calc proof step.
By delaying it, we can perform quick fixes such as:
- adding symmetry
- adding !
- adding subst
*/
constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
old_local_context const & ctx, expr const & m, expr const & e,
constraint_seq const & cs, unifier_config const & cfg,
info_manager * im, update_type_info_fn const & fn);
void initialize_calc_proof_elaborator();
void finalize_calc_proof_elaborator();
}

17
src/frontends/lean/elaborator.cpp
View file

@ -52,7 +52,6 @@ Author: Leonardo de Moura
#include "frontends/lean/info_manager.h"
#include "frontends/lean/info_annotation.h"
#include "frontends/lean/elaborator.h"
#include "frontends/lean/calc_proof_elaborator.h"
#include "frontends/lean/info_tactic.h"
#include "frontends/lean/begin_end_annotation.h"
#include "frontends/lean/elaborator_exception.h"
@ -427,18 +426,10 @@ expr elaborator::visit_by(expr const & e, optional<expr> const & t, constraint_s
expr elaborator::visit_calc_proof(expr const & e, optional<expr> const & t, constraint_seq & cs) {
lean_assert(is_calc_annotation(e));
info_manager * im = nullptr;
if (infom())
im = &m_pre_info_data;
pair<expr, constraint_seq> ecs = visit(get_annotation_arg(e));
expr m = m_context.mk_meta(t, e.get_tag());
register_meta(m);
auto fn = [=](expr const & t) { save_type_data(get_annotation_arg(e), t); };
constraint c = mk_calc_proof_cnstr(env(), ios().get_options(),
m_context, m, ecs.first, ecs.second, m_unifier_config,
im, fn);
cs += c;
return m;
if (t)
return visit_expecting_type_of(get_annotation_arg(e), *t, cs);
else
return visit_core(get_annotation_arg(e), cs);
}
static bool is_implicit_pi(expr const & e) {

1
src/frontends/lean/elaborator.h
View file

@ -18,7 +18,6 @@ Author: Leonardo de Moura
#include "frontends/lean/elaborator_context.h"
#include "frontends/lean/coercion_elaborator.h"
#include "frontends/lean/util.h"
#include "frontends/lean/calc_proof_elaborator.h"
#include "frontends/lean/obtain_expr.h"
namespace lean {

3
src/frontends/lean/init_module.cpp
View file

@ -22,7 +22,6 @@ Author: Leonardo de Moura
#include "frontends/lean/parse_table.h"
#include "frontends/lean/token_table.h"
#include "frontends/lean/info_tactic.h"
#include "frontends/lean/calc_proof_elaborator.h"
#include "frontends/lean/find_cmd.h"
#include "frontends/lean/scanner.h"
#include "frontends/lean/pp.h"
@ -57,7 +56,6 @@ void initialize_frontend_lean_module() {
initialize_info_manager();
initialize_info_tactic();
initialize_pp();
initialize_calc_proof_elaborator();
initialize_server();
initialize_find_cmd();
initialize_local_ref_info();
@ -74,7 +72,6 @@ void finalize_frontend_lean_module() {
finalize_local_ref_info();
finalize_find_cmd();
finalize_server();
finalize_calc_proof_elaborator();
finalize_pp();
finalize_info_tactic();
finalize_info_manager();

3
src/shell/CMakeLists.txt
View file

@ -50,9 +50,6 @@ add_test(NAME "show_goal"
# add_test(NAME "issue_755"
# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
# COMMAND bash "./issue_755.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
add_test(NAME "show_goal_bag"
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
COMMAND bash "./show_goal_bag.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")
# add_test(NAME "print_info"
# WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/extra"
# COMMAND bash "./print_info.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")

26
tests/lean/calc_assistant.lean
View file

@ -1,26 +0,0 @@
import logic
open eq.ops
set_option elaborator.calc_assistant false
theorem tst1 (a b c : num) (H₁ : ∀ x, b = x) (H₂ : c = b) : a = c :=
calc a = b : H₁ -- error because calc assistant is off
... = c : H₂
theorem tst2 (a b c : num) (H₁ : ∀ x, b = x) (H₂ : c = b) : a = c :=
calc a = b : !H₁⁻¹
... = c : H₂ -- error because calc assistant is off
theorem tst3 (a b c : num) (H₁ : ∀ x, b = x) (H₂ : c = b) : a = c :=
calc a = b : !H₁⁻¹
... = c : H₂⁻¹
theorem tst4 (a b c : num) (H₁ : ∀ x, b = x) (H₂ : c = b) : a = c :=
calc a = b : eq.symm (H₁ a)
... = c : eq.symm H₂
set_option elaborator.calc_assistant true
theorem tst5 (a b c : num) (H₁ : ∀ x, b = x) (H₂ : c = b) : a = c :=
calc a = b : H₁
... = c : H₂

13
tests/lean/calc_assistant.lean.expected.out
View file

@ -1,13 +0,0 @@
calc_assistant.lean:7:14: error: type mismatch at term
H₁
has type
∀ (x : num),
b = x
but is expected to have type
a = b
calc_assistant.lean:12:14: error: type mismatch at term
H₂
has type
c = b
but is expected to have type
b = c

17
tests/lean/extra/bag.661.20.expected.out
View file

@ -1,17 +0,0 @@
LEAN_INFORMATION
position 661:20
A : Type,
decA : decidable_eq A,
all_of_subcount_eq_tt :
∀ {l₁ l₂ : list A},
subcount l₁ l₂ = tt → (∀ (a : A), list.count a l₁ ≤ list.count a l₂),
a : A,
l₁ l₂ : list A,
h : subcount (a :: l₁) l₂ = tt,
x : A,
this : subcount l₁ l₂ = tt,
ih : ∀ (a : A), list.count a l₁ ≤ list.count a l₂,
i : list.count a (a :: l₁) ≤ list.count a l₂,
this : x = a
⊢ list.count x (a :: l₁) ≤ list.count x l₂
END_LEAN_INFORMATION

15
tests/lean/extra/bag.671.8.expected.out
View file

@ -1,15 +0,0 @@
LEAN_INFORMATION
position 671:8
A : Type,
decA : decidable_eq A,
ex_of_subcount_eq_ff :
∀ {l₁ l₂ : list A},
subcount l₁ l₂ = ff → (∃ (a : A), ¬list.count a l₁ ≤ list.count a l₂),
a : A,
l₁ l₂ : list A,
h : subcount (a :: l₁) l₂ = ff,
i : list.count a (a :: l₁) ≤ list.count a l₂,
this : subcount l₁ l₂ ≠ ff,
this : subcount l₁ l₂ = tt
⊢ false
END_LEAN_INFORMATION

4
tests/lean/extra/bag.673.71.expected.out
View file

@ -1,4 +0,0 @@
LEAN_INFORMATION
position 674:6
no goals
END_LEAN_INFORMATION

16
tests/lean/extra/bag.677.47.expected.out
View file

@ -1,16 +0,0 @@
LEAN_INFORMATION
position 677:47
A : Type,
decA : decidable_eq A,
ex_of_subcount_eq_ff :
∀ {l₁ l₂ : list A},
subcount l₁ l₂ = ff → (∃ (a : A), ¬list.count a l₁ ≤ list.count a l₂),
a : A,
l₁ l₂ : list A,
h : subcount (a :: l₁) l₂ = ff,
i : list.count a (a :: l₁) ≤ list.count a l₂,
this : subcount l₁ l₂ = ff,
ih : ∃ (a : A), ¬list.count a l₁ ≤ list.count a l₂,
hw : ¬list.count a l₁ ≤ list.count a l₂
⊢ ¬list.count a (a :: l₁) ≤ list.count a l₂
END_LEAN_INFORMATION

690
tests/lean/extra/bag.lean
View file

@ -1,690 +0,0 @@
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
Finite bags.
-/
import data.nat data.list.perm algebra.binary
open nat quot list subtype binary function eq.ops algebra
open [decl] perm
variable {A : Type}
definition bag.setoid [instance] (A : Type) : setoid (list A) :=
setoid.mk (@perm A) (mk_equivalence (@perm A) (@perm.refl A) (@perm.symm A) (@perm.trans A))
definition bag (A : Type) : Type :=
quot (bag.setoid A)
namespace bag
definition of_list (l : list A) : bag A :=
⟦l⟧
definition empty : bag A :=
of_list nil
definition singleton (a : A) : bag A :=
of_list [a]
definition insert (a : A) (b : bag A) : bag A :=
quot.lift_on b (λ l, ⟦a::l⟧)
(λ l₁ l₂ h, quot.sound (perm.skip a h))
lemma insert_empty_eq_singleton (a : A) : insert a empty = singleton a :=
rfl
definition insert.comm (a₁ a₂ : A) (b : bag A) : insert a₁ (insert a₂ b) = insert a₂ (insert a₁ b) :=
quot.induction_on b (λ l, quot.sound !perm.swap)
definition append (b₁ b₂ : bag A) : bag A :=
quot.lift_on₂ b₁ b₂ (λ l₁ l₂, ⟦l₁++l₂⟧)
(λ l₁ l₂ l₃ l₄ h₁ h₂, quot.sound (perm_app h₁ h₂))
infix ++ := append
lemma append.comm (b₁ b₂ : bag A) : b₁ ++ b₂ = b₂ ++ b₁ :=
quot.induction_on₂ b₁ b₂ (λ l₁ l₂, quot.sound !perm_app_comm)
lemma append.assoc (b₁ b₂ b₃ : bag A) : (b₁ ++ b₂) ++ b₃ = b₁ ++ (b₂ ++ b₃) :=
quot.induction_on₃ b₁ b₂ b₃ (λ l₁ l₂ l₃, quot.sound (by rewrite list.append.assoc; apply perm.refl))
lemma append_empty_left (b : bag A) : empty ++ b = b :=
quot.induction_on b (λ l, quot.sound (by rewrite append_nil_left; apply perm.refl))
lemma append_empty_right (b : bag A) : b ++ empty = b :=
quot.induction_on b (λ l, quot.sound (by rewrite append_nil_right; apply perm.refl))
lemma append_insert_left (a : A) (b₁ b₂ : bag A) : insert a b₁ ++ b₂ = insert a (b₁ ++ b₂) :=
quot.induction_on₂ b₁ b₂ (λ l₁ l₂, quot.sound (by rewrite append_cons; apply perm.refl))
lemma append_insert_right (a : A) (b₁ b₂ : bag A) : b₁ ++ insert a b₂ = insert a (b₁ ++ b₂) :=
calc b₁ ++ insert a b₂ = insert a b₂ ++ b₁ : append.comm
... = insert a (b₂ ++ b₁) : append_insert_left
... = insert a (b₁ ++ b₂) : append.comm
protected lemma induction_on [recursor 3] {C : bag A → Prop} (b : bag A) (h₁ : C empty) (h₂ : ∀ a b, C b → C (insert a b)) : C b :=
quot.induction_on b (λ l, list.induction_on l h₁ (λ h t ih, h₂ h ⟦t⟧ ih))
section decidable_eq
variable [decA : decidable_eq A]
include decA
open decidable
definition has_decidable_eq [instance] (b₁ b₂ : bag A) : decidable (b₁ = b₂) :=
quot.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂,
match decidable_perm l₁ l₂ with
| inl h := inl (quot.sound h)
| inr h := inr (λ n, absurd (quot.exact n) h)
end)
end decidable_eq
section count
variable [decA : decidable_eq A]
include decA
definition count (a : A) (b : bag A) : nat :=
quot.lift_on b (λ l, count a l)
(λ l₁ l₂ h, count_eq_of_perm h a)
lemma count_empty (a : A) : count a empty = 0 :=
rfl
lemma count_insert (a : A) (b : bag A) : count a (insert a b) = succ (count a b) :=
quot.induction_on b (λ l, begin unfold [insert, count], rewrite count_cons_eq end)
lemma count_insert_of_ne {a₁ a₂ : A} (h : a₁ ≠ a₂) (b : bag A) : count a₁ (insert a₂ b) = count a₁ b :=
quot.induction_on b (λ l, begin unfold [insert, count], rewrite (count_cons_of_ne h) end)
lemma count_singleton (a : A) : count a (singleton a) = 1 :=
begin rewrite [-insert_empty_eq_singleton, count_insert] end
lemma count_append (a : A) (b₁ b₂ : bag A) : count a (append b₁ b₂) = count a b₁ + count a b₂ :=
quot.induction_on₂ b₁ b₂ (λ l₁ l₂, begin unfold [append, count], rewrite list.count_append end)
open perm decidable
protected lemma ext {b₁ b₂ : bag A} : (∀ a, count a b₁ = count a b₂) → b₁ = b₂ :=
quot.induction_on₂ b₁ b₂ (λ l₁ l₂ (h : ∀ a, count a ⟦l₁⟧ = count a ⟦l₂⟧),
have gen : ∀ (l₁ l₂ : list A), (∀ a, list.count a l₁ = list.count a l₂) → l₁ ~ l₂
| [] [] h₁ := !perm.refl
| [] (a₂::s₂) h₁ := assert list.count a₂ [] = list.count a₂ (a₂::s₂), from h₁ a₂, by rewrite [count_nil at this, count_cons_eq at this]; contradiction
| (a::s₁) s₂ h₁ :=
assert g₁ : list.count a (a::s₁) > 0, from count_gt_zero_of_mem !mem_cons,
assert list.count a (a::s₁) = list.count a s₂, from h₁ a,
assert list.count a s₂ > 0, by rewrite [-this]; exact g₁,
have a ∈ s₂, from mem_of_count_gt_zero this,
have ∃ l r, s₂ = l++(a::r), from mem_split this,
obtain l r (e₁ : s₂ = l++(a::r)), from this,
have ∀ a, list.count a s₁ = list.count a (l++r), from
take a₁,
assert e₂ : list.count a₁ (a::s₁) = list.count a₁ (l++(a::r)), by rewrite -e₁; exact h₁ a₁,
by_cases
(suppose a₁ = a, begin
rewrite [-this at e₂, list.count_append at e₂, *count_cons_eq at e₂, add_succ at e₂],
injection e₂ with e₃, rewrite e₃,
rewrite list.count_append
end)
(suppose a₁ ≠ a,
by rewrite [list.count_append at e₂, *count_cons_of_ne this at e₂, e₂, list.count_append]),
have ih : s₁ ~ l++r, from gen s₁ (l++r) this,
calc a::s₁ ~ a::(l++r) : perm.skip a ih
... ~ l++(a::r) : perm_middle
... = s₂ : e₁,
quot.sound (gen l₁ l₂ h))
definition insert.inj {a : A} {b₁ b₂ : bag A} : insert a b₁ = insert a b₂ → b₁ = b₂ :=
assume h, bag.ext (take x,
assert e : count x (insert a b₁) = count x (insert a b₂), by rewrite h,
by_cases
(suppose x = a, begin subst x, rewrite [*count_insert at e], injection e, assumption end)
(suppose x ≠ a, begin rewrite [*count_insert_of_ne this at e], assumption end))
end count
section extract
open decidable
variable [decA : decidable_eq A]
include decA
definition extract (a : A) (b : bag A) : bag A :=
quot.lift_on b (λ l, ⟦filter (λ c, c ≠ a) l⟧)
(λ l₁ l₂ h, quot.sound (perm_filter h))
lemma extract_singleton (a : A) : extract a (singleton a) = empty :=
begin unfold [extract, singleton, of_list, filter], rewrite [if_neg (λ h : a ≠ a, absurd rfl h)] end
lemma extract_insert (a : A) (b : bag A) : extract a (insert a b) = extract a b :=
quot.induction_on b (λ l, begin
unfold [insert, extract],
rewrite [@filter_cons_of_neg _ (λ c, c ≠ a) _ _ l (not_not_intro (eq.refl a))]
end)
lemma extract_insert_of_ne {a₁ a₂ : A} (h : a₁ ≠ a₂) (b : bag A) : extract a₁ (insert a₂ b) = insert a₂ (extract a₁ b) :=
quot.induction_on b (λ l, begin
unfold [insert, extract],
rewrite [@filter_cons_of_pos _ (λ c, c ≠ a₁) _ _ l (ne.symm h)]
end)
lemma count_extract (a : A) (b : bag A) : count a (extract a b) = 0 :=
bag.induction_on b rfl
(λ c b ih, by_cases
(suppose a = c, begin subst c, rewrite [extract_insert, ih] end)
(suppose a ≠ c, begin rewrite [extract_insert_of_ne this, count_insert_of_ne this, ih] end))
lemma count_extract_of_ne {a₁ a₂ : A} (h : a₁ ≠ a₂) (b : bag A) : count a₁ (extract a₂ b) = count a₁ b :=
bag.induction_on b rfl
(take x b ih, by_cases
(suppose x = a₁, begin subst x, rewrite [extract_insert_of_ne (ne.symm h), *count_insert, ih] end)
(suppose x ≠ a₁, by_cases
(suppose x = a₂, begin subst x, rewrite [extract_insert, ih, count_insert_of_ne h] end)
(suppose x ≠ a₂, begin
rewrite [count_insert_of_ne (ne.symm `x ≠ a₁`), extract_insert_of_ne (ne.symm this)],
rewrite [count_insert_of_ne (ne.symm `x ≠ a₁`), ih]
end)))
end extract
section erase
variable [decA : decidable_eq A]
include decA
definition erase (a : A) (b : bag A) : bag A :=
quot.lift_on b (λ l, ⟦erase a l⟧)
(λ l₁ l₂ h, quot.sound (erase_perm_erase_of_perm _ h))
lemma erase_empty (a : A) : erase a empty = empty :=
rfl
lemma erase_insert (a : A) (b : bag A) : erase a (insert a b) = b :=
quot.induction_on b (λ l, quot.sound (by rewrite erase_cons_head; apply perm.refl))
lemma erase_insert_of_ne {a₁ a₂ : A} (h : a₁ ≠ a₂) (b : bag A) : erase a₁ (insert a₂ b) = insert a₂ (erase a₁ b) :=
quot.induction_on b (λ l, quot.sound (by rewrite (erase_cons_tail _ h); apply perm.refl))
end erase
section member
variable [decA : decidable_eq A]
include decA
definition mem (a : A) (b : bag A) := count a b > 0
infix ∈ := mem
lemma mem_def (a : A) (b : bag A) : (a ∈ b) = (count a b > 0) :=
rfl
lemma mem_insert (a : A) (b : bag A) : a ∈ insert a b :=
begin unfold mem, rewrite count_insert, exact dec_trivial end
lemma mem_of_list_iff_mem (a : A) (l : list A) : a ∈ of_list l ↔ a ∈ l :=
iff.intro !mem_of_count_gt_zero !count_gt_zero_of_mem
lemma count_of_list_eq_count (a : A) (l : list A) : count a (of_list l) = list.count a l :=
rfl
end member
section union_inter
variable [decA : decidable_eq A]
include decA
open perm decidable
private definition union_list (l₁ l₂ : list A) :=
erase_dup (l₁ ++ l₂)
private lemma perm_union_list {l₁ l₂ l₃ l₄ : list A} (h₁ : l₁ ~ l₃) (h₂ : l₂ ~ l₄) : union_list l₁ l₂ ~ union_list l₃ l₄ :=
perm_erase_dup_of_perm (perm_app h₁ h₂)
private lemma nodup_union_list (l₁ l₂ : list A) : nodup (union_list l₁ l₂) :=
!nodup_erase_dup
private definition not_mem_of_not_mem_union_list_left {a : A} {l₁ l₂ : list A} (h : a ∉ union_list l₁ l₂) : a ∉ l₁ :=
suppose a ∈ l₁,
have a ∈ l₁ ++ l₂, from mem_append_left _ this,
have a ∈ erase_dup (l₁ ++ l₂), from mem_erase_dup this,
absurd this h
private definition not_mem_of_not_mem_union_list_right {a : A} {l₁ l₂ : list A} (h : a ∉ union_list l₁ l₂) : a ∉ l₂ :=
suppose a ∈ l₂,
have a ∈ l₁ ++ l₂, from mem_append_right _ this,
have a ∈ erase_dup (l₁ ++ l₂), from mem_erase_dup this,
absurd this h
private definition gen : nat → A → list A
| 0 a := nil
| (n+1) a := a :: gen n a
private lemma not_mem_gen_of_ne {a b : A} (h : a ≠ b) : ∀ n, a ∉ gen n b
| 0 := !not_mem_nil
| (n+1) := not_mem_cons_of_ne_of_not_mem h (not_mem_gen_of_ne n)
private lemma count_gen : ∀ (a : A) (n : nat), list.count a (gen n a) = n
| a 0 := rfl
| a (n+1) := begin unfold gen, rewrite [count_cons_eq, count_gen] end
private lemma count_gen_eq_zero_of_ne {a b : A} (h : a ≠ b) : ∀ n, list.count a (gen n b) = 0
| 0 := rfl
| (n+1) := begin unfold gen, rewrite [count_cons_of_ne h, count_gen_eq_zero_of_ne] end
private definition max_count (l₁ l₂ : list A) : list A → list A
| [] := []
| (a::l) := if list.count a l₁ ≥ list.count a l₂ then gen (list.count a l₁) a ++ max_count l else gen (list.count a l₂) a ++ max_count l
private definition min_count (l₁ l₂ : list A) : list A → list A
| [] := []
| (a::l) := if list.count a l₁ ≤ list.count a l₂ then gen (list.count a l₁) a ++ min_count l else gen (list.count a l₂) a ++ min_count l
private lemma not_mem_max_count_of_not_mem (l₁ l₂ : list A) : ∀ {a l}, a ∉ l → a ∉ max_count l₁ l₂ l
| a [] h := !not_mem_nil
| a (b::l) h :=
assert ih : a ∉ max_count l₁ l₂ l, from not_mem_max_count_of_not_mem (not_mem_of_not_mem_cons h),
assert a ≠ b, from ne_of_not_mem_cons h,
by_cases
(suppose list.count b l₁ ≥ list.count b l₂, begin
unfold max_count, rewrite [if_pos this],
exact not_mem_append (not_mem_gen_of_ne `a ≠ b` _) ih
end)
(suppose ¬ list.count b l₁ ≥ list.count b l₂, begin
unfold max_count, rewrite [if_neg this],
exact not_mem_append (not_mem_gen_of_ne `a ≠ b` _) ih
end)
private lemma max_count_eq (l₁ l₂ : list A) : ∀ {a : A} {l : list A}, a ∈ l → nodup l → list.count a (max_count l₁ l₂ l) = max (list.count a l₁) (list.count a l₂)
| a [] h₁ h₂ := absurd h₁ !not_mem_nil
| a (b::l) h₁ h₂ :=
assert nodup l, from nodup_of_nodup_cons h₂,
assert b ∉ l, from not_mem_of_nodup_cons h₂,
or.elim (eq_or_mem_of_mem_cons h₁)
(suppose a = b,
have a ∉ l, by rewrite this; assumption,
assert a ∉ max_count l₁ l₂ l, from not_mem_max_count_of_not_mem l₁ l₂ this,
by_cases
(suppose i : list.count a l₁ ≥ list.count a l₂, begin
unfold max_count, subst b,
rewrite [if_pos i, list.count_append, count_gen, max_eq_left i, count_eq_zero_of_not_mem `a ∉ max_count l₁ l₂ l`]
end)
(suppose i : ¬ list.count a l₁ ≥ list.count a l₂, begin
unfold max_count, subst b,
rewrite [if_neg i, list.count_append, count_gen, max_eq_right_of_lt (lt_of_not_ge i), count_eq_zero_of_not_mem `a ∉ max_count l₁ l₂ l`]
end))
(suppose a ∈ l,
assert a ≠ b, from suppose a = b, by subst b; contradiction,
assert ih : list.count a (max_count l₁ l₂ l) = max (list.count a l₁) (list.count a l₂), from max_count_eq `a ∈ l` `nodup l`,
by_cases
(suppose i : list.count b l₁ ≥ list.count b l₂, begin
unfold max_count,
rewrite [if_pos i, -ih, list.count_append, count_gen_eq_zero_of_ne `a ≠ b`, zero_add]
end)
(suppose i : ¬ list.count b l₁ ≥ list.count b l₂, begin
unfold max_count,
rewrite [if_neg i, -ih, list.count_append, count_gen_eq_zero_of_ne `a ≠ b`, zero_add]
end))
private lemma not_mem_min_count_of_not_mem (l₁ l₂ : list A) : ∀ {a l}, a ∉ l → a ∉ min_count l₁ l₂ l
| a [] h := !not_mem_nil
| a (b::l) h :=
assert ih : a ∉ min_count l₁ l₂ l, from not_mem_min_count_of_not_mem (not_mem_of_not_mem_cons h),
assert a ≠ b, from ne_of_not_mem_cons h,
by_cases
(suppose list.count b l₁ ≤ list.count b l₂, begin
unfold min_count, rewrite [if_pos this],
exact not_mem_append (not_mem_gen_of_ne `a ≠ b` _) ih
end)
(suppose ¬ list.count b l₁ ≤ list.count b l₂, begin
unfold min_count, rewrite [if_neg this],
exact not_mem_append (not_mem_gen_of_ne `a ≠ b` _) ih
end)
private lemma min_count_eq (l₁ l₂ : list A) : ∀ {a : A} {l : list A}, a ∈ l → nodup l → list.count a (min_count l₁ l₂ l) = min (list.count a l₁) (list.count a l₂)
| a [] h₁ h₂ := absurd h₁ !not_mem_nil
| a (b::l) h₁ h₂ :=
assert nodup l, from nodup_of_nodup_cons h₂,
assert b ∉ l, from not_mem_of_nodup_cons h₂,
or.elim (eq_or_mem_of_mem_cons h₁)
(suppose a = b,
have a ∉ l, by rewrite this; assumption,
assert a ∉ min_count l₁ l₂ l, from not_mem_min_count_of_not_mem l₁ l₂ this,
by_cases
(suppose i : list.count a l₁ ≤ list.count a l₂, begin
unfold min_count, subst b,
rewrite [if_pos i, list.count_append, count_gen, min_eq_left i, count_eq_zero_of_not_mem `a ∉ min_count l₁ l₂ l`]
end)
(suppose i : ¬ list.count a l₁ ≤ list.count a l₂, begin
unfold min_count, subst b,
rewrite [if_neg i, list.count_append, count_gen, min_eq_right (le_of_lt (lt_of_not_ge i)), count_eq_zero_of_not_mem `a ∉ min_count l₁ l₂ l`]
end))
(suppose a ∈ l,
assert a ≠ b, from suppose a = b, by subst b; contradiction,
assert ih : list.count a (min_count l₁ l₂ l) = min (list.count a l₁) (list.count a l₂), from min_count_eq `a ∈ l` `nodup l`,
by_cases
(suppose i : list.count b l₁ ≤ list.count b l₂, begin
unfold min_count,
rewrite [if_pos i, -ih, list.count_append, count_gen_eq_zero_of_ne `a ≠ b`, zero_add]
end)
(suppose i : ¬ list.count b l₁ ≤ list.count b l₂, begin
unfold min_count,
rewrite [if_neg i, -ih, list.count_append, count_gen_eq_zero_of_ne `a ≠ b`, zero_add]
end))
private lemma perm_max_count_left {l₁ l₂ l₃ l₄ : list A} (h₁ : l₁ ~ l₃) (h₂ : l₂ ~ l₄) : ∀ l, max_count l₁ l₂ l ~ max_count l₃ l₄ l
| [] := by esimp
| (a::l) :=
assert e₁ : list.count a l₁ = list.count a l₃, from count_eq_of_perm h₁ a,
assert e₂ : list.count a l₂ = list.count a l₄, from count_eq_of_perm h₂ a,
by_cases
(suppose list.count a l₁ ≥ list.count a l₂,
begin unfold max_count, rewrite [-e₁, -e₂, *if_pos this], exact perm_app !perm.refl !perm_max_count_left end)
(suppose ¬ list.count a l₁ ≥ list.count a l₂,
begin unfold max_count, rewrite [-e₁, -e₂, *if_neg this], exact perm_app !perm.refl !perm_max_count_left end)
private lemma perm_app_left_comm (l₁ l₂ l₃ : list A) : l₁ ++ (l₂ ++ l₃) ~ l₂ ++ (l₁ ++ l₃) :=
calc l₁ ++ (l₂ ++ l₃) = (l₁ ++ l₂) ++ l₃ : list.append.assoc
... ~ (l₂ ++ l₁) ++ l₃ : perm_app !perm_app_comm !perm.refl
... = l₂ ++ (l₁ ++ l₃) : list.append.assoc
private lemma perm_max_count_right {l r : list A} (h : l ~ r) : ∀ l₁ l₂, max_count l₁ l₂ l ~ max_count l₁ l₂ r :=
perm.induction_on h
(λ l₁ l₂, !perm.refl)
(λ x s₁ s₂ p ih l₁ l₂, by_cases
(suppose i : list.count x l₁ ≥ list.count x l₂,
begin unfold max_count, rewrite [*if_pos i], exact perm_app !perm.refl !ih end)
(suppose i : ¬ list.count x l₁ ≥ list.count x l₂,
begin unfold max_count, rewrite [*if_neg i], exact perm_app !perm.refl !ih end))
(λ x y l l₁ l₂, by_cases
(suppose i₁ : list.count x l₁ ≥ list.count x l₂, by_cases
(suppose i₂ : list.count y l₁ ≥ list.count y l₂,
begin unfold max_count, unfold max_count, rewrite [*if_pos i₁, *if_pos i₂], apply perm_app_left_comm end)
(suppose i₂ : ¬ list.count y l₁ ≥ list.count y l₂,
begin unfold max_count, unfold max_count, rewrite [*if_pos i₁, *if_neg i₂], apply perm_app_left_comm end))
(suppose i₁ : ¬ list.count x l₁ ≥ list.count x l₂, by_cases
(suppose i₂ : list.count y l₁ ≥ list.count y l₂,
begin unfold max_count, unfold max_count, rewrite [*if_neg i₁, *if_pos i₂], apply perm_app_left_comm end)
(suppose i₂ : ¬ list.count y l₁ ≥ list.count y l₂,
begin unfold max_count, unfold max_count, rewrite [*if_neg i₁, *if_neg i₂], apply perm_app_left_comm end)))
(λ s₁ s₂ s₃ p₁ p₂ ih₁ ih₂ l₁ l₂, perm.trans (ih₁ l₁ l₂) (ih₂ l₁ l₂))
private lemma perm_max_count {l₁ l₂ l₃ r₁ r₂ r₃ : list A} (p₁ : l₁ ~ r₁) (p₂ : l₂ ~ r₂) (p₃ : l₃ ~ r₃) : max_count l₁ l₂ l₃ ~ max_count r₁ r₂ r₃ :=
calc max_count l₁ l₂ l₃ ~ max_count r₁ r₂ l₃ : perm_max_count_left p₁ p₂
... ~ max_count r₁ r₂ r₃ : perm_max_count_right p₃
private lemma perm_min_count_left {l₁ l₂ l₃ l₄ : list A} (h₁ : l₁ ~ l₃) (h₂ : l₂ ~ l₄) : ∀ l, min_count l₁ l₂ l ~ min_count l₃ l₄ l
| [] := by esimp
| (a::l) :=
assert e₁ : list.count a l₁ = list.count a l₃, from count_eq_of_perm h₁ a,
assert e₂ : list.count a l₂ = list.count a l₄, from count_eq_of_perm h₂ a,
by_cases
(suppose list.count a l₁ ≤ list.count a l₂,
begin unfold min_count, rewrite [-e₁, -e₂, *if_pos this], exact perm_app !perm.refl !perm_min_count_left end)
(suppose ¬ list.count a l₁ ≤ list.count a l₂,
begin unfold min_count, rewrite [-e₁, -e₂, *if_neg this], exact perm_app !perm.refl !perm_min_count_left end)
private lemma perm_min_count_right {l r : list A} (h : l ~ r) : ∀ l₁ l₂, min_count l₁ l₂ l ~ min_count l₁ l₂ r :=
perm.induction_on h
(λ l₁ l₂, !perm.refl)
(λ x s₁ s₂ p ih l₁ l₂, by_cases
(suppose i : list.count x l₁ ≤ list.count x l₂,
begin unfold min_count, rewrite [*if_pos i], exact perm_app !perm.refl !ih end)
(suppose i : ¬ list.count x l₁ ≤ list.count x l₂,
begin unfold min_count, rewrite [*if_neg i], exact perm_app !perm.refl !ih end))
(λ x y l l₁ l₂, by_cases
(suppose i₁ : list.count x l₁ ≤ list.count x l₂, by_cases
(suppose i₂ : list.count y l₁ ≤ list.count y l₂,
begin unfold min_count, unfold min_count, rewrite [*if_pos i₁, *if_pos i₂], apply perm_app_left_comm end)
(suppose i₂ : ¬ list.count y l₁ ≤ list.count y l₂,
begin unfold min_count, unfold min_count, rewrite [*if_pos i₁, *if_neg i₂], apply perm_app_left_comm end))
(suppose i₁ : ¬ list.count x l₁ ≤ list.count x l₂, by_cases
(suppose i₂ : list.count y l₁ ≤ list.count y l₂,
begin unfold min_count, unfold min_count, rewrite [*if_neg i₁, *if_pos i₂], apply perm_app_left_comm end)
(suppose i₂ : ¬ list.count y l₁ ≤ list.count y l₂,
begin unfold min_count, unfold min_count, rewrite [*if_neg i₁, *if_neg i₂], apply perm_app_left_comm end)))
(λ s₁ s₂ s₃ p₁ p₂ ih₁ ih₂ l₁ l₂, perm.trans (ih₁ l₁ l₂) (ih₂ l₁ l₂))
private lemma perm_min_count {l₁ l₂ l₃ r₁ r₂ r₃ : list A} (p₁ : l₁ ~ r₁) (p₂ : l₂ ~ r₂) (p₃ : l₃ ~ r₃) : min_count l₁ l₂ l₃ ~ min_count r₁ r₂ r₃ :=
calc min_count l₁ l₂ l₃ ~ min_count r₁ r₂ l₃ : perm_min_count_left p₁ p₂
... ~ min_count r₁ r₂ r₃ : perm_min_count_right p₃
definition union (b₁ b₂ : bag A) : bag A :=
quot.lift_on₂ b₁ b₂ (λ l₁ l₂, ⟦max_count l₁ l₂ (union_list l₁ l₂)⟧)
(λ l₁ l₂ l₃ l₄ p₁ p₂, quot.sound (perm_max_count p₁ p₂ (perm_union_list p₁ p₂)))
infix ∪ := union
definition inter (b₁ b₂ : bag A) : bag A :=
quot.lift_on₂ b₁ b₂ (λ l₁ l₂, ⟦min_count l₁ l₂ (union_list l₁ l₂)⟧)
(λ l₁ l₂ l₃ l₄ p₁ p₂, quot.sound (perm_min_count p₁ p₂ (perm_union_list p₁ p₂)))
infix ∩ := inter
lemma count_union (a : A) (b₁ b₂ : bag A) : count a (b₁ ∪ b₂) = max (count a b₁) (count a b₂) :=
quot.induction_on₂ b₁ b₂ (λ l₁ l₂, by_cases
(suppose a ∈ union_list l₁ l₂, !max_count_eq this !nodup_union_list)
(suppose ¬ a ∈ union_list l₁ l₂,
assert ¬ a ∈ l₁, from not_mem_of_not_mem_union_list_left `¬ a ∈ union_list l₁ l₂`,
assert ¬ a ∈ l₂, from not_mem_of_not_mem_union_list_right `¬ a ∈ union_list l₁ l₂`,
assert n : ¬ a ∈ max_count l₁ l₂ (union_list l₁ l₂), from not_mem_max_count_of_not_mem l₁ l₂ `¬ a ∈ union_list l₁ l₂`,
begin
unfold [union, count],
rewrite [count_eq_zero_of_not_mem `¬ a ∈ l₁`, count_eq_zero_of_not_mem `¬ a ∈ l₂`, max_self],
rewrite [count_eq_zero_of_not_mem n]
end))
lemma count_inter (a : A) (b₁ b₂ : bag A) : count a (b₁ ∩ b₂) = min (count a b₁) (count a b₂) :=
quot.induction_on₂ b₁ b₂ (λ l₁ l₂, by_cases
(suppose a ∈ union_list l₁ l₂, !min_count_eq this !nodup_union_list)
(suppose ¬ a ∈ union_list l₁ l₂,
assert ¬ a ∈ l₁, from not_mem_of_not_mem_union_list_left `¬ a ∈ union_list l₁ l₂`,
assert ¬ a ∈ l₂, from not_mem_of_not_mem_union_list_right `¬ a ∈ union_list l₁ l₂`,
assert n : ¬ a ∈ min_count l₁ l₂ (union_list l₁ l₂), from not_mem_min_count_of_not_mem l₁ l₂ `¬ a ∈ union_list l₁ l₂`,
begin
unfold [inter, count],
rewrite [count_eq_zero_of_not_mem `¬ a ∈ l₁`, count_eq_zero_of_not_mem `¬ a ∈ l₂`, min_self],
rewrite [count_eq_zero_of_not_mem n]
end))
lemma union.comm (b₁ b₂ : bag A) : b₁ ∪ b₂ = b₂ ∪ b₁ :=
bag.ext (λ a, by rewrite [*count_union, max.comm])
lemma union.assoc (b₁ b₂ b₃ : bag A) : (b₁ ∪ b₂) ∪ b₃ = b₁ ∪ (b₂ ∪ b₃) :=
bag.ext (λ a, by rewrite [*count_union, max.assoc])
theorem union.left_comm (s₁ s₂ s₃ : bag A) : s₁ ∪ (s₂ ∪ s₃) = s₂ ∪ (s₁ ∪ s₃) :=
!left_comm union.comm union.assoc s₁ s₂ s₃
lemma union_self (b : bag A) : b ∪ b = b :=
bag.ext (λ a, by rewrite [*count_union, max_self])
lemma union_empty (b : bag A) : b ∪ empty = b :=
bag.ext (λ a, by rewrite [*count_union, count_empty, max_zero])
lemma empty_union (b : bag A) : empty ∪ b = b :=
calc empty ∪ b = b ∪ empty : union.comm
... = b : union_empty
lemma inter.comm (b₁ b₂ : bag A) : b₁ ∩ b₂ = b₂ ∩ b₁ :=
bag.ext (λ a, by rewrite [*count_inter, min.comm])
lemma inter.assoc (b₁ b₂ b₃ : bag A) : (b₁ ∩ b₂) ∩ b₃ = b₁ ∩ (b₂ ∩ b₃) :=
bag.ext (λ a, by rewrite [*count_inter, min.assoc])
theorem inter.left_comm (s₁ s₂ s₃ : bag A) : s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃) :=
!left_comm inter.comm inter.assoc s₁ s₂ s₃
lemma inter_self (b : bag A) : b ∩ b = b :=
bag.ext (λ a, by rewrite [*count_inter, min_self])
lemma inter_empty (b : bag A) : b ∩ empty = empty :=
bag.ext (λ a, by rewrite [*count_inter, count_empty, min_zero])
lemma empty_inter (b : bag A) : empty ∩ b = empty :=
calc empty ∩ b = b ∩ empty : inter.comm
... = empty : inter_empty
lemma append_union_inter (b₁ b₂ : bag A) : (b₁ ∪ b₂) ++ (b₁ ∩ b₂) = b₁ ++ b₂ :=
bag.ext (λ a, begin
rewrite [*count_append, count_inter, count_union],
apply (or.elim (lt_or_ge (count a b₁) (count a b₂))),
{ intro H, rewrite [min_eq_left_of_lt H, max_eq_right_of_lt H, add.comm] },
{ intro H, rewrite [min_eq_right H, max_eq_left H, add.comm] }
end)
lemma inter.left_distrib (b₁ b₂ b₃ : bag A) : b₁ ∩ (b₂ ∪ b₃) = (b₁ ∩ b₂) ∪ (b₁ ∩ b₃) :=
bag.ext (λ a, begin
rewrite [*count_inter, *count_union, *count_inter],
apply (@by_cases (count a b₁ ≤ count a b₂)),
{ intro H₁₂, apply (@by_cases (count a b₂ ≤ count a b₃)),
{ intro H₂₃,
have H₁₃ : count a b₁ ≤ count a b₃, from le.trans H₁₂ H₂₃,
rewrite [max_eq_right H₂₃, min_eq_left H₁₂, min_eq_left H₁₃, max_self]},
{ intro H₂₃,
rewrite [min_eq_left H₁₂, max.comm, max_eq_right_of_lt (lt_of_not_ge H₂₃) ],
apply (@by_cases (count a b₁ ≤ count a b₃)),
{ intro H₁₃, rewrite [min_eq_left H₁₃, max_self, min_eq_left H₁₂] },
{ intro H₁₃,
rewrite [min.comm (count a b₁) (count a b₃), min_eq_left_of_lt (lt_of_not_ge H₁₃),
min_eq_left H₁₂, max.comm, max_eq_right_of_lt (lt_of_not_ge H₁₃)]}}},
{ intro H₁₂, apply (@by_cases (count a b₂ ≤ count a b₃)),
{ intro H₂₃,
rewrite [max_eq_right H₂₃],
apply (@by_cases (count a b₁ ≤ count a b₃)),
{ intro H₁₃, rewrite [min_eq_left H₁₃, min.comm, min_eq_left_of_lt (lt_of_not_ge H₁₂), max_eq_right_of_lt (lt_of_not_ge H₁₂)] },
{ intro H₁₃, rewrite [min.comm, min_eq_left_of_lt (lt_of_not_ge H₁₃), min.comm, min_eq_left_of_lt (lt_of_not_ge H₁₂), max_eq_right H₂₃] } },
{ intro H₂₃,
have H₁₃ : count a b₁ > count a b₃, from lt.trans (lt_of_not_ge H₂₃) (lt_of_not_ge H₁₂),
rewrite [max.comm, max_eq_right_of_lt (lt_of_not_ge H₂₃), min.comm, min_eq_left_of_lt (lt_of_not_ge H₁₂)],
rewrite [min.comm, min_eq_left_of_lt H₁₃, max.comm, max_eq_right_of_lt (lt_of_not_ge H₂₃)] } }
end)
lemma inter.right_distrib (b₁ b₂ b₃ : bag A) : (b₁ ∪ b₂) ∩ b₃ = (b₁ ∩ b₃) ∪ (b₂ ∩ b₃) :=
calc (b₁ ∪ b₂) ∩ b₃ = b₃ ∩ (b₁ ∪ b₂) : inter.comm
... = (b₃ ∩ b₁) ∪ (b₃ ∩ b₂) : inter.left_distrib
... = (b₁ ∩ b₃) ∪ (b₃ ∩ b₂) : inter.comm
... = (b₁ ∩ b₃) ∪ (b₂ ∩ b₃) : inter.comm
end union_inter
section subbag
variable [decA : decidable_eq A]
include decA
definition subbag (b₁ b₂ : bag A) := ∀ a, count a b₁ ≤ count a b₂
infix ⊆ := subbag
lemma subbag.refl (b : bag A) : b ⊆ b :=
take a, !le.refl
lemma subbag.trans {b₁ b₂ b₃ : bag A} : b₁ ⊆ b₂ → b₂ ⊆ b₃ → b₁ ⊆ b₃ :=
assume h₁ h₂, take a, le.trans (h₁ a) (h₂ a)
lemma subbag.antisymm {b₁ b₂ : bag A} : b₁ ⊆ b₂ → b₂ ⊆ b₁ → b₁ = b₂ :=
assume h₁ h₂, bag.ext (take a, le.antisymm (h₁ a) (h₂ a))
lemma count_le_of_subbag {b₁ b₂ : bag A} : b₁ ⊆ b₂ → ∀ a, count a b₁ ≤ count a b₂ :=
assume h, h
lemma subbag.intro {b₁ b₂ : bag A} : (∀ a, count a b₁ ≤ count a b₂) → b₁ ⊆ b₂ :=
assume h, h
lemma empty_subbag (b : bag A) : empty ⊆ b :=
subbag.intro (take a, !zero_le)
lemma eq_empty_of_subbag_empty {b : bag A} : b ⊆ empty → b = empty :=
assume h, subbag.antisymm h (empty_subbag b)
lemma union_subbag_of_subbag_of_subbag {b₁ b₂ b₃ : bag A} : b₁ ⊆ b₃ → b₂ ⊆ b₃ → b₁ ∪ b₂ ⊆ b₃ :=
assume h₁ h₂, subbag.intro (λ a, calc
count a (b₁ ∪ b₂) = max (count a b₁) (count a b₂) : by rewrite count_union
... ≤ count a b₃ : max_le (h₁ a) (h₂ a))
lemma subbag_inter_of_subbag_of_subbag {b₁ b₂ b₃ : bag A} : b₁ ⊆ b₂ → b₁ ⊆ b₃ → b₁ ⊆ b₂ ∩ b₃ :=
assume h₁ h₂, subbag.intro (λ a, calc
count a b₁ ≤ min (count a b₂) (count a b₃) : le_min (h₁ a) (h₂ a)
... = count a (b₂ ∩ b₃) : by rewrite count_inter)
lemma subbag_union_left (b₁ b₂ : bag A) : b₁ ⊆ b₁ ∪ b₂ :=
subbag.intro (take a, by rewrite [count_union]; apply le_max_left)
lemma subbag_union_right (b₁ b₂ : bag A) : b₂ ⊆ b₁ ∪ b₂ :=
subbag.intro (take a, by rewrite [count_union]; apply le_max_right)
lemma inter_subbag_left (b₁ b₂ : bag A) : b₁ ∩ b₂ ⊆ b₁ :=
subbag.intro (take a, by rewrite [count_inter]; apply min_le_left)
lemma inter_subbag_right (b₁ b₂ : bag A) : b₁ ∩ b₂ ⊆ b₂ :=
subbag.intro (take a, by rewrite [count_inter]; apply min_le_right)
lemma subbag_append_left (b₁ b₂ : bag A) : b₁ ⊆ b₁ ++ b₂ :=
subbag.intro (take a, by rewrite [count_append]; apply le_add_right)
lemma subbag_append_right (b₁ b₂ : bag A) : b₂ ⊆ b₁ ++ b₂ :=
subbag.intro (take a, by rewrite [count_append]; apply le_add_left)
lemma inter_subbag_union (b₁ b₂ : bag A) : b₁ ∩ b₂ ⊆ b₁ ∪ b₂ :=
subbag.trans (inter_subbag_left b₁ b₂) (subbag_union_left b₁ b₂)
open decidable
lemma union_subbag_append (b₁ b₂ : bag A) : b₁ ∪ b₂ ⊆ b₁ ++ b₂ :=
subbag.intro (take a, begin
rewrite [count_append, count_union],
exact (or.elim !lt_or_ge)
(suppose count a b₁ < count a b₂, by rewrite [max_eq_right_of_lt this]; apply le_add_left)
(suppose count a b₁ ≥ count a b₂, by rewrite [max_eq_left this]; apply le_add_right)
end)
lemma subbag_insert (a : A) (b : bag A) : b ⊆ insert a b :=
subbag.intro (take x, by_cases
(suppose x = a, by rewrite [this, count_insert]; apply le_succ)
(suppose x ≠ a, by rewrite [count_insert_of_ne this]))
lemma mem_of_subbag_of_mem {a : A} {b₁ b₂ : bag A} : b₁ ⊆ b₂ → a ∈ b₁ → a ∈ b₂ :=
assume h₁ h₂,
have count a b₁ ≤ count a b₂, from count_le_of_subbag h₁ a,
have count a b₁ > 0, from h₂,
show count a b₂ > 0, from lt_of_lt_of_le `0 < count a b₁` `count a b₁ ≤ count a b₂`
lemma extract_subbag (a : A) (b : bag A) : extract a b ⊆ b :=
subbag.intro (take x, by_cases
(suppose x = a, by rewrite [this, count_extract]; apply zero_le)
(suppose x ≠ a, by rewrite [count_extract_of_ne this]))
open bool
private definition subcount : list A → list A → bool
| [] l₂ := tt
| (a::l₁) l₂ := if list.count a (a::l₁) ≤ list.count a l₂ then subcount l₁ l₂ else ff
private lemma all_of_subcount_eq_tt : ∀ {l₁ l₂ : list A}, subcount l₁ l₂ = tt → ∀ a, list.count a l₁ ≤ list.count a l₂
| [] l₂ h := take x, !zero_le
| (a::l₁) l₂ h := take x,
have subcount l₁ l₂ = tt, from by_contradiction (suppose subcount l₁ l₂ ≠ tt,
assert subcount l₁ l₂ = ff, from eq_ff_of_ne_tt this,
begin unfold subcount at h, rewrite [this at h, if_t_t at h], contradiction end),
assert ih : ∀ a, list.count a l₁ ≤ list.count a l₂, from all_of_subcount_eq_tt this,
assert i : list.count a (a::l₁) ≤ list.count a l₂, from by_contradiction (suppose ¬ list.count a (a::l₁) ≤ list.count a l₂,
begin unfold subcount at h, rewrite [if_neg this at h], contradiction end),
by_cases
(suppose x = a, by rewrite this; apply i)
(suppose x ≠ a, by rewrite [list.count_cons_of_ne this]; apply ih)
private lemma ex_of_subcount_eq_ff : ∀ {l₁ l₂ : list A}, subcount l₁ l₂ = ff → ∃ a, ¬ list.count a l₁ ≤ list.count a l₂
| [] l₂ h := by contradiction
| (a::l₁) l₂ h := by_cases
(suppose i : list.count a (a::l₁) ≤ list.count a l₂,
have subcount l₁ l₂ = ff, from by_contradiction (suppose subcount l₁ l₂ ≠ ff,
assert subcount l₁ l₂ = tt, from eq_tt_of_ne_ff this,
begin
unfold subcount at h,
rewrite [if_pos i at h, this at h],
contradiction
end),
have ih : ∃ a, ¬ list.count a l₁ ≤ list.count a l₂, from ex_of_subcount_eq_ff this,
obtain w hw, from ih, by_cases
(suppose w = a, begin subst w, existsi a, rewrite list.count_cons_eq, apply not_lt_of_ge, apply le_of_lt (lt_of_not_ge hw) end)
(suppose w ≠ a, exists.intro w (by rewrite (list.count_cons_of_ne `w ≠ a`); exact hw)))
(suppose ¬ list.count a (a::l₁) ≤ list.count a l₂, exists.intro a this)
definition decidable_subbag [instance] (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) :=
quot.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂,
match subcount l₁ l₂ with
| tt := suppose subcount l₁ l₂ = tt, inl (all_of_subcount_eq_tt this)
| ff := suppose subcount l₁ l₂ = ff, inr (suppose h : (∀ a, list.count a l₁ ≤ list.count a l₂),
obtain w hw, from ex_of_subcount_eq_ff `subcount l₁ l₂ = ff`,
absurd (h w) hw)
end rfl)
end subbag
end bag

37
tests/lean/extra/show_goal_bag.sh
View file

@ -1,37 +0,0 @@
#!/bin/bash
set -e
if [ $# -ne 1 ]; then
echo "Usage: show_goal_bag.sh [lean-executable-path]"
exit 1
fi
LEAN=$1
export LEAN_PATH=../../../library:.
lines=('671' '673' '677' '661');
cols=('8' '71' '47' '20');
size=${#lines[@]}
i=0
while [ $i -lt $size ]; do
line=${lines[$i]}
col=${cols[$i]}
let i=i+1
produced=bag.$line.$col.produced.out
expected=bag.$line.$col.expected.out
if ! $LEAN --line=$line --col=$col --goal bag.lean &> $produced; then
echo "ERROR: lean failed"
exit 1
fi
if test -f $expected; then
if diff --ignore-all-space -I "executing external script" "$produced" "$expected"; then
echo "-- checked"
else
echo "ERROR: file $produced does not match $expected"
exit 1
fi
else
echo "ERROR: file $expected does not exist"
exit 1
fi
done
echo "done"

8
tests/lean/run/calc_heq_symm.lean
View file

@ -2,10 +2,10 @@ import logic
theorem tst {A B C D : Type} {a₁ a₂ : A} {b : B} {c : C} {d : D}
(H₀ : a₁ = a₂) (H₁ : a₂ == b) (H₂ : b == c) (H₃ : c == d) : d == a₁ :=
calc d == c : H₃
... == b : H₂
... == a₂ : H₁
... = a₁ : H₀
calc d == c : heq.symm H₃
... == b : heq.symm H₂
... == a₂ : heq.symm H₁
... = a₁ : eq.symm H₀
reveal tst
print definition tst

29
tests/lean/run/finbug.lean
View file

@ -1,29 +0,0 @@
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
Finite ordinals.
-/
open nat
inductive fin : nat → Type :=
| fz : Π n, fin (succ n)
| fs : Π {n}, fin n → fin (succ n)
namespace fin
definition to_nat : Π {n}, fin n → nat
| to_nat (fz n) := zero
| to_nat (@fs n f) := succ (@to_nat n f)
definition lift : Π {n : nat}, fin n → Π (m : nat), fin (add m n)
| lift (fz n) m := fz (add m n)
| lift (@fs n f) m := fs (@lift n f m)
theorem to_nat_lift : ∀ {n : nat} (f : fin n) (m : nat), to_nat f = to_nat (lift f m)
| to_nat_lift (fz n) m := rfl
| to_nat_lift (@fs n f) m := calc
to_nat (fs f) = (to_nat f) + 1 : rfl
... = (to_nat (lift f m)) + 1 : to_nat_lift f
... = to_nat (lift (fs f) m) : rfl
end fin

29
tests/lean/run/finbug2.lean
View file

@ -1,29 +0,0 @@
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
Finite ordinals.
-/
open nat
inductive fin : nat → Type :=
| fz : Π n, fin (succ n)
| fs : Π {n}, fin n → fin (succ n)
namespace fin
definition to_nat : Π {n}, fin n → nat
| @to_nat (succ n) (fz n) := zero
| @to_nat (succ n) (fs f) := succ (@to_nat n f)
definition lift : Π {n : nat}, fin n → Π (m : nat), fin (add m n)
| @lift (succ n) (fz n) m := fz (add m n)
| @lift (succ n) (@fs n f) m := fs (@lift n f m)
theorem to_nat_lift : ∀ {n : nat} (f : fin n) (m : nat), to_nat f = to_nat (lift f m)
| to_nat_lift (fz n) m := rfl
| to_nat_lift (@fs n f) m := calc
to_nat (fs f) = (to_nat f) + 1 : rfl
... = (to_nat (lift f m)) + 1 : to_nat_lift f
... = to_nat (lift (fs f) m) : rfl
end fin

194
tests/lean/run/finset.lean
View file

@ -1,194 +0,0 @@
import data.list
open list setoid quot decidable nat
namespace finset
definition eqv {A : Type} (l₁ l₂ : list A) :=
∀ a, a ∈ l₁ ↔ a ∈ l₂
infix `~` := eqv
theorem eqv.refl {A : Type} (l : list A) : l ~ l :=
λ a, !iff.refl
theorem eqv.symm {A : Type} {l₁ l₂ : list A} : l₁ ~ l₂ → l₂ ~ l₁ :=
λ H a, iff.symm (H a)
theorem eqv.trans {A : Type} {l₁ l₂ l₃ : list A} : l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃ :=
λ H₁ H₂ a, iff.trans (H₁ a) (H₂ a)
theorem eqv.is_equivalence (A : Type) : equivalence (@eqv A) :=
and.intro (@eqv.refl A) (and.intro (@eqv.symm A) (@eqv.trans A))
definition norep {A : Type} [H : decidable_eq A] : list A → list A
| [] := []
| (x :: xs) := if x ∈ xs then norep xs else x :: norep xs
definition eqv_norep {A : Type} [H : decidable_eq A] : ∀ l : list A, l ~ norep l
| [] := (λ a, iff.rfl)
| (x :: xs) :=
take y,
assert ih : xs ~ norep xs, from eqv_norep xs,
show y ∈ x :: xs ↔ y ∈ if x ∈ xs then norep xs else x :: norep xs,
begin
apply (@by_cases (x ∈ xs)),
begin
intro xin, rewrite (if_pos xin),
apply iff.intro,
{intro yinxxs, apply (or.elim (iff.mp !mem_cons_iff yinxxs)),
intro yeqx, rewrite -yeqx at xin, exact (iff.mp (ih y) xin),
intro yeqxs, exact (iff.mp (ih y) yeqxs)},
{intro yinnrep, show y ∈ x::xs, from or.inr (iff.mpr (ih y) yinnrep)}
end,
begin
intro xnin, rewrite (if_neg xnin),
apply iff.intro,
{intro yinxxs, apply (or.elim (iff.mp !mem_cons_iff yinxxs)),
intro yeqx, rewrite yeqx, apply mem_cons,
intro yinxs, show y ∈ x:: norep xs, from or.inr (iff.mp (ih y) yinxs)},
{intro yinxnrep, apply (or.elim (iff.mp !mem_cons_iff yinxnrep)),
intro yeqx, rewrite yeqx, apply mem_cons,
intro yinrep, show y ∈ x::xs, from or.inr (iff.mpr (ih y) yinrep)}
end
end
definition sub {A : Type} (l₁ l₂ : list A) := ∀ a, a ∈ l₁ → a ∈ l₂
infix ⊆ := sub
theorem eqv_of_sub_of_sub {A : Type} {l₁ l₂ : list A} : l₁ ⊆ l₂ → l₂ ⊆ l₁ → l₁ ~ l₂ :=
assume h₁ h₂ a, iff.intro (h₁ a) (h₂ a)
theorem sub_of_eqv_left {A : Type} {l₁ l₂ : list A} : l₁ ~ l₂ → l₁ ⊆ l₂ :=
assume h₁ a ainl₁, iff.mp (h₁ a) ainl₁
theorem sub_of_eqv_right {A : Type} {l₁ l₂ : list A} : l₁ ~ l₂ → l₂ ⊆ l₁ :=
assume h₁ a ainl₂, iff.mpr (h₁ a) ainl₂
definition sub_of_cons_sub {A : Type} {a : A} {l₁ l₂ : list A} : a :: l₁ ⊆ l₂ → l₁ ⊆ l₂ :=
assume s, take b, assume binl₁, s b (or.inr binl₁)
definition decidable_sub [instance] {A : Type} [H : decidable_eq A] : ∀ l₁ l₂ : list A, decidable (l₁ ⊆ l₂)
| [] ys := inl (λ a h, absurd h !not_mem_nil)
| (x::xs) ys :=
if xinys : x ∈ ys then
match decidable_sub xs ys with
| (inl xs_sub_ys) := inl (λ y yinxxs, or.elim (iff.mp !mem_cons_iff yinxxs)
(λ yeqx, by rewrite yeqx; exact xinys)
(λ yinxs, xs_sub_ys y yinxs))
| (inr nxs_sub_ys) := inr (λ h, absurd (sub_of_cons_sub h) nxs_sub_ys)
end
else
inr (λ h, absurd (h x !mem_cons) xinys)
example : [(1 : nat), 2, 3] ⊆ [1,3,4,1,2] :=
dec_trivial
definition decidable_eqv [instance] {A : Type} [H : decidable_eq A] : ∀ l₁ l₂ : list A, decidable (l₁ ~ l₂) :=
take l₁ l₂ : list A,
match decidable_sub l₁ l₂ with
| (inl s₁) :=
match decidable_sub l₂ l₁ with
| (inl s₂) := inl (eqv_of_sub_of_sub s₁ s₂)
| (inr n₂) := inr (λ h, absurd (sub_of_eqv_right h) n₂)
end
| (inr n₁) := inr (λ h, absurd (sub_of_eqv_left h) n₁)
end
example : [(1:nat), 2, 3, 2, 2, 2] ~ [1,3,3,1,2] :=
dec_trivial
definition finset_setoid [instance] (A : Type) : setoid (list A) :=
setoid.mk (@eqv A) (eqv.is_equivalence A)
definition finset (A : Type) : Type :=
quot (finset_setoid A)
definition has_decidable_eq [instance] {A : Type} [H : decidable_eq A] : ∀ s₁ s₂ : finset A, decidable (s₁ = s₂) :=
take s₁ s₂, quot.rec_on_subsingleton₂ s₁ s₂
(take l₁ l₂,
match decidable_eqv l₁ l₂ with
| inl e := inl (quot.sound e)
| inr d := inr (λ e, absurd (quot.exact e) d)
end)
definition to_finset {A : Type} (l : list A) : finset A :=
⟦l⟧
definition mem {A : Type} (a : A) (s : finset A) : Prop :=
quot.lift_on s
(λ l : list A, a ∈ l)
(λ l₁ l₂ r, propext (r a))
infix ∈ := mem
theorem mem_list {A : Type} {a : A} {l : list A} : a ∈ l → a ∈ ⟦l⟧ :=
λ H, H
definition empty {A : Type} : finset A :=
⟦nil⟧
notation `∅` := empty
definition union {A : Type} (s₁ s₂ : finset A) : finset A :=
quot.lift_on₂ s₁ s₂
(λ l₁ l₂ : list A, ⟦l₁ ++ l₂⟧)
(λ l₁ l₂ l₃ l₄ r₁ r₂,
begin
apply quot.sound,
intro a,
apply iff.intro,
begin
intro inl₁l₂,
apply (or.elim (mem_or_mem_of_mem_append inl₁l₂)),
intro inl₁, exact (mem_append_of_mem_or_mem (or.inl (iff.mp (r₁ a) inl₁))),
intro inl₂, exact (mem_append_of_mem_or_mem (or.inr (iff.mp (r₂ a) inl₂)))
end,
begin
intro inl₃l₄,
apply (or.elim (mem_or_mem_of_mem_append inl₃l₄)),
intro inl₃, exact (mem_append_of_mem_or_mem (or.inl (iff.mpr (r₁ a) inl₃))),
intro inl₄, exact (mem_append_of_mem_or_mem (or.inr (iff.mpr (r₂ a) inl₄)))
end,
end)
infix `∪` := union
theorem mem_union_left {A : Type} (s₁ s₂ : finset A) (a : A) : a ∈ s₁ → a ∈ s₁ ∪ s₂ :=
quot.ind₂ (λ l₁ l₂ ainl₁, mem_append_left l₂ ainl₁) s₁ s₂
theorem mem_union_right {A : Type} (s₁ s₂ : finset A) (a : A) : a ∈ s₂ → a ∈ s₁ ∪ s₂ :=
quot.ind₂ (λ l₁ l₂ ainl₂, mem_append_right l₁ ainl₂) s₁ s₂
theorem union_empty {A : Type} (s : finset A) : s ∪ ∅ = s :=
quot.induction_on s (λ l, quot.sound (λ a, by rewrite append_nil_right))
theorem empty_union {A : Type} (s : finset A) : ∅ ∪ s = s :=
quot.induction_on s (λ l, quot.sound (λ a, by rewrite append_nil_left))
example : to_finset ((1:nat)::2::nil) ∪ to_finset (2::3::nil) = ⟦1 :: 2 :: 2 :: 3 :: nil⟧ :=
rfl
example : to_finset [(1:nat), 1, 2, 3] = to_finset [2, 3, 1, 2, 2, 3] :=
dec_trivial
example : to_finset [(1:nat), 1, 4, 2, 3] ≠ to_finset [2, 3, 1, 2, 2, 3] :=
dec_trivial
definition clean {A : Type} [H : decidable_eq A] (s : finset A) : finset A :=
quot.lift_on s (λ l, ⟦norep l⟧)
(λ l₁ l₂ e, calc
⟦norep l₁⟧ = ⟦l₁⟧ : quot.sound (eqv_norep l₁)
... = ⟦l₂⟧ : quot.sound e
... = ⟦norep l₂⟧ : quot.sound (eqv_norep l₂))
theorem eq_clean {A : Type} [H : decidable_eq A] : ∀ s : finset A, clean s = s :=
take s, quot.induction_on s (λ l, eq.symm (quot.sound (eqv_norep l)))
theorem eq_of_clean_eq_clean {A : Type} [H : decidable_eq A] : ∀ s₁ s₂ : finset A, clean s₁ = clean s₂ → s₁ = s₂ :=
take s₁ s₂, by rewrite *eq_clean; intro H; apply H
example : to_finset [(1:nat), 1, 2, 3] = to_finset [1, 2, 2, 2, 3, 3] :=
!eq_of_clean_eq_clean rfl
end finset

20
tests/lean/run/group4.lean
View file

@ -109,15 +109,15 @@ section examples
theorem test1 {S : Semigroup} (a b c d : S) : a * (b * c) * d = a * b * (c * d) :=
calc
a * (b * c) * d = a * b * c * d : mul_assoc
... = a * b * (c * d) : mul_assoc
a * (b * c) * d = a * b * c * d : by rewrite -mul_assoc
... = a * b * (c * d) : by rewrite mul_assoc
theorem test2 {M : CommSemigroup} (a b : M) : a * b = a * b := rfl
theorem test3 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) :=
calc
a * (b * c) * d = a * b * c * d : mul_assoc
... = a * b * (c * d) : mul_assoc
a * (b * c) * d = a * b * c * d : by rewrite -mul_assoc
... = a * b * (c * d) : by rewrite mul_assoc
-- for test4b to work, we need instances at the level of the bundled structures as well
definition Monoid_Semigroup [coercion] [reducible] (M : Monoid) : Semigroup :=
@ -129,20 +129,20 @@ test1 a b c d
theorem test5 {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
calc
a * 1 * b * c = a * b * c : by rewrite mul_right_id
... = a * (b * c) : mul_assoc
... = a * (b * c) : by rewrite mul_assoc
theorem test5a {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
calc
a * 1 * b * c = a * b * c : by rewrite mul_right_id
... = a * (b * c) : mul_assoc
... = a * (b * c) : by rewrite mul_assoc
theorem test5b {A : Type} {M : monoid A} (a b c : A) : a * 1 * b * c = a * (b * c) :=
calc
a * 1 * b * c = a * b * c : mul_right_id
... = a * (b * c) : mul_assoc
a * 1 * b * c = a * b * c : by rewrite mul_right_id
... = a * (b * c) : by rewrite mul_assoc
theorem test6 {M : CommMonoid} (a b c : M) : a * 1 * b * c = a * (b * c) :=
calc
a * 1 * b * c = a * b * c : mul_right_id
... = a * (b * c) : mul_assoc
a * 1 * b * c = a * b * c : by rewrite mul_right_id
... = a * (b * c) : by rewrite mul_assoc
end examples

4
tests/lean/run/imp_curly.lean
View file

@ -6,5 +6,5 @@ nat.induction_on n
!nat.add_zero
(take m IH, show 0 + succ m = succ m, from
calc
0 + succ m = succ (0 + m) : add_succ
... = succ m : IH)
0 + succ m = succ (0 + m) : by rewrite add_succ
... = succ m : by rewrite IH)

2
tests/lean/run/local_eqns.lean
View file

@ -30,7 +30,7 @@ theorem add_eq_addl : ∀ x y, x + y = x ⊕ y
| 0 := rfl
| (succ a) := calc
(succ a) ⊕ 0 = succ (a ⊕ 0) : rfl
... = succ a : addl_z,
... = succ a : by rewrite addl_z,
rewrite addl_z
end
| 0 (succ y) :=

2
tests/lean/run/mul_zero.lean
View file

@ -2,4 +2,4 @@ import data.nat
open nat
example (x : ℕ) : 0 = x * 0 :=
calc 0 = x * 0 : nat.mul_zero
calc 0 = x * 0 : by rewrite nat.mul_zero

4
tests/lean/run/nested_rec.lean
View file

@ -35,6 +35,6 @@ theorem g_all_zero (a : nat) : g a = zero :=
nat.induction_on a
g_zero
(λ a₁ (ih : g a₁ = 0), calc
g (succ a₁) = g (g a₁) : g_succ
... = g 0 : ih
g (succ a₁) = g (g a₁) : !g_succ
... = g 0 : by rewrite ih
... = 0 : g_zero)

2
tests/lean/run/refine3.lean
View file

@ -9,6 +9,6 @@ nat.induction_on n
refine
(calc
0 + succ m = succ (0 + m) : _
... = succ m : IH),
... = succ m : by rewrite IH),
esimp
end)