michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library): rename exists_elim and exists_intro to exists.elim

Browse source 
and exists.intro
This commit is contained in:
Leonardo de Moura 2014-12-15 19:05:03 -08:00
parent 2b56a2b891
commit 5cf8064269
30 changed files with 104 additions and 104 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/lean/test_single.sh
View file

@ -22,7 +22,7 @@ while read -r line; do
rm -f $f.$i.lean
elif [[ $line =~ ^#\+END_SRC ]]; then
if [[ $in_code_block -eq 1 ]]; then
if $LEAN $f.$i.lean > $f.$i.produced.out; then
if $LEAN -t 100000 $f.$i.lean > $f.$i.produced.out; then
echo "code fragment #$i worked"
else
echo "ERROR executing $f.$i.lean, for in_code_block block starting at $lastbegin, produced output:"

40
doc/lean/tutorial.org
View file

@ -685,8 +685,8 @@ In Lean, the existential quantifier can be written as =exists x : A, B
x= or =∃ x : A, B x=. Actually both versions are just
notational convenience for =Exists (fun x : A, B x)=. That is, the existential quantifier
is actually a constant defined in the file =logic.lean=.
This file also defines the =exists_intro= and =exists_elim=.
To build a proof for =∃ x : A, B x=, we should provide a term =w : A= and a proof term =Hw : B w= to =exists_intro=.
This file also defines the =exists.intro= and =exists.elim=.
To build a proof for =∃ x : A, B x=, we should provide a term =w : A= and a proof term =Hw : B w= to =exists.intro=.
We say =w= is the witness for the existential introduction. In previous examples,
=nat_trans3i Hxy Hzy Hzw= was a proof term for =x = w=. Then, we can create a proof term
for =∃ a : nat, a = w= using
@ -703,32 +703,32 @@ for =∃ a : nat, a = w= using
axiom Hzy : z = y
axiom Hzw : z = w
theorem ex_a_eq_w : exists a, a = w := exists_intro x (nat_trans3i Hxy Hzy Hzw)
theorem ex_a_eq_w : exists a, a = w := exists.intro x (nat_trans3i Hxy Hzy Hzw)
check ex_a_eq_w
#+END_SRC
Note that =exists_intro= also has implicit arguments. For example, Lean has to infer the implicit argument
Note that =exists.intro= also has implicit arguments. For example, Lean has to infer the implicit argument
=P : A → Bool=, a predicate (aka function to Prop). This creates complications. For example, suppose
we have =Hg : g 0 0 = 0= and we invoke =exists_intro 0 Hg=. There are different possible values for =P=.
we have =Hg : g 0 0 = 0= and we invoke =exists.intro 0 Hg=. There are different possible values for =P=.
Each possible value corresponds to a different theorem: =∃ x, g x x = x=, =∃ x, g x x = 0=,
=∃ x, g x 0 = x=, etc. Lean uses the context where =exists_intro= occurs to infer the users intent.
=∃ x, g x 0 = x=, etc. Lean uses the context where =exists.intro= occurs to infer the users intent.
In the example above, we were trying to prove the theorem =∃ a, a = w=. So, we are implicitly telling
Lean how to choose =P=. In the following example, we demonstrate this issue. We ask Lean to display
the implicit arguments using the option =pp.implicit=. We see that each instance of =exists_intro 0 Hg=
the implicit arguments using the option =pp.implicit=. We see that each instance of =exists.intro 0 Hg=
has different values for the implicit argument =P=.
#+BEGIN_SRC lean
import data.nat
open nat
check @exists_intro
check @exists.intro
constant g : nat → nat → nat
axiom Hg : g 0 0 = 0
theorem gex1 : ∃ x, g x x = x := exists_intro 0 Hg
theorem gex2 : ∃ x, g x 0 = x := exists_intro 0 Hg
theorem gex3 : ∃ x, g 0 0 = x := exists_intro 0 Hg
theorem gex4 : ∃ x, g x x = 0 := exists_intro 0 Hg
theorem gex1 : ∃ x, g x x = x := exists.intro 0 Hg
theorem gex2 : ∃ x, g x 0 = x := exists.intro 0 Hg
theorem gex3 : ∃ x, g 0 0 = x := exists.intro 0 Hg
theorem gex4 : ∃ x, g x x = 0 := exists.intro 0 Hg
set_option pp.implicit true -- display implicit arguments
check gex1
check gex2
@ -736,14 +736,14 @@ has different values for the implicit argument =P=.
check gex4
#+END_SRC
We can view =exists_intro= (aka existential introduction) as an information hiding procedure.
We can view =exists.intro= (aka existential introduction) as an information hiding procedure.
We are "hiding" what is the witness for some fact. The existential elimination performs the opposite
operation. The =exists_elim= theorem allows us to prove some proposition =B= from =∃ x : A, B x=
operation. The =exists.elim= theorem allows us to prove some proposition =B= from =∃ x : A, B x=
if we can derive =B= using an "abstract" witness =w= and a proof term =Hw : B w=.
#+BEGIN_SRC lean
import logic
check @exists_elim
check @exists.elim
#+END_SRC
In the following example, we define =even a= as =∃ b, a = 2*b=, and then we show that the sum
@ -755,9 +755,9 @@ of two even numbers is an even number.
definition even (a : nat) := ∃ b, a = 2*b
theorem EvenPlusEven {a b : nat} (H1 : even a) (H2 : even b) : even (a + b) :=
exists_elim H1 (fun (w1 : nat) (Hw1 : a = 2*w1),
exists_elim H2 (fun (w2 : nat) (Hw2 : b = 2*w2),
exists_intro (w1 + w2)
exists.elim H1 (fun (w1 : nat) (Hw1 : a = 2*w1),
exists.elim H2 (fun (w2 : nat) (Hw2 : b = 2*w2),
exists.intro (w1 + w2)
(calc a + b = 2*w1 + b : {Hw1}
... = 2*w1 + 2*w2 : {Hw2}
... = 2*(w1 + w2) : eq.symm !mul.distr_left)))
@ -767,7 +767,7 @@ of two even numbers is an even number.
The example above also uses [[./calc.org][calculational proofs]] to show that =a + b = 2*(w1 + w2)=.
The =calc= construct is just syntax sugar for creating proofs using transitivity and substitution.
In Lean, we can use =obtain _, from _, _= as syntax sugar for =exists_elim=.
In Lean, we can use =obtain _, from _, _= as syntax sugar for =exists.elim=.
With this macro we can write the example above in a more natural way
#+BEGIN_SRC lean
@ -777,7 +777,7 @@ With this macro we can write the example above in a more natural way
theorem EvenPlusEven {a b : nat} (H1 : even a) (H2 : even b) : even (a + b) :=
obtain (w1 : nat) (Hw1 : a = 2*w1), from H1,
obtain (w2 : nat) (Hw2 : b = 2*w2), from H2,
exists_intro (w1 + w2)
exists.intro (w1 + w2)
(calc a + b = 2*w1 + b : {Hw1}
... = 2*w1 + 2*w2 : {Hw2}
... = 2*(w1 + w2) : eq.symm !mul.distr_left)

2
library/algebra/ring.lean
View file

@ -66,7 +66,7 @@ theorem dvd.intro [s : has_dvd A] {a b c : A} : a * b = c → a | c := !has_dvd.
theorem dvd.ex [s : has_dvd A] {a b : A} : a | b → ∃c, a * c = b := !has_dvd.dvd_ex
theorem dvd.elim [s : has_dvd A] {P : Prop} {a b : A} (H₁ : a | b) (H₂ : ∀c, a * c = b → P) : P :=
exists_elim (dvd.ex H₁) H₂
exists.elim (dvd.ex H₁) H₂
structure comm_semiring_dvd [class] (A : Type) extends comm_semiring A, has_dvd A

8
library/data/int/basic.lean
View file

@ -385,8 +385,8 @@ nat.cases_on m
theorem cases (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - n) :=
cases_on a
(take n, or.inl (exists_intro n rfl))
(take n', or.inr (exists_intro (succ n') rfl))
(take n, or.inl (exists.intro n rfl))
(take n', or.inr (exists.intro (succ n') rfl))
theorem by_cases {P : ℤ → Prop} (a : ℤ) (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-n)) :
P a :=
@ -407,11 +407,11 @@ or.elim (cases a)
a = -(of_nat n) : H2
... = -(of_nat 0) : {H3}
... = of_nat 0 : neg_zero,
or.inl (exists_intro 0 H4))
or.inl (exists.intro 0 H4))
(take k : ℕ,
assume H3 : n = succ k,
have H4 : a = -(of_nat (succ k)), from H3 ▸ H2,
or.inr (exists_intro k H4)))
or.inr (exists.intro k H4)))
theorem int_by_cases_succ {P : ℤ → Prop} (a : ℤ)
(H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-(of_nat (succ n)))) : P a :=

