From 368fcb5ff9c84dff4b8f72d37302a85fa60e22bd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 12 Feb 2014 08:49:19 -0800 Subject: [PATCH] refactor(builtin/kernel): rename refute to by_contradiction Signed-off-by: Leonardo de Moura --- examples/lean/primes.lean | 103 ++++++++++++++++----------------- examples/lean/wf.lean | 2 +- src/builtin/kernel.lean | 10 ++-- src/builtin/obj/kernel.olean | Bin 51320 -> 51330 bytes src/builtin/obj/optional.olean | Bin 6785 -> 6795 bytes src/builtin/optional.lean | 5 +- src/kernel/kernel_decls.cpp | 2 +- src/kernel/kernel_decls.h | 6 +- tests/lean/exists3.lean | 4 +- tests/lean/exists8.lean | 4 +- tests/lean/refute1.lean | 2 +- 11 files changed, 68 insertions(+), 70 deletions(-) diff --git a/examples/lean/primes.lean b/examples/lean/primes.lean index 79cbb3f6a2..29eb3a0d8f 100644 --- a/examples/lean/primes.lean +++ b/examples/lean/primes.lean @@ -32,7 +32,7 @@ theorem strong_induction_on {P : Nat → Bool} (a : Nat) (H : ∀ n, (∀ m, m < theorem one_ne_zero : 1 ≠ 0 := succ_nz 0 theorem two_ne_zero : 2 ≠ 0 := succ_nz 1 --- +-- -- observation: the proof of lt_le_trans in Nat is not needed -- @@ -74,21 +74,21 @@ theorem lt_succ_eq (a b : Nat) : a < b + 1 ↔ a ≤ b theorem le_or_lt (a : Nat) : ∀ b : Nat, a ≤ b ∨ b < a := induction_on a ( - show ∀b, 0 ≤ b ∨ b < 0, + show ∀b, 0 ≤ b ∨ b < 0, from take b, or_introl (le_zero b) _ ) ( take a, assume ih : ∀b, a ≤ b ∨ b < a, - show ∀b, a + 1 ≤ b ∨ b < a + 1, - from + show ∀b, a + 1 ≤ b ∨ b < a + 1, + from take b, cases_on b ( - show a + 1 ≤ 0 ∨ 0 < a + 1, + show a + 1 ≤ 0 ∨ 0 < a + 1, from or_intror _ (le_add (le_zero a) 1) ) ( take b, have H : a ≤ b ∨ b < a, from ih b, - show a + 1 ≤ b + 1 ∨ b + 1 < a + 1, + show a + 1 ≤ b + 1 ∨ b + 1 < a + 1, from or_elim H ( assume H1 : a ≤ b, or_introl (le_add H1 1) (b + 1 < a + 1) @@ -118,23 +118,23 @@ theorem not_lt_iff {a b : Nat} : ¬ a < b ↔ b ≤ a := iff_intro (@not_lt_le a b) (@le_not_lt b a) theorem le_iff {a b : Nat} : a ≤ b ↔ a < b ∨ a = b -:= +:= iff_intro ( - assume H : a ≤ b, - show a < b ∨ a = b, + assume H : a ≤ b, + show a < b ∨ a = b, from or_elim (em (a = b)) ( take H1 : a = b, show a < b ∨ a = b, from or_intror _ H1 ) ( take H2 : a ≠ b, - have H3 : ¬ b ≤ a, - from not_intro (take H4: b ≤ a, absurd (le_antisym H H4) H2), + have H3 : ¬ b ≤ a, + from not_intro (take H4: b ≤ a, absurd (le_antisym H H4) H2), have H4 : a < b, from resolve1 (le_or_lt b a) H3, show a < b ∨ a = b, from or_introl H4 _ ) )( - assume H : a < b ∨ a = b, - show a ≤ b, + assume H : a < b ∨ a = b, + show a ≤ b, from or_elim H ( take H1 : a < b, lt_le H1 ) ( @@ -147,12 +147,12 @@ theorem ne_symm_iff {A : (Type U)} (a b : A) : a ≠ b ↔ b ≠ a theorem lt_iff (a b : Nat) : a < b ↔ a ≤ b ∧ a ≠ b := - calc + calc a < b = ¬ b ≤ a : symm (not_le_iff) ... = ¬ (b < a ∨ b = a) : { le_iff } ... = ¬ b < a ∧ b ≠ a : not_or _ _ ... = a ≤ b ∧ b ≠ a : { not_lt_iff } - ... = a ≤ b ∧ a ≠ b : { ne_symm_iff _ _ } + ... = a ≤ b ∧ a ≠ b : { ne_symm_iff _ _ } theorem ne_zero_ge_one {x : Nat} (H : x ≠ 0) : x ≥ 1 := resolve2 (le_iff ◂ (le_zero x)) (ne_symm H) @@ -163,14 +163,14 @@ theorem ne_zero_one_ge_two {x : Nat} (H0 : x ≠ 0) (H1 : x ≠ 1) : x ≥ 2 -- the forward direction can be replaced by ne_zero_ge_one, but -- note the comments below theorem ne_zero_iff (n : Nat) : n ≠ 0 ↔ n > 0 -:= +:= iff_intro ( assume H : n ≠ 0, - refute ( + by_contradiction ( assume H1 : ¬ n > 0, -- curious: if you make the arguments implicit in the next line, -- it fails (the evaluator is getting in the way, I think) - have H2 : n = 0, from le_antisym (@not_lt_le 0 n H1) (le_zero n), + have H2 : n = 0, from le_antisym (@not_lt_le 0 n H1) (le_zero n), absurd H2 H ) ) ( @@ -181,11 +181,11 @@ theorem ne_zero_iff (n : Nat) : n ≠ 0 ↔ n > 0 -- Note: this differs from Leo's naming conventions theorem mul_right_mono {x y : Nat} (H : x ≤ y) (z : Nat) : x * z ≤ y * z := - obtain (w : Nat) (Hw : x + w = y), + obtain (w : Nat) (Hw : x + w = y), from le_elim H, le_intro ( - show x * z + w * z = y * z, - from calc + show x * z + w * z = y * z, + from calc x * z + w * z = (x + w) * z : symm (distributel x w z) ... = y * z : { Hw } ) @@ -204,15 +204,15 @@ theorem add_left_mono {a b : Nat} (c : Nat) (H : a ≤ b) : c + a ≤ c + b theorem mul_right_strict_mono {x y z : Nat} (H : x < y) (znez : z ≠ 0) : x * z < y * z := - obtain (w : Nat) (Hw : x + 1 + w = y), + obtain (w : Nat) (Hw : x + 1 + w = y), from le_elim H, - have H1 : y * z = x * z + w * z + z, + have H1 : y * z = x * z + w * z + z, from calc y * z = (x + 1 + w) * z : { symm Hw } ... = (x + (1 + w)) * z : { add_assoc _ _ _ } ... = (x + (w + 1)) * z : { add_comm _ _ } ... = (x + w + 1) * z : { symm (add_assoc _ _ _) } - ... = (x + w) * z + 1 * z : distributel _ _ _ + ... = (x + w) * z + 1 * z : distributel _ _ _ ... = (x + w) * z + z : { mul_onel _ } ... = x * z + w * z + z : { distributel _ _ _ }, have H2 : x * z ≤ x * z + w * z, from le_addr _ _, @@ -222,26 +222,26 @@ theorem mul_right_strict_mono {x y z : Nat} (H : x < y) (znez : z ≠ 0) : x * z theorem mul_left_strict_mono {x y z : Nat} (H : x < y) (znez : z ≠ 0) : z * x < z * y := subst (subst (mul_right_strict_mono H znez) (mul_comm x z)) (mul_comm y z) -theorem mul_left_le_cancel {a b c : Nat} (H : a * b ≤ a * c) (anez : a ≠ 0) : b ≤ c +theorem mul_left_le_cancel {a b c : Nat} (H : a * b ≤ a * c) (anez : a ≠ 0) : b ≤ c := - refute ( + by_contradiction ( assume H1 : ¬ b ≤ c, have H2 : a * c < a * b, from mul_left_strict_mono (not_le_lt H1) anez, show false, from absurd H (lt_not_le H2) ) -theorem mul_right_le_cancel {a b c : Nat} (H : b * a ≤ c * a) (anez : a ≠ 0) : b ≤ c +theorem mul_right_le_cancel {a b c : Nat} (H : b * a ≤ c * a) (anez : a ≠ 0) : b ≤ c := mul_left_le_cancel (subst (subst H (mul_comm b a)) (mul_comm c a)) anez theorem mul_left_lt_cancel {a b c : Nat} (H : a * b < a * c) : b < c := - refute ( + by_contradiction ( assume H1 : ¬ b < c, have H2 : a * c ≤ a * b, from mul_left_mono a (not_lt_le H1), show false, from absurd H (le_not_lt H2) ) -theorem mul_right_lt_cancel {a b c : Nat} (H : b * a < c * a) : b < c +theorem mul_right_lt_cancel {a b c : Nat} (H : b * a < c * a) : b < c := mul_left_lt_cancel (subst (subst H (mul_comm b a)) (mul_comm c a)) theorem add_right_comm (a b c : Nat) : a + b + c = a + c + b @@ -286,7 +286,7 @@ theorem dvd_intro {a b c : Nat} (H : a * c = b) : a | b theorem dvd_elim {a b : Nat} (H : a | b) : ∃ c, a * c = b := H - + theorem dvd_self (n : Nat) : n | n := dvd_intro (mul_oner n) theorem one_dvd (a : Nat) : 1 | a @@ -301,7 +301,7 @@ theorem dvd_zero (a : Nat) : a | 0 := exists_intro 0 (mul_zeror _) theorem dvd_trans {a b c} (H1 : a | b) (H2 : b | c) : a | c -:= +:= obtain (w1 : Nat) (Hw1 : a * w1 = b), from H1, obtain (w2 : Nat) (Hw2 : b * w2 = c), from H2, exists_intro (w1 * w2) @@ -325,7 +325,7 @@ theorem dvd_mul_right {a b : Nat} (H : a | b) (c : Nat) : a | b * c := obtain (d : Nat) (Hd : a * d = b), from dvd_elim H, dvd_intro ( - calc + calc a * (d * c) = (a * d) * c : symm (mul_assoc _ _ _) ... = b * c : { Hd } ) @@ -338,7 +338,7 @@ theorem dvd_add {a b c : Nat} (H1 : a | b) (H2 : a | c) : a | b + c obtain (w1 : Nat) (Hw1 : a * w1 = b), from H1, obtain (w2 : Nat) (Hw2 : a * w2 = c), from H2, exists_intro (w1 + w2) - calc a * (w1 + w2) = a * w1 + a * w2 : distributer _ _ _ + calc a * (w1 + w2) = a * w1 + a * w2 : distributer _ _ _ ... = b + a * w2 : { Hw1 } ... = b + c : { Hw2 } @@ -346,13 +346,13 @@ theorem dvd_add_cancel {a b c : Nat} (H1 : a | b + c) (H2 : a | b) : a | c := or_elim (em (a = 0)) ( assume az : a = 0, - have H3 : c = 0, from + have H3 : c = 0, from calc c = 0 + c : symm (add_zerol _) ... = b + c : { symm (zero_dvd (subst H2 az)) } ... = 0 : zero_dvd (subst H1 az), show a | c, from subst (dvd_zero a) (symm H3) ) ( - assume anz : a ≠ 0, + assume anz : a ≠ 0, obtain (w1 : Nat) (Hw1 : a * w1 = b + c), from H1, obtain (w2 : Nat) (Hw2 : a * w2 = b), from H2, have H3 : a * w1 = a * w2 + c, from subst Hw1 (symm Hw2), @@ -360,7 +360,7 @@ theorem dvd_add_cancel {a b c : Nat} (H1 : a | b + c) (H2 : a | b) : a | c have H5 : w2 ≤ w1, from mul_left_le_cancel H4 anz, obtain (w3 : Nat) (Hw3 : w2 + w3 = w1), from le_elim H5, have H6 : b + a * w3 = b + c, from - calc + calc b + a * w3 = a * w2 + a * w3 : { symm Hw2 } ... = a * (w2 + w3) : symm (distributer _ _ _) ... = a * w1 : { Hw3 } @@ -376,7 +376,7 @@ theorem dvd_add_cancel {a b c : Nat} (H1 : a | b + c) (H2 : a | b) : a | c definition prime p := p ≥ 2 ∧ forall m, m | p → m = 1 ∨ m = p theorem not_prime_has_divisor {n : Nat} (H1 : n ≥ 2) (H2 : ¬ prime n) : ∃ m, m | n ∧ m ≠ 1 ∧ m ≠ n -:= +:= have H3 : ¬ n ≥ 2 ∨ ¬ (∀ m : Nat, m | n → m = 1 ∨ m = n), from not_and _ _ ◂ H2, have H4 : ¬ ¬ n ≥ 2, @@ -392,7 +392,7 @@ theorem not_prime_has_divisor {n : Nat} (H1 : n ≥ 2) (H2 : ¬ prime n) : ∃ m show ∃ m, m | n ∧ m ≠ 1 ∧ m ≠ n, from exists_intro m H8 -theorem not_prime_has_divisor2 {n : Nat} (H1 : n ≥ 2) (H2 : ¬ prime n) : +theorem not_prime_has_divisor2 {n : Nat} (H1 : n ≥ 2) (H2 : ¬ prime n) : ∃ m, m | n ∧ m ≥ 2 ∧ m < n := have n_ne_0 : n ≠ 0, from @@ -402,7 +402,7 @@ theorem not_prime_has_divisor2 {n : Nat} (H1 : n ≥ 2) (H2 : ¬ prime n) : let m_dvd_n := and_eliml Hm in let m_ne_1 := and_eliml (and_elimr Hm) in let m_ne_n := and_elimr (and_elimr Hm) in - have m_ne_0 : m ≠ 0, from + have m_ne_0 : m ≠ 0, from not_intro ( take m0 : m = 0, have n0 : n = 0, from zero_dvd (subst m_dvd_n m0), @@ -431,7 +431,7 @@ theorem has_prime_divisor {n : Nat} : n ≥ 2 → ∃ p, prime p ∧ p | n exists_intro n (and_intro H (dvd_self n)) ) ( assume H : ¬ prime n, - obtain (m : Nat) (Hm : m | n ∧ m ≥ 2 ∧ m < n), + obtain (m : Nat) (Hm : m | n ∧ m ≥ 2 ∧ m < n), from not_prime_has_divisor2 n_ge_2 H, obtain (p : Nat) (Hp : prime p ∧ p | m), from ih m (and_elimr (and_elimr Hm)) (and_eliml (and_elimr Hm)), @@ -475,15 +475,15 @@ theorem fact_ne_0 (n : Nat) : fact n ≠ 0 assume H : fact (n + 1) = 0, have H1 : n + 1 = 0, from mul_right_cancel ( - calc + calc (n + 1) * fact n = fact (n + 1) : symm (fact_succ n) ... = 0 : H ... = 0 * fact n : symm (mul_zerol _) ) ih, absurd H1 (succ_nz _) ) - ) - + ) + theorem dvd_fact {m n : Nat} (m_gt_0 : m > 0) (m_le_n : m ≤ n) : m | fact n := obtain (m' : Nat) (Hm' : 1 + m' = m), from le_elim m_gt_0, @@ -498,28 +498,28 @@ theorem dvd_fact {m n : Nat} (m_gt_0 : m > 0) (m_le_n : m ≤ n) : m | fact n from calc m' + 1 = 0 + 1 : { le_antisym m'_le_0 (le_zero m') } ... = 1 : add_zerol _, - show m' + 1 | fact (0 + 1), from subst (one_dvd _) (symm Hm') + show m' + 1 | fact (0 + 1), from subst (one_dvd _) (symm Hm') ) ( take n', assume ih : ∀m', m' ≤ n' → m' + 1 | fact (n' + 1), take m', - assume Hm' : m' ≤ n' + 1, + assume Hm' : m' ≤ n' + 1, have H1 : m' < n' + 1 ∨ m' = n' + 1, from le_iff ◂ Hm', or_elim H1 ( assume H2 : m' < n' + 1, have H3 : m' ≤ n', from lt_succ H2, have H4 : m' + 1 | fact (n' + 1), from ih _ H3, - have H5 : m' + 1 | (n' + 1 + 1) * fact (n' + 1), from dvd_mul_left H4 _, + have H5 : m' + 1 | (n' + 1 + 1) * fact (n' + 1), from dvd_mul_left H4 _, show m' + 1 | fact (n' + 1 + 1), from subst H5 (symm (fact_succ _)) ) ( assume H2 : m' = n' + 1, have H3 : m' + 1 | n' + 1 + 1, from subst (dvd_self _) H2, - have H4 : m' + 1 | (n' + 1 + 1) * fact (n' + 1), from dvd_mul_right H3 _, - show m' + 1 | fact (n' + 1 + 1), from subst H4 (symm (fact_succ _)) + have H4 : m' + 1 | (n' + 1 + 1) * fact (n' + 1), from dvd_mul_right H3 _, + show m' + 1 | fact (n' + 1 + 1), from subst H4 (symm (fact_succ _)) ) ), have H1 : m' + 1 | fact (n' + 1), from H _ _ m'_le_n', - show m | fact n, + show m | fact n, from (subst (subst (subst (subst H1 (add_comm m' 1)) Hm') (add_comm n' 1)) Hn') theorem primes_infinite (n : Nat) : ∃ p, p ≥ n ∧ prime p @@ -534,9 +534,9 @@ theorem primes_infinite (n : Nat) : ∃ p, p ≥ n ∧ prime p have p_ge_2 : p ≥ 2, from and_eliml prime_p, have two_gt_0 : 2 > 0, from (ne_zero_iff 2) ◂ (succ_nz 1), -- fails if arguments are left implicit - have p_gt_0 : p > 0, from @lt_le_trans 0 2 p two_gt_0 p_ge_2, + have p_gt_0 : p > 0, from @lt_le_trans 0 2 p two_gt_0 p_ge_2, have p_ge_n : p ≥ n, from - refute ( + by_contradiction ( assume H1 : ¬ p ≥ n, have H2 : p < n, from not_le_lt H1, have H3 : p ≤ n + 1, from lt_le (lt_le_trans H2 (le_addr n 1)), @@ -547,4 +547,3 @@ theorem primes_infinite (n : Nat) : ∃ p, p ≥ n ∧ prime p absurd H7 (lt_nrefl 1) ), exists_intro p (and_intro p_ge_n prime_p) - \ No newline at end of file diff --git a/examples/lean/wf.lean b/examples/lean/wf.lean index ee157ed91b..ab82f75f61 100644 --- a/examples/lean/wf.lean +++ b/examples/lean/wf.lean @@ -9,7 +9,7 @@ definition wf {A : (Type U)} (R : A → A → Bool) : Bool -- Well-founded induction theorem theorem wf_induction {A : (Type U)} {R : A → A → Bool} {P : A → Bool} (Hwf : wf R) (iH : ∀ x, (∀ y, R y x → P y) → P x) : ∀ x, P x -:= refute (λ N : ¬ ∀ x, P x, +:= by_contradiction (assume N : ¬ ∀ x, P x, obtain (w : A) (Hw : ¬ P w), from not_forall_elim N, -- The main "trick" is to define Q x as ¬ P x. -- Since R is well-founded, there must be a R-minimal element r s.t. Q r (which is ¬ P r) diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index 3ee82915e4..1d8447b44a 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -269,7 +269,7 @@ theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c absurd (H3 (resolve1 H1 (mt (assume Ha : a, H2 Ha) H))) H) -theorem refute {a : Bool} (H : ¬ a → false) : a +theorem by_contradiction {a : Bool} (H : ¬ a → false) : a := or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1)) theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a = b @@ -434,7 +434,7 @@ theorem not_congr {a b : Bool} (H : a ↔ b) : ¬ a ↔ ¬ b -- Recall that exists is defined as ¬ ∀ x : A, ¬ P x theorem exists_elim {A : (Type U)} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B -:= refute (λ R : ¬ B, +:= by_contradiction (assume R : ¬ B, absurd (take a : A, mt (assume H : P a, H2 a H) R) H1) @@ -485,7 +485,7 @@ theorem inhabited_ex_intro {A : (Type U)} {P : A → Bool} (H : ∃ x, P x) : in -- If a function space is non-empty, then for every 'a' in the domain, the range (B a) is not empty theorem inhabited_range {A : (Type U)} {B : A → (Type U)} (H : inhabited (∀ x, B x)) (a : A) : inhabited (B a) -:= refute (λ N : ¬ inhabited (B a), +:= by_contradiction (assume N : ¬ inhabited (B a), let s1 : ¬ ∃ x : B a, true := N, s2 : ∀ x : B a, false := take x : B a, absurd_not_true (not_exists_elim s1 x), s3 : ∃ y : (∀ x, B x), true := H @@ -738,7 +738,7 @@ theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x theorem not_forall (A : (Type U)) (P : A → Bool) : ¬ (∀ x : A, P x) ↔ (∃ x : A, ¬ P x) := boolext - (assume H, refute (λ N : ¬ (∃ x, ¬ P x), + (assume H, by_contradiction (assume N : ¬ (∃ x, ¬ P x), absurd (take x, not_not_elim (not_exists_elim N x)) H)) (assume (H : ∃ x, ¬ P x) (N : ∀ x, P x), obtain w Hw, from H, @@ -759,7 +759,7 @@ theorem exists_imp_distribute {A : (Type U)} (φ ψ : A → Bool) : (∃ x, φ x ... = (∀ x, φ x) → (∃ x, ψ x) : symm (imp_or _ _) theorem forall_uninhabited {A : (Type U)} {B : A → Bool} (H : ¬ inhabited A) : ∀ x, B x -:= refute (λ N : ¬ (∀ x, B x), +:= by_contradiction (assume N : ¬ (∀ x, B x), obtain w Hw, from not_forall_elim N, absurd (inhabited_intro w) H) diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 8e510311194a4c14999214a954196a5633e2b3a4..816c3407a6aac538ab39cfe3b52909fa92253a27 100644 GIT binary patch delta 31 ncmew{fw^fS^M)zv0!fwe$@zIDMTsey$t9Wjd7Edc-&+6x)0Yjp delta 21 dcmZpg$oyjh^M)zvY(=SQr6sAGm#E)c003mC37P-^ diff --git a/src/builtin/obj/optional.olean b/src/builtin/obj/optional.olean index 5d99ce1dd965fb44605eab29128801aa74b9c543..d961bd392bcbc76222b08eba7edd6cde19c4557c 100644 GIT binary patch delta 29 kcmZoP?Ka(TolhXCGCny!ucRn3B{R7sGe2+hUA`sU0J6Fa6aWAK delta 19 acmeA+Z8Y6*osX?3HLbKHb@Ow+CENf{M+fu( diff --git a/src/builtin/optional.lean b/src/builtin/optional.lean index e6a4c223cc..aa7b685fc6 100644 --- a/src/builtin/optional.lean +++ b/src/builtin/optional.lean @@ -70,9 +70,8 @@ theorem singleton_pred {A : (Type U)} {p : A → Bool} {w : A} (H : p w ∧ ∀ := funext (take x, iff_intro (assume Hpx : p x, show x = w, - from refute (assume N : x ≠ w, - show false, - from absurd Hpx (and_elimr H x N))) + from by_contradiction (assume N : x ≠ w, + show false, from absurd Hpx (and_elimr H x N))) (assume Heq : x = w, show p x, from subst (and_eliml H) (symm Heq))) diff --git a/src/kernel/kernel_decls.cpp b/src/kernel/kernel_decls.cpp index a6ef1fbd8e..5abb88af51 100644 --- a/src/kernel/kernel_decls.cpp +++ b/src/kernel/kernel_decls.cpp @@ -75,7 +75,7 @@ MK_CONSTANT(and_intro_fn, name("and_intro")); MK_CONSTANT(and_eliml_fn, name("and_eliml")); MK_CONSTANT(and_elimr_fn, name("and_elimr")); MK_CONSTANT(or_elim_fn, name("or_elim")); -MK_CONSTANT(refute_fn, name("refute")); +MK_CONSTANT(by_contradiction_fn, name("by_contradiction")); MK_CONSTANT(boolext_fn, name("boolext")); MK_CONSTANT(iff_intro_fn, name("iff_intro")); MK_CONSTANT(eqt_intro_fn, name("eqt_intro")); diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index 0320f9c565..c9b3782eca 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -212,9 +212,9 @@ inline expr mk_and_elimr_th(expr const & e1, expr const & e2, expr const & e3) { expr mk_or_elim_fn(); bool is_or_elim_fn(expr const & e); inline expr mk_or_elim_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_or_elim_fn(), e1, e2, e3, e4, e5, e6}); } -expr mk_refute_fn(); -bool is_refute_fn(expr const & e); -inline expr mk_refute_th(expr const & e1, expr const & e2) { return mk_app({mk_refute_fn(), e1, e2}); } +expr mk_by_contradiction_fn(); +bool is_by_contradiction_fn(expr const & e); +inline expr mk_by_contradiction_th(expr const & e1, expr const & e2) { return mk_app({mk_by_contradiction_fn(), e1, e2}); } expr mk_boolext_fn(); bool is_boolext_fn(expr const & e); inline expr mk_boolext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_boolext_fn(), e1, e2, e3, e4}); } diff --git a/tests/lean/exists3.lean b/tests/lean/exists3.lean index 6630b6b056..438f94f972 100644 --- a/tests/lean/exists3.lean +++ b/tests/lean/exists3.lean @@ -10,14 +10,14 @@ theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) := axiom Ax : forall x, exists y, P x y theorem T2 : exists x y, P x y := - refute (fun R : not (exists x y, P x y), + by_contradiction (fun R : not (exists x y, P x y), let L1 : forall x y, not (P x y) := fun a b, (not_not_elim ((not_not_elim R) a)) b, L2 : exists y, P 0 y := Ax 0 in exists_elim L2 (fun (w : Int) (H : P 0 w), absurd H (L1 0 w))). theorem T3 (A : (Type U)) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y := - refute (fun R : not (exists x y, P x y), + by_contradiction (fun R : not (exists x y, P x y), let L1 : forall x y, not (P x y) := fun a b, (not_not_elim ((not_not_elim R) a)) b, L2 : exists y, P a y := H1 a diff --git a/tests/lean/exists8.lean b/tests/lean/exists8.lean index 725cceaed9..5de1b40fa8 100644 --- a/tests/lean/exists8.lean +++ b/tests/lean/exists8.lean @@ -8,7 +8,7 @@ theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) := axiom Ax : forall x, exists y, P x y theorem T2 : exists x y, P x y := - refute (fun R : not (exists x y, P x y), + by_contradiction (fun R : not (exists x y, P x y), let L1 : forall x y, not (P x y) := fun a b, (not_exists_elim ((not_exists_elim R) a)) b, L2 : exists y, P 0 y := Ax 0 @@ -16,7 +16,7 @@ theorem T2 : exists x y, P x y := absurd H (L1 0 w))). theorem T3 (A : (Type U)) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y := - refute (fun R : not (exists x y, P x y), + by_contradiction (fun R : not (exists x y, P x y), let L1 : forall x y, not (P x y) := fun a b, (not_exists_elim ((not_exists_elim R) a)) b, L2 : exists y, P a y := H1 a diff --git a/tests/lean/refute1.lean b/tests/lean/refute1.lean index 148af23d5d..7b7cdaf33a 100644 --- a/tests/lean/refute1.lean +++ b/tests/lean/refute1.lean @@ -1,3 +1,3 @@ variables a b : Bool axiom H : a /\ b -theorem T : a := refute (fun R, absurd (and_eliml H) R) +theorem T : a := by_contradiction (fun R, absurd (and_eliml H) R)