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

refactor(frontends/lean/calc): remove '{}' notation for eq.subst in calc mode

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-03 14:18:20 -08:00
parent d7de521126
commit 2c70ca83a8
19 changed files with 55 additions and 130 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -405,7 +405,7 @@ list.rec_on l
calc
find x (y::l) = if x = y then 0 else succ (find x l) : !find_cons
... = succ (find x l) : if_neg (and.elim_left this)
... = succ (length l) : {iH (and.elim_right this)}
... = succ (length l) : by rewrite (iH (and.elim_right this))
... = length (y::l) : !length_cons⁻¹)
lemma find_le_length : ∀ {a} {l : list T}, find a l ≤ length l

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

@ -70,11 +70,11 @@ theorem length_map [simp] (f : A → B) : ∀ l : list A, length (map f l) = len
by rewrite (length_map l)
theorem map_ne_nil_of_ne_nil (f : A → B) {l : list A} (H : l ≠ nil) : map f l ≠ nil :=
suppose map f l = nil,
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 : length_nil
... = length (map f l) : {eq.symm `map f l = nil`}
0 = length (@nil B) : 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),
H this
@ -369,7 +369,7 @@ theorem length_mapAccumR
length (pr₂ (mapAccumR f x s)) = length x
| f (a::x) s := calc
length (pr₂ (mapAccumR f (a::x) s))
= length x + 1 : { length_mapAccumR f x s }
= length x + 1 : by rewrite -(length_mapAccumR f x s)
... = length (a::x) : rfl
| f [] s := calc
length (pr₂ (mapAccumR f [] s))

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

@ -30,16 +30,16 @@ nat.induction_on x
rfl
(λ y₁ ih, calc
0 + succ y₁ = succ (0 + y₁) : rfl
... = succ (0 ⊕ y₁) : {ih}
... = succ (0 ⊕ y₁) : by rewrite ih
... = 0 ⊕ (succ y₁) : rfl))
(λ x₁ ih₁ y, nat.induction_on y
(calc
succ x₁ + 0 = succ (x₁ + 0) : rfl
... = succ (x₁ ⊕ 0) : {ih₁ 0}
... = succ (x₁ ⊕ 0) : by rewrite (ih₁ 0)
... = succ x₁ ⊕ 0 : rfl)
(λ y₁ ih₂, calc
succ x₁ + succ y₁ = succ (succ x₁ + y₁) : rfl
... = succ (succ x₁ ⊕ y₁) : {ih₂}
... = succ (succ x₁ ⊕ y₁) : by rewrite ih₂
... = succ x₁ ⊕ succ y₁ : addl_succ_right))
/- successor and predecessor -/

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

@ -43,7 +43,7 @@ theorem add_div_self (x : ℕ) {z : ℕ} (H : z > 0) : (x + z) / z = succ (x / z
calc
(x + z) / z = if 0 < z ∧ z ≤ x + z then (x + z - z) / z + 1 else 0 : !div_def
... = (x + z - z) / z + 1 : if_pos (and.intro H (le_add_left z x))
... = succ (x / z) : {!nat.add_sub_cancel}
... = succ (x / z) : by rewrite nat.add_sub_cancel
theorem add_div_self_left {x : ℕ} (z : ℕ) (H : x > 0) : (x + z) / x = succ (z / x) :=
!add.comm ▸ !add_div_self H
@ -551,7 +551,7 @@ calc
by rewrite [mul.comm m, nat.mul_sub_right_distrib]
... = ((n - k / m - 1) * m + m - (k % m + 1)) / m :
by rewrite [H3 at {1}, right_distrib, nat.one_mul]
... = ((n - k / m - 1) * m + (m - (k % m + 1))) / m : {nat.add_sub_assoc H5 _}
... = ((n - k / m - 1) * m + (m - (k % m + 1))) / m : by rewrite (nat.add_sub_assoc H5 _)
... = (m - (k % m + 1)) / m + (n - k / m - 1) :
by rewrite [add.comm, (add_mul_div_self H4)]
... = n - k / m - 1 :

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

@ -303,7 +303,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) : {sub_eq_zero_of_le H}
dist n m = 0 + (m - n) : by rewrite -(sub_eq_zero_of_le H)
... = m - n : zero_add
theorem dist_eq_sub_of_lt {n m : ℕ} (H : n < m) : dist n m = m - n :=
@ -337,7 +337,7 @@ begin rewrite [add.comm k n, add.comm k m]; apply dist_add_add_right end
theorem dist_add_eq_of_ge {n m : ℕ} (H : n ≥ m) : dist n m + m = n :=
calc
dist n m + m = n - m + m : {dist_eq_sub_of_ge H}
dist n m + m = n - m + m : by rewrite (dist_eq_sub_of_ge H)
... = n : nat.sub_add_cancel H
theorem dist_eq_intro {n m k l : ℕ} (H : n + m = k + l) : dist n k = dist l m :=