10
library/data/int/order.lean
View file

@ -18,7 +18,7 @@ open int eq.ops
namespace int
theorem nonneg_elim {a : ℤ} : nonneg a → ∃n : ℕ, a = n :=
cases_on a (take n H, exists_intro n rfl) (take n' H, false.elim H)
cases_on a (take n H, exists.intro n rfl) (take n' H, false.elim H)
theorem le_intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b :=
have H1 : b - a = n, from add_imp_sub_right (!add_comm ▸ H),
@ -27,7 +27,7 @@ show nonneg (b - a), from H1⁻¹ ▸ H2
theorem le_elim {a b : ℤ} (H : a ≤ b) : ∃n : ℕ, a + n = b :=
obtain (n : ℕ) (H1 : b - a = n), from nonneg_elim H,
exists_intro n (!add_comm ▸ sub_imp_add H1)
exists.intro n (!add_comm ▸ sub_imp_add H1)
-- ### partial order
@ -216,7 +216,7 @@ have H2 : a + succ n = b, from
calc
a + succ n = a + 1 + n : by simp
... = b : Hn,
exists_intro n H2
exists.intro n H2
-- -- ### basic facts
@ -409,13 +409,13 @@ or_resolve_right (le_or_gt a b) H
theorem pos_imp_exists_nat {a : ℤ} (H : a ≥ 0) : ∃n : ℕ, a = n :=
obtain (n : ℕ) (Hn : of_nat 0 + n = a), from le_elim H,
exists_intro n (Hn⁻¹ ⬝ add_zero_left n)
exists.intro n (Hn⁻¹ ⬝ add_zero_left n)
theorem neg_imp_exists_nat {a : ℤ} (H : a ≤ 0) : ∃n : ℕ, a = -n :=
have H2 : -a ≥ 0, from zero_le_neg H,
obtain (n : ℕ) (Hn : -a = n), from pos_imp_exists_nat H2,
have H3 : a = -n, from (neg_move Hn)⁻¹,
exists_intro n H3
exists.intro n H3
theorem nat_abs_nonneg_eq {a : ℤ} (H : a ≥ 0) : (nat_abs a) = a :=
obtain (n : ℕ) (Hn : a = n), from pos_imp_exists_nat H,

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

@ -173,13 +173,13 @@ induction_on l
assume H : x ∈ y::l,
or.elim H
(assume H1 : x = y,
exists_intro nil (!exists_intro (H1 ▸ rfl)))
exists.intro nil (!exists.intro (H1 ▸ rfl)))
(assume H1 : x ∈ l,
obtain s (H2 : ∃t : list T, l = s ++ (x::t)), from IH H1,
obtain t (H3 : l = s ++ (x::t)), from H2,
have H4 : y :: l = (y::s) ++ (x::t),
from H3 ▸ rfl,
!exists_intro (!exists_intro H4)))
!exists.intro (!exists.intro H4)))
definition mem.is_decidable [instance] (H : decidable_eq T) (x : T) (l : list T) : decidable (x ∈ l) :=
rec_on l

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

