diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org index c4de00b7b9..7a96361d9c 100644 --- a/doc/lean/tutorial.org +++ b/doc/lean/tutorial.org @@ -91,14 +91,14 @@ that =n=, =m= and =o= have type =nat=. The command =variables n m o : nat= can be used as a shorthand for the three commands above. In Lean, proofs are also expressions, and all functionality provided for manipulating -expressions is also available for manipulating proofs. For example, =refl n= is a proof -for =n = n=. In Lean, =refl= is the reflexivity theorem. +expressions is also available for manipulating proofs. For example, =eq.refl n= is a proof +for =n = n=. In Lean, =eq.refl= is the reflexivity theorem. #+BEGIN_SRC lean import data.nat open nat variable n : nat - check refl n + check eq.refl n #+END_SRC The command =axiom= postulates that a given proposition holds. @@ -196,11 +196,11 @@ is quite simple, we are just instructing Lean to automatically insert the placeh Sometimes, Lean will not be able to infer the parameters automatically. The annotation =@f= instructs Lean that we want to provide the implicit arguments for =f= explicitly. -The theorems =refl=, =trans= and =symm= all have implicit arguments. +The theorems =eq.refl=, =trans= and =symm= all have implicit arguments. #+BEGIN_SRC lean import logic - check @refl + check @eq.refl check @symm check @trans #+END_SRC @@ -249,13 +249,13 @@ In the command above, Lean reports that =Type.{l_1}= that lives in universe =l_1= has type =Type.{succ l_1}=. That is, its type lives in the universe =l_1 + 1=. -Definitions such as =refl=, =symm= and =trans= are all universe +Definitions such as =eq.refl=, =symm= and =trans= are all universe polymorphic. #+BEGIN_SRC lean import logic set_option pp.universes true - check @refl + check @eq.refl check @symm check @trans #+END_SRC @@ -416,13 +416,13 @@ In Lean, we say two terms are _definitionally equal_ if the have the same normal form. For example, the terms =(λ x : nat, x + 1) a= and =a + 1= are definitionally equal. The Lean type/proof checker uses the normalizer when checking types/proofs. So, we can prove that two definitionally equal terms -are equal using just =refl=. Here is a simple example. +are equal using just =eq.refl=. Here is a simple example. #+BEGIN_SRC lean import data.nat open nat - theorem def_eq_th (a : nat) : ((λ x : nat, x + 1) a) = a + 1 := refl (a+1) + theorem def_eq_th (a : nat) : ((λ x : nat, x + 1) a) = a + 1 := eq.refl (a+1) #+END_SRC ** Provable equality @@ -443,15 +443,15 @@ and elimination theorems for the basic Boolean connectives. *** And (conjunction) -The expression =and_intro H1 H2= creates a proof for =a ∧ b= using proofs -=H1 : a= and =H2 : b=. We say =and_intro= is the _and-introduction_ operation. -In the following example we use =and_intro= for creating a proof for +The expression =and.intro H1 H2= creates a proof for =a ∧ b= using proofs +=H1 : a= and =H2 : b=. We say =and.intro= is the _and-introduction_ operation. +In the following example we use =and.intro= for creating a proof for =p → q → p ∧ q=. #+BEGIN_SRC lean import logic variables p q : Prop - check fun (Hp : p) (Hq : q), and_intro Hp Hq + check fun (Hp : p) (Hq : q), and.intro Hp Hq #+END_SRC The expression =and_elim_left H= creates a proof =a= from a proof =H : a ∧ b=. @@ -471,7 +471,7 @@ Now, we prove =p ∧ q → q ∧ p= with the following simple proof term. #+BEGIN_SRC lean import logic variables p q : Prop - check fun H : p ∧ q, and_intro (and_elim_right H) (and_elim_left H) + check fun H : p ∧ q, and.intro (and_elim_right H) (and_elim_left H) #+END_SRC Note that the proof term is very similar to a function that just swaps the @@ -479,17 +479,17 @@ elements of a pair. *** (disjunction) -The expression =or_intro_left b H1= creates a proof for =a ∨ b= using a proof =H1 : a=. -Similarly, =or_intro_right a H2= creates a proof for =a ∨ b= using a proof =H2 : b=. +The expression =or.intro_left b H1= creates a proof for =a ∨ b= using a proof =H1 : a=. +Similarly, =or.intro_right a H2= creates a proof for =a ∨ b= using a proof =H2 : b=. We say they are the _left/right or-introduction_. #+BEGIN_SRC lean import logic variables p q : Prop -- Proof for p → p ∨ q - check fun H : p, or_intro_left q H + check fun H : p, or.intro_left q H -- Proof for q → p ∨ q - check fun H : q, or_intro_right p H + check fun H : q, or.intro_right p H #+END_SRC The or-elimination rule is slightly more complicated. The basic idea is the @@ -503,15 +503,15 @@ In the following example, we use =or_elim= to prove that =p v q → q ∨ p=. variables p q : Prop check fun H : p ∨ q, or_elim H - (fun Hp : p, or_intro_right q Hp) - (fun Hq : q, or_intro_left p Hq) + (fun Hp : p, or.intro_right q Hp) + (fun Hq : q, or.intro_left p Hq) #+END_SRC -In most cases, the first argument of =or_intro_right= and -=or_intro_left= can be inferred automatically by Lean. Moreover, Lean -provides =or_inr= and =or_inl= as shorthands for =or_intro_right _= -and =or_intro_left _=. These two shorthands are extensively used in +In most cases, the first argument of =or.intro_right= and +=or.intro_left= can be inferred automatically by Lean. Moreover, Lean +provides =or_inr= and =or_inl= as shorthands for =or.intro_right _= +and =or.intro_left _=. These two shorthands are extensively used in the Lean standard library. #+BEGIN_SRC lean @@ -573,8 +573,8 @@ Here is the proof term for =a ∧ b ↔ b ∧ a= import logic variables a b : Prop check iff_intro - (fun H : a ∧ b, and_intro (and_elim_right H) (and_elim_left H)) - (fun H : b ∧ a, and_intro (and_elim_right H) (and_elim_left H)) + (fun H : a ∧ b, and.intro (and_elim_right H) (and_elim_left H)) + (fun H : b ∧ a, and.intro (and_elim_right H) (and_elim_left H)) #+END_SRC In Lean, we can use =assume= instead of =fun= to make proof terms look @@ -584,8 +584,8 @@ more like proofs found in text books. import logic variables a b : Prop check iff_intro - (assume H : a ∧ b, and_intro (and_elim_right H) (and_elim_left H)) - (assume H : b ∧ a, and_intro (and_elim_right H) (and_elim_left H)) + (assume H : a ∧ b, and.intro (and_elim_right H) (and_elim_left H)) + (assume H : b ∧ a, and.intro (and_elim_right H) (and_elim_left H)) #+END_SRC *** True and False @@ -634,7 +634,7 @@ In Lean, the dependent functions is written as =forall a : A, B a=, =Pi a : A, B a=, =∀ x : A, B a=, or =Π x : A, B a=. We usually use =forall= and =∀= for propositions, and =Pi= and =Π= for everything else. In the previous examples, we have seen many examples of -dependent functions. The theorems =refl=, =trans= and =symm=, and the +dependent functions. The theorems =eq.refl=, =trans= and =symm=, and the equality are all dependent functions. The universal quantifier is just a dependent function. diff --git a/library/data/bool.lean b/library/data/bool.lean index 08aa6a9a5e..47fb6d15d7 100644 --- a/library/data/bool.lean +++ b/library/data/bool.lean @@ -16,13 +16,13 @@ theorem cases_on {p : bool → Prop} (b : bool) (H0 : p ff) (H1 : p tt) : p b := rec H0 H1 b theorem bool_inhabited [instance] : inhabited bool := -inhabited_mk ff +inhabited.mk ff definition cond {A : Type} (b : bool) (t e : A) := rec e t b theorem dichotomy (b : bool) : b = ff ∨ b = tt := -cases_on b (or_inl (refl ff)) (or_inr (refl tt)) +cases_on b (or_inl (eq.refl ff)) (or_inr (eq.refl tt)) theorem cond_ff {A : Type} (t e : A) : cond ff t e = e := rfl @@ -39,8 +39,8 @@ assume H : ff = tt, absurd theorem decidable_eq [instance] (a b : bool) : decidable (a = b) := rec - (rec (inl (refl ff)) (inr ff_ne_tt) b) - (rec (inr (ne_symm ff_ne_tt)) (inl (refl tt)) b) + (rec (inl (eq.refl ff)) (inr ff_ne_tt) b) + (rec (inr (ne_symm ff_ne_tt)) (inl (eq.refl tt)) b) a definition bor (a b : bool) := @@ -52,21 +52,21 @@ rfl infixl `||` := bor theorem bor_tt_right (a : bool) : a || tt = tt := -cases_on a (refl (ff || tt)) (refl (tt || tt)) +cases_on a (eq.refl (ff || tt)) (eq.refl (tt || tt)) theorem bor_ff_left (a : bool) : ff || a = a := -cases_on a (refl (ff || ff)) (refl (ff || tt)) +cases_on a (eq.refl (ff || ff)) (eq.refl (ff || tt)) theorem bor_ff_right (a : bool) : a || ff = a := -cases_on a (refl (ff || ff)) (refl (tt || ff)) +cases_on a (eq.refl (ff || ff)) (eq.refl (tt || ff)) theorem bor_id (a : bool) : a || a = a := -cases_on a (refl (ff || ff)) (refl (tt || tt)) +cases_on a (eq.refl (ff || ff)) (eq.refl (tt || tt)) theorem bor_comm (a b : bool) : a || b = b || a := cases_on a - (cases_on b (refl (ff || ff)) (refl (ff || tt))) - (cases_on b (refl (tt || ff)) (refl (tt || tt))) + (cases_on b (eq.refl (ff || ff)) (eq.refl (ff || tt))) + (cases_on b (eq.refl (tt || ff)) (eq.refl (tt || tt))) theorem bor_assoc (a b c : bool) : (a || b) || c = a || (b || c) := cases_on a @@ -81,7 +81,7 @@ rec (assume H : ff || b = tt, have Hb : b = tt, from (bor_ff_left b) ▸ H, or_inr Hb) - (assume H, or_inl (refl tt)) + (assume H, or_inl (eq.refl tt)) a definition band (a b : bool) := @@ -93,21 +93,21 @@ theorem band_ff_left (a : bool) : ff && a = ff := rfl theorem band_tt_left (a : bool) : tt && a = a := -cases_on a (refl (tt && ff)) (refl (tt && tt)) +cases_on a (eq.refl (tt && ff)) (eq.refl (tt && tt)) theorem band_ff_right (a : bool) : a && ff = ff := -cases_on a (refl (ff && ff)) (refl (tt && ff)) +cases_on a (eq.refl (ff && ff)) (eq.refl (tt && ff)) theorem band_tt_right (a : bool) : a && tt = a := -cases_on a (refl (ff && tt)) (refl (tt && tt)) +cases_on a (eq.refl (ff && tt)) (eq.refl (tt && tt)) theorem band_id (a : bool) : a && a = a := -cases_on a (refl (ff && ff)) (refl (tt && tt)) +cases_on a (eq.refl (ff && ff)) (eq.refl (tt && tt)) theorem band_comm (a b : bool) : a && b = b && a := cases_on a - (cases_on b (refl (ff && ff)) (refl (ff && tt))) - (cases_on b (refl (tt && ff)) (refl (tt && tt))) + (cases_on b (eq.refl (ff && ff)) (eq.refl (ff && tt))) + (cases_on b (eq.refl (tt && ff)) (eq.refl (tt && tt))) theorem band_assoc (a b c : bool) : (a && b) && c = a && (b && c) := cases_on a @@ -135,7 +135,7 @@ definition bnot (a : bool) := rec tt ff a notation `!` x:max := bnot x theorem bnot_bnot (a : bool) : !!a = a := -cases_on a (refl (!!ff)) (refl (!!tt)) +cases_on a (eq.refl (!!ff)) (eq.refl (!!tt)) theorem bnot_false : !ff = tt := rfl diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index 37cb7af224..ac1526b199 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -47,10 +47,10 @@ have H3 : pr1 a + pr2 c + pr2 b = pr2 a + pr1 c + pr2 b, from show pr1 a + pr2 c = pr2 a + pr1 c, from add_cancel_right H3 theorem rel_equiv : is_equivalence rel := -is_equivalence_mk - (is_reflexive_mk @rel_refl) - (is_symmetric_mk @rel_symm) - (is_transitive_mk @rel_trans) +is_equivalence.mk + (is_reflexive.mk @rel_refl) + (is_symmetric.mk @rel_symm) + (is_transitive.mk @rel_trans) theorem rel_flip {a b : ℕ × ℕ} (H : rel a b) : rel (flip a) (flip b) := calc @@ -288,7 +288,7 @@ obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a, by simp theorem pos_eq_neg {n m : ℕ} (H : n = -m) : n = 0 ∧ m = 0 := -have H2 : ∀n : ℕ, n = psub (pair n 0), from take n : ℕ, refl (n), +have H2 : ∀n : ℕ, n = psub (pair n 0), from take n : ℕ, rfl, have H3 : psub (pair n 0) = psub (pair 0 m), from iff_mp (by simp) H, have H4 : rel (pair n 0) (pair 0 m), from R_intro_refl quotient @rel_refl H3, have H5 : n + m = 0, from @@ -314,7 +314,7 @@ or_imp_or (or_swap (proj_zero_or (rep a))) a = psub (rep a) : symm (psub_rep a) ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {symm (prod_ext (rep a))} ... = psub (pair (pr1 (rep a)) 0) : {H2} - ... = of_nat (pr1 (rep a)) : refl _)) + ... = of_nat (pr1 (rep a)) : rfl)) (assume H : pr1 (proj (rep a)) = 0, have H2 : pr1 (rep a) = 0, from subst Hrep H, exists_intro (pr2 (rep a)) @@ -323,7 +323,7 @@ or_imp_or (or_swap (proj_zero_or (rep a))) ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {symm (prod_ext (rep a))} ... = psub (pair 0 (pr2 (rep a))) : {H2} ... = -(psub (pair (pr2 (rep a)) 0)) : by simp - ... = -(of_nat (pr2 (rep a))) : refl _)) + ... = -(of_nat (pr2 (rep a))) : rfl)) opaque_hint (hiding int) @@ -363,7 +363,7 @@ theorem of_nat_eq_neg_of_nat {n m : ℕ} (H : n = - m) : n = 0 ∧ m = 0 := have H2 : n = psub (pair 0 m), from calc n = -m : H - ... = -(psub (pair m 0)) : refl (-m) + ... = -(psub (pair m 0)) : rfl ... = psub (pair 0 m) : by simp, have H3 : rel (pair n 0) (pair 0 m), from R_intro_refl quotient @rel_refl H2, have H4 : n + m = 0, from @@ -417,7 +417,7 @@ right_comm add_comm add_assoc a b c theorem add_zero_right (a : ℤ) : a + 0 = a := obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a, -have H0 : 0 = psub (pair 0 0), from refl 0, +have H0 : 0 = psub (pair 0 0), from rfl, by simp theorem add_zero_left (a : ℤ) : 0 + a = a := @@ -446,7 +446,7 @@ by simp -- TODO: note, we have to add #nat to get the right interpretation theorem add_of_nat (n m : nat) : of_nat n + of_nat m = #nat n + m := -- this is of_nat (n + m) -have H : ∀n : ℕ, n = psub (pair n 0), from take n : ℕ, refl n, +have H : ∀n : ℕ, n = psub (pair n 0), from take n : ℕ, rfl, by simp -- add_rewrite add_of_nat @@ -459,10 +459,10 @@ definition sub (a b : ℤ) : ℤ := a + -b infixl `-` := int.sub theorem sub_def (a b : ℤ) : a - b = a + -b := -refl (a - b) +rfl theorem add_neg_right (a b : ℤ) : a + -b = a - b := -refl (a - b) +rfl theorem add_neg_left (a b : ℤ) : -a + b = b - a := add_comm (-a) b @@ -470,7 +470,7 @@ add_comm (-a) b -- opaque_hint (hiding int.sub) theorem sub_neg_right (a b : ℤ) : a - (-b) = a + b := -subst (neg_neg b) (refl (a - (-b))) +subst (neg_neg b) (eq.refl (a - (-b))) theorem sub_neg_neg (a b : ℤ) : -a - (-b) = b - a := subst (neg_neg b) (add_comm (-a) (-(-b))) @@ -656,7 +656,7 @@ right_comm mul_comm mul_assoc theorem mul_zero_right (a : ℤ) : a * 0 = 0 := obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a, -have H0 : 0 = psub (pair 0 0), from refl 0, +have H0 : 0 = psub (pair 0 0), from rfl, by simp theorem mul_zero_left (a : ℤ) : 0 * a = 0 := @@ -664,7 +664,7 @@ subst (mul_comm a 0) (mul_zero_right a) theorem mul_one_right (a : ℤ) : a * 1 = a := obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a, -have H1 : 1 = psub (pair 1 0), from refl 1, +have H1 : 1 = psub (pair 1 0), from rfl, by simp theorem mul_one_left (a : ℤ) : 1 * a = a := @@ -707,7 +707,7 @@ calc ... = a * b + - (a * c) : {mul_neg_right a c} theorem mul_of_nat (n m : ℕ) : of_nat n * of_nat m = n * m := -have H : ∀n : ℕ, n = psub (pair n 0), from take n : ℕ, refl n, +have H : ∀n : ℕ, n = psub (pair n 0), from take n : ℕ, rfl, by simp theorem mul_to_nat (a b : ℤ) : (to_nat (a * b)) = #nat (to_nat a) * (to_nat b) := diff --git a/library/data/int/order.lean b/library/data/int/order.lean index b5d6098d65..b35875261e 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -76,7 +76,7 @@ show a = b, from -- ### interaction with add theorem le_add_of_nat_right (a : ℤ) (n : ℕ) : a ≤ a + n := -le_intro (refl (a + n)) +le_intro (eq.refl (a + n)) theorem le_add_of_nat_left (a : ℤ) (n : ℕ) : a ≤ n + a := le_intro (add_comm a n) @@ -371,7 +371,7 @@ int_by_cases a show n ≤ -succ m ∨ n > -succ m, from have H0 : -succ m < -m, from lt_neg (subst (symm (of_nat_succ m)) (self_lt_succ m)), have H : -succ m < n, from lt_le_trans H0 (neg_le_pos m n), - or_intro_right _ H)) + or_inr H)) (take n : ℕ, int_by_cases_succ b (take m : ℕ, diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index 5214f93933..01baafb365 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -9,7 +9,7 @@ import logic data.num tools.tactic struc.binary tools.helper_tactics -open num tactic binary eq_ops +open tactic binary eq_ops open decidable (hiding induction_on rec_on) open relation -- for subst_iff open helper_tactics @@ -44,8 +44,8 @@ abbreviation plus (x y : ℕ) : ℕ := nat.rec x (λ n r, succ r) y definition to_nat [coercion] [inline] (n : num) : ℕ := -num.num.rec zero - (λ n, num.pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n +num.rec zero + (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n -- Successor and predecessor @@ -73,7 +73,7 @@ opaque_hint (hiding pred) theorem zero_or_succ_pred (n : ℕ) : n = 0 ∨ n = succ (pred n) := induction_on n - (or_inl (refl 0)) + (or_inl rfl) (take m IH, or_inr (show succ m = succ (pred (succ m)), from congr_arg succ pred_succ⁻¹)) @@ -107,7 +107,7 @@ have general : ∀n, decidable (n = m), from rec_on m (take n, rec_on n - (inl (refl 0)) + (inl rfl) (λ m iH, inr succ_ne_zero)) (λ (m' : ℕ) (iH1 : ∀n, decidable (n = m')), take n, rec_on n @@ -126,11 +126,11 @@ theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1) (H3 : ∀ (n : ℕ) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) : P a := have stronger : P a ∧ P (succ a), from induction_on a - (and_intro H1 H2) + (and.intro H1 H2) (take k IH, have IH1 : P k, from and_elim_left IH, have IH2 : P (succ k), from and_elim_right IH, - and_intro IH2 (H3 k IH1 IH2)), + and.intro IH2 (H3 k IH1 IH2)), and_elim_left stronger theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m) @@ -229,7 +229,7 @@ have H2 : m + n = m + k, from add_comm ⬝ H ⬝ add_comm, theorem add_eq_zero_left {n m : ℕ} : n + m = 0 → n = 0 := induction_on n - (take (H : 0 + m = 0), refl 0) + (take (H : 0 + m = 0), rfl) (take k IH, assume H : succ k + m = 0, absurd @@ -242,7 +242,7 @@ theorem add_eq_zero_right {n m : ℕ} (H : n + m = 0) : m = 0 := add_eq_zero_left (add_comm ⬝ H) theorem add_eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0 := -and_intro (add_eq_zero_left H) (add_eq_zero_right H) +and.intro (add_eq_zero_left H) (add_eq_zero_right H) -- ### misc diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index d88e1ac40a..af160ad1b0 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -103,7 +103,7 @@ case_strong_induction_on m have H3 : restrict default measure f (succ m) x = rec_val x f, from calc restrict default measure f (succ m) x = f x : if_pos H1 - ... = f' (succ m') x : refl _ + ... = f' (succ m') x : eq.refl _ ... = if measure x < succ m' then rec_val x (f' m') else default : rfl ... = rec_val x (f' m') : if_pos self_lt_succ ... = rec_val x f : rec_decreasing _ _ _ H3a, @@ -164,8 +164,8 @@ show lhs = rhs, from lhs = 0 : if_pos H1 ... = rhs : (if_pos H1)⁻¹) (assume H1 : ¬ (y = 0 ∨ x < y), - have H2a : y ≠ 0, from assume H, H1 (or_intro_left _ H), - have H2b : ¬ x < y, from assume H, H1 (or_intro_right _ H), + have H2a : y ≠ 0, from assume H, H1 (or_inl H), + have H2b : ¬ x < y, from assume H, H1 (or_inr H), have ypos : y > 0, from ne_zero_imp_pos H2a, have xgey : x ≥ y, from not_lt_imp_ge H2b, have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos, @@ -240,8 +240,8 @@ show lhs = rhs, from lhs = x : if_pos H1 ... = rhs : (if_pos H1)⁻¹) (assume H1 : ¬ (y = 0 ∨ x < y), - have H2a : y ≠ 0, from assume H, H1 (or_intro_left _ H), - have H2b : ¬ x < y, from assume H, H1 (or_intro_right _ H), + have H2a : y ≠ 0, from assume H, H1 (or_inl H), + have H2b : ¬ x < y, from assume H, H1 (or_inr H), have ypos : y > 0, from ne_zero_imp_pos H2a, have xgey : x ≥ y, from not_lt_imp_ge H2b, have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos, @@ -676,7 +676,7 @@ gcd_induct m n dvd_add (dvd_trans (and_elim_left IH) dvd_mul_self_right) (and_elim_right IH), have H1 : gcd n (m mod n) | m, from div_mod_eq⁻¹ ▸ H, have gcd_eq : gcd n (m mod n) = gcd m n, from symm (gcd_pos _ npos), - show (gcd m n | m) ∧ (gcd m n | n), from gcd_eq ▸ (and_intro H1 (and_elim_left IH))) + show (gcd m n | m) ∧ (gcd m n | n), from gcd_eq ▸ (and.intro H1 (and_elim_left IH))) theorem gcd_dvd_left (m n : ℕ) : (gcd m n | m) := and_elim_left (gcd_dvd _ _) diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index f1c28b62e3..80cf6660c8 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -158,7 +158,7 @@ or_imp_or_left (le_imp_succ_le_or_eq H) theorem succ_le_imp_le_and_ne {n m : ℕ} (H : succ n ≤ m) : n ≤ m ∧ n ≠ m := obtain (k : ℕ) (H2 : succ n + k = m), from (le_elim H), - and_intro + and.intro (have H3 : n + succ k = m, from calc n + succ k = succ n + k : add_move_succ⁻¹ @@ -235,20 +235,20 @@ have general : ∀n, decidable (n ≤ m), from rec_on m (take n, rec_on n - (inl le_refl) - (take m iH, inr not_succ_zero_le)) + (decidable.inl le_refl) + (take m iH, decidable.inr not_succ_zero_le)) (take (m' : ℕ) (iH1 : ∀n, decidable (n ≤ m')) (n : ℕ), rec_on n - (inl zero_le) + (decidable.inl zero_le) (take (n' : ℕ) (iH2 : decidable (n' ≤ succ m')), have d1 : decidable (n' ≤ m'), from iH1 n', decidable.rec_on d1 - (assume Hp : n' ≤ m', inl (succ_le Hp)) + (assume Hp : n' ≤ m', decidable.inl (succ_le Hp)) (assume Hn : ¬ n' ≤ m', have H : ¬ succ n' ≤ succ m', from assume Hle : succ n' ≤ succ m', absurd (succ_le_cancel Hle) Hn, - inr H))), + decidable.inr H))), general n -- Less than, Greater than, Greater than or equal @@ -266,7 +266,7 @@ infix `≥` := ge abbreviation gt (n m : ℕ) := m < n infix `>` := gt -theorem lt_def (n m : ℕ) : (n < m) = (succ n ≤ m) := refl (n < m) +theorem lt_def (n m : ℕ) : (n < m) = (succ n ≤ m) := rfl -- add_rewrite gt_def ge_def --it might be possible to remove this in Lean 0.2 diff --git a/library/data/num.lean b/library/data/num.lean index c7255d9396..c5058ce154 100644 --- a/library/data/num.lean +++ b/library/data/num.lean @@ -3,10 +3,8 @@ -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura ---------------------------------------------------------------------------------------------------- - import logic.classes.inhabited -namespace num -- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26. -- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))). -- This representation can be coerced in whatever we want (e.g., naturals, integers, reals, etc). @@ -20,9 +18,7 @@ zero : num, pos : pos_num → num theorem inhabited_pos_num [instance] : inhabited pos_num := -inhabited_mk one +inhabited.mk pos_num.one theorem num_inhabited [instance] : inhabited num := -inhabited_mk zero - -end num +inhabited.mk num.zero diff --git a/library/data/option.lean b/library/data/option.lean index 06922e8b4c..dbd779df1a 100644 --- a/library/data/option.lean +++ b/library/data/option.lean @@ -5,22 +5,22 @@ import logic.core.eq logic.classes.inhabited logic.classes.decidable open eq_ops decidable -namespace option - inductive option (A : Type) : Type := none {} : option A, some : A → option A +namespace option + theorem induction_on [protected] {A : Type} {p : option A → Prop} (o : option A) (H1 : p none) (H2 : ∀a, p (some a)) : p o := -option.rec H1 H2 o +rec H1 H2 o definition rec_on [protected] {A : Type} {C : option A → Type} (o : option A) (H1 : C none) (H2 : ∀a, C (some a)) : C o := -option.rec H1 H2 o +rec H1 H2 o definition is_none {A : Type} (o : option A) : Prop := -option.rec true (λ a, false) o +rec true (λ a, false) o theorem is_none_none {A : Type} : is_none (@none A) := trivial @@ -37,7 +37,7 @@ theorem some_inj {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = congr_arg (option.rec a₁ (λ a, a)) H theorem option_inhabited [instance] (A : Type) : inhabited (option A) := -inhabited_mk none +inhabited.mk none theorem decidable_eq [instance] {A : Type} {H : ∀a₁ a₂ : A, decidable (a₁ = a₂)} (o₁ o₂ : option A) : decidable (o₁ = o₂) := diff --git a/library/data/prod.lean b/library/data/prod.lean index 4d8ff8b612..52f1a9b35f 100644 --- a/library/data/prod.lean +++ b/library/data/prod.lean @@ -12,12 +12,14 @@ import logic.classes.inhabited logic.core.eq logic.classes.decidable open inhabited decidable inductive prod (A B : Type) : Type := -pair : A → B → prod A B +mk : A → B → prod A B + +abbreviation pair := @prod.mk infixr `×` := prod -- notation for n-ary tuples -notation `(` h `,` t:(foldl `,` (e r, pair r e) h) `)` := t +notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t namespace prod @@ -38,7 +40,7 @@ section rec H p theorem prod_ext (p : prod A B) : pair (pr1 p) (pr2 p) = p := - destruct p (λx y, refl (x, y)) + destruct p (λx y, eq.refl (x, y)) theorem pair_eq {a1 a2 : A} {b1 b2 : B} (H1 : a1 = a2) (H2 : b1 = b2) : (a1, b1) = (a2, b2) := subst H1 (subst H2 rfl) @@ -47,13 +49,13 @@ section destruct p1 (take a1 b1, destruct p2 (take a2 b2 H1 H2, pair_eq H1 H2)) theorem prod_inhabited [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) := - inhabited_destruct H1 (λa, inhabited_destruct H2 (λb, inhabited_mk (pair a b))) + inhabited.destruct H1 (λa, inhabited.destruct H2 (λb, inhabited.mk (pair a b))) theorem prod_eq_decidable [instance] (u v : A × B) (H1 : decidable (pr1 u = pr1 v)) (H2 : decidable (pr2 u = pr2 v)) : decidable (u = v) := have H3 : u = v ↔ (pr1 u = pr1 v) ∧ (pr2 u = pr2 v), from iff_intro - (assume H, subst H (and_intro rfl rfl)) + (assume H, subst H (and.intro rfl rfl)) (assume H, and_elim H (assume H4 H5, prod_eq H4 H5)), decidable_iff_equiv _ (iff_symm H3) diff --git a/library/data/quotient/aux.lean b/library/data/quotient/aux.lean index e0fe7a31e2..cb9b1f2871 100644 --- a/library/data/quotient/aux.lean +++ b/library/data/quotient/aux.lean @@ -17,7 +17,7 @@ namespace quotient definition flip {A B : Type} (a : A × B) : B × A := pair (pr2 a) (pr1 a) -theorem flip_def {A B : Type} (a : A × B) : flip a = pair (pr2 a) (pr1 a) := refl (flip a) +theorem flip_def {A B : Type} (a : A × B) : flip a = pair (pr2 a) (pr1 a) := eq.refl (flip a) theorem flip_pair {A B : Type} (a : A) (b : B) : flip (pair a b) = pair b a := rfl diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean index 93169a2685..b81c169877 100644 --- a/library/data/quotient/basic.lean +++ b/library/data/quotient/basic.lean @@ -27,10 +27,10 @@ abbreviation is_quotient {A B : Type} (R : A → A → Prop) (abs : A → B) (re theorem intro {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (H1 : ∀b, abs (rep b) = b) (H2 : ∀b, R (rep b) (rep b)) (H3 : ∀r s, R r s ↔ (R r r ∧ R s s ∧ abs r = abs s)) : is_quotient R abs rep := -and_intro H1 (and_intro H2 H3) +and.intro H1 (and.intro H2 H3) theorem and_absorb_left {a : Prop} (b : Prop) (Ha : a) : a ∧ b ↔ b := -iff_intro (assume Hab, and_elim_right Hab) (assume Hb, and_intro Ha Hb) +iff_intro (assume Hab, and_elim_right Hab) (assume Hb, and.intro Ha Hb) theorem intro_refl {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (H1 : reflexive R) (H2 : ∀b, abs (rep b) = b) @@ -70,11 +70,11 @@ and_elim_right (and_elim_right (iff_elim_left (R_iff Q r s) H)) theorem R_intro {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) {r s : A} (H1 : R r r) (H2 : R s s) (H3 : abs r = abs s) : R r s := -iff_elim_right (R_iff Q r s) (and_intro H1 (and_intro H2 H3)) +iff_elim_right (R_iff Q r s) (and.intro H1 (and.intro H2 H3)) theorem R_intro_refl {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) (H1 : reflexive R) {r s : A} (H2 : abs r = abs s) : R r s := -iff_elim_right (R_iff Q r s) (and_intro (H1 r) (and_intro (H1 s) H2)) +iff_elim_right (R_iff Q r s) (and.intro (H1 r) (and.intro (H1 s) H2)) theorem rep_eq {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) {a b : B} (H : R (rep a) (rep b)) : a = b := @@ -115,18 +115,18 @@ R_intro Q Ha Hc Hac definition rec {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) {C : B → Type} (f : forall (a : A), C (abs a)) (b : B) : C b := -eq_rec_on (abs_rep Q b) (f (rep b)) +eq.rec_on (abs_rep Q b) (f (rep b)) theorem comp {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) {C : B → Type} {f : forall (a : A), C (abs a)} - (H : forall (r s : A) (H' : R r s), eq_rec_on (eq_abs Q H') (f r) = f s) + (H : forall (r s : A) (H' : R r s), eq.rec_on (eq_abs Q H') (f r) = f s) {a : A} (Ha : R a a) : rec Q f (abs a) = f a := have H2 [fact] : R a (rep (abs a)), from R_rep_abs Q Ha, calc - rec Q f (abs a) = eq_rec_on _ (f (rep (abs a))) : rfl - ... = eq_rec_on _ (eq_rec_on _ (f a)) : {symm (H _ _ H2)} - ... = eq_rec_on _ (f a) : eq_rec_on_compose (eq_abs Q H2) _ _ - ... = f a : eq_rec_on_id (trans (eq_abs Q H2) (abs_rep Q (abs a))) _ + rec Q f (abs a) = eq.rec_on _ (f (rep (abs a))) : rfl + ... = eq.rec_on _ (eq.rec_on _ (f a)) : {symm (H _ _ H2)} + ... = eq.rec_on _ (f a) : eq.rec_on_compose (eq_abs Q H2) _ _ + ... = f a : eq.rec_on_id (trans (eq_abs Q H2) (abs_rep Q (abs a))) _ definition rec_constant {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A} (Q : is_quotient R abs rep) {C : Type} (f : A → C) (b : B) : C := @@ -204,10 +204,10 @@ opaque_hint (hiding rec rec_constant rec_binary quotient_map quotient_map_binary abbreviation 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) +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) diff --git a/library/data/quotient/classical.lean b/library/data/quotient/classical.lean index b53903c1d8..4378ea3d5b 100644 --- a/library/data/quotient/classical.lean +++ b/library/data/quotient/classical.lean @@ -16,7 +16,7 @@ open relation nonempty subtype definition prelim_map {A : Type} (R : A → A → Prop) (a : A) := -- TODO: it is interesting how the elaborator fails here -- epsilon (fun b, R a b) -@epsilon _ (nonempty_intro a) (fun b, R a b) +@epsilon _ (nonempty.intro a) (fun b, R a b) -- TODO: only needed R reflexive (or weaker: R a a) theorem prelim_map_rel {A : Type} {R : A → A → Prop} (H : is_equivalence R) (a : A) @@ -35,7 +35,7 @@ have H3 : ∀c, R a c ↔ R b c, from (assume H4 : R a c, transR (symmR H2) H4) (assume H4 : R b c, transR H2 H4), have H4 : (fun c, R a c) = (fun c, R b c), from funext (take c, iff_to_eq (H3 c)), -show @epsilon _ (nonempty_intro a) (λc, R a c) = @epsilon _ (nonempty_intro b) (λc, R b c), +show @epsilon _ (nonempty.intro a) (λc, R a c) = @epsilon _ (nonempty.intro b) (λc, R b c), from congr_arg _ H4 definition quotient {A : Type} (R : A → A → Prop) : Type := image (prelim_map R) diff --git a/library/data/set.lean b/library/data/set.lean index 9b3c060bca..c70b70cf7a 100644 --- a/library/data/set.lean +++ b/library/data/set.lean @@ -45,7 +45,7 @@ infixl `∩` := inter theorem mem_inter {T : Type} (x : T) (A B : set T) : x ∈ A ∩ B ↔ (x ∈ A ∧ x ∈ B) := iff_intro - (assume H, and_intro (band_eq_tt_elim_left H) (band_eq_tt_elim_right H)) + (assume H, and.intro (band_eq_tt_elim_left H) (band_eq_tt_elim_right H)) (assume H, have e1 : A x = tt, from and_elim_left H, have e2 : B x = tt, from and_elim_right H, diff --git a/library/data/sigma.lean b/library/data/sigma.lean index 841290a50c..59b92a69bc 100644 --- a/library/data/sigma.lean +++ b/library/data/sigma.lean @@ -12,16 +12,14 @@ dpair : Πx : A, B x → sigma B notation `Σ` binders `,` r:(scoped P, sigma P) := r namespace sigma - section - parameters {A : Type} {B : A → Type} abbreviation dpr1 (p : Σ x, B x) : A := rec (λ a b, a) p abbreviation dpr2 {A : Type} {B : A → Type} (p : Σ x, B x) : B (dpr1 p) := rec (λ a b, b) p - theorem dpr1_dpair (a : A) (b : B a) : dpr1 (dpair a b) = a := refl a - theorem dpr2_dpair (a : A) (b : B a) : dpr2 (dpair a b) = b := refl b + theorem dpr1_dpair (a : A) (b : B a) : dpr1 (dpair a b) = a := rfl + theorem dpr2_dpair (a : A) (b : B a) : dpr2 (dpair a b) = b := rfl -- TODO: remove prefix when we can protect it theorem sigma_destruct {P : sigma B → Prop} (p : sigma B) (H : ∀a b, P (dpair a b)) : P p := @@ -31,29 +29,26 @@ section sigma_destruct p (take a b, rfl) -- Note that we give the general statment explicitly, to help the unifier - theorem dpair_eq {a1 a2 : A} {b1 : B a1} {b2 : B a2} (H1 : a1 = a2) (H2 : eq_rec_on H1 b1 = b2) : + theorem dpair_eq {a1 a2 : A} {b1 : B a1} {b2 : B a2} (H1 : a1 = a2) (H2 : eq.rec_on H1 b1 = b2) : dpair a1 b1 = dpair a2 b2 := - (show ∀(b2 : B a2) (H1 : a1 = a2) (H2 : eq_rec_on H1 b1 = b2), dpair a1 b1 = dpair a2 b2, from + (show ∀(b2 : B a2) (H1 : a1 = a2) (H2 : eq.rec_on H1 b1 = b2), dpair a1 b1 = dpair a2 b2, from eq.rec (take (b2' : B a1), assume (H1' : a1 = a1), - assume (H2' : eq_rec_on H1' b1 = b2'), + assume (H2' : eq.rec_on H1' b1 = b2'), show dpair a1 b1 = dpair a1 b2', from calc - dpair a1 b1 = dpair a1 (eq_rec_on H1' b1) : {symm (eq_rec_on_id H1' b1)} + dpair a1 b1 = dpair a1 (eq.rec_on H1' b1) : {symm (eq.rec_on_id H1' b1)} ... = dpair a1 b2' : {H2'}) H1) b2 H1 H2 theorem sigma_eq {p1 p2 : Σx : A, B x} : - ∀(H1 : dpr1 p1 = dpr1 p2) (H2 : eq_rec_on H1 (dpr2 p1) = (dpr2 p2)), p1 = p2 := + ∀(H1 : dpr1 p1 = dpr1 p2) (H2 : eq.rec_on H1 (dpr2 p1) = (dpr2 p2)), p1 = p2 := sigma_destruct p1 (take a1 b1, sigma_destruct p2 (take a2 b2 H1 H2, dpair_eq H1 H2)) theorem sigma_inhabited [instance] (H1 : inhabited A) (H2 : inhabited (B (default A))) : inhabited (sigma B) := - inhabited_destruct H1 (λa, inhabited_destruct H2 (λb, inhabited_mk (dpair (default A) b))) + inhabited.destruct H1 (λa, inhabited.destruct H2 (λb, inhabited.mk (dpair (default A) b))) end - -instance sigma_inhabited - end sigma diff --git a/library/data/string.lean b/library/data/string.lean index 9c73b2412d..64261555df 100644 --- a/library/data/string.lean +++ b/library/data/string.lean @@ -6,19 +6,15 @@ import data.bool open bool inhabited -namespace string - inductive char : Type := -ascii : bool → bool → bool → bool → bool → bool → bool → bool → char +mk : bool → bool → bool → bool → bool → bool → bool → bool → char inductive string : Type := empty : string, str : char → string → string theorem char_inhabited [instance] : inhabited char := -inhabited_mk (ascii ff ff ff ff ff ff ff ff) +inhabited.mk (char.mk ff ff ff ff ff ff ff ff) theorem string_inhabited [instance] : inhabited string := -inhabited_mk empty - -end string +inhabited.mk string.empty diff --git a/library/data/subtype.lean b/library/data/subtype.lean index 636b350ea9..c70977178d 100644 --- a/library/data/subtype.lean +++ b/library/data/subtype.lean @@ -21,7 +21,7 @@ section definition elt_of (a : {x, P x}) : A := rec (λ x y, x) a theorem has_property (a : {x, P x}) : P (elt_of a) := rec (λ x y, y) a - theorem elt_of_tag (a : A) (H : P a) : elt_of (tag a H) = a := refl a + theorem elt_of_tag (a : A) (H : P a) : elt_of (tag a H) = a := rfl theorem destruct [protected] {Q : {x, P x} → Prop} (a : {x, P x}) (H : ∀(x : A) (H1 : P x), Q (tag x H1)) : Q a := @@ -40,7 +40,7 @@ section destruct a1 (take x1 H1, destruct a2 (take x2 H2 H, tag_eq H)) theorem subtype_inhabited [instance] {a : A} (H : P a) : inhabited {x, P x} := - inhabited_mk (tag a H) + inhabited.mk (tag a H) theorem eq_decidable [protected] [instance] (a1 a2 : {x, P x}) (H : decidable (elt_of a1 = elt_of a2)) : decidable (a1 = a2) := diff --git a/library/data/sum.lean b/library/data/sum.lean index 7e50e12ec9..35b0c4c4aa 100644 --- a/library/data/sum.lean +++ b/library/data/sum.lean @@ -11,13 +11,12 @@ import logic.core.prop logic.classes.inhabited logic.classes.decidable open inhabited decidable -namespace sum - -- TODO: take this outside the namespace when the inductive package handles it better inductive sum (A B : Type) : Type := inl : A → sum A B, inr : B → sum A B +namespace sum infixr `⊎` := sum namespace sum_plus_notation @@ -57,10 +56,10 @@ have H2 : f (inr A b2), from subst H H1, H2 theorem sum_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A ⊎ B) := -inhabited_mk (inl B (default A)) +inhabited.mk (inl B (default A)) theorem sum_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabited (A ⊎ B) := -inhabited_mk (inr A (default B)) +inhabited.mk (inr A (default B)) theorem sum_eq_decidable [instance] {A B : Type} (s1 s2 : A ⊎ B) (H1 : ∀a1 a2 : A, decidable (inl B a1 = inl B a2)) diff --git a/library/data/unit.lean b/library/data/unit.lean index 53a13e0d5a..412db7f0dd 100644 --- a/library/data/unit.lean +++ b/library/data/unit.lean @@ -1,28 +1,27 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Author: Leonardo de Moura - import logic.classes.decidable logic.classes.inhabited open decidable -namespace unit - inductive unit : Type := star : unit +namespace unit + notation `⋆`:max := star -theorem unit_eq (a b : unit) : a = b := +theorem at_most_one (a b : unit) : a = b := rec (rec rfl b) a -theorem unit_eq_star (a : unit) : a = star := -unit_eq a star +theorem eq_star (a : unit) : a = star := +at_most_one a star theorem unit_inhabited [instance] : inhabited unit := -inhabited_mk ⋆ +inhabited.mk ⋆ theorem decidable_eq [instance] (a b : unit) : decidable (a = b) := -inl (unit_eq a b) +inl (at_most_one a b) end unit diff --git a/library/hott/path.lean b/library/hott/path.lean index 96d7bc8260..9d087fc693 100644 --- a/library/hott/path.lean +++ b/library/hott/path.lean @@ -20,6 +20,7 @@ idpath : path a a infix `≈` := path notation x `≈` y:50 `:>`:0 A:0 := @path A x y -- TODO: is this right? +abbreviation idpath := @path.idpath notation `idp`:max := idpath _ -- TODO: can we / should we use `1`? namespace path diff --git a/library/hott/trunc.lean b/library/hott/trunc.lean index b5ccad61aa..c0ee4f54dd 100644 --- a/library/hott/trunc.lean +++ b/library/hott/trunc.lean @@ -31,8 +31,8 @@ definition IsTrunc (n : trunc_index) : Type → Type := trunc_index.rec (λA, Contr A) (λn trunc_n A, (Π(x y : A), trunc_n (x ≈ y))) n -- TODO: in the Coq version, this is notation -abbreviation minus_one := trunc_S minus_two +abbreviation minus_one := trunc_index.trunc_S trunc_index.minus_two abbreviation IsHProp := IsTrunc minus_one -abbreviation IsHSet := IsTrunc (trunc_S minus_one) +abbreviation IsHSet := IsTrunc (trunc_index.trunc_S minus_one) prefix `!`:75 := center diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean index da1fa57bf3..16f9dcc1c6 100644 --- a/library/logic/axioms/classical.lean +++ b/library/logic/axioms/classical.lean @@ -27,8 +27,8 @@ or_elim (prop_complete a) theorem prop_complete_swapped (a : Prop) : a = false ∨ a = true := cases (λ x, x = false ∨ x = true) - (or_inr (refl true)) - (or_inl (refl false)) + (or_inr rfl) + (or_inl rfl) a theorem propext {a b : Prop} (Hab : a → b) (Hba : b → a) : a = b := @@ -50,7 +50,7 @@ propext open relation theorem iff_congruence [instance] (P : Prop → Prop) : congruence iff iff P := -congruence_mk +congruence.mk (take (a b : Prop), assume H : a ↔ b, - show P a ↔ P b, from eq_to_iff (subst (iff_to_eq H) (refl (P a)))) + show P a ↔ P b, from eq_to_iff (subst (iff_to_eq H) (eq.refl (P a)))) diff --git a/library/logic/axioms/examples/diaconescu.lean b/library/logic/axioms/examples/diaconescu.lean index 3b28bfcb1c..3b4b1b0bdf 100644 --- a/library/logic/axioms/examples/diaconescu.lean +++ b/library/logic/axioms/examples/diaconescu.lean @@ -18,10 +18,10 @@ definition u [private] := epsilon (λx, x = true ∨ p) definition v [private] := epsilon (λx, x = false ∨ p) lemma u_def [private] : u = true ∨ p := -epsilon_spec (exists_intro true (or_inl (refl true))) +epsilon_spec (exists_intro true (or_inl rfl)) lemma v_def [private] : v = false ∨ p := -epsilon_spec (exists_intro false (or_inl (refl false))) +epsilon_spec (exists_intro false (or_inl rfl)) lemma uv_implies_p [private] : ¬(u = v) ∨ p := or_elim u_def @@ -43,7 +43,7 @@ assume Hp : p, show (x = true ∨ p) = (x = false ∨ p), from propext Hl Hr), show u = v, from - Hpred ▸ (refl (epsilon (λ x, x = true ∨ p))) + Hpred ▸ (eq.refl (epsilon (λ x, x = true ∨ p))) theorem em : p ∨ ¬p := have H : ¬(u = v) → ¬p, from mt p_implies_uv, diff --git a/library/logic/axioms/funext.lean b/library/logic/axioms/funext.lean index 4cf47ae411..508e799b76 100644 --- a/library/logic/axioms/funext.lean +++ b/library/logic/axioms/funext.lean @@ -14,15 +14,15 @@ namespace function section parameters {A B C D: Type} theorem compose_assoc (f : C → D) (g : B → C) (h : A → B) : (f ∘ g) ∘ h = f ∘ (g ∘ h) := - funext (take x, refl _) + funext (take x, rfl) theorem compose_id_left (f : A → B) : id ∘ f = f := - funext (take x, refl _) + funext (take x, rfl) theorem compose_id_right (f : A → B) : f ∘ id = f := - funext (take x, refl _) + funext (take x, rfl) theorem compose_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b) := - funext (take x, refl _) + funext (take x, rfl) end end function diff --git a/library/logic/axioms/hilbert.lean b/library/logic/axioms/hilbert.lean index db62aa0866..e6d88b561b 100644 --- a/library/logic/axioms/hilbert.lean +++ b/library/logic/axioms/hilbert.lean @@ -25,14 +25,14 @@ 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 : A, (∃x : A, true) → true} := strong_indefinite_description (λa, true) H in -inhabited_mk (elt_of u) +inhabited.mk (elt_of u) theorem exists_imp_inhabited {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A := -nonempty_imp_inhabited (obtain w Hw, from H, nonempty_intro w) +nonempty_imp_inhabited (obtain w Hw, from H, nonempty.intro w) -- the Hilbert epsilon function @@ -53,8 +53,8 @@ theorem epsilon_spec {A : Type} {P : A → Prop} (Hex : ∃y, P y) : P (@epsilon A (exists_imp_nonempty Hex) P) := epsilon_spec_aux (exists_imp_nonempty Hex) P Hex -theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (nonempty_intro a) (λx, x = a) = a := -epsilon_spec (exists_intro a (refl a)) +theorem epsilon_singleton {A : Type} (a : A) : @epsilon A (nonempty.intro a) (λx, x = a) = a := +epsilon_spec (exists_intro a (eq.refl a)) -- the axiom of choice diff --git a/library/logic/axioms/piext.lean b/library/logic/axioms/piext.lean index db6e21128f..69f982f478 100644 --- a/library/logic/axioms/piext.lean +++ b/library/logic/axioms/piext.lean @@ -14,13 +14,13 @@ axiom piext {A : Type} {B B' : A → Type} {H : inhabited (Π x, B x)} : theorem cast_app {A : Type} {B B' : A → Type} (H : (Π x, B x) = (Π x, B' x)) (f : Π x, B x) (a : A) : cast H f a == f a := -have Hi [fact] : inhabited (Π x, B x), from inhabited_mk f, +have Hi [fact] : inhabited (Π x, B x), from inhabited.mk f, have Hb : B = B', from piext H, cast_app' Hb f a theorem hcongr_fun {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A) (H : f == f') : f a == f' a := -have Hi [fact] : inhabited (Π x, B x), from inhabited_mk f, +have Hi [fact] : inhabited (Π x, B x), from inhabited.mk f, have Hb : B = B', from piext (type_eq H), hcongr_fun' a H Hb diff --git a/library/logic/axioms/prop_decidable.lean b/library/logic/axioms/prop_decidable.lean index 43ff8f809e..d469c826b4 100644 --- a/library/logic/axioms/prop_decidable.lean +++ b/library/logic/axioms/prop_decidable.lean @@ -14,8 +14,8 @@ open decidable inhabited nonempty theorem decidable_inhabited [instance] (a : Prop) : inhabited (decidable a) := nonempty_imp_inhabited (or_elim (em a) - (assume Ha, nonempty_intro (inl Ha)) - (assume Hna, nonempty_intro (inr Hna))) + (assume Ha, nonempty.intro (inl Ha)) + (assume Hna, nonempty.intro (inr Hna))) -- Note that decidable_inhabited is marked as an instance, and it is silently used -- for synthesizing the implicit argument in the following 'epsilon' diff --git a/library/logic/classes/decidable.lean b/library/logic/classes/decidable.lean index 42494e5426..cfd98d9ad8 100644 --- a/library/logic/classes/decidable.lean +++ b/library/logic/classes/decidable.lean @@ -26,12 +26,12 @@ decidable.rec H1 H2 H theorem irrelevant {p : Prop} (d1 d2 : decidable p) : d1 = d2 := decidable.rec (assume Hp1 : p, decidable.rec - (assume Hp2 : p, congr_arg inl (refl Hp1)) -- using proof irrelevance for Prop + (assume Hp2 : p, congr_arg inl (eq.refl Hp1)) -- using proof irrelevance for Prop (assume Hnp2 : ¬p, absurd Hp1 Hnp2) d2) (assume Hnp1 : ¬p, decidable.rec (assume Hp2 : p, absurd Hp2 Hnp1) - (assume Hnp2 : ¬p, congr_arg inr (refl Hnp1)) -- using proof irrelevance for Prop + (assume Hnp2 : ¬p, congr_arg inr (eq.refl Hnp1)) -- using proof irrelevance for Prop d2) d1 @@ -50,7 +50,7 @@ theorem and_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable decidable (a ∧ b) := rec_on Ha (assume Ha : a, rec_on Hb - (assume Hb : b, inl (and_intro Ha Hb)) + (assume Hb : b, inl (and.intro Ha Hb)) (assume Hnb : ¬b, inr (and_not_right a Hnb))) (assume Hna : ¬a, inr (and_not_left b Hna)) diff --git a/library/logic/classes/inhabited.lean b/library/logic/classes/inhabited.lean index 3467a35d0f..9089caeb16 100644 --- a/library/logic/classes/inhabited.lean +++ b/library/logic/classes/inhabited.lean @@ -5,19 +5,19 @@ import logic.core.connectives inductive inhabited (A : Type) : Type := -inhabited_mk : A → inhabited A +mk : A → inhabited A namespace inhabited -definition inhabited_destruct {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B := +definition destruct [protected] {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B := inhabited.rec H2 H1 definition Prop_inhabited [instance] : inhabited Prop := -inhabited_mk true +mk true definition fun_inhabited [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B) := -inhabited_destruct H (take b, inhabited_mk (λa, b)) +destruct H (take b, mk (λa, b)) -definition default (A : Type) {H : inhabited A} : A := inhabited_destruct H (take a, a) +definition default (A : Type) {H : inhabited A} : A := destruct H (take a, a) end inhabited diff --git a/library/logic/classes/nonempty.lean b/library/logic/classes/nonempty.lean index e7b2c7ae60..9a08cf9adf 100644 --- a/library/logic/classes/nonempty.lean +++ b/library/logic/classes/nonempty.lean @@ -1,20 +1,16 @@ -- Copyright (c) 2014 Microsoft Corporation. All rights reserved. -- Released under Apache 2.0 license as described in the file LICENSE. -- Authors: Leonardo de Moura, Jeremy Avigad - import .inhabited - open inhabited -namespace nonempty - inductive nonempty (A : Type) : Prop := -nonempty_intro : A → nonempty A +intro : A → nonempty A -definition nonempty_elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B := -nonempty.rec H2 H1 - -theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A := -nonempty_intro (default A) +namespace nonempty + definition elim [protected] {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B := + rec H2 H1 + theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A := + intro (default A) end nonempty diff --git a/library/logic/core/cast.lean b/library/logic/core/cast.lean index 39abcadb6d..a773ad0f79 100644 --- a/library/logic/core/cast.lean +++ b/library/logic/core/cast.lean @@ -11,14 +11,14 @@ open eq_ops definition cast {A B : Type} (H : A = B) (a : A) : B := eq.rec a H -theorem cast_refl {A : Type} (a : A) : cast (refl A) a = a := -refl (cast (refl A) a) +theorem cast_refl {A : Type} (a : A) : cast (eq.refl A) a = a := +eq.refl (cast (eq.refl A) a) theorem cast_proof_irrel {A B : Type} (H1 H2 : A = B) (a : A) : cast H1 a = cast H2 a := -refl (cast H1 a) +eq.refl (cast H1 a) theorem cast_eq {A : Type} (H : A = A) (a : A) : cast H a = a := -calc cast H a = cast (refl A) a : cast_proof_irrel H (refl A) a +calc cast H a = cast (eq.refl A) a : cast_proof_irrel H (eq.refl A) a ... = a : cast_refl a definition heq {A B : Type} (a : A) (b : B) := @@ -34,7 +34,7 @@ theorem heq_type_eq {A B : Type} {a : A} {b : B} (H : a == b) : A = B := obtain w Hw, from H, w theorem eq_to_heq {A : Type} {a b : A} (H : a = b) : a == b := -exists_intro (refl A) (cast_refl a ⬝ H) +exists_intro (eq.refl A) (cast_refl a ⬝ H) theorem heq_to_eq {A : Type} {a b : A} (H : a == b) : a = b := obtain (w : A = A) (Hw : cast w a = b), from H, @@ -42,7 +42,7 @@ calc a = cast w a : (cast_eq w a)⁻¹ ... = b : Hw theorem hrefl {A : Type} (a : A) : a == a := -eq_to_heq (refl a) +eq_to_heq (eq.refl a) theorem heqt_elim {a : Prop} (H : a == true) : a := eq_true_elim (heq_to_eq H) @@ -74,7 +74,7 @@ calc_trans htrans_left calc_trans htrans_right theorem type_eq {A B : Type} {a : A} {b : B} (H : a == b) : A = B := -hsubst H (refl A) +hsubst H (eq.refl A) theorem cast_heq {A B : Type} (H : A = B) (a : A) : cast H a == a := have H1 : ∀ (H : A = A) (a : A), cast H a == a, from @@ -101,7 +101,7 @@ have e3 : cast (congr_arg B H) (f a) = f b, from cast_eq_to_heq e3 theorem pi_eq {A : Type} {B B' : A → Type} (H : B = B') : (Π x, B x) = (Π x, B' x) := -subst H (refl (Π x, B x)) +subst H (eq.refl (Π x, B x)) theorem cast_app' {A : Type} {B B' : A → Type} (H : B = B') (f : Π x, B x) (a : A) : cast (pi_eq H) f a == f a := @@ -121,5 +121,5 @@ theorem hcongr_fun' {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B : f a == f' a := heq_elim H1 (λ (Ht : (Π x, B x) = (Π x, B' x)) (Hw : cast Ht f = f'), calc f a == cast (pi_eq H2) f a : hsymm (cast_app' H2 f a) - ... = cast Ht f a : refl (cast Ht f a) + ... = cast Ht f a : eq.refl (cast Ht f a) ... = f' a : congr_fun Hw a) diff --git a/library/logic/core/connectives.lean b/library/logic/core/connectives.lean index aa79f4d1c3..2ecf629fc0 100644 --- a/library/logic/core/connectives.lean +++ b/library/logic/core/connectives.lean @@ -8,7 +8,7 @@ import general_notation .eq -- --- inductive and (a b : Prop) : Prop := -and_intro : a → b → and a b +intro : a → b → and a b infixr `/\` := and infixr `∧` := and @@ -23,7 +23,7 @@ theorem and_elim_right {a b : Prop} (H : a ∧ b) : b := and.rec (λa b, b) H theorem and_swap {a b : Prop} (H : a ∧ b) : b ∧ a := -and_intro (and_elim_right H) (and_elim_left H) +and.intro (and_elim_right H) (and_elim_left H) theorem and_not_left {a : Prop} (b : Prop) (Hna : ¬a) : ¬(a ∧ b) := assume H : a ∧ b, absurd (and_elim_left H) Hna @@ -32,27 +32,27 @@ theorem and_not_right (a : Prop) {b : Prop} (Hnb : ¬b) : ¬(a ∧ b) := assume H : a ∧ b, absurd (and_elim_right H) Hnb theorem and_imp_and {a b c d : Prop} (H1 : a ∧ b) (H2 : a → c) (H3 : b → d) : c ∧ d := -and_elim H1 (assume Ha : a, assume Hb : b, and_intro (H2 Ha) (H3 Hb)) +and_elim H1 (assume Ha : a, assume Hb : b, and.intro (H2 Ha) (H3 Hb)) theorem imp_and_left {a b c : Prop} (H1 : a ∧ c) (H : a → b) : b ∧ c := -and_elim H1 (assume Ha : a, assume Hc : c, and_intro (H Ha) Hc) +and_elim H1 (assume Ha : a, assume Hc : c, and.intro (H Ha) Hc) theorem imp_and_right {a b c : Prop} (H1 : c ∧ a) (H : a → b) : c ∧ b := -and_elim H1 (assume Hc : c, assume Ha : a, and_intro Hc (H Ha)) +and_elim H1 (assume Hc : c, assume Ha : a, and.intro Hc (H Ha)) -- or -- -- inductive or (a b : Prop) : Prop := -or_intro_left : a → or a b, -or_intro_right : b → or a b +intro_left : a → or a b, +intro_right : b → or a b infixr `\/` := or infixr `∨` := or -theorem or_inl {a b : Prop} (Ha : a) : a ∨ b := or_intro_left b Ha -theorem or_inr {a b : Prop} (Hb : b) : a ∨ b := or_intro_right a Hb +theorem or_inl {a b : Prop} (Ha : a) : a ∨ b := or.intro_left b Ha +theorem or_inr {a b : Prop} (Hb : b) : a ∨ b := or.intro_right a Hb theorem or_elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c := or.rec H2 H3 H1 @@ -101,7 +101,7 @@ infix `↔` := iff theorem iff_def {a b : Prop} : (a ↔ b) = ((a → b) ∧ (b → a)) := rfl -theorem iff_intro {a b : Prop} (H1 : a → b) (H2 : b → a) : a ↔ b := and_intro H1 H2 +theorem iff_intro {a b : Prop} (H1 : a → b) (H2 : b → a) : a ↔ b := and.intro H1 H2 theorem iff_elim {a b c : Prop} (H1 : (a → b) → (b → a) → c) (H2 : a ↔ b) : c := and.rec H1 H2 @@ -155,11 +155,11 @@ iff_intro (λH, and_swap H) (λH, and_swap H) theorem and_assoc {a b c : Prop} : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) := iff_intro - (assume H, and_intro + (assume H, and.intro (and_elim_left (and_elim_left H)) - (and_intro (and_elim_right (and_elim_left H)) (and_elim_right H))) - (assume H, and_intro - (and_intro (and_elim_left H) (and_elim_left (and_elim_right H))) + (and.intro (and_elim_right (and_elim_left H)) (and_elim_right H))) + (assume H, and.intro + (and.intro (and_elim_left H) (and_elim_left (and_elim_right H))) (and_elim_right (and_elim_right H))) theorem or_comm {a b : Prop} : a ∨ b ↔ b ∨ a := diff --git a/library/logic/core/eq.lean b/library/logic/core/eq.lean index 2bfccdc8b1..20690eb221 100644 --- a/library/logic/core/eq.lean +++ b/library/logic/core/eq.lean @@ -16,9 +16,9 @@ inductive eq {A : Type} (a : A) : A → Prop := refl : eq a a infix `=` := eq -notation `rfl` := refl _ +notation `rfl` := eq.refl _ -theorem eq_id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (refl a) := rfl +theorem eq_id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (eq.refl a) := rfl theorem eq_irrel {A : Type} {a b : A} (H1 H2 : a = b) : H1 = H2 := rfl @@ -29,11 +29,11 @@ theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c := subst H2 H1 calc_subst subst -calc_refl refl +calc_refl eq.refl calc_trans trans theorem symm {A : Type} {a b : A} (H : a = b) : b = a := -subst H (refl a) +subst H (eq.refl a) namespace eq_ops postfix `⁻¹` := symm @@ -46,32 +46,34 @@ theorem true_ne_false : ¬true = false := assume H : true = false, subst H trivial +namespace eq -- eq_rec with arguments swapped, for transporting an element of a dependent type -definition eq_rec_on {A : Type} {a1 a2 : A} {B : A → Type} (H1 : a1 = a2) (H2 : B a1) : B a2 := +definition rec_on {A : Type} {a1 a2 : A} {B : A → Type} (H1 : a1 = a2) (H2 : B a1) : B a2 := eq.rec H2 H1 -theorem eq_rec_on_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : eq_rec_on H b = b := -refl (eq_rec_on rfl b) +theorem rec_on_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec_on H b = b := +refl (rec_on rfl b) -theorem eq_rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : eq.rec b H = b := -eq_rec_on_id H b +theorem rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec b H = b := +rec_on_id H b -theorem eq_rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c) +theorem rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c) (u : P a) : - eq_rec_on H2 (eq_rec_on H1 u) = eq_rec_on (trans H1 H2) u := -(show ∀(H2 : b = c), eq_rec_on H2 (eq_rec_on H1 u) = eq_rec_on (trans H1 H2) u, - from eq_rec_on H2 (take (H2 : b = b), eq_rec_on_id H2 _)) + rec_on H2 (rec_on H1 u) = rec_on (trans H1 H2) u := +(show ∀(H2 : b = c), rec_on H2 (rec_on H1 u) = rec_on (trans H1 H2) u, + from rec_on H2 (take (H2 : b = b), rec_on_id H2 _)) H2 +end eq theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a := -H ▸ refl (f a) +H ▸ eq.refl (f a) theorem congr_arg {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b := -H ▸ refl (f a) +H ▸ eq.refl (f a) theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b := -H1 ▸ H2 ▸ refl (f a) +H1 ▸ H2 ▸ eq.refl (f a) theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x := take x, congr_fun H x @@ -111,9 +113,9 @@ theorem ne_intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b := H theorem ne_elim {A : Type} {a b : A} (H1 : a ≠ b) (H2 : a = b) : false := H1 H2 -theorem a_neq_a_elim {A : Type} {a : A} (H : a ≠ a) : false := H (refl a) +theorem a_neq_a_elim {A : Type} {a : A} (H : a ≠ a) : false := H rfl -theorem ne_irrefl {A : Type} {a : A} (H : a ≠ a) : false := H (refl a) +theorem ne_irrefl {A : Type} {a : A} (H : a ≠ a) : false := H rfl theorem ne_symm {A : Type} {a b : A} (H : a ≠ b) : b ≠ a := assume H1 : b = a, H (H1⁻¹) diff --git a/library/logic/core/identities.lean b/library/logic/core/identities.lean index 79050a4a6f..4ccbd861a2 100644 --- a/library/logic/core/identities.lean +++ b/library/logic/core/identities.lean @@ -58,7 +58,7 @@ iff_intro (assume Ha, absurd (or_inl Ha) H) (assume Hna, or_elim (em b) (assume Hb, absurd (or_inr Hb) H) - (assume Hnb, and_intro Hna Hnb))) + (assume Hnb, and.intro Hna Hnb))) (assume (H : ¬a ∧ ¬b) (N : a ∨ b), or_elim N (assume Ha, absurd Ha (and_elim_left H)) @@ -68,7 +68,7 @@ theorem not_and {a b : Prop} {Da : decidable a} {Db : decidable b} : (¬(a ∧ b iff_intro (assume H, or_elim (em a) (assume Ha, or_elim (em b) - (assume Hb, absurd (and_intro Ha Hb) H) + (assume Hb, absurd (and.intro Ha Hb) H) (assume Hnb, or_inr Hnb)) (assume Hna, or_inl Hna)) (assume (H : ¬a ∨ ¬b) (N : a ∧ b), @@ -125,7 +125,7 @@ iff_intro (assume H, false_elim H) theorem eq_id {A : Type} (a : A) : (a = a) ↔ true := -iff_true_intro (refl a) +iff_true_intro rfl theorem heq_id {A : Type} (a : A) : (a == a) ↔ true := iff_true_intro (hrefl a) diff --git a/library/logic/core/if.lean b/library/logic/core/if.lean index d9a68166fd..cfb188dd95 100644 --- a/library/logic/core/if.lean +++ b/library/logic/core/if.lean @@ -14,20 +14,20 @@ notation `if` c `then` t `else` e:45 := ite c t e theorem if_pos {c : Prop} {H : decidable c} (Hc : c) {A : Type} {t e : A} : (if c then t else e) = t := decidable.rec - (assume Hc : c, refl (@ite c (inl Hc) A t e)) + (assume Hc : c, eq.refl (@ite c (inl Hc) A t e)) (assume Hnc : ¬c, absurd Hc Hnc) H theorem if_neg {c : Prop} {H : decidable c} (Hnc : ¬c) {A : Type} {t e : A} : (if c then t else e) = e := decidable.rec (assume Hc : c, absurd Hc Hnc) - (assume Hnc : ¬c, refl (@ite c (inr Hnc) A t e)) + (assume Hnc : ¬c, eq.refl (@ite c (inr Hnc) A t e)) H theorem if_t_t (c : Prop) {H : decidable c} {A : Type} (t : A) : (if c then t else t) = t := decidable.rec - (assume Hc : c, refl (@ite c (inl Hc) A t t)) - (assume Hnc : ¬c, refl (@ite c (inr Hnc) A t t)) + (assume Hc : c, eq.refl (@ite c (inl Hc) A t t)) + (assume Hnc : ¬c, eq.refl (@ite c (inr Hnc) A t t)) H theorem if_true {A : Type} (t e : A) : (if true then t else e) = t := diff --git a/library/logic/core/instances.lean b/library/logic/core/instances.lean index 5ad8671ffb..c454359c5e 100644 --- a/library/logic/core/instances.lean +++ b/library/logic/core/instances.lean @@ -15,14 +15,14 @@ open relation -- --------------------- theorem congruence_not : congruence iff iff not := -congruence_mk +congruence.mk (take a b, assume H : a ↔ b, iff_intro (assume H1 : ¬a, assume H2 : b, H1 (iff_elim_right H H2)) (assume H1 : ¬b, assume H2 : a, H1 (iff_elim_left H H2))) theorem congruence_and : congruence2 iff iff iff and := -congruence2_mk +congruence2.mk (take a1 b1 a2 b2, assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2, iff_intro @@ -30,7 +30,7 @@ congruence2_mk (assume H3 : b1 ∧ b2, and_imp_and H3 (iff_elim_right H1) (iff_elim_right H2))) theorem congruence_or : congruence2 iff iff iff or := -congruence2_mk +congruence2.mk (take a1 b1 a2 b2, assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2, iff_intro @@ -38,7 +38,7 @@ congruence2_mk (assume H3 : b1 ∨ b2, or_imp_or H3 (iff_elim_right H1) (iff_elim_right H2))) theorem congruence_imp : congruence2 iff iff iff imp := -congruence2_mk +congruence2.mk (take a1 b1 a2 b2, assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2, iff_intro @@ -46,7 +46,7 @@ congruence2_mk (assume H3 : b1 → b2, assume Ha1 : a1, iff_elim_right H2 (H3 ((iff_elim_left H1) Ha1)))) theorem congruence_iff : congruence2 iff iff iff iff := -congruence2_mk +congruence2.mk (take a1 b1 a2 b2, assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2, iff_intro @@ -77,37 +77,37 @@ end general_operations -- ---------------------------- theorem is_reflexive_eq [instance] (T : Type) : relation.is_reflexive (@eq T) := -relation.is_reflexive_mk (@refl T) +relation.is_reflexive.mk (@eq.refl T) theorem is_symmetric_eq [instance] (T : Type) : relation.is_symmetric (@eq T) := -relation.is_symmetric_mk (@symm T) +relation.is_symmetric.mk (@symm T) theorem is_transitive_eq [instance] (T : Type) : relation.is_transitive (@eq T) := -relation.is_transitive_mk (@trans T) +relation.is_transitive.mk (@trans T) -- TODO: this is only temporary, needed to inform Lean that is_equivalence is a class theorem is_equivalence_eq [instance] (T : Type) : relation.is_equivalence (@eq T) := -relation.is_equivalence_mk _ _ _ +relation.is_equivalence.mk _ _ _ -- iff is an equivalence relation -- ------------------------------ theorem is_reflexive_iff [instance] : relation.is_reflexive iff := -relation.is_reflexive_mk (@iff_refl) +relation.is_reflexive.mk (@iff_refl) theorem is_symmetric_iff [instance] : relation.is_symmetric iff := -relation.is_symmetric_mk (@iff_symm) +relation.is_symmetric.mk (@iff_symm) theorem is_transitive_iff [instance] : relation.is_transitive iff := -relation.is_transitive_mk (@iff_trans) +relation.is_transitive.mk (@iff_trans) -- Mp-like for iff -- --------------- theorem mp_like_iff [instance] (a b : Prop) (H : a ↔ b) : @relation.mp_like iff a b H := -relation.mp_like_mk (iff_elim_left H) +relation.mp_like.mk (iff_elim_left H) -- Substition for iff diff --git a/library/logic/core/prop.lean b/library/logic/core/prop.lean index c2f45043a2..a43b63d944 100644 --- a/library/logic/core/prop.lean +++ b/library/logic/core/prop.lean @@ -22,7 +22,9 @@ theorem false_elim {c : Prop} (H : false) : c := false.rec c H inductive true : Prop := -trivial : true +intro : true + +abbreviation trivial := true.intro abbreviation not (a : Prop) := a → false prefix `¬` := not diff --git a/library/logic/core/quantifiers.lean b/library/logic/core/quantifiers.lean index 1fe15f406a..9baee9fce0 100644 --- a/library/logic/core/quantifiers.lean +++ b/library/logic/core/quantifiers.lean @@ -7,7 +7,9 @@ import .connectives ..classes.nonempty open inhabited nonempty inductive Exists {A : Type} (P : A → Prop) : Prop := -exists_intro : ∀ (a : A), P a → Exists P +intro : ∀ (a : A), P a → Exists P + +abbreviation exists_intro := @Exists.intro notation `exists` binders `,` r:(scoped P, Exists P) := r notation `∃` binders `,` r:(scoped P, Exists P) := r @@ -31,7 +33,7 @@ definition exists_unique {A : Type} (p : A → Prop) := 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, y ≠ w → ¬p y) : ∃!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, y ≠ x → ¬p y) → b) : b := @@ -54,17 +56,17 @@ theorem forall_true_iff_true (A : Type) : (∀x : A, true) ↔ true := iff_intro (assume H, trivial) (assume H, take x, trivial) theorem forall_p_iff_p (A : Type) {H : inhabited A} (p : Prop) : (∀x : A, p) ↔ p := -iff_intro (assume Hl, inhabited_destruct H (take x, Hl x)) (assume Hr, take x, Hr) +iff_intro (assume Hl, inhabited.destruct H (take x, Hl x)) (assume Hr, take x, Hr) 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) := iff_intro - (assume H, and_intro (take x, and_elim_left (H x)) (take x, and_elim_right (H x))) - (assume H, take x, and_intro (and_elim_left H x) (and_elim_right H x)) + (assume H, and.intro (take x, and_elim_left (H x)) (take x, and_elim_right (H x))) + (assume H, take x, and.intro (and_elim_left H x) (and_elim_right H x)) theorem exists_or_distribute {A : Type} (φ ψ : A → Prop) : (∃x, φ x ∨ ψ x) ↔ (∃x, φ x) ∨ (∃x, ψ x) := iff_intro @@ -79,4 +81,4 @@ iff_intro exists_intro w (or_inr Hw))) theorem exists_imp_nonempty {A : Type} {P : A → Prop} (H : ∃x, P x) : nonempty A := -obtain w Hw, from H, nonempty_intro w +obtain w Hw, from H, nonempty.intro w diff --git a/library/logic/examples/nuprl_examples.lean b/library/logic/examples/nuprl_examples.lean index 0c2929f09c..3c06b226d0 100644 --- a/library/logic/examples/nuprl_examples.lean +++ b/library/logic/examples/nuprl_examples.lean @@ -65,7 +65,7 @@ theorem thm12 {P Q : Prop} : ¬(P ∨ Q) → ¬P ∧ ¬Q := assume H : ¬(P ∨ Q), have Hnp : ¬P, from assume Hp : P, absurd (or_inl Hp) H, have Hnq : ¬Q, from assume Hq : Q, absurd (or_inr Hq) H, - and_intro Hnp Hnq + and.intro Hnp Hnq theorem thm13 {P Q : Prop} : ¬P ∧ ¬Q → ¬(P ∨ Q) := assume (H : ¬P ∧ ¬Q) (Hn : P ∨ Q), @@ -193,23 +193,23 @@ 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), - and_intro Hex (and_elim_right Hw) + and.intro Hex (and_elim_right Hw) theorem thm24a : (∀x, P x) ∧ C → (∀x, P x ∧ C) := assume H, take x, - and_intro (and_elim_left H x) (and_elim_right H) + and.intro (and_elim_left H x) (and_elim_right H) theorem thm24b : (∃x : T, true) → (∀x, P x ∧ C) → (∀x, P x) ∧ C := assume Hin H, obtain (w : T) (Hw : true), from Hin, have Hc : C, from and_elim_right (H w), have Hx : ∀x, P x, from take x, and_elim_left (H x), - and_intro Hx Hc + and.intro Hx Hc end -- of section diff --git a/library/struc/relation.lean b/library/struc/relation.lean index c32ecdb539..405579076d 100644 --- a/library/struc/relation.lean +++ b/library/struc/relation.lean @@ -19,7 +19,7 @@ abbreviation transitive {T : Type} (R : T → T → Type) : Type := ∀⦃x y z inductive is_reflexive {T : Type} (R : T → T → Type) : Prop := -is_reflexive_mk : reflexive R → is_reflexive R +mk : reflexive R → is_reflexive R namespace is_reflexive @@ -33,7 +33,7 @@ end is_reflexive inductive is_symmetric {T : Type} (R : T → T → Type) : Prop := -is_symmetric_mk : symmetric R → is_symmetric R +mk : symmetric R → is_symmetric R namespace is_symmetric @@ -47,7 +47,7 @@ end is_symmetric inductive is_transitive {T : Type} (R : T → T → Type) : Prop := -is_transitive_mk : transitive R → is_transitive R +mk : transitive R → is_transitive R namespace is_transitive @@ -61,7 +61,7 @@ end is_transitive inductive is_equivalence {T : Type} (R : T → T → Type) : Prop := -is_equivalence_mk : is_reflexive R → is_symmetric R → is_transitive R → is_equivalence R +mk : is_reflexive R → is_symmetric R → is_transitive R → is_equivalence R namespace is_equivalence @@ -83,7 +83,7 @@ instance is_equivalence.is_transitive -- partial equivalence relation inductive is_PER {T : Type} (R : T → T → Type) : Prop := -is_PER_mk : is_symmetric R → is_transitive R → is_PER R +mk : is_symmetric R → is_transitive R → is_PER R namespace is_PER @@ -104,23 +104,23 @@ instance is_PER.is_transitive inductive congruence {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop) (f : T1 → T2) : Prop := -congruence_mk : (∀x y, R1 x y → R2 (f x) (f y)) → congruence R1 R2 f +mk : (∀x y, R1 x y → R2 (f x) (f y)) → congruence R1 R2 f -- for binary functions inductive congruence2 {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop) {T3 : Type} (R3 : T3 → T3 → Prop) (f : T1 → T2 → T3) : Prop := -congruence2_mk : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) → +mk : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) → congruence2 R1 R2 R3 f namespace congruence abbreviation app {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop} {f : T1 → T2} (C : congruence R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) := - congruence.rec (λu, u) C x y + rec (λu, u) C x y theorem infer {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop) (f : T1 → T2) {C : congruence R1 R2 f} ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) := - congruence.rec (λu, u) C x y + rec (λu, u) C x y abbreviation app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop} {T3 : Type} {R3 : T3 → T3 → Prop} @@ -137,7 +137,7 @@ namespace congruence ⦃T1 : Type⦄ {R1 : T1 → T1 → Prop} {f : T1 → T2} (C1 : congruence R1 R2 f) : congruence R1 R3 (λx, g (f x)) := - congruence_mk (λx1 x2 H, app C2 (app C1 H)) + mk (λx1 x2 H, app C2 (app C1 H)) theorem compose21 {T2 : Type} {R2 : T2 → T2 → Prop} @@ -148,12 +148,12 @@ namespace congruence {f1 : T1 → T2} (C1 : congruence R1 R2 f1) {f2 : T1 → T3} (C2 : congruence R1 R3 f2) : congruence R1 R4 (λx, g (f1 x) (f2 x)) := - congruence_mk (λx1 x2 H, app2 C3 (app C1 H) (app C2 H)) + mk (λx1 x2 H, app2 C3 (app C1 H) (app C2 H)) theorem const {T2 : Type} (R2 : T2 → T2 → Prop) (H : relation.reflexive R2) ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) : congruence R1 R2 (λu : T1, c) := - congruence_mk (λx y H1, H c) + mk (λx y H1, H c) end congruence @@ -167,22 +167,22 @@ congruence.const R2 (is_reflexive.app C) R1 c theorem congruence_trivial [instance] {T : Type} (R : T → T → Prop) : congruence R R (λu, u) := -congruence_mk (λx y H, H) +congruence.mk (λx y H, H) -- Relations that can be coerced to functions / implications -- --------------------------------------------------------- inductive mp_like {R : Type → Type → Prop} {a b : Type} (H : R a b) : Prop := -mp_like_mk {} : (a → b) → @mp_like R a b H +mk {} : (a → b) → @mp_like R a b H namespace mp_like definition app {R : Type → Type → Prop} {a : Type} {b : Type} {H : R a b} - (C : mp_like H) : a → b := mp_like.rec (λx, x) C + (C : mp_like H) : a → b := rec (λx, x) C definition infer ⦃R : Type → Type → Prop⦄ {a : Type} {b : Type} (H : R a b) - {C : mp_like H} : a → b := mp_like.rec (λx, x) C + {C : mp_like H} : a → b := rec (λx, x) C end mp_like diff --git a/library/tools/helper_tactics.lean b/library/tools/helper_tactics.lean index 5bad613302..bda430b3b5 100644 --- a/library/tools/helper_tactics.lean +++ b/library/tools/helper_tactics.lean @@ -12,6 +12,6 @@ import .tactic open tactic namespace helper_tactics - definition apply_refl := apply @refl + definition apply_refl := apply @eq.refl tactic_hint apply_refl end helper_tactics diff --git a/library/tools/tactic.lean b/library/tools/tactic.lean index 08513d43fb..80c4e0b178 100644 --- a/library/tools/tactic.lean +++ b/library/tools/tactic.lean @@ -5,43 +5,41 @@ ---------------------------------------------------------------------------------------------------- import data.string data.num -open string -open num - -namespace tactic -- This is just a trick to embed the 'tactic language' as a -- Lean expression. We should view 'tactic' as automation -- that when execute produces a term. --- builtin_tactic is just a "dummy" for creating the +-- tactic.builtin is just a "dummy" for creating the -- definitions that are actually implemented in C++ inductive tactic : Type := -builtin_tactic : tactic +builtin : tactic + +namespace tactic -- Remark the following names are not arbitrary, the tactic module -- uses them when converting Lean expressions into actual tactic objects. -- The bultin 'by' construct triggers the process of converting a -- a term of type 'tactic' into a tactic that sythesizes a term -definition and_then (t1 t2 : tactic) : tactic := builtin_tactic -definition or_else (t1 t2 : tactic) : tactic := builtin_tactic -definition append (t1 t2 : tactic) : tactic := builtin_tactic -definition interleave (t1 t2 : tactic) : tactic := builtin_tactic -definition par (t1 t2 : tactic) : tactic := builtin_tactic -definition fixpoint (f : tactic → tactic) : tactic := builtin_tactic -definition repeat (t : tactic) : tactic := builtin_tactic -definition at_most (t : tactic) (k : num) : tactic := builtin_tactic -definition discard (t : tactic) (k : num) : tactic := builtin_tactic -definition focus_at (t : tactic) (i : num) : tactic := builtin_tactic -definition try_for (t : tactic) (ms : num) : tactic := builtin_tactic -definition now : tactic := builtin_tactic -definition assumption : tactic := builtin_tactic -definition eassumption : tactic := builtin_tactic -definition state : tactic := builtin_tactic -definition fail : tactic := builtin_tactic -definition id : tactic := builtin_tactic -definition beta : tactic := builtin_tactic -definition apply {B : Type} (b : B) : tactic := builtin_tactic -definition unfold {B : Type} (b : B) : tactic := builtin_tactic -definition exact {B : Type} (b : B) : tactic := builtin_tactic -definition trace (s : string) : tactic := builtin_tactic +definition and_then (t1 t2 : tactic) : tactic := builtin +definition or_else (t1 t2 : tactic) : tactic := builtin +definition append (t1 t2 : tactic) : tactic := builtin +definition interleave (t1 t2 : tactic) : tactic := builtin +definition par (t1 t2 : tactic) : tactic := builtin +definition fixpoint (f : tactic → tactic) : tactic := builtin +definition repeat (t : tactic) : tactic := builtin +definition at_most (t : tactic) (k : num) : tactic := builtin +definition discard (t : tactic) (k : num) : tactic := builtin +definition focus_at (t : tactic) (i : num) : tactic := builtin +definition try_for (t : tactic) (ms : num) : tactic := builtin +definition now : tactic := builtin +definition assumption : tactic := builtin +definition eassumption : tactic := builtin +definition state : tactic := builtin +definition fail : tactic := builtin +definition id : tactic := builtin +definition beta : tactic := builtin +definition apply {B : Type} (b : B) : tactic := builtin +definition unfold {B : Type} (b : B) : tactic := builtin +definition exact {B : Type} (b : B) : tactic := builtin +definition trace (s : string) : tactic := builtin precedence `;`:200 infixl ; := and_then notation `!` t:max := repeat t diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 4b6675a65b..3e080400a1 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -99,22 +99,25 @@ struct inductive_cmd_fn { /** \brief Parse the name of an inductive datatype or introduction rule, prefix the current namespace to it and return it. */ - name parse_decl_name(bool is_intro) { + name parse_decl_name(optional const & ind_name) { m_pos = m_p.pos(); name id = m_p.check_id_next("invalid declaration, identifier expected"); check_atomic(id); - name full_id = m_namespace + id; - if (is_intro) { + if (ind_name) { + // for intro rules, we append the name of the inductive datatype + name full_id = *ind_name + id; m_decl_info.emplace_back(full_id, g_intro, m_pos); + return full_id; } else { + name full_id = m_namespace + id; m_decl_info.emplace_back(full_id, g_inductive, m_pos); m_decl_info.emplace_back(mk_rec_name(full_id), g_recursor, m_pos); + return full_id; } - return full_id; } - name parse_inductive_decl_name() { return parse_decl_name(false); } - name parse_intro_decl_name() { return parse_decl_name(true); } + name parse_inductive_decl_name() { return parse_decl_name(optional()); } + name parse_intro_decl_name(name const & ind_name) { return parse_decl_name(optional(ind_name)); } /** \brief Parse inductive declaration universe parameters. If this is the first declaration in a mutually recursive block, then this method @@ -266,10 +269,10 @@ struct inductive_cmd_fn { /** \brief Parse introduction rules in the scope of the given parameters. Introduction rules with the annotation '{}' are marked for relaxed (aka non-strict) implicit parameter inference. */ - list parse_intro_rules(buffer & params) { + list parse_intro_rules(name const & ind_name, buffer & params) { buffer intros; while (true) { - name intro_name = parse_intro_decl_name(); + name intro_name = parse_intro_decl_name(ind_name); bool strict = true; if (m_p.curr_is_token(g_lcurly)) { m_p.next(); @@ -315,7 +318,7 @@ struct inductive_cmd_fn { } else { buffer params; add_params_to_local_scope(d_type, params); - auto d_intro_rules = parse_intro_rules(params); + auto d_intro_rules = parse_intro_rules(d_name, params); decls.push_back(inductive_decl(d_name, d_type, d_intro_rules)); } if (!m_p.curr_is_token(g_with)) { @@ -509,8 +512,12 @@ struct inductive_cmd_fn { } /** \brief Create an alias for the fully qualified name \c full_id. */ - environment create_alias(environment env, name const & full_id, levels const & section_leves, buffer const & section_params) { - name id(full_id.get_string()); + environment create_alias(environment env, bool composite, name const & full_id, levels const & section_leves, buffer const & section_params) { + name id; + if (composite) + id = name(name(full_id.get_prefix().get_string()), full_id.get_string()); + else + id = name(full_id.get_string()); if (in_section_or_context(env)) { expr r = mk_explicit(mk_constant(full_id, section_leves)); r = mk_app(r, section_params); @@ -529,13 +536,13 @@ struct inductive_cmd_fn { for (auto & d : decls) { name d_name = inductive_decl_name(d); name d_short_name(d_name.get_string()); - env = create_alias(env, d_name, section_levels, section_params); + env = create_alias(env, false, d_name, section_levels, section_params); name rec_name = mk_rec_name(d_name); - env = create_alias(env, rec_name, section_levels, section_params); + env = create_alias(env, true, rec_name, section_levels, section_params); env = add_protected(env, rec_name); for (intro_rule const & ir : inductive_decl_intros(d)) { name ir_name = intro_rule_name(ir); - env = create_alias(env, ir_name, section_levels, section_params); + env = create_alias(env, true, ir_name, section_levels, section_params); } } return env; diff --git a/src/frontends/lean/tactic_hint.cpp b/src/frontends/lean/tactic_hint.cpp index 63ae1a51d1..d37ee60e7f 100644 --- a/src/frontends/lean/tactic_hint.cpp +++ b/src/frontends/lean/tactic_hint.cpp @@ -92,7 +92,7 @@ expr parse_tactic_name(parser & p) { auto pos = p.pos(); name pre_tac = p.check_constant_next("invalid tactic name, constant expected"); expr pre_tac_type = p.env().get(pre_tac).get_type(); - if (!is_constant(pre_tac_type) || const_name(pre_tac_type) != name({"tactic", "tactic"})) + if (!is_constant(pre_tac_type) || const_name(pre_tac_type) != name("tactic")) throw parser_error(sstream() << "invalid tactic name, '" << pre_tac << "' is not a tactic", pos); return mk_constant(pre_tac); } diff --git a/src/library/num.cpp b/src/library/num.cpp index 665944b46a..3cd64397ab 100644 --- a/src/library/num.cpp +++ b/src/library/num.cpp @@ -8,13 +8,13 @@ Author: Leonardo de Moura #include "library/num.h" namespace lean { -static expr g_num(Const({"num", "num"})); -static expr g_pos_num(Const({"num", "pos_num"})); +static expr g_num(Const("num")); +static expr g_pos_num(Const("pos_num")); static expr g_zero(Const({"num", "zero"})); static expr g_pos(Const({"num", "pos"})); -static expr g_one(Const({"num", "one"})); -static expr g_bit0(Const({"num", "bit0"})); -static expr g_bit1(Const({"num", "bit1"})); +static expr g_one(Const({"pos_num", "one"})); +static expr g_bit0(Const({"pos_num", "bit0"})); +static expr g_bit1(Const({"pos_num", "bit1"})); bool has_num_decls(environment const & env) { try { diff --git a/src/library/string.cpp b/src/library/string.cpp index dd62a5eaf9..2143d5d9cd 100644 --- a/src/library/string.cpp +++ b/src/library/string.cpp @@ -15,11 +15,11 @@ static name g_string_macro("string_macro"); static std::string g_string_opcode("Str"); static expr g_bool(Const(name("bool"))); -static expr g_ff(Const(name("ff"))); -static expr g_tt(Const(name("tt"))); -static expr g_char(Const(name("string", "char"))); -static expr g_ascii(Const(name("string", "ascii"))); -static expr g_string(Const(name("string", "string"))); +static expr g_ff(Const(name("bool", "ff"))); +static expr g_tt(Const(name("bool", "tt"))); +static expr g_char(Const(name("char"))); +static expr g_ascii(Const(name("char", "mk"))); +static expr g_string(Const(name("string"))); static expr g_empty(Const(name("string", "empty"))); static expr g_str(Const(name("string", "str"))); diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 2725e412a1..068e2f048a 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -26,14 +26,14 @@ void register_expr_to_tactic(name const & n, expr_to_tactic_fn const & fn) { get_expr_to_tactic_map().insert(mk_pair(n, fn)); } -static name g_tac("tactic"), g_tac_name(g_tac, "tactic"), g_builtin_tac_name(g_tac, "builtin_tactic"); +static name g_tac("tactic"), g_builtin_tac_name(g_tac, "builtin"); static name g_exact_tac_name(g_tac, "exact"), g_and_then_tac_name(g_tac, "and_then"); static name g_or_else_tac_name(g_tac, "or_else"), g_repeat_tac_name(g_tac, "repeat"), g_fixpoint_name(g_tac, "fixpoint"); static name g_determ_tac_name(g_tac, "determ"); static expr g_exact_tac_fn(Const(g_exact_tac_name)), g_and_then_tac_fn(Const(g_and_then_tac_name)); static expr g_or_else_tac_fn(Const(g_or_else_tac_name)), g_repeat_tac_fn(Const(g_repeat_tac_name)); static expr g_determ_tac_fn(Const(g_determ_tac_name)); -static expr g_tac_type(Const(g_tac_name)), g_builtin_tac(Const(g_builtin_tac_name)), g_fixpoint_tac(Const(g_fixpoint_name)); +static expr g_tac_type(Const(g_tac)), g_builtin_tac(Const(g_builtin_tac_name)), g_fixpoint_tac(Const(g_fixpoint_name)); expr const & get_exact_tac_fn() { return g_exact_tac_fn; } expr const & get_and_then_tac_fn() { return g_and_then_tac_fn; } expr const & get_or_else_tac_fn() { return g_or_else_tac_fn; } @@ -58,7 +58,7 @@ static void throw_failed(expr const & e) { throw expr_to_tactic_exception(e, "failed to convert expression into tactic"); } -/** \brief Return true if v is the constant tactic.builtin_tactic or the constant function that returns tactic.builtin_tactic */ +/** \brief Return true if v is the constant tactic.builtin or the constant function that returns tactic.builtin_tactic */ static bool is_builtin_tactic(expr const & v) { if (is_lambda(v)) return is_builtin_tactic(binding_body(v)); diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/tactic/expr_to_tactic.h index b6ec142674..a03b8ad039 100644 --- a/src/library/tactic/expr_to_tactic.h +++ b/src/library/tactic/expr_to_tactic.h @@ -12,7 +12,7 @@ namespace lean { /** \brief Return true iff the environment \c env contains the following declarations in the namespace 'tactic' - builtin_tactic : tactic + tactic.builtin : tactic and_then : tactic -> tactic -> tactic or_else : tactic -> tactic -> tactic repeat : tactic -> tactic @@ -21,7 +21,7 @@ bool has_tactic_decls(environment const & env); /** \brief Creates a tactic by 'executing' \c e. Definitions are unfolded, whnf procedure is invoked, - and definitions marked as 'tactic.builtin_tactic' are handled by the code registered using + and definitions marked as 'tactic.builtin' are handled by the code registered using \c register_expr_to_tactic. */ tactic expr_to_tactic(environment const & env, expr const & e, pos_info_provider const *p); diff --git a/tests/lean/empty.lean.expected.out b/tests/lean/empty.lean.expected.out index 88c2487e33..94d8939ec8 100644 --- a/tests/lean/empty.lean.expected.out +++ b/tests/lean/empty.lean.expected.out @@ -1,7 +1,7 @@ empty.lean:6:25: error: type error in placeholder assigned to - Prop_inhabited + char_inhabited placeholder has type - inhabited Prop + inhabited char but is expected to have type inhabited ?M_1 the assignment was attempted when trying to solve diff --git a/tests/lean/interactive/class_bug.lean b/tests/lean/interactive/class_bug.lean index 414181caee..98d6edc918 100644 --- a/tests/lean/interactive/class_bug.lean +++ b/tests/lean/interactive/class_bug.lean @@ -1,6 +1,6 @@ import logic.axioms.hilbert data.nat.basic open nonempty inhabited nat -theorem int_inhabited [instance] : inhabited nat := inhabited_mk zero +theorem int_inhabited [instance] : inhabited nat := inhabited.mk zero check epsilon (λ x : nat, true) diff --git a/tests/lean/interactive/in5.input.expected.out b/tests/lean/interactive/in5.input.expected.out index fd64ea25e0..025467f6f9 100644 --- a/tests/lean/interactive/in5.input.expected.out +++ b/tests/lean/interactive/in5.input.expected.out @@ -3,7 +3,7 @@ A → B → and A B -- ACK -- IDENTIFIER|4|0 -and_intro +and.intro -- ACK -- TYPE|4|10 A diff --git a/tests/lean/interactive/sorry2.lean b/tests/lean/interactive/sorry2.lean index c067dbe5df..cc3cc0cfca 100644 --- a/tests/lean/interactive/sorry2.lean +++ b/tests/lean/interactive/sorry2.lean @@ -1,4 +1,4 @@ import logic theorem tst (A B : Prop) : A ∧ B := -and_intro sorry sorry +and.intro sorry sorry diff --git a/tests/lean/let3.lean b/tests/lean/let3.lean index b4e9babd85..d49dee2ebb 100644 --- a/tests/lean/let3.lean +++ b/tests/lean/let3.lean @@ -1,5 +1,5 @@ import data.num -open num + variable f : num → num → num → num diff --git a/tests/lean/let4.lean b/tests/lean/let4.lean index 1c1817cca6..1e26fc6f59 100644 --- a/tests/lean/let4.lean +++ b/tests/lean/let4.lean @@ -1,5 +1,5 @@ import data.num -open num + variable f : num → num → num → num diff --git a/tests/lean/num.lean b/tests/lean/num.lean index d431a69db5..5c58f8b32b 100644 --- a/tests/lean/num.lean +++ b/tests/lean/num.lean @@ -1,5 +1,5 @@ import data.num -open num + check 10 check 20 diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean index f53850c030..6ce0a6d730 100644 --- a/tests/lean/run/algebra1.lean +++ b/tests/lean/run/algebra1.lean @@ -1,5 +1,4 @@ import logic -open num abbreviation Type1 := Type.{1} @@ -17,10 +16,10 @@ end namespace algebra inductive mul_struct (A : Type) : Type := - mk_mul_struct : (A → A → A) → mul_struct A + mk : (A → A → A) → mul_struct A inductive add_struct (A : Type) : Type := - mk_add_struct : (A → A → A) → add_struct A + mk : (A → A → A) → add_struct A definition mul [inline] {A : Type} {s : mul_struct A} (a b : A) := mul_struct.rec (fun f, f) s a b @@ -33,29 +32,30 @@ namespace algebra infixl `+`:65 := add end algebra -namespace nat inductive nat : Type := zero : nat, succ : nat → nat +namespace nat + variable add : nat → nat → nat variable mul : nat → nat → nat definition is_mul_struct [inline] [instance] : algebra.mul_struct nat - := algebra.mk_mul_struct mul + := algebra.mul_struct.mk mul definition is_add_struct [inline] [instance] : algebra.add_struct nat - := algebra.mk_add_struct add + := algebra.add_struct.mk add definition to_nat (n : num) : nat := #algebra - num.num.rec zero (λ n, num.pos_num.rec (succ zero) (λ n r, r + r) (λ n r, r + r + succ zero) n) n + num.rec nat.zero (λ n, pos_num.rec (succ zero) (λ n r, r + r) (λ n r, r + r + succ zero) n) n end nat namespace algebra namespace semigroup inductive semigroup_struct (A : Type) : Type := - mk_semigroup_struct : Π (mul : A → A → A), is_assoc mul → semigroup_struct A + mk : Π (mul : A → A → A), is_assoc mul → semigroup_struct A definition mul [inline] {A : Type} (s : semigroup_struct A) (a b : A) := semigroup_struct.rec (fun f h, f) s a b @@ -64,10 +64,10 @@ namespace semigroup := semigroup_struct.rec (fun f h, h) s definition is_mul_struct [inline] [instance] (A : Type) (s : semigroup_struct A) : mul_struct A - := mk_mul_struct (mul s) + := mul_struct.mk (mul s) inductive semigroup : Type := - mk_semigroup : Π (A : Type), semigroup_struct A → semigroup + mk : Π (A : Type), semigroup_struct A → semigroup definition carrier [inline] [coercion] (g : semigroup) := semigroup.rec (fun c s, c) g @@ -90,7 +90,7 @@ namespace monoid open semigroup definition is_semigroup_struct [inline] [instance] (A : Type) (s : monoid_struct A) : semigroup_struct A - := mk_semigroup_struct (mul s) (assoc s) + := semigroup_struct.mk (mul s) (assoc s) inductive monoid : Type := mk_monoid : Π (A : Type), monoid_struct A → monoid diff --git a/tests/lean/run/alias1.lean b/tests/lean/run/alias1.lean index b3b1a4eeb5..4aa8a7c8f8 100644 --- a/tests/lean/run/alias1.lean +++ b/tests/lean/run/alias1.lean @@ -28,21 +28,21 @@ check foo x a check foo a b theorem T1 : foo a b = N1.foo a b -:= refl _ +:= eq.refl _ definition aux1 := foo a b -- System elaborated it to N1.foo a b #erase_cache T2 theorem T2 : aux1 = N1.foo a b -:= refl _ +:= eq.refl _ open N1 definition aux2 := foo a b -- Now N1 is in the end of the queue, this is elaborated to N2.foo (f a) (f b) check aux2 theorem T3 : aux2 = N2.foo (f a) (f b) -:= refl aux2 +:= eq.refl aux2 check foo a b theorem T4 : foo a b = N2.foo a b -:= refl _ +:= eq.refl _ diff --git a/tests/lean/run/alias2.lean b/tests/lean/run/alias2.lean index ad27b49a52..aec611e391 100644 --- a/tests/lean/run/alias2.lean +++ b/tests/lean/run/alias2.lean @@ -19,4 +19,4 @@ coercion f definition aux2 := foo a b check aux2 theorem T3 : aux2 = N1.foo a b -:= refl _ +:= eq.refl _ diff --git a/tests/lean/run/bug5.lean b/tests/lean/run/bug5.lean index d791222f1b..76307d1737 100644 --- a/tests/lean/run/bug5.lean +++ b/tests/lean/run/bug5.lean @@ -1,4 +1,4 @@ import logic theorem symm2 {A : Type} {a b : A} (H : a = b) : b = a -:= subst H (refl a) +:= subst H (eq.refl a) diff --git a/tests/lean/run/calc.lean b/tests/lean/run/calc.lean index 513fa3f57c..90b57ee67e 100644 --- a/tests/lean/run/calc.lean +++ b/tests/lean/run/calc.lean @@ -1,5 +1,5 @@ import data.num -open num + namespace foo variable le : num → num → Prop diff --git a/tests/lean/run/class1.lean b/tests/lean/run/class1.lean index c7b2dc17b2..2edc27d8f7 100644 --- a/tests/lean/run/class1.lean +++ b/tests/lean/run/class1.lean @@ -1,5 +1,5 @@ import logic data.prod -open num prod inhabited +open prod inhabited definition H : inhabited (Prop × num × (num → num)) := _ diff --git a/tests/lean/run/class2.lean b/tests/lean/run/class2.lean index 95554944a4..302ce888e2 100644 --- a/tests/lean/run/class2.lean +++ b/tests/lean/run/class2.lean @@ -1,5 +1,5 @@ import logic data.prod -open num prod nonempty inhabited +open prod nonempty inhabited theorem H {A B : Type} (H1 : inhabited A) : inhabited (Prop × A × (B → num)) := _ diff --git a/tests/lean/run/class3.lean b/tests/lean/run/class3.lean index b4c655a0e0..f31403bdec 100644 --- a/tests/lean/run/class3.lean +++ b/tests/lean/run/class3.lean @@ -1,5 +1,5 @@ import logic data.prod -open num prod inhabited +open prod inhabited section parameter {A : Type} diff --git a/tests/lean/run/class4.lean b/tests/lean/run/class4.lean index be6e7e412e..66984cc80b 100644 --- a/tests/lean/run/class4.lean +++ b/tests/lean/run/class4.lean @@ -4,6 +4,9 @@ inductive nat : Type := zero : nat, succ : nat → nat +abbreviation refl := @eq.refl + +namespace nat definition add (x y : nat) := nat.rec x (λ n r, succ r) y @@ -26,8 +29,8 @@ 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)))) + (or.intro_left _ (refl zero)) + (λ 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 @@ -54,16 +57,16 @@ theorem not_zero_add (x y : nat) (H : ¬ is_zero y) : ¬ is_zero (x + y) subst (symm H1) H2) inductive not_zero (x : nat) : Prop := -not_zero_intro : ¬ is_zero x → not_zero x +intro : ¬ is_zero x → not_zero x theorem not_zero_not_is_zero {x : nat} (H : not_zero x) : ¬ is_zero x := not_zero.rec (λ H1, H1) H theorem not_zero_add_right [instance] (x y : nat) (H : not_zero y) : not_zero (x + y) -:= not_zero_intro (not_zero_add x y (not_zero_not_is_zero H)) +:= not_zero.intro (not_zero_add x y (not_zero_not_is_zero H)) theorem not_zero_succ [instance] (x : nat) : not_zero (succ x) -:= not_zero_intro (not_is_zero_succ x) +:= not_zero.intro (not_is_zero_succ x) variable dvd : Π (x y : nat) {H : not_zero y}, nat @@ -85,3 +88,5 @@ check dvd a (a + (succ b)) opaque_hint (exposing add) check dvd a (a + (succ b)) + +end nat diff --git a/tests/lean/run/class5.lean b/tests/lean/run/class5.lean index 5be795e132..007716c1ef 100644 --- a/tests/lean/run/class5.lean +++ b/tests/lean/run/class5.lean @@ -2,7 +2,7 @@ import logic namespace algebra inductive mul_struct (A : Type) : Type := - mk_mul_struct : (A → A → A) → mul_struct A + mk : (A → A → A) → mul_struct A definition mul [inline] {A : Type} {s : mul_struct A} (a b : A) := mul_struct.rec (λ f, f) s a b @@ -19,7 +19,7 @@ namespace nat variable add : nat → nat → nat definition mul_struct [instance] : algebra.mul_struct nat - := algebra.mk_mul_struct mul + := algebra.mul_struct.mk mul end nat section @@ -50,7 +50,7 @@ section open nat set_option pp.implicit true definition add_struct [instance] : algebra.mul_struct nat - := algebra.mk_mul_struct add + := algebra.mul_struct.mk add variables a b c : nat check #algebra a*b*c -- << is open add instead of mul diff --git a/tests/lean/run/class6.lean b/tests/lean/run/class6.lean index 5e31b412ed..3b75c188e8 100644 --- a/tests/lean/run/class6.lean +++ b/tests/lean/run/class6.lean @@ -8,10 +8,10 @@ inductive t2 : Type := mk2 : t2 theorem inhabited_t1 : inhabited t1 -:= inhabited_mk mk1 +:= inhabited.mk t1.mk1 theorem inhabited_t2 : inhabited t2 -:= inhabited_mk mk2 +:= inhabited.mk t2.mk2 instance inhabited_t1 inhabited_t2 diff --git a/tests/lean/run/class7.lean b/tests/lean/run/class7.lean index 0d36c6f11f..a1eed0c45c 100644 --- a/tests/lean/run/class7.lean +++ b/tests/lean/run/class7.lean @@ -1,16 +1,16 @@ import logic -open num tactic +open tactic inductive inh (A : Type) : Type := -inh_intro : A -> inh A +intro : A -> inh A -instance inh_intro +instance inh.intro theorem inh_bool [instance] : inh Prop -:= inh_intro true +:= inh.intro true theorem inh_fun [instance] {A B : Type} (H : inh B) : inh (A → B) -:= inh.rec (λ b, inh_intro (λ a : A, b)) H +:= inh.rec (λ b, inh.intro (λ a : A, b)) H definition assump := eassumption; now diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean index fa75573b42..bf9905e71c 100644 --- a/tests/lean/run/class8.lean +++ b/tests/lean/run/class8.lean @@ -1,25 +1,25 @@ import logic data.prod -open num tactic prod +open tactic prod inductive inh (A : Type) : Prop := -inh_intro : A -> inh A +intro : A -> inh A -instance inh_intro +instance inh.intro theorem inh_elim {A : Type} {B : Prop} (H1 : inh A) (H2 : A → B) : B := inh.rec H2 H1 theorem inh_exists [instance] {A : Type} {P : A → Prop} (H : ∃x, P x) : inh A -:= obtain w Hw, from H, inh_intro w +:= obtain w Hw, from H, inh.intro w theorem inh_bool [instance] : inh Prop -:= inh_intro true +:= inh.intro true theorem inh_fun [instance] {A B : Type} (H : inh B) : inh (A → B) -:= inh.rec (λb, inh_intro (λa : A, b)) H +:= inh.rec (λb, inh.intro (λa : A, b)) H theorem pair_inh [instance] {A : Type} {B : Type} (H1 : inh A) (H2 : inh B) : inh (prod A B) -:= inh_elim H1 (λa, inh_elim H2 (λb, inh_intro (pair a b))) +:= inh_elim H1 (λa, inh_elim H2 (λb, inh.intro (pair a b))) definition assump := eassumption tactic_hint assump diff --git a/tests/lean/run/class_coe.lean b/tests/lean/run/class_coe.lean index cdb7ea140e..32e4cedc7d 100644 --- a/tests/lean/run/class_coe.lean +++ b/tests/lean/run/class_coe.lean @@ -1,5 +1,5 @@ import data.num -open num + variables int nat real : Type.{1} variable nat_add : nat → nat → nat @@ -14,9 +14,9 @@ add_struct.rec (λ m, m) S a b infixl `+`:65 := add -definition add_nat_struct [instance] : add_struct nat := mk nat_add -definition add_int_struct [instance] : add_struct int := mk int_add -definition add_real_struct [instance] : add_struct real := mk real_add +definition add_nat_struct [instance] : add_struct nat := add_struct.mk nat_add +definition add_int_struct [instance] : add_struct int := add_struct.mk int_add +definition add_real_struct [instance] : add_struct real := add_struct.mk real_add variables n m : nat variables i j : int diff --git a/tests/lean/run/coe1.lean b/tests/lean/run/coe1.lean index 01f106c8e7..a2abf1369f 100644 --- a/tests/lean/run/coe1.lean +++ b/tests/lean/run/coe1.lean @@ -18,13 +18,13 @@ set_option pp.universes true check eq a1 b1 inductive pair (A : Type) (B: Type) : Type := -mk_pair : A → B → pair A B +mk : A → B → pair A B -check mk_pair a1 b2 +check pair.mk a1 b2 check B -check mk_pair +check pair.mk set_option pp.unicode false -check mk_pair +check pair.mk set_option pp.implicit false -check mk_pair -check pair \ No newline at end of file +check pair.mk +check pair diff --git a/tests/lean/run/coe3.lean b/tests/lean/run/coe3.lean index c9c180e588..1931874afd 100644 --- a/tests/lean/run/coe3.lean +++ b/tests/lean/run/coe3.lean @@ -15,16 +15,16 @@ namespace setoid coercion carrier inductive morphism (s1 s2 : setoid) : Type := - mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2 + mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2 set_option pp.universes true - check mk_morphism + check morphism.mk check λ (s1 s2 : setoid), s1 check λ (s1 s2 : Type), s1 inductive morphism2 (s1 : setoid) (s2 : setoid) : Type := - mk_morphism2 : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2 + mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2 - check mk_morphism2 + check morphism2.mk end setoid diff --git a/tests/lean/run/coe4.lean b/tests/lean/run/coe4.lean index a1c761f96f..0406d9a090 100644 --- a/tests/lean/run/coe4.lean +++ b/tests/lean/run/coe4.lean @@ -20,15 +20,15 @@ namespace setoid coercion carrier inductive morphism (s1 s2 : setoid) : Type := - mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2 + mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2 - check mk_morphism + check morphism.mk check λ (s1 s2 : setoid), s1 check λ (s1 s2 : Type), s1 inductive morphism2 (s1 : setoid) (s2 : setoid) : Type := - mk_morphism2 : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2 + mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2 check morphism2 - check mk_morphism2 + check morphism2.mk end setoid diff --git a/tests/lean/run/coe5.lean b/tests/lean/run/coe5.lean index 0107967e1f..8752fe847f 100644 --- a/tests/lean/run/coe5.lean +++ b/tests/lean/run/coe5.lean @@ -20,17 +20,17 @@ namespace setoid coercion carrier inductive morphism (s1 s2 : setoid) : Type := - mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2 + mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2 - check mk_morphism + check morphism.mk check λ (s1 s2 : setoid), s1 check λ (s1 s2 : Type), s1 inductive morphism2 (s1 : setoid) (s2 : setoid) : Type := - mk_morphism2 : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2 + mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism2 s1 s2 check morphism2 - check mk_morphism2 + check morphism2.mk inductive my_struct : Type := mk_foo : Π (s1 s2 : setoid) (s3 s4 : setoid), morphism2 s1 s2 → morphism2 s3 s4 → my_struct diff --git a/tests/lean/run/coe7.lean b/tests/lean/run/coe7.lean index 8c000c9a09..f6caa150db 100644 --- a/tests/lean/run/coe7.lean +++ b/tests/lean/run/coe7.lean @@ -7,5 +7,5 @@ coercion of_nat theorem tst (n : nat) : n = n := have H : true, from trivial, -calc n = n : refl _ - ... = n : refl _ \ No newline at end of file +calc n = n : eq.refl _ + ... = n : eq.refl _ diff --git a/tests/lean/run/coercion_bug2.lean b/tests/lean/run/coercion_bug2.lean index 758e4dc30e..6698eab4da 100644 --- a/tests/lean/run/coercion_bug2.lean +++ b/tests/lean/run/coercion_bug2.lean @@ -6,5 +6,5 @@ nil {} : list T, cons : T → list T → list T definition length {T : Type} : list T → nat := list.rec 0 (fun x l m, succ m) -theorem length_nil {T : Type} : length (@nil T) = 0 -:= refl _ +theorem length_nil {T : Type} : length (@list.nil T) = 0 +:= eq.refl _ diff --git a/tests/lean/run/congr_imp_bug.lean b/tests/lean/run/congr_imp_bug.lean index 7c67cfc7bd..a53e1dadde 100644 --- a/tests/lean/run/congr_imp_bug.lean +++ b/tests/lean/run/congr_imp_bug.lean @@ -36,7 +36,7 @@ theorem compose21 {R1 : T1 → T1 → Prop} {f1 : T1 → T2} (C1 : congr.struc R1 R2 f1) {f2 : T1 → T3} (C2 : congr.struc R1 R3 f2) : - congr.struc R1 R4 (λx, g (f1 x) (f2 x)) := mk (take x1 x2 H, app2 C3 (app C1 H) (app C2 H)) + congr.struc R1 R4 (λx, g (f1 x) (f2 x)) := struc.mk (take x1 x2 H, app2 C3 (app C1 H) (app C2 H)) theorem congr_and : congr.struc2 iff iff iff and := sorry diff --git a/tests/lean/run/e14.lean b/tests/lean/run/e14.lean index 718715d351..18d0efcc3e 100644 --- a/tests/lean/run/e14.lean +++ b/tests/lean/run/e14.lean @@ -1,21 +1,25 @@ inductive nat : Type := zero : nat, succ : nat → nat +namespace nat end nat open nat inductive list (A : Type) : Type := nil {} : list A, cons : A → list A → list A +abbreviation nil := @list.nil +abbreviation cons := @list.cons check nil check nil.{1} check @nil.{1} nat check @nil nat -check cons zero nil +check cons nat.zero nil inductive vector (A : Type) : nat → Type := vnil {} : vector A zero, vcons : forall {n : nat}, A → vector A n → vector A (succ n) +namespace vector end vector open vector check vcons zero vnil variable n : nat diff --git a/tests/lean/run/e15.lean b/tests/lean/run/e15.lean index 3c5f08315a..cbc0d17274 100644 --- a/tests/lean/run/e15.lean +++ b/tests/lean/run/e15.lean @@ -1,11 +1,12 @@ inductive nat : Type := zero : nat, succ : nat → nat +namespace nat end nat open nat inductive list (A : Type) : Type := nil {} : list A, cons : A → list A → list A - +namespace list end list open list check nil check nil.{1} check @nil.{1} nat @@ -16,6 +17,7 @@ check cons zero nil inductive vector (A : Type) : nat → Type := vnil {} : vector A zero, vcons : forall {n : nat}, A → vector A n → vector A (succ n) +namespace vector end vector open vector check vcons zero vnil variable n : nat diff --git a/tests/lean/run/e16.lean b/tests/lean/run/e16.lean index 06bfbbeeb8..a28e4ea526 100644 --- a/tests/lean/run/e16.lean +++ b/tests/lean/run/e16.lean @@ -1,10 +1,12 @@ inductive nat : Type := zero : nat, succ : nat → nat +namespace nat end nat open nat inductive list (A : Type) : Type := nil {} : list A, cons : A → list A → list A +namespace list end list open list check nil check nil.{1} @@ -16,6 +18,7 @@ check cons zero nil inductive vector (A : Type) : nat → Type := vnil {} : vector A zero, vcons : forall {n : nat}, A → vector A n → vector A (succ n) +namespace vector end vector open vector check vcons zero vnil variable n : nat diff --git a/tests/lean/run/e17.lean b/tests/lean/run/e17.lean index 67745fe966..7fe86e4e06 100644 --- a/tests/lean/run/e17.lean +++ b/tests/lean/run/e17.lean @@ -10,13 +10,14 @@ inductive int : Type := of_nat : nat → int, neg : nat → int -coercion of_nat +coercion int.of_nat variables n m : nat variables i j : int +namespace list end list open list check cons i (cons i nil) check cons n (cons n nil) check cons i (cons n nil) check cons n (cons i nil) -check cons n (cons i (cons m (cons j nil))) \ No newline at end of file +check cons n (cons i (cons m (cons j nil))) diff --git a/tests/lean/run/e18.lean b/tests/lean/run/e18.lean index 9aa3dcdba8..1ab4026c1f 100644 --- a/tests/lean/run/e18.lean +++ b/tests/lean/run/e18.lean @@ -10,14 +10,15 @@ inductive int : Type := of_nat : nat → int, neg : nat → int -coercion of_nat +coercion int.of_nat variables n m : nat variables i j : int variable l : list nat +namespace list end list open list check cons i (cons i nil) check cons n (cons n nil) check cons i (cons n nil) check cons n (cons i nil) -check cons n (cons i (cons m (cons j nil))) \ No newline at end of file +check cons n (cons i (cons m (cons j nil))) diff --git a/tests/lean/run/e5.lean b/tests/lean/run/e5.lean index a9c3635eac..b893a69f83 100644 --- a/tests/lean/run/e5.lean +++ b/tests/lean/run/e5.lean @@ -34,6 +34,7 @@ theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c inductive nat : Type := zero : nat, succ : nat → nat +namespace nat end nat open nat print "using strict implicit arguments" abbreviation symmetric {A : Type} (R : A → A → Prop) := ∀ ⦃a b⦄, R a b → R b a diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean index 76fe338902..7d6e6220b7 100644 --- a/tests/lean/run/elab_bug1.lean +++ b/tests/lean/run/elab_bug1.lean @@ -30,11 +30,11 @@ theorem congr_app {T1 : Type} {T2 : Type} (R1 : T1 → T1 → Prop) (R2 : T2 → -- -------------------------------- theorem congr_trivial [instance] {T : Type} (R : T → T → Prop) : congruence R R id := -mk (take x y H, H) +congruence.mk (take x y H, H) theorem congr_const {T2 : Type} (R2 : T2 → T2 → Prop) (H : reflexive R2) : ∀(T1 : Type) (R1 : T1 → T1 → Prop) (c : T2), congruence R1 R2 (const T1 c) := -take T1 R1 c, mk (take x y H1, H c) +take T1 R1 c, congruence.mk (take x y H1, H c) -- congruences for logic diff --git a/tests/lean/run/elim.lean b/tests/lean/run/elim.lean index c20b5d83d6..896926d025 100644 --- a/tests/lean/run/elim.lean +++ b/tests/lean/run/elim.lean @@ -1,5 +1,5 @@ import logic -open num + variable 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 diff --git a/tests/lean/run/elim2.lean b/tests/lean/run/elim2.lean index 351d31dc6f..c7a33fa81a 100644 --- a/tests/lean/run/elim2.lean +++ b/tests/lean/run/elim2.lean @@ -1,5 +1,5 @@ import logic -open num tactic +open tactic variable 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 diff --git a/tests/lean/run/full.lean b/tests/lean/run/full.lean index 0ee5e64a1d..63a5580baf 100644 --- a/tests/lean/run/full.lean +++ b/tests/lean/run/full.lean @@ -1,8 +1,7 @@ import logic namespace foo - variable x : num.num + variable x : num check x - open num check x set_option pp.full_names true check x diff --git a/tests/lean/run/fun.lean b/tests/lean/run/fun.lean index 3eabd935f8..6cca45f94d 100644 --- a/tests/lean/run/fun.lean +++ b/tests/lean/run/fun.lean @@ -1,5 +1,5 @@ import logic struc.function -open function num bool +open function bool variable f : num → bool @@ -13,9 +13,9 @@ check num → num ⟨is_typeof⟩ id variable h : num → bool → num check flip h -check flip h ff zero +check flip h ff num.zero -check typeof flip h ff zero : num +check typeof flip h ff num.zero : num variable f1 : num → num → bool variable f2 : bool → num diff --git a/tests/lean/run/group.lean b/tests/lean/run/group.lean index c589513698..b74370e510 100644 --- a/tests/lean/run/group.lean +++ b/tests/lean/run/group.lean @@ -1,5 +1,4 @@ import logic -open num section parameter {A : Type} diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean index 4019b3fa2d..c432a20ba4 100644 --- a/tests/lean/run/group2.lean +++ b/tests/lean/run/group2.lean @@ -1,5 +1,4 @@ import logic -open num section parameter {A : Type} @@ -14,10 +13,10 @@ section end inductive group_struct (A : Type) : Type := -mk_group_struct : Π (mul : A → A → A) (one : A) (inv : A → A), is_assoc mul → is_id mul one → is_inv mul one inv → group_struct A +mk : Π (mul : A → A → A) (one : A) (inv : A → A), is_assoc mul → is_id mul one → is_inv mul one inv → group_struct A inductive group : Type := -mk_group : Π (A : Type), group_struct A → group +mk : Π (A : Type), group_struct A → group definition carrier (g : group) : Type := group.rec (λ c s, c) g @@ -57,11 +56,11 @@ axiom H2 : is_id rmul rone axiom H3 : is_inv rmul rone rinv definition real_group_struct [inline] [instance] : group_struct pos_real -:= mk_group_struct rmul rone rinv H1 H2 H3 +:= group_struct.mk rmul rone rinv H1 H2 H3 variables x y : pos_real check x * y set_option pp.implicit true print "---------------" theorem T (a b : pos_real): (rmul a b) = a*b -:= refl (rmul a b) +:= eq.refl (rmul a b) diff --git a/tests/lean/run/id.lean b/tests/lean/run/id.lean index 9a44fb2f04..6ec7968114 100644 --- a/tests/lean/run/id.lean +++ b/tests/lean/run/id.lean @@ -4,7 +4,7 @@ check id id set_option pp.universes true check id id check id Prop -check id num.num +check id num check @id.{0} check @id.{1} check id num.zero diff --git a/tests/lean/run/ind1.lean b/tests/lean/run/ind1.lean index bb53c11719..2450b79c3c 100644 --- a/tests/lean/run/ind1.lean +++ b/tests/lean/run/ind1.lean @@ -1,7 +1,7 @@ inductive list (A : Type) : Type := nil : list A, cons : A → list A → list A - +namespace list end list open list check list.{1} check cons.{1} check list.rec.{1 1} diff --git a/tests/lean/run/ind2.lean b/tests/lean/run/ind2.lean index 94b3685252..d9a8dbcc95 100644 --- a/tests/lean/run/ind2.lean +++ b/tests/lean/run/ind2.lean @@ -1,11 +1,12 @@ inductive nat : Type := zero : nat, succ : nat → nat +namespace nat end nat open nat inductive vector (A : Type) : nat → Type := vnil : vector A zero, vcons : Π {n : nat}, A → vector A n → vector A (succ n) - +namespace vector end vector open vector check vector.{1} check vnil.{1} check vcons.{1} diff --git a/tests/lean/run/ind4.lean b/tests/lean/run/ind4.lean index fde14a2d38..3977276829 100644 --- a/tests/lean/run/ind4.lean +++ b/tests/lean/run/ind4.lean @@ -6,7 +6,7 @@ section end check list.{1} -check cons.{1} +check list.cons.{1} section parameter A : Type @@ -20,4 +20,4 @@ section end check tree.{1} -check forest.{1} \ No newline at end of file +check forest.{1} diff --git a/tests/lean/run/ind5.lean b/tests/lean/run/ind5.lean index 6316907c17..1e24d829a5 100644 --- a/tests/lean/run/ind5.lean +++ b/tests/lean/run/ind5.lean @@ -1,9 +1,9 @@ definition Prop [inline] : Type.{1} := Type.{0} inductive or (A B : Prop) : Prop := -or_intro_left : A → or A B, -or_intro_right : B → or A B +intro_left : A → or A B, +intro_right : B → or A B check or -check or_intro_left +check or.intro_left check or.rec diff --git a/tests/lean/run/ind7.lean b/tests/lean/run/ind7.lean index d6cfa6c20e..fae5f6192b 100644 --- a/tests/lean/run/ind7.lean +++ b/tests/lean/run/ind7.lean @@ -4,7 +4,7 @@ namespace list cons : A → list A → list A check list.{1} - check cons.{1} + check list.cons.{1} check list.rec.{1 1} end list diff --git a/tests/lean/run/is_nil.lean b/tests/lean/run/is_nil.lean index e9f9b4898d..debdee21ed 100644 --- a/tests/lean/run/is_nil.lean +++ b/tests/lean/run/is_nil.lean @@ -4,6 +4,8 @@ open tactic inductive list (A : Type) : Type := nil {} : list A, cons : A → list A → list A +namespace list end list open list +open eq definition is_nil {A : Type} (l : list A) : Prop := list.rec true (fun h t r, false) l @@ -25,7 +27,7 @@ theorem T : is_nil (@nil Prop) (* local list = Const("list", {1})(Prop) local isNil = Const("is_nil", {1})(Prop) -local Nil = Const("nil", {1})(Prop) +local Nil = Const({"list", "nil"}, {1})(Prop) local m = mk_metavar("m", list) print(isNil(Nil)) print(isNil(m)) diff --git a/tests/lean/run/list_elab1.lean b/tests/lean/run/list_elab1.lean index 07e2a16cd5..8a28ee97b5 100644 --- a/tests/lean/run/list_elab1.lean +++ b/tests/lean/run/list_elab1.lean @@ -15,6 +15,7 @@ inductive list (T : Type) : Type := nil {} : list T, cons : T → list T → list T +namespace list theorem list_induction_on {T : Type} {P : list T → Prop} (l : list T) (Hnil : P nil) (Hind : forall x : T, forall l : list T, forall H : P l, P (cons x l)) : P l := list.rec Hnil Hind l @@ -23,6 +24,7 @@ definition concat {T : Type} (s t : list T) : list T := list.rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s theorem concat_nil {T : Type} (t : list T) : concat t nil = t := -list_induction_on t (refl (concat nil nil)) +list_induction_on t (eq.refl (concat nil nil)) (take (x : T) (l : list T) (H : concat l nil = l), - H ▸ (refl (concat (cons x l) nil))) + H ▸ (eq.refl (concat (cons x l) nil))) +end list diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean index 0dc67b2e91..ff1110a11e 100644 --- a/tests/lean/run/match1.lean +++ b/tests/lean/run/match1.lean @@ -23,6 +23,6 @@ end local f = Const("f") local two1 = Const("two1") local two2 = Const("two2") -local succ = Const({"succ"}) +local succ = Const({"nat", "succ"}) tst_match(f(succ(mk_var(0)), two1), f(two2, two2)) *) diff --git a/tests/lean/run/nat_bug.lean b/tests/lean/run/nat_bug.lean index 1dcf118290..ce758d21c4 100644 --- a/tests/lean/run/nat_bug.lean +++ b/tests/lean/run/nat_bug.lean @@ -4,7 +4,8 @@ open decidable inductive nat : Type := zero : nat, succ : nat → nat - +abbreviation refl := @eq.refl +namespace nat theorem induction_on {P : nat → Prop} (a : nat) (H1 : P zero) (H2 : ∀ (n : nat) (IH : P n), P (succ n)) : P a := nat.rec H1 H2 a @@ -14,12 +15,13 @@ theorem pred_succ (n : nat) : pred (succ n) = n := refl _ theorem zero_or_succ (n : nat) : n = zero ∨ n = succ (pred n) := induction_on n - (or_intro_left _ (refl zero)) - (take m IH, or_intro_right _ + (or.intro_left _ (refl zero)) + (take m IH, or.intro_right _ (show succ m = succ (pred (succ m)), from congr_arg succ (symm (pred_succ m)))) theorem zero_or_succ2 (n : nat) : n = zero ∨ n = succ (pred n) := @induction_on _ n - (or_intro_left _ (refl zero)) - (take m IH, or_intro_right _ + (or.intro_left _ (refl zero)) + (take m IH, or.intro_right _ (show succ m = succ (pred (succ m)), from congr_arg succ (symm (pred_succ m)))) +end nat diff --git a/tests/lean/run/nat_bug2.lean b/tests/lean/run/nat_bug2.lean index b8ea09247d..b4315496a9 100644 --- a/tests/lean/run/nat_bug2.lean +++ b/tests/lean/run/nat_bug2.lean @@ -1,14 +1,15 @@ import logic -open num eq_ops +open eq_ops inductive nat : Type := zero : nat, succ : nat → nat +namespace nat abbreviation plus (x y : nat) : nat := nat.rec x (λn r, succ r) y definition to_nat [coercion] [inline] (n : num) : nat -:= num.num.rec zero (λn, num.pos_num.rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n +:= num.rec zero (λn, pos_num.rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n definition add (x y : nat) : nat := plus x y variable le : nat → nat → Prop @@ -20,3 +21,5 @@ axiom add_le_right {n m : nat} (H : n ≤ m) (k : nat) : n + k ≤ m + k theorem succ_le {n m : nat} (H : n ≤ m) : succ n ≤ succ m := add_one m ▸ add_one n ▸ add_le_right H 1 + +end nat diff --git a/tests/lean/run/nat_bug3.lean b/tests/lean/run/nat_bug3.lean index 9a9bac47bc..6a864c78b6 100644 --- a/tests/lean/run/nat_bug3.lean +++ b/tests/lean/run/nat_bug3.lean @@ -1,14 +1,15 @@ import logic -open num eq_ops +open eq_ops inductive nat : Type := zero : nat, succ : nat → nat +namespace nat abbreviation plus (x y : nat) : nat := nat.rec x (λn r, succ r) y definition to_nat [coercion] [inline] (n : num) : nat -:= num.num.rec zero (λn, num.pos_num.rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n +:= num.rec zero (λn, pos_num.rec (succ zero) (λn r, plus r (plus r (succ zero))) (λn r, plus r r) n) n definition add (x y : nat) : nat := plus x y variable le : nat → nat → Prop @@ -20,3 +21,5 @@ axiom add_le_right_inv {n m k : nat} (H : n + k ≤ m + k) : n ≤ m theorem succ_le_cancel {n m : nat} (H : succ n ≤ succ m) : n ≤ m := add_le_right_inv (add_one m⁻¹ ▸ add_one n⁻¹ ▸ H) + +end nat diff --git a/tests/lean/run/nat_bug4.lean b/tests/lean/run/nat_bug4.lean index 1db03ce5da..32fe496230 100644 --- a/tests/lean/run/nat_bug4.lean +++ b/tests/lean/run/nat_bug4.lean @@ -1,10 +1,10 @@ import logic -open num eq_ops +open eq_ops inductive nat : Type := zero : nat, succ : nat → nat - +namespace nat definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y infixl `+`:65 := add definition mul (n m : nat) := nat.rec zero (fun m x, x + n) m @@ -13,4 +13,5 @@ infixl `*`:75 := mul axiom mul_succ_right (n m : nat) : n * succ m = n * m + n theorem small2 (n m l : nat) : n * succ l + m = n * l + n + m -:= subst (mul_succ_right _ _) (refl (n * succ l + m)) +:= subst (mul_succ_right _ _) (eq.refl (n * succ l + m)) +end nat diff --git a/tests/lean/run/nat_bug5.lean b/tests/lean/run/nat_bug5.lean index 69cdca9c6b..f374cc10b5 100644 --- a/tests/lean/run/nat_bug5.lean +++ b/tests/lean/run/nat_bug5.lean @@ -1,10 +1,11 @@ import logic -open num eq_ops +open eq_ops inductive nat : Type := zero : nat, succ : nat → nat +namespace nat definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y infixl `+`:65 := add definition mul (n m : nat) := nat.rec zero (fun m x, x + n) m @@ -21,8 +22,8 @@ set_option unifier.max_steps 50000 theorem mul_add_distr_left (n m k : nat) : (n + m) * k = n * k + m * k := induction_on k (calc - (n + m) * zero = zero : refl _ - ... = n * zero + m * zero : refl _) + (n + m) * zero = zero : eq.refl _ + ... = n * zero + m * zero : eq.refl _) (take l IH, calc (n + m) * succ l = (n + m) * l + (n + m) : mul_succ_right _ _ @@ -32,3 +33,4 @@ theorem mul_add_distr_left (n m k : nat) : (n + m) * k = n * k + m * k ... = 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 _ _)}) +end nat diff --git a/tests/lean/run/nat_bug6.lean b/tests/lean/run/nat_bug6.lean index b8669f59bc..fae9bfa415 100644 --- a/tests/lean/run/nat_bug6.lean +++ b/tests/lean/run/nat_bug6.lean @@ -5,6 +5,7 @@ inductive nat : Type := zero : nat, succ : nat → nat +namespace nat definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y infixl `+`:65 := add definition mul (n m : nat) := nat.rec zero (fun m x, x + n) m @@ -17,3 +18,4 @@ variable P : nat → Prop print "===========================" theorem tst (n : nat) (H : P (n * zero)) : P zero := subst (mul_zero_right _) H +end nat diff --git a/tests/lean/run/nat_bug7.lean b/tests/lean/run/nat_bug7.lean index ed6318f61d..fddd53e0c0 100644 --- a/tests/lean/run/nat_bug7.lean +++ b/tests/lean/run/nat_bug7.lean @@ -4,6 +4,7 @@ inductive nat : Type := zero : nat, succ : nat → nat +namespace nat definition add (x y : nat) : nat := nat.rec x (λn r, succ r) y infixl `+`:65 := add @@ -11,4 +12,5 @@ axiom add_right_comm (n m k : nat) : n + m + k = n + k + m print "===========================" theorem bug (a b c d : nat) : a + b + c + d = a + c + b + d -:= subst (add_right_comm _ _ _) (refl (a + b + c + d)) +:= subst (add_right_comm _ _ _) (eq.refl (a + b + c + d)) +end nat diff --git a/tests/lean/run/nat_coe.lean b/tests/lean/run/nat_coe.lean index bea135107e..3d54ab4641 100644 --- a/tests/lean/run/nat_coe.lean +++ b/tests/lean/run/nat_coe.lean @@ -18,9 +18,9 @@ variables i j : int abbreviation c1 := a + b theorem T1 : c1 = nat_add a b := -refl _ +eq.refl _ abbreviation c2 := i + j theorem T2 : c2 = int_add i j := -refl _ +eq.refl _ diff --git a/tests/lean/run/opaque_hint_bug.lean b/tests/lean/run/opaque_hint_bug.lean index 24349158f2..726b37ea60 100644 --- a/tests/lean/run/opaque_hint_bug.lean +++ b/tests/lean/run/opaque_hint_bug.lean @@ -7,7 +7,7 @@ section variable {T : Type} definition concat (s t : list T) : list T - := list.rec t (fun x l u, cons x u) s + := list.rec t (fun x l u, list.cons x u) s opaque_hint (hiding concat) diff --git a/tests/lean/run/rel.lean b/tests/lean/run/rel.lean index b7569974ba..df7a75f47c 100644 --- a/tests/lean/run/rel.lean +++ b/tests/lean/run/rel.lean @@ -22,7 +22,7 @@ instance is_equivalence.is_symmetric instance is_equivalence.is_transitive theorem and_inhabited_left {a : Prop} (b : Prop) (Ha : a) : a ∧ b ↔ b := -iff_intro (take Hab, and_elim_right Hab) (take Hb, and_intro Ha Hb) +iff_intro (take Hab, and_elim_right Hab) (take Hb, and.intro Ha Hb) theorem test (a b c : Prop) (P : Prop → Prop) (H1 : a ↔ b) (H2 : c ∧ a) : c ∧ b := subst_iff H1 H2 diff --git a/tests/lean/run/root.lean b/tests/lean/run/root.lean index 4d1f43e285..61bf52ae5a 100644 --- a/tests/lean/run/root.lean +++ b/tests/lean/run/root.lean @@ -1,5 +1,5 @@ import logic -open num + variable foo : Prop diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean index e6e15bb678..454cb35650 100644 --- a/tests/lean/run/sum_bug.lean +++ b/tests/lean/run/sum_bug.lean @@ -6,13 +6,13 @@ import logic.core.prop logic.classes.inhabited logic.classes.decidable open inhabited decidable -namespace sum - -- TODO: take this outside the namespace when the inductive package handles it better inductive sum (A B : Type) : Type := inl : A → sum A B, inr : B → sum A B +namespace sum + infixr `+`:25 := sum abbreviation rec_on {A B : Type} {C : (A + B) → Type} (s : A + B) @@ -43,10 +43,10 @@ have H2 : f (inr A b2), from subst H H1, H2 theorem sum_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A + B) := -inhabited_mk (inl B (default A)) +inhabited.mk (inl B (default A)) theorem sum_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabited (A + B) := -inhabited_mk (inr A (default B)) +inhabited.mk (inr A (default B)) theorem sum_eq_decidable [instance] {A B : Type} (s1 s2 : A + B) (H1 : ∀a1 a2 : A, decidable (inl B a1 = inl B a2)) diff --git a/tests/lean/run/tac1.lean b/tests/lean/run/tac1.lean index 47e648b3ce..82bb786e34 100644 --- a/tests/lean/run/tac1.lean +++ b/tests/lean/run/tac1.lean @@ -1,6 +1,6 @@ import tools.tactic open tactic -definition mytac := apply @and_intro; apply @refl +definition mytac := apply @and.intro; apply @eq.refl check @mytac diff --git a/tests/lean/run/tactic12.lean b/tests/lean/run/tactic12.lean index c4ca364e2a..1728c64810 100644 --- a/tests/lean/run/tactic12.lean +++ b/tests/lean/run/tactic12.lean @@ -2,7 +2,7 @@ import logic open tactic theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b -:= by apply and_intro; +:= by apply and.intro; apply not_intro; exact (assume Ha, or_elim H diff --git a/tests/lean/run/tactic13.lean b/tests/lean/run/tactic13.lean index 034e5c727e..7a8c5d8166 100644 --- a/tests/lean/run/tactic13.lean +++ b/tests/lean/run/tactic13.lean @@ -3,7 +3,7 @@ open tactic theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b := begin - apply and_intro, + apply and.intro, apply not_intro, assume Ha, or_elim H (assume Hna, @absurd _ false Ha Hna) diff --git a/tests/lean/run/tactic14.lean b/tests/lean/run/tactic14.lean index e0a9eecaee..08058a12b7 100644 --- a/tests/lean/run/tactic14.lean +++ b/tests/lean/run/tactic14.lean @@ -2,7 +2,7 @@ import logic open tactic definition basic_tac : tactic -:= repeat [apply @and_intro | assumption] +:= repeat [apply @and.intro | assumption] set_begin_end_tactic basic_tac -- basic_tac is automatically applied to each element of a proof-qed block diff --git a/tests/lean/run/tactic15.lean b/tests/lean/run/tactic15.lean index 30be170f88..956ac914e4 100644 --- a/tests/lean/run/tactic15.lean +++ b/tests/lean/run/tactic15.lean @@ -9,4 +9,4 @@ theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a (f b b) = f b (f c c) trace "trying again... "; state; apply (subst H2); - apply refl + apply eq.refl diff --git a/tests/lean/run/tactic16.lean b/tests/lean/run/tactic16.lean index a56c49102c..d8233ef2f6 100644 --- a/tests/lean/run/tactic16.lean +++ b/tests/lean/run/tactic16.lean @@ -8,4 +8,4 @@ theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a (f b b) = f b (f c c) := by discard (apply (subst H1)) 3; -- discard the first 3 solutions produced by apply trace "after subst H1"; apply (subst H2); - apply refl + apply eq.refl diff --git a/tests/lean/run/tactic18.lean b/tests/lean/run/tactic18.lean index d5f7468ab7..13a8772610 100644 --- a/tests/lean/run/tactic18.lean +++ b/tests/lean/run/tactic18.lean @@ -7,5 +7,5 @@ variable f : A → A → A theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c := by apply (@congr A A); apply (subst H2); - apply refl; + apply eq.refl; assumption diff --git a/tests/lean/run/tactic19.lean b/tests/lean/run/tactic19.lean index aaaf7013aa..e4384b68cd 100644 --- a/tests/lean/run/tactic19.lean +++ b/tests/lean/run/tactic19.lean @@ -4,5 +4,5 @@ open tactic theorem tst {A : Type} {f : A → A → A} {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c := by apply congr; apply (subst H2); - apply refl; + apply eq.refl; assumption diff --git a/tests/lean/run/tactic21.lean b/tests/lean/run/tactic21.lean index 09868af7d4..ece085fa95 100644 --- a/tests/lean/run/tactic21.lean +++ b/tests/lean/run/tactic21.lean @@ -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()) diff --git a/tests/lean/run/tactic22.lean b/tests/lean/run/tactic22.lean index 72d529a456..ae413ac8a3 100644 --- a/tests/lean/run/tactic22.lean +++ b/tests/lean/run/tactic22.lean @@ -2,4 +2,4 @@ import logic open tactic theorem T (a b c d : Prop) (Ha : a) (Hb : b) (Hc : c) (Hd : d) : a ∧ b ∧ c ∧ d -:= by fixpoint (λ f, [apply @and_intro; f | assumption; f | id]) +:= by fixpoint (λ f, [apply @and.intro; f | assumption; f | id]) diff --git a/tests/lean/run/tactic23.lean b/tests/lean/run/tactic23.lean index a9f14f247a..6f49e54683 100644 --- a/tests/lean/run/tactic23.lean +++ b/tests/lean/run/tactic23.lean @@ -1,11 +1,11 @@ import logic -open num (num pos_num num.rec pos_num.rec) open tactic inductive nat : Type := zero : nat, succ : nat → nat +namespace nat definition add [inline] (a b : nat) : nat := nat.rec a (λ n r, succ r) b infixl `+`:65 := add @@ -33,4 +33,6 @@ definition is_zero (n : nat) := nat.rec true (λ n r, false) n theorem T2 : ∃ a, (is_zero a) = true -:= by apply exists_intro; apply refl +:= by apply exists_intro; apply eq.refl + +end nat diff --git a/tests/lean/run/tactic24.lean b/tests/lean/run/tactic24.lean index 91de99bd3e..a56c8abf76 100644 --- a/tests/lean/run/tactic24.lean +++ b/tests/lean/run/tactic24.lean @@ -1,8 +1,8 @@ import logic open tactic -definition my_tac1 := apply @refl -definition my_tac2 := repeat (apply @and_intro; assumption) +definition my_tac1 := apply @eq.refl +definition my_tac2 := repeat (apply @and.intro; assumption) tactic_hint my_tac1 tactic_hint my_tac2 @@ -13,8 +13,8 @@ theorem T1 {A : Type.{2}} (a : A) : a = a theorem T2 {a b c : Prop} (Ha : a) (Hb : b) (Hc : c) : a ∧ b ∧ c := _ -definition my_tac3 := fixpoint (λ f, [apply @or_intro_left; f | - apply @or_intro_right; f | +definition my_tac3 := fixpoint (λ f, [apply @or.intro_left; f | + apply @or.intro_right; f | assumption]) tactic_hint [or] my_tac3 diff --git a/tests/lean/run/tactic25.lean b/tests/lean/run/tactic25.lean index 39d86f45aa..2d5014dbae 100644 --- a/tests/lean/run/tactic25.lean +++ b/tests/lean/run/tactic25.lean @@ -1,8 +1,8 @@ import logic open tactic -definition my_tac1 := apply @refl -definition my_tac2 := repeat (apply @and_intro; assumption) +definition my_tac1 := apply @eq.refl +definition my_tac2 := repeat (apply @and.intro; assumption) tactic_hint my_tac1 tactic_hint my_tac2 @@ -11,8 +11,8 @@ theorem T1 {A : Type.{2}} (a : A) : a = a theorem T2 {a b c : Prop} (Ha : a) (Hb : b) (Hc : c) : a ∧ b ∧ c -definition my_tac3 := fixpoint (λ f, [apply @or_intro_left; f | - apply @or_intro_right; f | +definition my_tac3 := fixpoint (λ f, [apply @or.intro_left; f | + apply @or.intro_right; f | assumption]) tactic_hint [or] my_tac3 diff --git a/tests/lean/run/tactic26.lean b/tests/lean/run/tactic26.lean index 70c72c4b03..4d98a5c5a8 100644 --- a/tests/lean/run/tactic26.lean +++ b/tests/lean/run/tactic26.lean @@ -7,18 +7,18 @@ inl : A → sum A B, inr : B → sum A B theorem inl_inhabited {A : Type} (B : Type) (H : inhabited A) : inhabited (sum A B) -:= inhabited_destruct H (λ a, inhabited_mk (inl B a)) +:= inhabited.destruct H (λ a, inhabited.mk (sum.inl B a)) theorem inr_inhabited (A : Type) {B : Type} (H : inhabited B) : inhabited (sum A B) -:= inhabited_destruct H (λ b, inhabited_mk (inr A b)) +:= inhabited.destruct H (λ b, inhabited.mk (sum.inr A b)) definition my_tac := fixpoint (λ t, [ apply @inl_inhabited; t | apply @inr_inhabited; t - | apply @num.num_inhabited + | apply @num_inhabited ]) tactic_hint [inhabited] my_tac -theorem T : inhabited (sum false num.num) +theorem T : inhabited (sum false num) end foo diff --git a/tests/lean/run/tactic27.lean b/tests/lean/run/tactic27.lean index 64a635017c..560471864d 100644 --- a/tests/lean/run/tactic27.lean +++ b/tests/lean/run/tactic27.lean @@ -1,8 +1,8 @@ import logic open tactic -definition my_tac := repeat ([ apply @and_intro - | apply @refl +definition my_tac := repeat ([ apply @and.intro + | apply @eq.refl ]) tactic_hint my_tac diff --git a/tests/lean/run/tactic28.lean b/tests/lean/run/tactic28.lean index ebc5df4a8e..7fb0139939 100644 --- a/tests/lean/run/tactic28.lean +++ b/tests/lean/run/tactic28.lean @@ -7,21 +7,21 @@ inl : A → sum A B, inr : B → sum A B theorem inl_inhabited {A : Type} (B : Type) (H : inhabited A) : inhabited (sum A B) -:= inhabited_destruct H (λ a, inhabited_mk (inl B a)) +:= inhabited.destruct H (λ a, inhabited.mk (sum.inl B a)) theorem inr_inhabited (A : Type) {B : Type} (H : inhabited B) : inhabited (sum A B) -:= inhabited_destruct H (λ b, inhabited_mk (inr A b)) +:= inhabited.destruct H (λ b, inhabited.mk (sum.inr A b)) infixl `..`:100 := append definition my_tac := repeat (trace "iteration"; state; ( apply @inl_inhabited; trace "used inl" .. apply @inr_inhabited; trace "used inr" - .. apply @num.num_inhabited; trace "used num")) ; now + .. apply @num_inhabited; trace "used num")) ; now tactic_hint [inhabited] my_tac -theorem T : inhabited (sum false num.num) +theorem T : inhabited (sum false num) end foo diff --git a/tests/lean/run/tactic29.lean b/tests/lean/run/tactic29.lean index 7c54d48799..213318a619 100644 --- a/tests/lean/run/tactic29.lean +++ b/tests/lean/run/tactic29.lean @@ -12,7 +12,7 @@ section check H check H2 theorem test : a = b ∧ a = a - := by apply and_intro; apply H; apply refl + := by apply and.intro; apply H; apply eq.refl end check @test diff --git a/tests/lean/run/tactic30.lean b/tests/lean/run/tactic30.lean index 77e93a9ee3..2f78b7351d 100644 --- a/tests/lean/run/tactic30.lean +++ b/tests/lean/run/tactic30.lean @@ -8,7 +8,7 @@ section parameters {a b : A} parameter H : a = b theorem test : a = b ∧ a = a - := including H, by apply and_intro; assumption; apply refl + := including H, by apply and.intro; assumption; apply eq.refl end check @test diff --git a/tests/lean/run/tactic7.lean b/tests/lean/run/tactic7.lean index b9a378a819..da314e6521 100644 --- a/tests/lean/run/tactic7.lean +++ b/tests/lean/run/tactic7.lean @@ -2,10 +2,10 @@ import logic open tactic theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A -:= by apply and_intro; state; assumption; apply and_intro; !assumption +:= by apply and.intro; state; assumption; apply and.intro; !assumption check tst theorem tst2 {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A -:= by !([apply @and_intro | assumption] ; trace "STEP"; state; trace "----------") +:= by !([apply @and.intro | assumption] ; trace "STEP"; state; trace "----------") check tst2 diff --git a/tests/lean/run/tactic8.lean b/tests/lean/run/tactic8.lean index 8a6d143791..1150e2a542 100644 --- a/tests/lean/run/tactic8.lean +++ b/tests/lean/run/tactic8.lean @@ -2,8 +2,8 @@ import logic open tactic theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A -:= by (apply @and_intro; +:= by (apply @and.intro; apply (show A, from H1); - apply (show B ∧ A, from and_intro H2 H1)) + apply (show B ∧ A, from and.intro H2 H1)) check @tst diff --git a/tests/lean/run/tactic9.lean b/tests/lean/run/tactic9.lean index f9d0c2fc29..ce73ab2f34 100644 --- a/tests/lean/run/tactic9.lean +++ b/tests/lean/run/tactic9.lean @@ -2,4 +2,4 @@ import logic open tactic theorem tst {A B : Prop} (H1 : A) (H2 : B) : ((fun x : Prop, x) A) ∧ B ∧ A -:= by apply and_intro; beta; assumption; apply and_intro; !assumption +:= by apply and.intro; beta; assumption; apply and.intro; !assumption diff --git a/tests/lean/run/trans.lean b/tests/lean/run/trans.lean index 768dedf130..86dd0b2014 100644 --- a/tests/lean/run/trans.lean +++ b/tests/lean/run/trans.lean @@ -3,6 +3,8 @@ -- Author: Leonardo de Moura import logic +abbreviation refl := @eq.refl + definition transport {A : Type} {a b : A} {P : A → Type} (p : a = b) (H : P a) : P b := eq.rec H p diff --git a/tests/lean/run/trick.lean b/tests/lean/run/trick.lean index aaa7cc379d..9588d1987d 100644 --- a/tests/lean/run/trick.lean +++ b/tests/lean/run/trick.lean @@ -1,11 +1,10 @@ import logic -open num definition proj1 (x : num) (y : num) := x definition One := 1 (* -local num = Const({"num", "num"}) +local num = Const("num") local m = mk_metavar("m", num) local proj1 = Const("proj1") local zero = Const({"num", "zero"}) diff --git a/tests/lean/run/univ_bug1.lean b/tests/lean/run/univ_bug1.lean index 736c5facdc..6ba5fd71da 100644 --- a/tests/lean/run/univ_bug1.lean +++ b/tests/lean/run/univ_bug1.lean @@ -23,6 +23,6 @@ simplifies_to.rec (λx, x) C theorem simp_app [instance] (S T : Type) (f1 f2 : S → T) (s1 s2 : S) (C1 : simplifies_to f1 f2) (C2 : simplifies_to s1 s2) : simplifies_to (f1 s1) (f2 s2) := -mk (congr (get_eq C1) (get_eq C2)) +simplifies_to.mk (congr (get_eq C1) (get_eq C2)) end simp diff --git a/tests/lean/run/univ_bug2.lean b/tests/lean/run/univ_bug2.lean index 51f9b06294..5c58b2ee59 100644 --- a/tests/lean/run/univ_bug2.lean +++ b/tests/lean/run/univ_bug2.lean @@ -7,11 +7,12 @@ import logic data.nat open nat -namespace simp -- first define a class of homogeneous equality inductive simplifies_to {T : Type} (t1 t2 : T) : Prop := mk : t1 = t2 → simplifies_to t1 t2 +namespace simplifies_to + theorem get_eq {T : Type} {t1 t2 : T} (C : simplifies_to t1 t2) : t1 = t2 := simplifies_to.rec (λx, x) C @@ -28,4 +29,4 @@ have Rs [fact] : simplifies_to f1 f2, from mk Hf, have Cs [fact] : simplifies_to s1 s2, from mk Hs, infer_eq _ _ -end simp +end simplifies_to diff --git a/tests/lean/run/uuu.lean b/tests/lean/run/uuu.lean index a9dba1d69c..8b8a099369 100644 --- a/tests/lean/run/uuu.lean +++ b/tests/lean/run/uuu.lean @@ -5,25 +5,28 @@ notation `take` binders `,` r:(scoped f, f) := r inductive empty : Type inductive unit : Type := tt : unit +abbreviation tt := @unit.tt inductive nat : Type := O : nat, S : nat → nat inductive paths {A : Type} (a : A) : A → Type := idpath : paths a a +abbreviation idpath := @paths.idpath inductive sum (A : Type) (B : Type) : Type := inl : A -> sum A B, inr : B -> sum A B definition coprod := sum -definition ii1fun {A : Type} (B : Type) (a : A) := inl B a -definition ii2fun (A : Type) {B : Type} (b : B) := inr A b -definition ii1 {A : Type} {B : Type} (a : A) := inl B a -definition ii2 {A : Type} {B : Type} (b : B) := inl A b +definition ii1fun {A : Type} (B : Type) (a : A) := sum.inl B a +definition ii2fun (A : Type) {B : Type} (b : B) := sum.inr A b +definition ii1 {A : Type} {B : Type} (a : A) := sum.inl B a +definition ii2 {A : Type} {B : Type} (b : B) := sum.inl A b inductive total2 {T: Type} (P: T → Type) : Type := tpair : Π (t : T) (tp : P t), total2 P +abbreviation tpair := @total2.tpair definition pr1 {T : Type} {P : T → Type} (tp : total2 P) : T := total2.rec (λ a b, a) tp diff --git a/tests/lean/slow/list_elab2.lean b/tests/lean/slow/list_elab2.lean index aa5817c4a5..2be0119311 100644 --- a/tests/lean/slow/list_elab2.lean +++ b/tests/lean/slow/list_elab2.lean @@ -16,15 +16,17 @@ open nat -- open congr open eq_ops +inductive list (T : Type) : Type := +nil {} : list T, +cons : T → list T → list T + +abbreviation refl := @eq.refl + namespace list -- Type -- ---- -inductive list (T : Type) : Type := -nil {} : list T, -cons : T → list T → list T - infix `::` : 65 := cons section diff --git a/tests/lean/slow/nat_bug1.lean b/tests/lean/slow/nat_bug1.lean index c2c1ea9b3c..0b09113515 100644 --- a/tests/lean/slow/nat_bug1.lean +++ b/tests/lean/slow/nat_bug1.lean @@ -4,7 +4,7 @@ -- Author: Floris van Doorn ---------------------------------------------------------------------------------------------------- import logic -open tactic num +open tactic inductive nat : Type := zero : nat, @@ -12,12 +12,14 @@ succ : nat → nat notation `ℕ`:max := nat +namespace nat abbreviation plus (x y : ℕ) : ℕ := nat.rec x (λ n r, succ r) y definition to_nat [coercion] [inline] (n : num) : ℕ -:= num.num.rec zero (λ n, num.pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n +:= num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n print "==================" theorem nat_rec_zero {P : ℕ → Type} (x : P 0) (f : ∀m, P m → P (succ m)) : nat.rec x f 0 = x := -refl _ +eq.refl _ +end nat diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean index 140a8d2dd9..4cf8de44e2 100644 --- a/tests/lean/slow/nat_bug2.lean +++ b/tests/lean/slow/nat_bug2.lean @@ -4,21 +4,27 @@ -- Author: Floris van Doorn ---------------------------------------------------------------------------------------------------- import logic struc.binary -open tactic num binary eq_ops +open tactic binary eq_ops open decidable -namespace nat +abbreviation refl := @eq.refl +abbreviation and_intro := @and.intro +abbreviation or_intro_left := @or.intro_left +abbreviation or_intro_right := @or.intro_right + inductive nat : Type := zero : nat, succ : nat → nat +namespace nat + notation `ℕ`:max := nat abbreviation plus (x y : ℕ) : ℕ := nat.rec x (λ n r, succ r) y definition to_nat [coercion] [inline] (n : num) : ℕ -:= num.num.rec zero (λ n, num.pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n +:= num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n namespace helper_tactics definition apply_refl := apply @refl @@ -55,8 +61,8 @@ theorem pred_succ (n : ℕ) : pred (succ n) = n theorem zero_or_succ (n : ℕ) : n = 0 ∨ n = succ (pred n) := induction_on n - (or_intro_left _ (refl 0)) - (take m IH, or_intro_right _ + (or.intro_left _ (refl 0)) + (take m IH, or.intro_right _ (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 diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean index 15c68dd90f..53649a0e46 100644 --- a/tests/lean/slow/nat_wo_hints.lean +++ b/tests/lean/slow/nat_wo_hints.lean @@ -4,24 +4,25 @@ -- Author: Floris van Doorn ---------------------------------------------------------------------------------------------------- import logic struc.binary -open tactic num binary eq_ops +open tactic binary eq_ops open decidable -namespace nat inductive nat : Type := zero : nat, succ : nat → nat + +namespace nat notation `ℕ`:max := nat abbreviation plus (x y : ℕ) : ℕ := nat.rec x (λ n r, succ r) y definition to_nat [coercion] [inline] (n : num) : ℕ -:= num.num.rec zero (λ n, num.pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n +:= num.rec zero (λ n, pos_num.rec (succ zero) (λ n r, plus r (plus r (succ zero))) (λ n r, plus r r) n) n namespace helper_tactics - definition apply_refl := apply @refl + definition apply_refl := apply @eq.refl tactic_hint apply_refl end helper_tactics open helper_tactics @@ -55,8 +56,8 @@ theorem pred_succ (n : ℕ) : pred (succ n) = n theorem zero_or_succ (n : ℕ) : n = 0 ∨ n = succ (pred n) := induction_on n - (or_intro_left _ (refl 0)) - (take m IH, or_intro_right _ + (or.intro_left _ (eq.refl 0)) + (take m IH, or.intro_right _ (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 @@ -88,7 +89,7 @@ theorem decidable_eq [instance] (n m : ℕ) : decidable (n = m) rec_on m (take n, rec_on n - (inl (refl 0)) + (inl (eq.refl 0)) (λ m iH, inr (succ_ne_zero m))) (λ (m' : ℕ) (iH1 : ∀n, decidable (n = m')), take n, rec_on n @@ -107,11 +108,11 @@ theorem two_step_induction_on {P : ℕ → Prop} (a : ℕ) (H1 : P 0) (H2 : P 1) (H3 : ∀ (n : ℕ) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) : P a := have stronger : P a ∧ P (succ a), from induction_on a - (and_intro H1 H2) + (and.intro H1 H2) (take k IH, have IH1 : P k, from and_elim_left IH, have IH2 : P (succ k), from and_elim_right IH, - and_intro IH2 (H3 k IH1 IH2)), + and.intro IH2 (H3 k IH1 IH2)), and_elim_left stronger theorem sub_induction {P : ℕ → ℕ → Prop} (n m : ℕ) (H1 : ∀m, P 0 m) @@ -225,7 +226,7 @@ theorem add_cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k theorem add_eq_zero_left {n m : ℕ} : n + m = 0 → n = 0 := induction_on n - (take (H : 0 + m = 0), refl 0) + (take (H : 0 + m = 0), eq.refl 0) (take k IH, assume (H : succ k + m = 0), absurd @@ -239,7 +240,7 @@ theorem add_eq_zero_right {n m : ℕ} (H : n + m = 0) : m = 0 := add_eq_zero_left (trans (add_comm m n) H) theorem add_eq_zero {n m : ℕ} (H : n + m = 0) : n = 0 ∧ m = 0 -:= and_intro (add_eq_zero_left H) (add_eq_zero_right H) +:= and.intro (add_eq_zero_left H) (add_eq_zero_right H) -- add_eq_self below @@ -310,8 +311,8 @@ theorem mul_add_distr_left (n m k : ℕ) : (n + m) * k = n * k + m * k (calc (n + m) * 0 = 0 : mul_zero_right _ ... = 0 + 0 : symm (add_zero_right _) - ... = n * 0 + 0 : refl _ - ... = n * 0 + m * 0 : refl _) + ... = n * 0 + 0 : eq.refl _ + ... = n * 0 + m * 0 : eq.refl _) (take l IH, calc (n + m) * succ l = (n + m) * l + (n + m) : mul_succ_right _ _ ... = n * l + m * l + (n + m) : {IH} @@ -363,11 +364,11 @@ theorem mul_one_left (n : ℕ) : 1 * n = n theorem mul_eq_zero {n m : ℕ} (H : n * m = 0) : n = 0 ∨ m = 0 := discriminate - (take Hn : n = 0, or_intro_left _ Hn) + (take Hn : n = 0, or.intro_left _ Hn) (take (k : ℕ), assume (Hk : n = succ k), discriminate - (take (Hm : m = 0), or_intro_right _ Hm) + (take (Hm : m = 0), or.intro_right _ Hm) (take (l : ℕ), assume (Hl : m = succ l), have Heq : succ (k * succ l + l) = n * m, from @@ -394,7 +395,7 @@ theorem le_elim {n m : ℕ} (H : n ≤ m) : ∃ k, n + k = m ---------- partial order (totality is part of lt) theorem le_intro2 (n m : ℕ) : n ≤ n + m -:= le_intro (refl (n + m)) +:= le_intro (eq.refl (n + m)) theorem le_refl (n : ℕ) : n ≤ n := le_intro (add_zero_right n) @@ -490,7 +491,7 @@ theorem succ_le_left_or {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m n = n + 0 : (add_zero_right n)⁻¹ ... = n + k : {H3⁻¹} ... = m : Hk, - or_intro_right _ Heq) + or.intro_right _ Heq) (take l:ℕ, assume H3 : k = succ l, have Hlt : succ n ≤ m, from @@ -499,7 +500,7 @@ theorem succ_le_left_or {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m succ n + l = n + succ l : add_move_succ n l ... = n + k : {H3⁻¹} ... = m : Hk)), - or_intro_left _ Hlt) + or.intro_left _ Hlt) theorem succ_le_left {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m := resolve_left (succ_le_left_or H1) H2 @@ -511,7 +512,7 @@ theorem succ_le_right_inv {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ theorem succ_le_left_inv {n m : ℕ} (H : succ n ≤ m) : n ≤ m ∧ n ≠ m := obtain (k : ℕ) (H2 : succ n + k = m), from (le_elim H), - and_intro + and.intro (have H3 : n + succ k = m, from calc n + succ k = succ n + k : symm (add_move_succ n k) @@ -551,7 +552,7 @@ theorem pred_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m theorem pred_le_left_inv {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = succ m := discriminate (take Hn : n = 0, - or_intro_left _ (subst (symm Hn) (zero_le m))) + or.intro_left _ (subst (symm Hn) (zero_le m))) (take k : ℕ, assume Hn : n = succ k, have H2 : pred n = k, @@ -577,7 +578,7 @@ theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m n = n + 0 : symm (add_zero_right n) ... = n + k : {symm H3} ... = m : Hk, - or_intro_right _ Heq) + or.intro_right _ Heq) (take l : nat, assume H3 : k = succ l, have Hlt : succ n ≤ m, from @@ -586,7 +587,7 @@ theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m succ n + l = n + succ l : add_move_succ n l ... = n + k : {symm H3} ... = m : Hk)), - or_intro_left _ Hlt) + or.intro_left _ Hlt) theorem le_ne_imp_succ_le {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m := resolve_left (le_imp_succ_le_or_eq H1) H2 @@ -597,7 +598,7 @@ theorem le_succ_imp_le_or_eq {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = su theorem succ_le_imp_le_and_ne {n m : ℕ} (H : succ n ≤ m) : n ≤ m ∧ n ≠ m := - and_intro + and.intro (le_trans (self_le_succ n) H) (assume H2 : n = m, have H3 : succ n ≤ n, from subst (symm H2) H, @@ -614,7 +615,7 @@ theorem pred_le_imp_le_or_eq {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = su := discriminate (take Hn : n = 0, - or_intro_left _ (subst (symm Hn) (zero_le m))) + or.intro_left _ (subst (symm Hn) (zero_le m))) (take k : nat, assume Hn : n = succ k, have H2 : pred n = k, @@ -682,7 +683,7 @@ theorem lt_ne {n m : ℕ} (H : n < m) : n ≠ m := and_elim_right (succ_le_left_inv H) theorem lt_irrefl (n : ℕ) : ¬ n < n -:= assume H : n < n, absurd (refl n) (lt_ne H) +:= assume H : n < n, absurd (eq.refl n) (lt_ne H) theorem lt_zero (n : ℕ) : 0 < succ n := succ_le (zero_le n) @@ -784,7 +785,7 @@ theorem succ_lt_right {n m : ℕ} (H : n < m) : n < succ m theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n := induction_on n - (or_intro_left _ (zero_le m)) + (or.intro_left _ (zero_le m)) (take (k : ℕ), assume IH : k ≤ m ∨ m < k, or_elim IH @@ -798,7 +799,7 @@ theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n ... = k + 0 : {H2} ... = k : add_zero_right k, have H4 : m < succ k, from subst H3 (lt_self_succ m), - or_intro_right _ H4) + or.intro_right _ H4) (take l2 : ℕ, assume H2 : l = succ l2, have H3 : succ k + l2 = m, @@ -806,8 +807,8 @@ theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n succ k + l2 = k + succ l2 : add_move_succ k l2 ... = k + l : {symm H2} ... = m : Hl, - or_intro_left _ (le_intro H3))) - (assume H : m < k, or_intro_right _ (succ_lt_right H))) + or.intro_left _ (le_intro H3))) + (assume H : m < k, or.intro_right _ (succ_lt_right H))) theorem trichotomy_alt (n m : ℕ) : (n < m ∨ n = m) ∨ m < n := or_imp_or (le_or_lt n m) (assume H : n ≤ m, le_imp_lt_or_eq H) (assume H : m < n, H) @@ -866,7 +867,7 @@ theorem add_eq_self {n m : ℕ} (H : n + m = n) : m = 0 ... = n : H, have H3 : n < n, from lt_intro H2, have H4 : n ≠ n, from lt_ne H3, - absurd (refl n) H4) + absurd (eq.refl n) H4) -------------------------------------------------- positivity @@ -1067,7 +1068,7 @@ theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 := mul_eq_one_left (subst (mul_comm n m) H) theorem mul_eq_one {n m : ℕ} (H : n * m = 1) : n = 1 ∧ m = 1 -:= and_intro (mul_eq_one_left H) (mul_eq_one_right H) +:= and.intro (mul_eq_one_left H) (mul_eq_one_right H) -------------------------------------------------- sub @@ -1380,7 +1381,7 @@ theorem dist_eq_zero {n m : ℕ} (H : dist n m = 0) : n = m theorem dist_le {n m : ℕ} (H : n ≤ m) : dist n m = m - n := calc - dist n m = (n - m) + (m - n) : refl _ + dist n m = (n - m) + (m - n) : eq.refl _ ... = 0 + (m - n) : {le_imp_sub_eq_zero H} ... = m - n : add_zero_left (m - n) @@ -1401,7 +1402,7 @@ theorem dist_intro {n m k : ℕ} (H : n + m = k) : dist k n = m theorem dist_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)) : refl _ + dist (n + k) (m + k) = ((n+k) - (m+k)) + ((m+k)-(n+k)) : eq.refl _ ... = (n - m) + ((m + k) - (n + k)) : {sub_add_add_right _ _ _} ... = (n - m) + (m - n) : {sub_add_add_right _ _ _} diff --git a/tests/lean/slow/path_groupoids.lean b/tests/lean/slow/path_groupoids.lean index dd7c825542..e0a3e72720 100644 --- a/tests/lean/slow/path_groupoids.lean +++ b/tests/lean/slow/path_groupoids.lean @@ -15,7 +15,7 @@ infixl `∘`:60 := compose inductive path {A : Type} (a : A) : A → Type := idpath : path a a - +abbreviation idpath := @path.idpath infix `≈`:50 := path -- TODO: is this right? notation x `≈` y:50 `:>`:0 A:0 := @path A x y