2
library/init/funext.lean
View file

@ -52,7 +52,7 @@ section
theorem funext {f₁ f₂ : Πx : A, B x} : (∀x, f₁ x = f₂ x) → f₁ = f₂ :=
assume H, calc
f₁ = extfun_app ⟦f₁⟧ : rfl
... = extfun_app ⟦f₂⟧ : {sound H}
... = extfun_app ⟦f₂⟧ : by rewrite (@sound _ _ f₁ f₂ H)
... = f₂ : rfl
end

4
library/init/logic.lean
View file

@ -229,8 +229,8 @@ 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 : {proof_irrel (eq.refl A) (eq.refl A ⬝ eq.refl A)}
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))
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)

8
library/logic/identities.lean
View file

@ -12,13 +12,13 @@ open decidable
theorem or.right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
calc
(a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or.assoc
... ↔ a ∨ (c ∨ b) : {or.comm}
... ↔ a ∨ (c ∨ b) : by rewrite (@or.comm b c)
... ↔ (a ∨ c) ∨ b : iff.symm or.assoc
theorem and.right_comm (a b c : Prop) : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b :=
calc
(a ∧ b) ∧ c ↔ a ∧ (b ∧ c) : and.assoc
... ↔ a ∧ (c ∧ b) : {and.comm}
... ↔ a ∧ (c ∧ b) : by rewrite (@and.comm b c)
... ↔ (a ∧ c) ∧ b : iff.symm and.assoc
theorem or_not_self_iff (a : Prop) [D : decidable a] : a ∨ ¬ a ↔ true :=
@ -70,9 +70,9 @@ iff.intro
theorem not_implies_iff_and_not (a b : Prop) [Da : decidable a] :
¬(a → b) ↔ a ∧ ¬b :=
calc
¬(a → b) ↔ ¬(¬a ∨ b) : {imp_iff_not_or a b}
¬(a → b) ↔ ¬(¬a ∨ b) : by rewrite (imp_iff_not_or a b)
... ↔ ¬¬a ∧ ¬b : not_or_iff_not_and_not
... ↔ a ∧ ¬b : {not_not_iff a}
... ↔ 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 :=
iff.mp !not_implies_iff_and_not H

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

@ -88,31 +88,10 @@ static expr mk_op_fn(parser & p, name const & op, unsigned num_placeholders, pos
static void parse_calc_proof(parser & p, buffer<calc_pred> const & preds, std::vector<calc_step> & steps) {
steps.clear();
auto pos = p.pos();
p.check_token_next(get_colon_tk(), "invalid 'calc' expression, ':' expected");
if (p.curr_is_token(get_lcurly_tk())) {
p.next();
environment const & env = p.env();
expr pr = p.parse_expr();
p.check_token_next(get_rcurly_tk(), "invalid 'calc' expression, '}' expected");
for (auto const & pred : preds) {
if (auto refl_it = get_refl_extra_info(env, pred_op(pred))) {
if (auto subst_it = get_subst_extra_info(env, pred_op(pred))) {
expr refl = mk_op_fn(p, refl_it->m_name, refl_it->m_num_args-1, pos);
expr refl_pr = p.mk_app(refl, pred_lhs(pred), pos);
expr subst = mk_op_fn(p, subst_it->m_name, subst_it->m_num_args-2, pos);
expr subst_pr = p.mk_app({subst, pr, refl_pr}, pos);
steps.emplace_back(pred, subst_pr);
}
}
}
if (steps.empty())
throw parser_error("invalid 'calc' expression, reflexivity and/or substitution rule is not defined for operator", pos);
} else {
expr pr = p.parse_expr();
for (auto const & pred : preds)
steps.emplace_back(pred, mk_calc_annotation(pr));
}
expr pr = p.parse_expr();
for (auto const & pred : preds)
steps.emplace_back(pred, mk_calc_annotation(pr));
}
/** \brief Collect distinct rhs's */

2
tests/lean/K_bug.lean
View file

@ -12,7 +12,7 @@ theorem pred_succ (n : Nat) : pred (succ n) = n := rfl
theorem succ.inj {n m : Nat} (H : succ n = succ m) : n = m
:= calc
n = pred (succ n) : pred_succ n
... = pred (succ m) : {H}
... = pred (succ m) : by rewrite H
... = m : pred_succ m
end Nat

4
tests/lean/interactive/eq2.lean
View file

@ -122,8 +122,8 @@ theorem congr_arg2_dep {A : Type} {B : A → Type} {C : Type} {a₁ a₂ : A}
eq.drec_on H₁
(λ (b₂ : B a₁) (H₁ : a₁ = a₁) (H₂ : eq.drec_on H₁ b₁ = b₂),
calc
f a₁ b₁ = f a₁ (eq.drec_on H₁ b₁) : {(eq.drec_on_id H₁ b₁)⁻¹}
... = f a₁ b₂ : {H₂})
f a₁ b₁ = f a₁ (eq.drec_on H₁ b₁) : sorry -- {(eq.drec_on_id H₁ b₁)⁻¹}
... = f a₁ b₂ : sorry)
b₂ H₁ H₂

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

@ -51,7 +51,7 @@ theorem not_zero_add (x y : nat) (H : ¬ is_zero y) : ¬ is_zero (x + y)
:= exists.elim (is_not_zero_to_eq H)
(λ (w : nat) (Hw : y = succ w),
have H1 : x + y = succ (x + w), from
calc x + y = x + succ w : {Hw}
calc x + y = x + succ w : by rewrite Hw
... = succ (x + w) : refl _,
have H2 : ¬ is_zero (succ (x + w)), from
not_is_zero_succ (x+w),

12
tests/lean/run/group3.lean
View file

@ -217,14 +217,14 @@ 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 : {symm !mul_assoc}
a * (b * c) * d = a * b * c * d : by rewrite -mul_assoc
... = a * b * (c * d) : !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 : {symm !mul_assoc}
a * (b * c) * d = a * b * c * d : by rewrite -mul_assoc
... = a * b * (c * d) : !mul_assoc
-- for test4b to work, we need instances at the level of the bundled structures as well
@ -236,21 +236,21 @@ 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 : {!mul_right_id}
a * 1 * b * c = a * b * c : by rewrite mul_right_id
... = a * (b * c) : !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 : {!mul_right_id}
a * 1 * b * c = a * b * c : by rewrite mul_right_id
... = a * (b * c) : !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 * 1 * b * c = a * b * c : by rewrite mul_right_id
... = a * (b * c) : !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 * 1 * b * c = a * b * c : by rewrite mul_right_id
... = a * (b * c) : !mul_assoc
end examples

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

@ -128,12 +128,12 @@ 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 : {!mul_right_id}
a * 1 * b * c = a * b * c : by rewrite mul_right_id
... = a * (b * c) : 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 : {!mul_right_id}
a * 1 * b * c = a * b * c : by rewrite mul_right_id
... = a * (b * c) : mul_assoc
theorem test5b {A : Type} {M : monoid A} (a b c : A) : a * 1 * b * c = a * (b * c) :=

10
tests/lean/run/group5.lean
View file

@ -107,14 +107,14 @@ 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 : {symm !mul_assoc}
a * (b * c) * d = a * b * c * d : by rewrite -mul_assoc
... = a * b * (c * d) : !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 : {symm !mul_assoc}
a * (b * c) * d = a * b * c * d : by rewrite -mul_assoc
... = a * b * (c * d) : !mul_assoc
-- for test4b to work, we need instances at the level of the bundled structures as well
@ -126,17 +126,17 @@ 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 : {!mul_right_id}
a * 1 * b * c = a * b * c : by rewrite mul_right_id
... = a * (b * c) : !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 : {!mul_right_id}
a * 1 * b * c = a * b * c : by rewrite mul_right_id
... = a * (b * c) : !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 * 1 * b * c = a * b * c : by rewrite mul_right_id
... = a * (b * c) : !mul_assoc
end examples

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

@ -17,7 +17,7 @@ theorem cons_ne_nil {A : Type} (a : A) (l : list A) : ¬ cons a l = nil
:= not.intro (assume H : cons a l = nil,
absurd
(calc true = is_nil (@nil A) : refl _
... = is_nil (cons a l) : { symm H }
... = is_nil (cons a l) : by rewrite H
... = false : refl _)
true_ne_false)

10
tests/lean/run/nat_bug5.lean
View file

@ -26,11 +26,11 @@ theorem mul_add_distr_left (n m k : nat) : (n + m) * k = n * k + m * k
(take l IH,
calc
(n + m) * succ l = (n + m) * l + (n + m) : mul_succ_right _ _
... = n * l + m * l + (n + m) : {IH}
... = n * l + m * l + (n + m) : by rewrite IH
... = n * l + m * l + n + m : symm (add_assoc _ _ _)
... = n * l + n + m * l + m : {add_right_comm _ _ _}
... = n * l + n + (m * l + m) : add_assoc _ _ _
... = n * succ l + (m * l + m) : {symm (mul_succ_right _ _)}
... = n * succ l + m * succ l : {symm (mul_succ_right _ _)})
... = n * l + n + m * l + m : by rewrite (add_right_comm _ (m*l))
... = n * l + n + (m * l + m) : add_assoc _ _ _
... = n * succ l + (m * l + m) : by rewrite mul_succ_right
... = n * succ l + m * succ l : by rewrite mul_succ_right)
end nat
end foo

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

@ -29,7 +29,7 @@ theorem g_succ (a : nat) : g (succ a) = g (g a) :=
have aux : well_founded.fix g.F (succ a) = sigma.mk (g (g a)) _, from
well_founded.fix_eq g.F (succ a),
calc g (succ a) = pr₁ (well_founded.fix g.F (succ a)) : rfl
... = g (g a) : {aux}
... = g (g a) : by rewrite aux
theorem g_all_zero (a : nat) : g a = zero :=
nat.induction_on a

72
tests/lean/slow/list_elab2.lean
View file

@ -75,27 +75,14 @@ list_induction_on s (refl _)
H ▸ refl _)
theorem concat_assoc2 (s t u : list T) : s ++ t ++ u = s ++ (t ++ u) :=
list_induction_on s (refl _)
(take x l,
assume H : concat (concat l t) u = concat l (concat t u),
calc concat (concat (cons x l) t) u = cons x (concat (concat l t) u) : refl _
... = concat (cons x l) (concat t u) : { H })
sorry
theorem concat_assoc3 (s t u : list T) : s ++ t ++ u = s ++ (t ++ u) :=
list_induction_on s (refl _)
(take x l,
assume H : concat (concat l t) u = concat l (concat t u),
calc concat (concat (cons x l) t) u = cons x (concat l (concat t u)) : { H }
... = concat (cons x l) (concat t u) : refl _)
sorry
theorem concat_assoc4 (s t u : list T) : s ++ t ++ u = s ++ (t ++ u) :=
list_induction_on s (refl _)
(take x l,
assume H : concat (concat l t) u = concat l (concat t u),
calc
concat (concat (cons x l) t) u = cons x (concat (concat l t) u) : refl _
... = cons x (concat l (concat t u)) : { H }
... = concat (cons x l) (concat t u) : refl _)
sorry
-- Length
-- ------
@ -108,18 +95,7 @@ theorem length_nil : length (@nil T) = zero := refl _
theorem length_cons (x : T) (t : list T) : length (x :: t) = succ (length t) := refl _
theorem length_concat (s t : list T) : length (s ++ t) = length s + length t :=
list_induction_on s
(calc
length (concat nil t) = length t : refl _
... = 0 + length t : {symm !zero_add}
... = length (@nil T) + length t : refl _)
(take x s,
assume H : length (concat s t) = length s + length t,
calc
length (concat (cons x s) t ) = succ (length (concat s t)) : refl _
... = succ (length s + length t) : { H }
... = succ (length s) + length t : {symm !succ_add}
... = length (cons x s) + length t : refl _)
sorry
-- Reverse
-- -------
@ -133,30 +109,11 @@ theorem reverse_cons (x : T) (l : list T) : reverse (x :: l) = (reverse l) ++ (c
-- opaque_hint (hiding reverse)
theorem reverse_concat (s t : list T) : reverse (s ++ t) = (reverse t) ++ (reverse s) :=
list_induction_on s
(calc
reverse (concat nil t) = reverse t : { nil_concat _ }
... = concat (reverse t) nil : symm (concat_nil _)
... = concat (reverse t) (reverse nil) : {symm (reverse_nil)})
(take x l,
assume H : reverse (concat l t) = concat (reverse t) (reverse l),
calc
reverse (concat (cons x l) t) = concat (reverse (concat l t)) (cons x nil) : refl _
... = concat (concat (reverse t) (reverse l)) (cons x nil) : { H }
... = concat (reverse t) (concat (reverse l) (cons x nil)) : concat_assoc _ _ _
... = concat (reverse t) (reverse (cons x l)) : refl _)
sorry
-- -- add_rewrite length_nil length_cons
theorem reverse_reverse (l : list T) : reverse (reverse l) = l :=
list_induction_on l (refl _)
(take x l',
assume H: reverse (reverse l') = l',
show reverse (reverse (cons x l')) = cons x l', from
calc
reverse (reverse (cons x l')) =
concat (reverse (cons x nil)) (reverse (reverse l')) : {reverse_concat _ _}
... = cons x l' : {H})
sorry
-- Append
-- ------
@ -175,18 +132,7 @@ list_induction_on l (refl _)
P ▸ refl _)
theorem append_eq_reverse_cons (x : T) (l : list T) : append x l = reverse (x :: reverse l) :=
list_induction_on l
(calc
append x nil = [x] : (refl _)
... = concat nil [x] : {symm (nil_concat _)}
... = concat (reverse nil) [x] : {symm (reverse_nil)}
... = reverse [x] : {symm (reverse_cons _ _)}
... = reverse (x :: (reverse nil)) : {symm (reverse_nil)})
(take y l',
assume H : append x l' = reverse (x :: reverse l'),
calc
append x (y :: l') = (y :: l') ++ [ x ] : append_eq_concat _ _
... = concat (reverse (reverse (y :: l'))) [ x ] : {symm (reverse_reverse _)}
... = reverse (x :: (reverse (y :: l'))) : refl _)
sorry
end
end list