@ -64,7 +64,7 @@ induction_on n
theorem zero_or_exists_succ (n : ℕ) : n = 0 ∨ ∃k, n = succ k :=
or_of_or_of_imp_of_imp (zero_or_succ_pred n) (assume H, H)
(assume H : n = succ (pred n), exists_intro (pred n) H)
(assume H : n = succ (pred n), exists.intro (pred n) H)
theorem case {P : ℕ → Prop} (n : ℕ) (H1: P 0) (H2 : ∀m, P (succ m)) : P n :=
induction_on n H1 (take m IH, H2 m)

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

@ -29,16 +29,16 @@ namespace nat
definition bex_succ {P : nat → Prop} {n : nat} (H : bex n P) : bex (succ n) P :=
obtain (w : nat) (Hw : w < n ∧ P w), from H,
and.rec_on Hw (λ hlt hp, exists_intro w (and.intro (lt.step hlt) hp))
and.rec_on Hw (λ hlt hp, exists.intro w (and.intro (lt.step hlt) hp))
definition bex_succ_of_pred {P : nat → Prop} {a : nat} (H : P a) : bex (succ a) P :=
exists_intro a (and.intro (lt.base a) H)
exists.intro a (and.intro (lt.base a) H)
definition not_bex_succ {P : nat → Prop} {n : nat} (H₁ : ¬ bex n P) (H₂ : ¬ P n) : ¬ bex (succ n) P :=
λ H, obtain (w : nat) (Hw : w < succ n ∧ P w), from H,
and.rec_on Hw (λ hltsn hp, or.rec_on (eq_or_lt_of_le hltsn)
(λ heq : w = n, absurd (eq.rec_on heq hp) H₂)
(λ hltn : w < n, absurd (exists_intro w (and.intro hltn hp)) H₁))
(λ hltn : w < n, absurd (exists.intro w (and.intro hltn hp)) H₁))
definition ball_zero (P : nat → Prop) : ball zero P :=
λ x Hlt, absurd Hlt !not_lt_zero

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

@ -300,7 +300,7 @@ show x mod y = 0, from
theorem dvd_iff_exists_mul (x y : ℕ) : x | y ↔ ∃z, z * x = y :=
iff.intro
(assume H : x | y,
show ∃z, z * x = y, from exists_intro _ (dvd_imp_div_mul_eq H))
show ∃z, z * x = y, from exists.intro _ (dvd_imp_div_mul_eq H))
(assume H : ∃z, z * x = y,
obtain (z : ℕ) (zx_eq : z * x = y), from H,
show x | y, from mul_eq_imp_dvd zx_eq)
@ -341,14 +341,14 @@ have H4 : k = k div n * (n div m) * m, from calc
k = k div n * n : dvd_imp_div_mul_eq H2
... = k div n * (n div m * m) : H3
... = k div n * (n div m) * m : mul.assoc,
mp (!dvd_iff_exists_mul⁻¹) (exists_intro (k div n * (n div m)) (H4⁻¹))
mp (!dvd_iff_exists_mul⁻¹) (exists.intro (k div n * (n div m)) (H4⁻¹))
theorem dvd_add {m n1 n2 : ℕ} (H1 : m | n1) (H2 : m | n2) : m | (n1 + n2) :=
have H : (n1 div m + n2 div m) * m = n1 + n2, from calc
(n1 div m + n2 div m) * m = n1 div m * m + n2 div m * m : mul.distr_right
... = n1 + n2 div m * m : dvd_imp_div_mul_eq H1
... = n1 + n2 : dvd_imp_div_mul_eq H2,
mp (!dvd_iff_exists_mul⁻¹) (exists_intro _ H)
mp (!dvd_iff_exists_mul⁻¹) (exists.intro _ H)
theorem dvd_add_cancel_left {m n1 n2 : ℕ} : m | (n1 + n2) → m | n1 → m | n2 :=
case_zero_pos m
@ -373,7 +373,7 @@ case_zero_pos m
... = n1 div m * m + n2 div m * m : add.comm
... = n1 + n2 div m * m : dvd_imp_div_mul_eq H2,
have H4 : n2 = n2 div m * m, from add.cancel_left H3,
mp (!dvd_iff_exists_mul⁻¹) (exists_intro _ (H4⁻¹)))
mp (!dvd_iff_exists_mul⁻¹) (exists.intro _ (H4⁻¹)))
theorem dvd_add_cancel_right {m n1 n2 : ℕ} (H : m | (n1 + n2)) : m | n2 → m | n1 :=
dvd_add_cancel_left (!add.comm ▸ H)

