From 153e3927acd33825c7c5fa499e117de2f901867d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 1 Oct 2014 18:50:17 -0700 Subject: [PATCH] feat(frontends/lean/elaborator): modify '!' semantics: it stops consuming arguments as soon it finds an argument that does not occur in the rest of the type. --- doc/lean/calc.org | 2 +- library/data/int/order.lean | 2 +- library/data/nat/basic.lean | 12 ++++++------ library/data/nat/div.lean | 2 +- library/data/nat/order.lean | 2 +- library/data/vector.lean | 4 ++-- src/frontends/lean/elaborator.cpp | 12 +++++++++++- tests/lean/run/occurs_check_bug1.lean | 2 +- 8 files changed, 24 insertions(+), 14 deletions(-) diff --git a/doc/lean/calc.org b/doc/lean/calc.org index 3864ec4fe..7d6d179d1 100644 --- a/doc/lean/calc.org +++ b/doc/lean/calc.org @@ -60,7 +60,7 @@ some form of transitivity. It can even combine different relations. := calc a = b : H1 ... = c + 1 : H2 ... = succ c : add.one c - ... ≠ 0 : succ_ne_zero + ... ≠ 0 : succ_ne_zero c #+END_SRC The Lean simplifier can be used to reduce the size of calculational proofs. diff --git a/library/data/int/order.lean b/library/data/int/order.lean index ab2a39c3e..bd3a5b2e9 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -227,7 +227,7 @@ not_intro ... = a + 0 : by simp, have H3 : succ n = 0, from add_cancel_left H2, have H4 : succ n = 0, from of_nat_inj H3, - absurd H4 succ_ne_zero) + absurd H4 !succ_ne_zero) theorem lt_imp_ne {a b : ℤ} (H : a < b) : a ≠ b := not_intro (assume H2 : a = b, absurd (H2 ▸ H) (lt_irrefl b)) diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index 7cd93bb43..6e9980ac2 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -54,7 +54,7 @@ num.rec zero -- Successor and predecessor -- ------------------------- -theorem succ_ne_zero {n : ℕ} : succ n ≠ 0 := +theorem succ_ne_zero (n : ℕ) : succ n ≠ 0 := assume H : succ n = 0, have H2 : true = false, from let f := (nat.rec false (fun a b, true)) in @@ -101,7 +101,7 @@ calc theorem succ.ne_self {n : ℕ} : succ n ≠ n := induction_on n (take H : 1 = 0, - have ne : 1 ≠ 0, from succ_ne_zero, + have ne : 1 ≠ 0, from !succ_ne_zero, absurd H ne) (take k IH H, IH (succ.inj H)) @@ -112,10 +112,10 @@ have general : ∀n, decidable (n = m), from (take n, rec_on n (inl rfl) - (λ m iH, inr succ_ne_zero)) + (λ m iH, inr !succ_ne_zero)) (λ (m' : ℕ) (iH1 : ∀n, decidable (n = m')), take n, rec_on n - (inr (ne.symm succ_ne_zero)) + (inr (ne.symm !succ_ne_zero)) (λ (n' : ℕ) (iH2 : decidable (n' = succ m')), decidable.by_cases (assume Heq : n' = m', inl (congr_arg succ Heq)) @@ -230,7 +230,7 @@ induction_on n (show succ (k + m) = 0, from calc succ (k + m) = succ k + m : !add.succ_left⁻¹ ... = 0 : H) - succ_ne_zero) + !succ_ne_zero) theorem add.eq_zero_right {n m : ℕ} (H : n + m = 0) : m = 0 := add.eq_zero_left (!add.comm ⬝ H) @@ -357,6 +357,6 @@ discriminate ... = succ k * succ l : {Hk} ... = k * succ l + succ l : !mul.succ_left ... = succ (k * succ l + l) : !add.succ_right)⁻¹, - absurd (Heq ⬝ H) succ_ne_zero)) + absurd (Heq ⬝ H) !succ_ne_zero)) end nat diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index 1f5f2e615..76d670b52 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -657,7 +657,7 @@ have aux : ∀m, P m n, from aux m theorem gcd_succ (m n : ℕ) : gcd m (succ n) = gcd (succ n) (m mod succ n) := -gcd_def _ _ ⬝ if_neg succ_ne_zero +!gcd_def ⬝ if_neg !succ_ne_zero theorem gcd_one (n : ℕ) : gcd n 1 = 1 := sorry -- (by simp) (gcd_succ n 0) diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 67ec3c66c..7eb360d18 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -48,7 +48,7 @@ theorem not_succ_zero_le {n : ℕ} : ¬ succ n ≤ 0 := not_intro (assume H : succ n ≤ 0, have H2 : succ n = 0, from le_zero H, - absurd H2 succ_ne_zero) + absurd H2 !succ_ne_zero) theorem le_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k := obtain (l1 : ℕ) (Hl1 : n + l1 = m), from le_elim H1, diff --git a/library/data/vector.lean b/library/data/vector.lean index 361a789a0..9214e4410 100644 --- a/library/data/vector.lean +++ b/library/data/vector.lean @@ -39,7 +39,7 @@ namespace vector ∀ H : n = 0, C (cast (congr_arg (vector T) H) v) := rec_on v (take H : 0 = 0, (eq.rec Hnil (cast_eq _ nil⁻¹))) (take (x : T) (n : ℕ) (w : vector T n) IH (H : succ n = 0), - false.rec_type _ (absurd H succ_ne_zero)) + false.rec_type _ (absurd H !succ_ne_zero)) theorem case_zero {C : vector T 0 → Type} (v : vector T 0) (Hnil : C nil) : C v := eq.rec (case_zero_lem v Hnil (eq.refl 0)) (cast_eq _ v) @@ -47,7 +47,7 @@ namespace vector private theorem rec_nonempty_lem {C : Π{n}, vector T (succ n) → Type} {n : ℕ} (v : vector T n) (Hone : Πa, C [a]) (Hcons : Πa {n} (v : vector T (succ n)), C v → C (a :: v)) : ∀{m} (H : n = succ m), C (cast (congr_arg (vector T) H) v) := - case_on v (take m (H : 0 = succ m), false.rec_type _ (absurd (H⁻¹) succ_ne_zero)) + case_on v (take m (H : 0 = succ m), false.rec_type _ (absurd (H⁻¹) !succ_ne_zero)) (take x n v m H, have H2 : C (x::v), from sorry, diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 0a297989c..c6efd459d 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -19,6 +19,7 @@ Author: Leonardo de Moura #include "kernel/replace_fn.h" #include "kernel/kernel_exception.h" #include "kernel/error_msgs.h" +#include "kernel/free_vars.h" #include "kernel/expr_maps.h" #include "library/coercion.h" #include "library/placeholder.h" @@ -842,7 +843,16 @@ public: expr r_type = whnf(infer_type(r, cs), cs); expr imp_arg; bool is_strict = true; - while (is_pi(r_type) && (consume_args || binding_info(r_type).is_implicit())) { + while (is_pi(r_type)) { + if (!binding_info(r_type).is_implicit()) { + if (!consume_args) + break; + if (!has_free_var(binding_body(r_type), 0)) { + // if the rest of the type does not reference argument, + // then we also stop consuming arguments + break; + } + } imp_arg = mk_placeholder_meta(some_expr(binding_domain(r_type)), g, is_strict, cs); r = mk_app(r, imp_arg, g); r_type = whnf(instantiate(binding_body(r_type), imp_arg), cs); diff --git a/tests/lean/run/occurs_check_bug1.lean b/tests/lean/run/occurs_check_bug1.lean index a2b63bba6..e40662a25 100644 --- a/tests/lean/run/occurs_check_bug1.lean +++ b/tests/lean/run/occurs_check_bug1.lean @@ -14,4 +14,4 @@ theorem gcd_def (x y : ℕ) : gcd x y = @ite (y = 0) (nat.has_decidable_eq (pr2 sorry theorem gcd_succ (m n : ℕ) : gcd m (succ n) = gcd (succ n) (m mod succ n) := -eq.trans (gcd_def _ _) (if_neg succ_ne_zero) +eq.trans (gcd_def _ _) (if_neg !succ_ne_zero)