8
library/data/nat/order.lean
View file

@ -32,12 +32,12 @@ h ▸ le.add_right n k
theorem le_elim {n m : ℕ} (h : n ≤ m) : ∃k, n + k = m :=
le.rec_on h
(exists_intro 0 rfl)
(exists.intro 0 rfl)
(λ m (h : n < m), lt.rec_on h
(exists_intro 1 rfl)
(exists.intro 1 rfl)
(λ b hlt (ih : ∃ (k : ℕ), n + k = b),
obtain (k : ℕ) (h : n + k = b), from ih,
exists_intro (succ k) (calc
exists.intro (succ k) (calc
n + succ k = succ (n + k) : add.succ_right
... = succ b : h)))
@ -261,7 +261,7 @@ theorem succ_pos (n : ℕ) : 0 < succ n :=
theorem lt_imp_eq_succ {n m : ℕ} (H : n < m) : exists k, m = succ k :=
discriminate
(take (Hm : m = 0), absurd (Hm ▸ H) !not_lt_zero)
(take (l : ℕ) (Hm : m = succ l), exists_intro l Hm)
(take (l : ℕ) (Hm : m = succ l), exists.intro l Hm)
-- ### interaction with le

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

@ -224,7 +224,7 @@ or.elim !le_total
theorem le_elim_sub {n m : ℕ} (H : n ≤ m) : ∃k, m - k = n :=
obtain (k : ℕ) (Hk : n + k = m), from le_elim H,
exists_intro k
exists.intro k
(calc
m - k = n + k - k : {Hk⁻¹}
... = n : !sub_add_left)

10
library/data/quotient/basic.lean
View file

@ -200,16 +200,16 @@ comp_quotient_map_binary Q H (Hrefl a) (Hrefl b)
definition image {A B : Type} (f : A → B) := subtype (fun b, ∃a, f a = b)
theorem image_inhabited {A B : Type} (f : A → B) (H : inhabited A) : inhabited (image f) :=
inhabited.mk (tag (f (default A)) (exists_intro (default A) rfl))
inhabited.mk (tag (f (default A)) (exists.intro (default A) rfl))
theorem image_inhabited2 {A B : Type} (f : A → B) (a : A) : inhabited (image f) :=
image_inhabited f (inhabited.mk a)
definition fun_image {A B : Type} (f : A → B) (a : A) : image f :=
tag (f a) (exists_intro a rfl)
tag (f a) (exists.intro a rfl)
theorem fun_image_def {A B : Type} (f : A → B) (a : A) :
fun_image f a = tag (f a) (exists_intro a rfl) := rfl
fun_image f a = tag (f a) (exists.intro a rfl) := rfl
theorem elt_of_fun_image {A B : Type} (f : A → B) (a : A) : elt_of (fun_image f a) = f a :=
elt_of.tag _ _
@ -221,11 +221,11 @@ theorem fun_image_surj {A B : Type} {f : A → B} (u : image f) : ∃a, fun_imag
subtype.destruct u
(take (b : B) (H : ∃a, f a = b),
obtain a (H': f a = b), from H,
(exists_intro a (tag_eq H')))
(exists.intro a (tag_eq H')))
theorem image_tag {A B : Type} {f : A → B} (u : image f) : ∃a H, tag (f a) H = u :=
obtain a (H : fun_image f a = u), from fun_image_surj u,
exists_intro a (exists_intro (exists_intro a rfl) H)
exists.intro a (exists.intro (exists.intro a rfl) H)
open eq.ops

2
library/data/quotient/classical.lean
View file

@ -21,7 +21,7 @@ definition prelim_map {A : Type} (R : A → A → Prop) (a : A) :=
theorem prelim_map_rel {A : Type} {R : A → A → Prop} (H : is_equivalence R) (a : A)
: R a (prelim_map R a) :=
have reflR : reflexive R, from is_equivalence.refl R,
epsilon_spec (exists_intro a (reflR a))
epsilon_spec (exists.intro a (reflR a))
-- TODO: only needed: R PER
theorem prelim_map_congr {A : Type} {R : A → A → Prop} (H1 : is_equivalence R) {a b : A}

4
library/init/logic.lean
View file

@ -238,12 +238,12 @@ calc_trans iff.trans
inductive Exists {A : Type} (P : A → Prop) : Prop :=
intro : ∀ (a : A), P a → Exists P
definition exists_intro := @Exists.intro
definition exists.intro := @Exists.intro
notation `exists` binders `,` r:(scoped P, Exists P) := r
notation `∃` binders `,` r:(scoped P, Exists P) := r
theorem exists_elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B :=
theorem exists.elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B :=
Exists.rec H2 H1
inductive decidable [class] (p : Prop) : Type :=

4
library/logic/axioms/examples/diaconescu.lean
View file

@ -17,10 +17,10 @@ private definition u := epsilon (λx, x = true ∨ p)
private definition v := epsilon (λx, x = false ∨ p)
private lemma u_def : u = true ∨ p :=
epsilon_spec (exists_intro true (or.inl rfl))
epsilon_spec (exists.intro true (or.inl rfl))
private lemma v_def : v = false ∨ p :=
epsilon_spec (exists_intro false (or.inl rfl))
epsilon_spec (exists.intro false (or.inl rfl))
private lemma uv_implies_p : ¬(u = v) ∨ p :=
or.elim u_def

8
library/logic/axioms/hilbert.lean
View file

@ -23,7 +23,7 @@ axiom strong_indefinite_description {A : Type} (P : A → Prop) (H : nonempty A)
-- axiom indefinite_description {A : Type} {P : A->Prop} (H : ∃x, P x) : {x : A, P x}
theorem nonempty_imp_exists_true {A : Type} (H : nonempty A) : ∃x : A, true :=
nonempty.elim H (take x, exists_intro x trivial)
nonempty.elim H (take x, exists.intro x trivial)
theorem nonempty_imp_inhabited {A : Type} (H : nonempty A) : inhabited A :=
let u : {x | (∃y : A, true) → true} := strong_indefinite_description (λa, true) H in
@ -52,7 +52,7 @@ theorem epsilon_spec {A : Type} {P : A → Prop} (Hex : ∃y, P y) :
epsilon_spec_aux (nonempty_of_exists Hex) P Hex
theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (nonempty.intro a) (λx, x = a) = a :=
epsilon_spec (exists_intro a (eq.refl a))
epsilon_spec (exists.intro a (eq.refl a))
-- the axiom of choice
@ -62,7 +62,7 @@ theorem axiom_of_choice {A : Type} {B : A → Type} {R : Πx, B x → Prop} (H :
∃f, ∀x, R x (f x) :=
let f := λx, @epsilon _ (nonempty_of_exists (H x)) (λy, R x y),
H := take x, epsilon_spec (H x)
in exists_intro f H
in exists.intro f H
theorem skolem {A : Type} {B : A → Type} {P : Πx, B x → Prop} :
(∀x, ∃y, P x y) ↔ ∃f, (∀x, P x (f x)) :=
@ -70,4 +70,4 @@ iff.intro
(assume H : (∀x, ∃y, P x y), axiom_of_choice H)
(assume H : (∃f, (∀x, P x (f x))),
take x, obtain (fw : ∀x, B x) (Hw : ∀x, P x (fw x)), from H,
exists_intro (fw x) (Hw x))
exists.intro (fw x) (Hw x))

2
library/logic/connectives.lean
View file

@ -139,7 +139,7 @@ notation `∃!` binders `,` r:(scoped P, exists_unique P) := r
theorem exists_unique.intro {A : Type} {p : A → Prop} (w : A) (H1 : p w) (H2 : ∀y, p y → y = w) :
∃!x, p x :=
exists_intro w (and.intro H1 H2)
exists.intro w (and.intro H1 H2)
theorem exists_unique.elim {A : Type} {p : A → Prop} {b : Prop}
(H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, p y → y = x) → b) : b :=

22
library/logic/examples/nuprl_examples.lean
View file

@ -112,7 +112,7 @@ assume (H : ∀x, C → P x) (Hc : C),
theorem thm18a : ((∃x, P x) → C) → (∀x, P x → C) :=
assume H : (∃x, P x) → C,
take x, assume Hp : P x,
have Hex : ∃x, P x, from exists_intro x Hp,
have Hex : ∃x, P x, from exists.intro x Hp,
H Hex
theorem thm18b : (∀x, P x → C) → (∃x, P x) → C :=
@ -126,28 +126,28 @@ assume (Hem : C ∨ ¬C) (Hin : ∃x : T, true) (H1 : C → ∃x, P x),
(assume Hc : C,
obtain (w : T) (Hw : P w), from H1 Hc,
have Hr : C → P w, from assume Hc, Hw,
exists_intro w Hr)
exists.intro w Hr)
(assume Hnc : ¬C,
obtain (w : T) (Hw : true), from Hin,
have Hr : C → P w, from assume Hc, absurd Hc Hnc,
exists_intro w Hr)
exists.intro w Hr)
theorem thm19b : (∃x, C → P x) → C → (∃x, P x) :=
assume (H : ∃x, C → P x) (Hc : C),
obtain (w : T) (Hw : C → P w), from H,
exists_intro w (Hw Hc)
exists.intro w (Hw Hc)
theorem thm20a : (C ∨ ¬C) → (∃x : T, true) → ((¬∀x, P x) → ∃x, ¬P x) → ((∀x, P x) → C) → (∃x, P x → C) :=
assume Hem Hin Hnf H,
or.elim Hem
(assume Hc : C,
obtain (w : T) (Hw : true), from Hin,
exists_intro w (assume H : P w, Hc))
exists.intro w (assume H : P w, Hc))
(assume Hnc : ¬C,
have H1 : ¬(∀x, P x), from mt H Hnc,
have H2 : ∃x, ¬P x, from Hnf H1,
obtain (w : T) (Hw : ¬P w), from H2,
exists_intro w (assume H : P w, absurd H Hw))
exists.intro w (assume H : P w, absurd H Hw))
theorem thm20b : (∃x, P x → C) → (∀ x, P x) → C :=
assume Hex Hall,
@ -159,16 +159,16 @@ assume Hin H,
or.elim H
(assume Hex : ∃x, P x,
obtain (w : T) (Hw : P w), from Hex,
exists_intro w (or.inl Hw))
exists.intro w (or.inl Hw))
(assume Hc : C,
obtain (w : T) (Hw : true), from Hin,
exists_intro w (or.inr Hc))
exists.intro w (or.inr Hc))
theorem thm21b : (∃x, P x ∨ C) → ((∃x, P x) ∨ C) :=
assume H,
obtain (w : T) (Hw : P w ∨ C), from H,
or.elim Hw
(assume H : P w, or.inl (exists_intro w H))
(assume H : P w, or.inl (exists.intro w H))
(assume Hc : C, or.inr Hc)
theorem thm22a : (∀x, P x) ∨ C → ∀x, P x ∨ C :=
@ -193,12 +193,12 @@ assume H,
have Hex : ∃x, P x, from and.elim_left H,
have Hc : C, from and.elim_right H,
obtain (w : T) (Hw : P w), from Hex,
exists_intro w (and.intro Hw Hc)
exists.intro w (and.intro Hw Hc)
theorem thm23b : (∃x, P x ∧ C) → (∃x, P x) ∧ C :=
assume H,
obtain (w : T) (Hw : P w ∧ C), from H,
have Hex : ∃x, P x, from exists_intro w (and.elim_left Hw),
have Hex : ∃x, P x, from exists.intro w (and.elim_left Hw),
and.intro Hex (and.elim_right Hw)
theorem thm24a : (∀x, P x) ∧ C → (∀x, P x ∧ C) :=

2
library/logic/identities.lean
View file

@ -102,7 +102,7 @@ assume H, by_contradiction (assume Hna : ¬a,
theorem forall_not_of_not_exists {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)]
(H : ¬∃x, P x) : ∀x, ¬P x :=
take x, or.elim (em (P x))
(assume Hp : P x, absurd (exists_intro x Hp) H)
(assume Hp : P x, absurd (exists.intro x Hp) H)
(assume Hn : ¬P x, Hn)
theorem exists_not_of_not_forall {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)]

16
library/logic/quantifiers.lean
View file

@ -28,9 +28,9 @@ iff.intro
theorem exists_congr {A : Type} {φ ψ : A → Prop} (H : ∀x, φ x ↔ ψ x) : (∃x, φ x) ↔ (∃x, ψ x) :=
iff.intro
(assume Hex, obtain w Pw, from Hex,
exists_intro w (iff.elim_left (H w) Pw))
exists.intro w (iff.elim_left (H w) Pw))
(assume Hex, obtain w Qw, from Hex,
exists_intro w (iff.elim_right (H w) Qw))
exists.intro w (iff.elim_right (H w) Qw))
theorem forall_true_iff_true (A : Type) : (∀x : A, true) ↔ true :=
iff.intro (assume H, trivial) (assume H, take x, trivial)
@ -41,7 +41,7 @@ iff.intro (assume Hl, inhabited.destruct H (take x, Hl x)) (assume Hr, take x, H
theorem exists_p_iff_p (A : Type) [H : inhabited A] (p : Prop) : (∃x : A, p) ↔ p :=
iff.intro
(assume Hl, obtain a Hp, from Hl, Hp)
(assume Hr, inhabited.destruct H (take a, exists_intro a Hr))
(assume Hr, inhabited.destruct H (take a, exists.intro a Hr))
theorem forall_and_distribute {A : Type} (φ ψ : A → Prop) :
(∀x, φ x ∧ ψ x) ↔ (∀x, φ x) ∧ (∀x, ψ x) :=
@ -54,13 +54,13 @@ theorem exists_or_distribute {A : Type} (φ ψ : A → Prop) :
iff.intro
(assume H, obtain (w : A) (Hw : φ w ∨ ψ w), from H,
or.elim Hw
(assume Hw1 : φ w, or.inl (exists_intro w Hw1))
(assume Hw2 : ψ w, or.inr (exists_intro w Hw2)))
(assume Hw1 : φ w, or.inl (exists.intro w Hw1))
(assume Hw2 : ψ w, or.inr (exists.intro w Hw2)))
(assume H, or.elim H
(assume H1, obtain (w : A) (Hw : φ w), from H1,
exists_intro w (or.inl Hw))
exists.intro w (or.inl Hw))
(assume H2, obtain (w : A) (Hw : ψ w), from H2,
exists_intro w (or.inr Hw)))
exists.intro w (or.inr Hw)))
theorem nonempty_of_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : nonempty A :=
obtain w Hw, from H, nonempty.intro w
@ -78,7 +78,7 @@ section
definition decidable_exists_eq [instance] : decidable (∃ x, x = a ∧ P x) :=
decidable.rec_on H
(λ pa, inl (exists_intro a (and.intro rfl pa)))
(λ pa, inl (exists.intro a (and.intro rfl pa)))
(λ npa, inr (λ h,
obtain (w : A) (Hw : w = a ∧ P w), from h,
absurd (and.rec_on Hw (λ h₁ h₂, h₁ ▸ h₂)) npa))

4
src/frontends/lean/builtin_exprs.cpp
View file

@ -331,7 +331,7 @@ static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos)
static name * g_exists_elim = nullptr;
static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & pos) {
if (!p.env().find(*g_exists_elim))
throw parser_error("invalid use of 'obtain' expression, environment does not contain 'exists_elim' theorem", pos);
throw parser_error("invalid use of 'obtain' expression, environment does not contain 'exists.elim' theorem", pos);
// exists_elim {A : Type} {P : A → Prop} {B : Prop} (H1 : ∃ x : A, P x) (H2 : ∀ (a : A) (H : P a), B)
buffer<expr> ps;
auto b_pos = p.pos();
@ -534,7 +534,7 @@ parse_table get_builtin_led_table() {
void initialize_builtin_exprs() {
notation::H_show = new name("H_show");
notation::g_exists_elim = new name("exists_elim");
notation::g_exists_elim = new name{"exists", "elim"};
notation::g_ite = new name("ite");
notation::g_dite = new name("dite");
notation::g_not = new expr(mk_constant("not"));

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

@ -31,14 +31,14 @@ theorem not_is_zero_succ (x : nat) : ¬ is_zero (succ x)
theorem dichotomy (m : nat) : m = zero ∨ (∃ n, m = succ n)
:= nat.rec
(or.intro_left _ (refl zero))
(λ m H, or.intro_right _ (exists_intro m (refl (succ m))))
(λ m H, or.intro_right _ (exists.intro m (refl (succ m))))
m
theorem is_zero_to_eq (x : nat) (H : is_zero x) : x = zero
:= or.elim (dichotomy x)
(assume Hz : x = zero, Hz)
(assume Hs : (∃ n, x = succ n),
exists_elim Hs (λ (w : nat) (Hw : x = succ w),
exists.elim Hs (λ (w : nat) (Hw : x = succ w),
absurd H (eq.subst (symm Hw) (not_is_zero_succ w))))
theorem is_not_zero_to_eq {x : nat} (H : ¬ is_zero x) : ∃ n, x = succ n
@ -48,7 +48,7 @@ theorem is_not_zero_to_eq {x : nat} (H : ¬ is_zero x) : ∃ n, x = succ n
(assume Hs, Hs)
theorem not_zero_add (x y : nat) (H : ¬ is_zero y) : ¬ is_zero (x + y)
:= exists_elim (is_not_zero_to_eq H)
:= 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}

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

@ -4,4 +4,4 @@ constant p : num → num → num → Prop
axiom H1 : ∃ x y z, p x y z
axiom H2 : ∀ {x y z : num}, p x y z → p x x x
theorem tst : ∃ x, p x x x
:= obtain a b c H, from H1, exists_intro a (H2 H)
:= obtain a b c H, from H1, exists.intro a (H2 H)

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

@ -5,4 +5,4 @@ axiom H1 : ∃ x y z, p x y z
axiom H2 : ∀ {x y z : num}, p x y z → p x x x
theorem tst : ∃ x, p x x x
:= obtain a b c H [visible], from H1,
by (apply exists_intro; apply H2; eassumption)
by (apply exists.intro; apply H2; eassumption)

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

@ -2,7 +2,7 @@ import logic
example : ∃ a : num, a = a :=
begin
fapply exists_intro,
fapply exists.intro,
exact 0,
apply rfl,
end

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

@ -69,7 +69,7 @@ pquot.rec_on q f (λ (a b : A) (H : R a b),
@cast_to_heq _ _ _ _ aux₂ aux₃)
theorem pquot.abs.surjective {A : Type} {R : A → A → Prop} : ∀ q : pquot R, ∃ x : A, pquot.abs R x = q :=
take q, pquot.induction_on q (take a, exists_intro a rfl)
take q, pquot.induction_on q (take a, exists.intro a rfl)
definition pquot.exact {A : Type} (R : A → A → Prop) :=
∀ a b : A, pquot.abs R a = pquot.abs R b → R a b

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

@ -4,10 +4,10 @@ open tactic
definition assump := eassumption
theorem tst1 {A : Type} {a b c : A} {p : A → A → Prop} (H1 : p a b) (H2 : p b c) : ∃ x, p a x ∧ p x c
:= by apply exists_intro; apply and.intro; assump; assump
:= by apply exists.intro; apply and.intro; assump; assump
theorem tst2 {A : Type} {a b c d : A} {p : A → A → Prop} (Ha : p a c) (H1 : p a b) (Hb : p b d) (H2 : p b c) : ∃ x, p a x ∧ p x c
:= by apply exists_intro; apply and.intro; assump; assump
:= by apply exists.intro; apply and.intro; assump; assump
(*
print(get_env():find("tst2"):value())

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

@ -26,13 +26,13 @@ check 2 + 3
definition assump : tactic := tactic.eassumption
theorem T1 {p : nat → Prop} {a : nat } (H : p (a+2)) : ∃ x, p (succ x)
:= by apply exists_intro; assump
:= by apply exists.intro; assump
definition is_zero (n : nat)
:= nat.rec true (λ n r, false) n
theorem T2 : ∃ a, (is_zero a) = true
:= by apply exists_intro; apply eq.refl
:= by apply exists.intro; apply eq.refl
end nat
end experiment

10
tests/lean/slow/nat_bug2.lean
View file

@ -60,7 +60,7 @@ theorem zero_or_succ (n : ℕ) : n = 0 ∨ n = succ (pred n)
(show succ m = succ (pred (succ m)), from congr_arg succ (pred_succ m⁻¹)))
theorem zero_or_succ2 (n : ℕ) : n = 0 ∨ ∃k, n = succ k
:= or_of_or_of_imp_of_imp (zero_or_succ n) (assume H, H) (assume H : n = succ (pred n), exists_intro (pred n) H)
:= or_of_or_of_imp_of_imp (zero_or_succ n) (assume H, H) (assume H : n = succ (pred n), exists.intro (pred n) H)
theorem case {P : ℕ → Prop} (n : ℕ) (H1: P 0) (H2 : ∀m, P (succ m)) : P n
:= induction_on n H1 (take m IH, H2 m)
@ -386,7 +386,7 @@ infix `<=` := le
infix `≤` := le
theorem le_intro {n m k : ℕ} (H : n + k = m) : n ≤ m
:= exists_intro k H
:= exists.intro k H
theorem le_elim {n m : ℕ} (H : n ≤ m) : ∃ k, n + k = m
:= H
@ -691,7 +691,7 @@ theorem lt_zero_inv (n : ℕ) : ¬ n < 0
theorem lt_positive {n m : ℕ} (H : n < m) : ∃k, m = succ k
:= discriminate
(take (Hm : m = 0), absurd (subst Hm H) (lt_zero_inv n))
(take (l : ℕ) (Hm : m = succ l), exists_intro l Hm)
(take (l : ℕ) (Hm : m = succ l), exists.intro l Hm)
---------- interaction with le
@ -882,7 +882,7 @@ theorem ne_zero_positive {n : ℕ} (H : n ≠ 0) : n > 0
theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : ∃l, n = succ l
:= discriminate
(take H2, absurd (subst H2 H) (lt_irrefl 0))
(take l Hl, exists_intro l Hl)
(take l Hl, exists.intro l Hl)
theorem add_positive_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n
:= obtain (l : ℕ) (Hl : k = succ l), from pos_imp_eq_succ H,
@ -1276,7 +1276,7 @@ theorem sub_le_self (n m : ℕ) : n - m ≤ n
theorem le_elim_sub (n m : ℕ) (H : n ≤ m) : ∃k, m - k = n
:=
obtain (k : ℕ) (Hk : n + k = m), from le_elim H,
exists_intro k
exists.intro k
(calc
m - k = n + k - k : {symm Hk}
... = n : sub_add_left n k)

10
tests/lean/slow/nat_wo_hints.lean
View file

@ -54,7 +54,7 @@ theorem zero_or_succ (n : ℕ) : n = 0 ∨ n = succ (pred n)
(show succ m = succ (pred (succ m)), from congr_arg succ (pred_succ m⁻¹)))
theorem zero_or_succ2 (n : ℕ) : n = 0 ∨ ∃k, n = succ k
:= or_of_or_of_imp_of_imp (zero_or_succ n) (assume H, H) (assume H : n = succ (pred n), exists_intro (pred n) H)
:= or_of_or_of_imp_of_imp (zero_or_succ n) (assume H, H) (assume H : n = succ (pred n), exists.intro (pred n) H)
theorem case {P : ℕ → Prop} (n : ℕ) (H1: P 0) (H2 : ∀m, P (succ m)) : P n
:= induction_on n H1 (take m IH, H2 m)
@ -380,7 +380,7 @@ infix `<=` := le
infix `≤` := le
theorem le_intro {n m k : ℕ} (H : n + k = m) : n ≤ m
:= exists_intro k H
:= exists.intro k H
theorem le_elim {n m : ℕ} (H : n ≤ m) : ∃ k, n + k = m
:= H
@ -689,7 +689,7 @@ theorem lt_zero_inv (n : ℕ) : ¬ n < 0
theorem lt_positive {n m : ℕ} (H : n < m) : ∃k, m = succ k
:= discriminate
(take (Hm : m = 0), absurd (subst Hm H) (lt_zero_inv n))
(take (l : ℕ) (Hm : m = succ l), exists_intro l Hm)
(take (l : ℕ) (Hm : m = succ l), exists.intro l Hm)
---------- interaction with le
@ -880,7 +880,7 @@ theorem ne_zero_positive {n : ℕ} (H : n ≠ 0) : n > 0
theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : ∃l, n = succ l
:= discriminate
(take H2, absurd (subst H2 H) (lt_irrefl 0))
(take l Hl, exists_intro l Hl)
(take l Hl, exists.intro l Hl)
theorem add_positive_right (n : ℕ) {k : ℕ} (H : k > 0) : n + k > n
:= obtain (l : ℕ) (Hl : k = succ l), from pos_imp_eq_succ H,
@ -1280,7 +1280,7 @@ theorem sub_le_self (n m : ℕ) : n - m ≤ n
theorem le_elim_sub (n m : ℕ) (H : n ≤ m) : ∃k, m - k = n
:=
obtain (k : ℕ) (Hk : n + k = m), from le_elim H,
exists_intro k
exists.intro k
(calc
m - k = n + k - k : {symm Hk}
... = n : sub_add_left n k)