diff --git a/doc/lean/calc.md b/doc/lean/calc.md index a73240c637..0937f7c664 100644 --- a/doc/lean/calc.md +++ b/doc/lean/calc.md @@ -35,7 +35,7 @@ Here is an example := calc a = b : Ax1 ... = c + 1 : Ax2 ... = d + 1 : { Ax3 } - ... = 1 + d : Nat::add::comm d 1 + ... = 1 + d : Nat::add_comm d 1 ... = e : symm Ax4. ``` @@ -45,7 +45,7 @@ proof expression using the given tactic or solver. Even when tactics and solvers are not used, we can still use the elaboration engine to fill gaps in our calculational proofs. In the previous examples, we can use `_` as arguments for the -`Nat::add::comm` theorem. The Lean elaboration engine will infer `d` and `1` for us. +`Nat::add_comm` theorem. The Lean elaboration engine will infer `d` and `1` for us. Here is the same example using placeholders. ```lean @@ -53,7 +53,7 @@ Here is the same example using placeholders. := calc a = b : Ax1 ... = c + 1 : Ax2 ... = d + 1 : { Ax3 } - ... = 1 + d : Nat::add::comm _ _ + ... = 1 + d : Nat::add_comm _ _ ... = e : symm Ax4. ``` @@ -64,7 +64,7 @@ Here is an example. theorem T2 (a b c : Nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0 := calc a = b : H1 ... = c + 1 : H2 - ... ≠ 0 : Nat::succ::nz _. + ... ≠ 0 : Nat::succ_nz _. ``` The Lean `let` construct can also be used to build calculational-like proofs. diff --git a/doc/lean/expr.md b/doc/lean/expr.md index 95752bb4d2..16f508b891 100644 --- a/doc/lean/expr.md +++ b/doc/lean/expr.md @@ -88,16 +88,16 @@ infix 50 = : eq ``` The curly braces indicate that the first argument of `eq` is implicit. The symbol `=` is just a syntax sugar for `eq`. -In the following example, we use the `set::option` command to force Lean to display implicit arguments and +In the following example, we use the `set_option` command to force Lean to display implicit arguments and disable notation when pretty printing expressions. ```lean -set::option pp::implicit true -set::option pp::notation false +set_option pp::implicit true +set_option pp::notation false check 1 = 2 -- restore default configuration -set::option pp::implicit false -set::option pp::notation true +set_option pp::implicit false +set_option pp::notation true check 1 = 2 ``` diff --git a/doc/lean/tutorial.md b/doc/lean/tutorial.md index 01650e44ba..c59371c183 100644 --- a/doc/lean/tutorial.md +++ b/doc/lean/tutorial.md @@ -76,7 +76,7 @@ In the following example we prove that `double x = 2 * x` ```lean theorem double_x_eq_2x (x : Nat) : double x = 2 * x := calc double x = x + x : refl (double x) - ... = 1*x + 1*x : { symm (mul::onel x) } + ... = 1*x + 1*x : { symm (mul_onel x) } ... = (1 + 1)*x : symm (distributel 1 1 x) ... = 2 * x : { refl (1 + 1) } ``` @@ -84,7 +84,7 @@ In the following example we prove that `double x = 2 * x` In the example above, we provided the proof manually using a calculational proof style. The terms after `:` are proof terms. They justify the equalities in the left-hand-side. The proof term `refl (double x)` produces a proof for `t = s` where `t` and `s` have the same -normal form of `(double x)`. The proof term `{ symm (mul::onel x) }` is a justification for +normal form of `(double x)`. The proof term `{ symm (mul_onel x) }` is a justification for the equality `x = 1*x`. The curly braces instruct Lean to replace `x` with `1*x`. Similarly `{ symm (distributel 1 1 x) }` is a proof for `1*x + 1*x = (1 + 1)*x`. The exact semantics of these expressions is not important at this point. diff --git a/emacs/lean.el b/emacs/lean.el index 5e8d1505b7..167323817c 100644 --- a/emacs/lean.el +++ b/emacs/lean.el @@ -23,7 +23,7 @@ (define-generic-mode 'lean-mode ;; name of the mode to create '("--") ;; comments start with - '("import" "definition" "variable" "variables" "print" "axiom" "theorem" "universe" "alias" "help" "set::option" "set::opaque" "environment" "options" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "scope" "pop::scope") ;; some keywords + '("import" "definition" "variable" "variables" "print" "axiom" "theorem" "universe" "alias" "help" "set_option" "set_opaque" "environment" "options" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "scope" "pop_scope") ;; some keywords '(("\\<\\(Bool\\|Int\\|Nat\\|Real\\|Type\\|TypeU\\|ℕ\\|ℤ\\)\\>" . 'font-lock-type-face) ("\\<\\(calc\\|have\\|in\\|let\\)\\>" . font-lock-keyword-face) ("\"[^\"]*\"" . 'font-lock-string-face) diff --git a/examples/lean/even.lean b/examples/lean/even.lean index 278d20e01d..a6134a68aa 100644 --- a/examples/lean/even.lean +++ b/examples/lean/even.lean @@ -14,7 +14,7 @@ definition odd (a : Nat) := ∃ b, a = 2*b + 1 -- It is syntax sugar for existential elimination. -- It expands to -- --- exists::elim [expr]_1 (fun [binding], [expr]_2) +-- exists_elim [expr]_1 (fun [binding], [expr]_2) -- -- It is defined in the file macros.lua. -- @@ -32,12 +32,12 @@ definition odd (a : Nat) := ∃ b, a = 2*b + 1 theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b) := obtain (w1 : Nat) (Hw1 : a = 2*w1), from H1, obtain (w2 : Nat) (Hw2 : b = 2*w2), from H2, - exists::intro (w1 + w2) + exists_intro (w1 + w2) (calc a + b = 2*w1 + b : { Hw1 } ... = 2*w1 + 2*w2 : { Hw2 } ... = 2*(w1 + w2) : symm (distributer 2 w1 w2)) --- In the following example, we omit the arguments for add::assoc, refl and distribute. +-- In the following example, we omit the arguments for add_assoc, refl and distribute. -- Lean can infer them automatically. -- -- refl is the reflexivity proof. (refl a) is a proof that two @@ -52,9 +52,9 @@ theorem EvenPlusEven {a b : Nat} (H1 : even a) (H2 : even b) : even (a + b) -- any theorems such as + associativity. theorem OddPlusOne {a : Nat} (H : odd a) : even (a + 1) := obtain (w : Nat) (Hw : a = 2*w + 1), from H, - exists::intro (w + 1) + exists_intro (w + 1) (calc a + 1 = 2*w + 1 + 1 : { Hw } - ... = 2*w + (1 + 1) : symm (add::assoc _ _ _) + ... = 2*w + (1 + 1) : symm (add_assoc _ _ _) ... = 2*w + 2*1 : refl _ ... = 2*(w + 1) : symm (distributer _ _ _)) @@ -64,7 +64,7 @@ print environment 2 -- By default, Lean does not display implicit arguments. -- The following command will force it to display them. -set::option pp::implicit true +set_option pp::implicit true print environment 2 diff --git a/examples/lean/ex1.lean b/examples/lean/ex1.lean index 8d4182bbb4..12395ae50c 100644 --- a/examples/lean/ex1.lean +++ b/examples/lean/ex1.lean @@ -18,9 +18,9 @@ axiom H2 : b = e -- Proof that (h a b) = (h c e) theorem T1 : (h a b) = (h c e) := - or::elim H1 - (λ C1, congrh ((and::eliml C1) ⋈ (and::elimr C1)) H2) - (λ C2, congrh ((and::elimr C2) ⋈ (and::eliml C2)) H2) + or_elim H1 + (λ C1, congrh ((and_eliml C1) ⋈ (and_elimr C1)) H2) + (λ C2, congrh ((and_elimr C2) ⋈ (and_eliml C2)) H2) -- We can use theorem T1 to prove other theorems theorem T2 : (h a (h a b)) = (h a (h c e)) := @@ -30,6 +30,6 @@ theorem T2 : (h a (h a b)) = (h a (h c e)) := print environment 2 -- print implicit arguments -set::option lean::pp::implicit true -set::option pp::width 150 +set_option lean::pp::implicit true +set_option pp::width 150 print environment 2 diff --git a/examples/lean/ex2.lean b/examples/lean/ex2.lean index 1ccbedbe64..91846928f7 100644 --- a/examples/lean/ex2.lean +++ b/examples/lean/ex2.lean @@ -2,11 +2,11 @@ import macros. theorem simple (p q r : Bool) : (p → q) ∧ (q → r) → p → r := λ H_pq_qr H_p, - let P_pq := and::eliml H_pq_qr, - P_qr := and::elimr H_pq_qr + let P_pq := and_eliml H_pq_qr, + P_qr := and_elimr H_pq_qr in P_qr (P_pq H_p) -set::option pp::implicit true. +set_option pp::implicit true. print environment 1. theorem simple2 (a b c : Bool) : (a → b → c) → (a → b) → a → c diff --git a/examples/lean/ex3.lean b/examples/lean/ex3.lean index 01f497f788..665210d4a0 100644 --- a/examples/lean/ex3.lean +++ b/examples/lean/ex3.lean @@ -1,13 +1,13 @@ import macros. -theorem and_comm (a b : Bool) : (a ∧ b) → (b ∧ a) -:= λ H_ab, and::intro (and::elimr H_ab) (and::eliml H_ab). +theorem my_and_comm (a b : Bool) : (a ∧ b) → (b ∧ a) +:= λ H_ab, and_intro (and_elimr H_ab) (and_eliml H_ab). -theorem or_comm (a b : Bool) : (a ∨ b) → (b ∨ a) +theorem my_or_comm (a b : Bool) : (a ∨ b) → (b ∨ a) := λ H_ab, - or::elim H_ab - (λ H_a, or::intror b H_a) - (λ H_b, or::introl H_b a). + or_elim H_ab + (λ H_a, or_intror b H_a) + (λ H_b, or_introl H_b a). -- (em a) is the excluded middle a ∨ ¬a -- (mt H H_na) is Modus Tollens with @@ -16,13 +16,13 @@ theorem or_comm (a b : Bool) : (a ∨ b) → (b ∨ a) -- produces -- ¬(a → b) -- --- not::imp::eliml applied to +-- not_imp_eliml applied to -- (MT H H_na) : ¬(a → b) -- produces -- a theorem pierce (a b : Bool) : ((a → b) → a) → a -:= λ H, or::elim (em a) +:= λ H, or_elim (em a) (λ H_a, H_a) - (λ H_na, not::imp::eliml (mt H H_na)). + (λ H_na, not_imp_eliml (mt H H_na)). print environment 3. \ No newline at end of file diff --git a/examples/lean/ex5.lean b/examples/lean/ex5.lean index ac375d2e05..5d64920426 100644 --- a/examples/lean/ex5.lean +++ b/examples/lean/ex5.lean @@ -12,7 +12,7 @@ scope let L1 : R w x := Symm x w H in Trans x w x H L1 -pop::scope +pop_scope scope -- Same example again. diff --git a/examples/lean/set.lean b/examples/lean/set.lean index 976b27755f..67c2b3a028 100644 --- a/examples/lean/set.lean +++ b/examples/lean/set.lean @@ -8,17 +8,17 @@ infix 60 ∈ : element definition subset {A : Type} (s1 : Set A) (s2 : Set A) := ∀ x, x ∈ s1 → x ∈ s2 infix 50 ⊆ : subset -theorem subset::trans {A : Type} {s1 s2 s3 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3) : s1 ⊆ s3 +theorem subset_trans {A : Type} {s1 s2 s3 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3) : s1 ⊆ s3 := λ (x : A) (Hin : x ∈ s1), have x ∈ s3 : let L1 : x ∈ s2 := H1 x Hin in H2 x L1 -theorem subset::ext {A : Type} {s1 s2 : Set A} (H : ∀ x, x ∈ s1 = x ∈ s2) : s1 = s2 +theorem subset_ext {A : Type} {s1 s2 : Set A} (H : ∀ x, x ∈ s1 = x ∈ s2) : s1 = s2 := funext H -theorem subset::antisym {A : Type} {s1 s2 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1) : s1 = s2 -:= subset::ext (have (∀ x, x ∈ s1 = x ∈ s2) : +theorem subset_antisym {A : Type} {s1 s2 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1) : s1 = s2 +:= subset_ext (have (∀ x, x ∈ s1 = x ∈ s2) : λ x, have x ∈ s1 = x ∈ s2 : boolext (have x ∈ s1 → x ∈ s2 : H1 x) (have x ∈ s2 → x ∈ s1 : H2 x)) diff --git a/examples/lean/tactic_in_lua.lean b/examples/lean/tactic_in_lua.lean index 1658448704..2c758c8784 100644 --- a/examples/lean/tactic_in_lua.lean +++ b/examples/lean/tactic_in_lua.lean @@ -42,7 +42,7 @@ local pb = s:proof_builder() local new_pb = function(m, a) - local Conj = Const({"and", "intro"}) + local Conj = Const("and_intro") local new_m = proof_map(m) -- Copy proof map m for _, p in ipairs(proof_info) do local n = p[1] -- n is the name of the goal splitted by this tactic diff --git a/src/builtin/Int.lean b/src/builtin/Int.lean index b5575081cb..09a4b317fb 100644 --- a/src/builtin/Int.lean +++ b/src/builtin/Int.lean @@ -46,14 +46,14 @@ infix 50 | : divides definition abs (a : Int) : Int := if (0 ≤ a) a (- a) notation 55 | _ | : abs -set::opaque sub true -set::opaque neg true -set::opaque mod true -set::opaque divides true -set::opaque abs true -set::opaque ge true -set::opaque lt true -set::opaque gt true +set_opaque sub true +set_opaque neg true +set_opaque mod true +set_opaque divides true +set_opaque abs true +set_opaque ge true +set_opaque lt true +set_opaque gt true end namespace Nat @@ -63,6 +63,6 @@ infixl 65 - : sub definition neg (a : Nat) : Int := - (nat_to_int a) notation 75 - _ : neg -set::opaque sub true -set::opaque neg true +set_opaque sub true +set_opaque neg true end \ No newline at end of file diff --git a/src/builtin/Nat.lean b/src/builtin/Nat.lean index d3612f71bb..f090586beb 100644 --- a/src/builtin/Nat.lean +++ b/src/builtin/Nat.lean @@ -30,219 +30,219 @@ infix 50 > : gt definition id (a : Nat) := a notation 55 | _ | : id -axiom succ::nz (a : Nat) : a + 1 ≠ 0 -axiom succ::inj {a b : Nat} (H : a + 1 = b + 1) : a = b -axiom add::zeror (a : Nat) : a + 0 = a -axiom add::succr (a b : Nat) : a + (b + 1) = (a + b) + 1 -axiom mul::zeror (a : Nat) : a * 0 = 0 -axiom mul::succr (a b : Nat) : a * (b + 1) = a * b + a -axiom le::def (a b : Nat) : a ≤ b = ∃ c, a + c = b +axiom succ_nz (a : Nat) : a + 1 ≠ 0 +axiom succ_inj {a b : Nat} (H : a + 1 = b + 1) : a = b +axiom add_zeror (a : Nat) : a + 0 = a +axiom add_succr (a b : Nat) : a + (b + 1) = (a + b) + 1 +axiom mul_zeror (a : Nat) : a * 0 = 0 +axiom mul_succr (a b : Nat) : a * (b + 1) = a * b + a +axiom le_def (a b : Nat) : a ≤ b = ∃ c, a + c = b axiom induction {P : Nat → Bool} (a : Nat) (H1 : P 0) (H2 : ∀ (n : Nat) (iH : P n), P (n + 1)) : P a -theorem pred::nz {a : Nat} : a ≠ 0 → ∃ b, b + 1 = a +theorem pred_nz {a : Nat} : a ≠ 0 → ∃ b, b + 1 = a := induction a - (λ H : 0 ≠ 0, false::elim (∃ b, b + 1 = 0) H) + (λ H : 0 ≠ 0, false_elim (∃ b, b + 1 = 0) H) (λ (n : Nat) (iH : n ≠ 0 → ∃ b, b + 1 = n) (H : n + 1 ≠ 0), - or::elim (em (n = 0)) - (λ Heq0 : n = 0, exists::intro 0 (calc 0 + 1 = n + 1 : { symm Heq0 })) + or_elim (em (n = 0)) + (λ Heq0 : n = 0, exists_intro 0 (calc 0 + 1 = n + 1 : { symm Heq0 })) (λ Hne0 : n ≠ 0, obtain (w : Nat) (Hw : w + 1 = n), from (iH Hne0), - exists::intro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw }))) + exists_intro (w + 1) (calc w + 1 + 1 = n + 1 : { Hw }))) theorem discriminate {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : ∀ n, a = n + 1 → B) : B -:= or::elim (em (a = 0)) +:= or_elim (em (a = 0)) (λ Heq0 : a = 0, H1 Heq0) - (λ Hne0 : a ≠ 0, obtain (w : Nat) (Hw : w + 1 = a), from (pred::nz Hne0), + (λ Hne0 : a ≠ 0, obtain (w : Nat) (Hw : w + 1 = a), from (pred_nz Hne0), H2 w (symm Hw)) -theorem add::zerol (a : Nat) : 0 + a = a +theorem add_zerol (a : Nat) : 0 + a = a := induction a (have 0 + 0 = 0 : trivial) (λ (n : Nat) (iH : 0 + n = n), - calc 0 + (n + 1) = (0 + n) + 1 : add::succr 0 n + calc 0 + (n + 1) = (0 + n) + 1 : add_succr 0 n ... = n + 1 : { iH }) -theorem add::succl (a b : Nat) : (a + 1) + b = (a + b) + 1 +theorem add_succl (a b : Nat) : (a + 1) + b = (a + b) + 1 := induction b - (calc (a + 1) + 0 = a + 1 : add::zeror (a + 1) - ... = (a + 0) + 1 : { symm (add::zeror a) }) + (calc (a + 1) + 0 = a + 1 : add_zeror (a + 1) + ... = (a + 0) + 1 : { symm (add_zeror a) }) (λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1), - calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : add::succr (a + 1) n + calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : add_succr (a + 1) n ... = ((a + n) + 1) + 1 : { iH } - ... = (a + (n + 1)) + 1 : { have (a + n) + 1 = a + (n + 1) : symm (add::succr a n) }) + ... = (a + (n + 1)) + 1 : { have (a + n) + 1 = a + (n + 1) : symm (add_succr a n) }) -theorem add::comm (a b : Nat) : a + b = b + a +theorem add_comm (a b : Nat) : a + b = b + a := induction b - (calc a + 0 = a : add::zeror a - ... = 0 + a : symm (add::zerol a)) + (calc a + 0 = a : add_zeror a + ... = 0 + a : symm (add_zerol a)) (λ (n : Nat) (iH : a + n = n + a), - calc a + (n + 1) = (a + n) + 1 : add::succr a n + calc a + (n + 1) = (a + n) + 1 : add_succr a n ... = (n + a) + 1 : { iH } - ... = (n + 1) + a : symm (add::succl n a)) + ... = (n + 1) + a : symm (add_succl n a)) -theorem add::assoc (a b c : Nat) : a + (b + c) = (a + b) + c +theorem add_assoc (a b c : Nat) : a + (b + c) = (a + b) + c := induction a - (calc 0 + (b + c) = b + c : add::zerol (b + c) - ... = (0 + b) + c : { symm (add::zerol b) }) + (calc 0 + (b + c) = b + c : add_zerol (b + c) + ... = (0 + b) + c : { symm (add_zerol b) }) (λ (n : Nat) (iH : n + (b + c) = (n + b) + c), - calc (n + 1) + (b + c) = (n + (b + c)) + 1 : add::succl n (b + c) + calc (n + 1) + (b + c) = (n + (b + c)) + 1 : add_succl n (b + c) ... = ((n + b) + c) + 1 : { iH } - ... = ((n + b) + 1) + c : symm (add::succl (n + b) c) - ... = ((n + 1) + b) + c : { have (n + b) + 1 = (n + 1) + b : symm (add::succl n b) }) + ... = ((n + b) + 1) + c : symm (add_succl (n + b) c) + ... = ((n + 1) + b) + c : { have (n + b) + 1 = (n + 1) + b : symm (add_succl n b) }) -theorem mul::zerol (a : Nat) : 0 * a = 0 +theorem mul_zerol (a : Nat) : 0 * a = 0 := induction a (have 0 * 0 = 0 : trivial) (λ (n : Nat) (iH : 0 * n = 0), - calc 0 * (n + 1) = (0 * n) + 0 : mul::succr 0 n + calc 0 * (n + 1) = (0 * n) + 0 : mul_succr 0 n ... = 0 + 0 : { iH } ... = 0 : trivial) -theorem mul::succl (a b : Nat) : (a + 1) * b = a * b + b +theorem mul_succl (a b : Nat) : (a + 1) * b = a * b + b := induction b - (calc (a + 1) * 0 = 0 : mul::zeror (a + 1) - ... = a * 0 : symm (mul::zeror a) - ... = a * 0 + 0 : symm (add::zeror (a * 0))) + (calc (a + 1) * 0 = 0 : mul_zeror (a + 1) + ... = a * 0 : symm (mul_zeror a) + ... = a * 0 + 0 : symm (add_zeror (a * 0))) (λ (n : Nat) (iH : (a + 1) * n = a * n + n), - calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : mul::succr (a + 1) n + calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : mul_succr (a + 1) n ... = a * n + n + (a + 1) : { iH } - ... = a * n + n + a + 1 : add::assoc (a * n + n) a 1 - ... = a * n + (n + a) + 1 : { have a * n + n + a = a * n + (n + a) : symm (add::assoc (a * n) n a) } - ... = a * n + (a + n) + 1 : { add::comm n a } - ... = a * n + a + n + 1 : { add::assoc (a * n) a n } - ... = a * (n + 1) + n + 1 : { symm (mul::succr a n) } - ... = a * (n + 1) + (n + 1) : symm (add::assoc (a * (n + 1)) n 1)) + ... = a * n + n + a + 1 : add_assoc (a * n + n) a 1 + ... = a * n + (n + a) + 1 : { have a * n + n + a = a * n + (n + a) : symm (add_assoc (a * n) n a) } + ... = a * n + (a + n) + 1 : { add_comm n a } + ... = a * n + a + n + 1 : { add_assoc (a * n) a n } + ... = a * (n + 1) + n + 1 : { symm (mul_succr a n) } + ... = a * (n + 1) + (n + 1) : symm (add_assoc (a * (n + 1)) n 1)) -theorem mul::onel (a : Nat) : 1 * a = a +theorem mul_onel (a : Nat) : 1 * a = a := induction a (have 1 * 0 = 0 : trivial) (λ (n : Nat) (iH : 1 * n = n), - calc 1 * (n + 1) = 1 * n + 1 : mul::succr 1 n + calc 1 * (n + 1) = 1 * n + 1 : mul_succr 1 n ... = n + 1 : { iH }) -theorem mul::oner (a : Nat) : a * 1 = a +theorem mul_oner (a : Nat) : a * 1 = a := induction a (have 0 * 1 = 0 : trivial) (λ (n : Nat) (iH : n * 1 = n), - calc (n + 1) * 1 = n * 1 + 1 : mul::succl n 1 + calc (n + 1) * 1 = n * 1 + 1 : mul_succl n 1 ... = n + 1 : { iH }) -theorem mul::comm (a b : Nat) : a * b = b * a +theorem mul_comm (a b : Nat) : a * b = b * a := induction b - (calc a * 0 = 0 : mul::zeror a - ... = 0 * a : symm (mul::zerol a)) + (calc a * 0 = 0 : mul_zeror a + ... = 0 * a : symm (mul_zerol a)) (λ (n : Nat) (iH : a * n = n * a), - calc a * (n + 1) = a * n + a : mul::succr a n + calc a * (n + 1) = a * n + a : mul_succr a n ... = n * a + a : { iH } - ... = (n + 1) * a : symm (mul::succl n a)) + ... = (n + 1) * a : symm (mul_succl n a)) theorem distributer (a b c : Nat) : a * (b + c) = a * b + a * c := induction a - (calc 0 * (b + c) = 0 : mul::zerol (b + c) + (calc 0 * (b + c) = 0 : mul_zerol (b + c) ... = 0 + 0 : trivial - ... = 0 * b + 0 : { symm (mul::zerol b) } - ... = 0 * b + 0 * c : { symm (mul::zerol c) }) + ... = 0 * b + 0 : { symm (mul_zerol b) } + ... = 0 * b + 0 * c : { symm (mul_zerol c) }) (λ (n : Nat) (iH : n * (b + c) = n * b + n * c), - calc (n + 1) * (b + c) = n * (b + c) + (b + c) : mul::succl n (b + c) + calc (n + 1) * (b + c) = n * (b + c) + (b + c) : mul_succl n (b + c) ... = n * b + n * c + (b + c) : { iH } - ... = n * b + n * c + b + c : add::assoc (n * b + n * c) b c - ... = n * b + (n * c + b) + c : { symm (add::assoc (n * b) (n * c) b) } - ... = n * b + (b + n * c) + c : { add::comm (n * c) b } - ... = n * b + b + n * c + c : { add::assoc (n * b) b (n * c) } - ... = (n + 1) * b + n * c + c : { symm (mul::succl n b) } - ... = (n + 1) * b + (n * c + c) : symm (add::assoc ((n + 1) * b) (n * c) c) - ... = (n + 1) * b + (n + 1) * c : { symm (mul::succl n c) }) + ... = n * b + n * c + b + c : add_assoc (n * b + n * c) b c + ... = n * b + (n * c + b) + c : { symm (add_assoc (n * b) (n * c) b) } + ... = n * b + (b + n * c) + c : { add_comm (n * c) b } + ... = n * b + b + n * c + c : { add_assoc (n * b) b (n * c) } + ... = (n + 1) * b + n * c + c : { symm (mul_succl n b) } + ... = (n + 1) * b + (n * c + c) : symm (add_assoc ((n + 1) * b) (n * c) c) + ... = (n + 1) * b + (n + 1) * c : { symm (mul_succl n c) }) theorem distributel (a b c : Nat) : (a + b) * c = a * c + b * c -:= calc (a + b) * c = c * (a + b) : mul::comm (a + b) c +:= calc (a + b) * c = c * (a + b) : mul_comm (a + b) c ... = c * a + c * b : distributer c a b - ... = a * c + c * b : { mul::comm c a } - ... = a * c + b * c : { mul::comm c b } + ... = a * c + c * b : { mul_comm c a } + ... = a * c + b * c : { mul_comm c b } -theorem mul::assoc (a b c : Nat) : a * (b * c) = a * b * c +theorem mul_assoc (a b c : Nat) : a * (b * c) = a * b * c := induction a - (calc 0 * (b * c) = 0 : mul::zerol (b * c) - ... = 0 * c : symm (mul::zerol c) - ... = (0 * b) * c : { symm (mul::zerol b) }) + (calc 0 * (b * c) = 0 : mul_zerol (b * c) + ... = 0 * c : symm (mul_zerol c) + ... = (0 * b) * c : { symm (mul_zerol b) }) (λ (n : Nat) (iH : n * (b * c) = n * b * c), - calc (n + 1) * (b * c) = n * (b * c) + (b * c) : mul::succl n (b * c) + calc (n + 1) * (b * c) = n * (b * c) + (b * c) : mul_succl n (b * c) ... = n * b * c + (b * c) : { iH } ... = (n * b + b) * c : symm (distributel (n * b) b c) - ... = (n + 1) * b * c : { symm (mul::succl n b) }) + ... = (n + 1) * b * c : { symm (mul_succl n b) }) -theorem add::inj {a b c : Nat} : a + b = a + c → b = c +theorem add_inj {a b c : Nat} : a + b = a + c → b = c := induction a (λ H : 0 + b = 0 + c, - calc b = 0 + b : symm (add::zerol b) + calc b = 0 + b : symm (add_zerol b) ... = 0 + c : H - ... = c : add::zerol c) + ... = c : add_zerol c) (λ (n : Nat) (iH : n + b = n + c → b = c) (H : n + 1 + b = n + 1 + c), let L1 : n + b + 1 = n + c + 1 - := (calc n + b + 1 = n + (b + 1) : symm (add::assoc n b 1) - ... = n + (1 + b) : { add::comm b 1 } - ... = n + 1 + b : add::assoc n 1 b + := (calc n + b + 1 = n + (b + 1) : symm (add_assoc n b 1) + ... = n + (1 + b) : { add_comm b 1 } + ... = n + 1 + b : add_assoc n 1 b ... = n + 1 + c : H - ... = n + (1 + c) : symm (add::assoc n 1 c) - ... = n + (c + 1) : { add::comm 1 c } - ... = n + c + 1 : add::assoc n c 1), - L2 : n + b = n + c := succ::inj L1 + ... = n + (1 + c) : symm (add_assoc n 1 c) + ... = n + (c + 1) : { add_comm 1 c } + ... = n + c + 1 : add_assoc n c 1), + L2 : n + b = n + c := succ_inj L1 in iH L2) -theorem add::eqz {a b : Nat} (H : a + b = 0) : a = 0 +theorem add_eqz {a b : Nat} (H : a + b = 0) : a = 0 := discriminate (λ H1 : a = 0, H1) (λ (n : Nat) (H1 : a = n + 1), - absurd::elim (a = 0) + absurd_elim (a = 0) H (calc a + b = n + 1 + b : { H1 } - ... = n + (1 + b) : symm (add::assoc n 1 b) - ... = n + (b + 1) : { add::comm 1 b } - ... = n + b + 1 : add::assoc n b 1 - ... ≠ 0 : succ::nz (n + b))) + ... = n + (1 + b) : symm (add_assoc n 1 b) + ... = n + (b + 1) : { add_comm 1 b } + ... = n + b + 1 : add_assoc n b 1 + ... ≠ 0 : succ_nz (n + b))) -theorem le::intro {a b c : Nat} (H : a + c = b) : a ≤ b -:= (symm (le::def a b)) ◂ (have (∃ x, a + x = b) : exists::intro c H) +theorem le_intro {a b c : Nat} (H : a + c = b) : a ≤ b +:= (symm (le_def a b)) ◂ (have (∃ x, a + x = b) : exists_intro c H) -theorem le::elim {a b : Nat} (H : a ≤ b) : ∃ x, a + x = b -:= (le::def a b) ◂ H +theorem le_elim {a b : Nat} (H : a ≤ b) : ∃ x, a + x = b +:= (le_def a b) ◂ H -theorem le::refl (a : Nat) : a ≤ a := le::intro (add::zeror a) +theorem le_refl (a : Nat) : a ≤ a := le_intro (add_zeror a) -theorem le::zero (a : Nat) : 0 ≤ a := le::intro (add::zerol a) +theorem le_zero (a : Nat) : 0 ≤ a := le_intro (add_zerol a) -theorem le::trans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c -:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le::elim H1), - obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le::elim H2), - le::intro (calc a + (w1 + w2) = a + w1 + w2 : add::assoc a w1 w2 +theorem le_trans {a b c : Nat} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c +:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le_elim H1), + obtain (w2 : Nat) (Hw2 : b + w2 = c), from (le_elim H2), + le_intro (calc a + (w1 + w2) = a + w1 + w2 : add_assoc a w1 w2 ... = b + w2 : { Hw1 } ... = c : Hw2) -theorem le::add {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c -:= obtain (w : Nat) (Hw : a + w = b), from (le::elim H), - le::intro (calc a + c + w = a + (c + w) : symm (add::assoc a c w) - ... = a + (w + c) : { add::comm c w } - ... = a + w + c : add::assoc a w c +theorem le_add {a b : Nat} (H : a ≤ b) (c : Nat) : a + c ≤ b + c +:= obtain (w : Nat) (Hw : a + w = b), from (le_elim H), + le_intro (calc a + c + w = a + (c + w) : symm (add_assoc a c w) + ... = a + (w + c) : { add_comm c w } + ... = a + w + c : add_assoc a w c ... = b + c : { Hw }) -theorem le::antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b -:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le::elim H1), - obtain (w2 : Nat) (Hw2 : b + w2 = a), from (le::elim H2), +theorem le_antisym {a b : Nat} (H1 : a ≤ b) (H2 : b ≤ a) : a = b +:= obtain (w1 : Nat) (Hw1 : a + w1 = b), from (le_elim H1), + obtain (w2 : Nat) (Hw2 : b + w2 = a), from (le_elim H2), let L1 : w1 + w2 = 0 - := add::inj (calc a + (w1 + w2) = a + w1 + w2 : { add::assoc a w1 w2 } + := add_inj (calc a + (w1 + w2) = a + w1 + w2 : { add_assoc a w1 w2 } ... = b + w2 : { Hw1 } ... = a : Hw2 - ... = a + 0 : symm (add::zeror a)), - L2 : w1 = 0 := add::eqz L1 - in calc a = a + 0 : symm (add::zeror a) + ... = a + 0 : symm (add_zeror a)), + L2 : w1 = 0 := add_eqz L1 + in calc a = a + 0 : symm (add_zeror a) ... = a + w1 : { symm L2 } ... = b : Hw1 -set::opaque add true -set::opaque mul true -set::opaque le true -set::opaque id true -set::opaque ge true -set::opaque lt true -set::opaque gt true -set::opaque id true +set_opaque add true +set_opaque mul true +set_opaque le true +set_opaque id true +set_opaque ge true +set_opaque lt true +set_opaque gt true +set_opaque id true end \ No newline at end of file diff --git a/src/builtin/cast.lean b/src/builtin/cast.lean index b4ec39743c..e79001af8f 100644 --- a/src/builtin/cast.lean +++ b/src/builtin/cast.lean @@ -8,7 +8,7 @@ universe U >= M + 1 definition TypeM := (Type M) -- Type equality axiom, if two values are equal, then their types are equal -theorem type::eq {A B : TypeM} {a : A} {b : B} (H : a == b) : A == B +theorem type_eq {A B : TypeM} {a : A} {b : B} (H : a == b) : A == B := hsubst (λ (T : TypeU) (x : T), A == T) (refl A) H -- Heterogenous symmetry @@ -24,10 +24,10 @@ theorem htrans {A B C : TypeU} {a : A} {b : B} {c : C} (H1 : a == b) (H2 : b == variable cast {A B : TypeU} : A == B → A → B -- The CastEq axiom states that for any cast of x is equal to x. -axiom cast::eq {A B : TypeU} (H : A == B) (x : A) : x == cast H x +axiom cast_eq {A B : TypeU} (H : A == B) (x : A) : x == cast H x -- The CastApp axiom "propagates" the cast over application -axiom cast::app {A A' : TypeU} {B : A → TypeU} {B' : A' → TypeU} +axiom cast_app {A A' : TypeU} {B : A → TypeU} {B' : A' → TypeU} (H1 : (∀ x : A, B x) == (∀ x : A', B' x)) (H2 : A == A') (f : ∀ x : A, B x) (x : A) : cast H1 f (cast H2 x) == f x @@ -39,19 +39,19 @@ theorem hcongr (H1 : f == g) (H2 : a == b) : f a == g b -:= let L1 : A == A' := type::eq H2, +:= let L1 : A == A' := type_eq H2, L2 : A' == A := symm L1, b' : A := cast L2 b, - L3 : b == b' := cast::eq L2 b, + L3 : b == b' := cast_eq L2 b, L4 : a == b' := htrans H2 L3, L5 : f a == f b' := congr2 f L4, - S1 : (∀ x : A', B' x) == (∀ x : A, B x) := symm (type::eq H1), + S1 : (∀ x : A', B' x) == (∀ x : A, B x) := symm (type_eq H1), g' : (∀ x : A, B x) := cast S1 g, - L6 : g == g' := cast::eq S1 g, + L6 : g == g' := cast_eq S1 g, L7 : f == g' := htrans H1 L6, L8 : f b' == g' b' := congr1 b' L7, L9 : f a == g' b' := htrans L5 L8, - L10 : g' b' == g b := cast::app S1 L2 g b + L10 : g' b' == g b := cast_app S1 L2 g b in htrans L9 L10 exit -- Stop here, the following axiom is not sound @@ -72,9 +72,8 @@ theorem unsat : false := let L1 : (∀ x : true, true) := (λ x : true, trivial), L2 : (∀ x : false, true) := (λ x : false, trivial), -- When we keep Pi/forall as different things, the following two steps can't be used - L3 : (∀ x : true, true) = true := eqt::intro L1, - L4 : (∀ x : false, true) = true := eqt::intro L2, + L3 : (∀ x : true, true) = true := eqt_intro L1, + L4 : (∀ x : false, true) = true := eqt_intro L2, L5 : (∀ x : true, true) = (∀ x : false, true) := trans L3 (symm L4), L6 : true = false := dominj L5 in L6 - diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean index d03d368096..2e1564288c 100644 --- a/src/builtin/kernel.lean +++ b/src/builtin/kernel.lean @@ -83,23 +83,23 @@ infixl 100 ◂ : eqmp theorem boolcomplete (a : Bool) : a == true ∨ a == false := case (λ x, x == true ∨ x == false) trivial trivial a -theorem false::elim (a : Bool) (H : false) : a +theorem false_elim (a : Bool) (H : false) : a := case (λ x, x) trivial H a -theorem imp::trans {a b c : Bool} (H1 : a → b) (H2 : b → c) : a → c +theorem imp_trans {a b c : Bool} (H1 : a → b) (H2 : b → c) : a → c := λ Ha, H2 (H1 Ha) -theorem imp::eq::trans {a b c : Bool} (H1 : a → b) (H2 : b == c) : a → c +theorem imp_eq_trans {a b c : Bool} (H1 : a → b) (H2 : b == c) : a → c := λ Ha, H2 ◂ (H1 Ha) -theorem eq::imp::trans {a b c : Bool} (H1 : a == b) (H2 : b → c) : a → c +theorem eq_imp_trans {a b c : Bool} (H1 : a == b) (H2 : b → c) : a → c := λ Ha, H2 (H1 ◂ Ha) -theorem not::not::eq (a : Bool) : (¬ ¬ a) == a +theorem not_not_eq (a : Bool) : (¬ ¬ a) == a := case (λ x, (¬ ¬ x) == x) trivial trivial a -theorem not::not::elim {a : Bool} (H : ¬ ¬ a) : a -:= (not::not::eq a) ◂ H +theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a +:= (not_not_eq a) ◂ H theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬ b) : ¬ a := λ Ha, absurd (H1 Ha) H2 @@ -107,16 +107,16 @@ theorem mt {a b : Bool} (H1 : a → b) (H2 : ¬ b) : ¬ a theorem contrapos {a b : Bool} (H : a → b) : ¬ b → ¬ a := λ Hnb : ¬ b, mt H Hnb -theorem absurd::elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b -:= false::elim b (absurd H1 H2) +theorem absurd_elim {a : Bool} (b : Bool) (H1 : a) (H2 : ¬ a) : b +:= false_elim b (absurd H1 H2) -theorem not::imp::eliml {a b : Bool} (Hnab : ¬ (a → b)) : a -:= not::not::elim +theorem not_imp_eliml {a b : Bool} (Hnab : ¬ (a → b)) : a +:= not_not_elim (have ¬ ¬ a : - λ Hna : ¬ a, absurd (have a → b : λ Ha : a, absurd::elim b Ha Hna) + λ Hna : ¬ a, absurd (have a → b : λ Ha : a, absurd_elim b Ha Hna) Hnab) -theorem not::imp::elimr {a b : Bool} (H : ¬ (a → b)) : ¬ b +theorem not_imp_elimr {a b : Bool} (H : ¬ (a → b)) : ¬ b := λ Hb : b, absurd (have a → b : λ Ha : a, Hb) (have ¬ (a → b) : H) @@ -124,30 +124,30 @@ theorem resolve1 {a b : Bool} (H1 : a ∨ b) (H2 : ¬ a) : b := H1 H2 -- Recall that and is defined as ¬ (a → ¬ b) -theorem and::intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b +theorem and_intro {a b : Bool} (H1 : a) (H2 : b) : a ∧ b := λ H : a → ¬ b, absurd H2 (H H1) -theorem and::eliml {a b : Bool} (H : a ∧ b) : a -:= not::imp::eliml H +theorem and_eliml {a b : Bool} (H : a ∧ b) : a +:= not_imp_eliml H -theorem and::elimr {a b : Bool} (H : a ∧ b) : b -:= not::not::elim (not::imp::elimr H) +theorem and_elimr {a b : Bool} (H : a ∧ b) : b +:= not_not_elim (not_imp_elimr H) -- Recall that or is defined as ¬ a → b -theorem or::introl {a : Bool} (H : a) (b : Bool) : a ∨ b -:= λ H1 : ¬ a, absurd::elim b H H1 +theorem or_introl {a : Bool} (H : a) (b : Bool) : a ∨ b +:= λ H1 : ¬ a, absurd_elim b H H1 -theorem or::intror {b : Bool} (a : Bool) (H : b) : a ∨ b +theorem or_intror {b : Bool} (a : Bool) (H : b) : a ∨ b := λ H1 : ¬ a, H -theorem or::elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c -:= not::not::elim +theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c +:= not_not_elim (λ H : ¬ c, absurd (have c : H3 (have b : resolve1 H1 (have ¬ a : (mt (λ Ha : a, H2 Ha) H)))) H) theorem refute {a : Bool} (H : ¬ a → false) : a -:= or::elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false::elim a (H H1)) +:= or_elim (em a) (λ H1 : a, H1) (λ H1 : ¬ a, false_elim a (H H1)) theorem symm {A : TypeU} {a b : A} (H : a == b) : b == a := subst (refl a) H @@ -157,16 +157,16 @@ theorem trans {A : TypeU} {a b c : A} (H1 : a == b) (H2 : b == c) : a == c infixl 100 ⋈ : trans -theorem ne::symm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a +theorem ne_symm {A : TypeU} {a b : A} (H : a ≠ b) : b ≠ a := λ H1 : b = a, H (symm H1) -theorem eq::ne::trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c +theorem eq_ne_trans {A : TypeU} {a b c : A} (H1 : a = b) (H2 : b ≠ c) : a ≠ c := subst H2 (symm H1) -theorem ne::eq::trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c +theorem ne_eq_trans {A : TypeU} {a b c : A} (H1 : a ≠ b) (H2 : b = c) : a ≠ c := subst H1 H2 -theorem eqt::elim {a : Bool} (H : a == true) : a +theorem eqt_elim {a : Bool} (H : a == true) : a := (symm H) ◂ trivial theorem congr1 {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} (a : A) (H : f == g) : f a == g a @@ -179,176 +179,176 @@ theorem congr {A : TypeU} {B : A → TypeU} {f g : ∀ x : A, B x} {a b : A} (H1 := subst (congr2 f H2) (congr1 b H1) -- Recall that exists is defined as ¬ ∀ x : A, ¬ P x -theorem exists::elim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B +theorem exists_elim {A : TypeU} {P : A → Bool} {B : Bool} (H1 : Exists A P) (H2 : ∀ (a : A) (H : P a), B) : B := refute (λ R : ¬ B, absurd (λ a : A, mt (λ H : P a, H2 a H) R) H1) -theorem exists::intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P +theorem exists_intro {A : TypeU} {P : A → Bool} (a : A) (H : P a) : Exists A P := λ H1 : (∀ x : A, ¬ P x), absurd H (H1 a) theorem boolext {a b : Bool} (Hab : a → b) (Hba : b → a) : a == b -:= or::elim (boolcomplete a) - (λ Hat : a == true, or::elim (boolcomplete b) +:= or_elim (boolcomplete a) + (λ Hat : a == true, or_elim (boolcomplete b) (λ Hbt : b == true, trans Hat (symm Hbt)) - (λ Hbf : b == false, false::elim (a == b) (subst (Hab (eqt::elim Hat)) Hbf))) - (λ Haf : a == false, or::elim (boolcomplete b) - (λ Hbt : b == true, false::elim (a == b) (subst (Hba (eqt::elim Hbt)) Haf)) + (λ Hbf : b == false, false_elim (a == b) (subst (Hab (eqt_elim Hat)) Hbf))) + (λ Haf : a == false, or_elim (boolcomplete b) + (λ Hbt : b == true, false_elim (a == b) (subst (Hba (eqt_elim Hbt)) Haf)) (λ Hbf : b == false, trans Haf (symm Hbf))) -definition iff::intro {a b : Bool} (Hab : a → b) (Hba : b → a) := boolext Hab Hba +definition iff_intro {a b : Bool} (Hab : a → b) (Hba : b → a) := boolext Hab Hba -theorem eqt::intro {a : Bool} (H : a) : a == true +theorem eqt_intro {a : Bool} (H : a) : a == true := boolext (λ H1 : a, trivial) (λ H2 : true, H) -theorem or::comm (a b : Bool) : (a ∨ b) == (b ∨ a) -:= boolext (λ H, or::elim H (λ H1, or::intror b H1) (λ H2, or::introl H2 a)) - (λ H, or::elim H (λ H1, or::intror a H1) (λ H2, or::introl H2 b)) +theorem or_comm (a b : Bool) : (a ∨ b) == (b ∨ a) +:= boolext (λ H, or_elim H (λ H1, or_intror b H1) (λ H2, or_introl H2 a)) + (λ H, or_elim H (λ H1, or_intror a H1) (λ H2, or_introl H2 b)) -theorem or::assoc (a b c : Bool) : ((a ∨ b) ∨ c) == (a ∨ (b ∨ c)) +theorem or_assoc (a b c : Bool) : ((a ∨ b) ∨ c) == (a ∨ (b ∨ c)) := boolext (λ H : (a ∨ b) ∨ c, - or::elim H (λ H1 : a ∨ b, or::elim H1 (λ Ha : a, or::introl Ha (b ∨ c)) (λ Hb : b, or::intror a (or::introl Hb c))) - (λ Hc : c, or::intror a (or::intror b Hc))) + or_elim H (λ H1 : a ∨ b, or_elim H1 (λ Ha : a, or_introl Ha (b ∨ c)) (λ Hb : b, or_intror a (or_introl Hb c))) + (λ Hc : c, or_intror a (or_intror b Hc))) (λ H : a ∨ (b ∨ c), - or::elim H (λ Ha : a, (or::introl (or::introl Ha b) c)) - (λ H1 : b ∨ c, or::elim H1 (λ Hb : b, or::introl (or::intror a Hb) c) - (λ Hc : c, or::intror (a ∨ b) Hc))) + or_elim H (λ Ha : a, (or_introl (or_introl Ha b) c)) + (λ H1 : b ∨ c, or_elim H1 (λ Hb : b, or_introl (or_intror a Hb) c) + (λ Hc : c, or_intror (a ∨ b) Hc))) -theorem or::id (a : Bool) : (a ∨ a) == a -:= boolext (λ H, or::elim H (λ H1, H1) (λ H2, H2)) - (λ H, or::introl H a) +theorem or_id (a : Bool) : (a ∨ a) == a +:= boolext (λ H, or_elim H (λ H1, H1) (λ H2, H2)) + (λ H, or_introl H a) -theorem or::falsel (a : Bool) : (a ∨ false) == a -:= boolext (λ H, or::elim H (λ H1, H1) (λ H2, false::elim a H2)) - (λ H, or::introl H false) +theorem or_falsel (a : Bool) : (a ∨ false) == a +:= boolext (λ H, or_elim H (λ H1, H1) (λ H2, false_elim a H2)) + (λ H, or_introl H false) -theorem or::falser (a : Bool) : (false ∨ a) == a -:= (or::comm false a) ⋈ (or::falsel a) +theorem or_falser (a : Bool) : (false ∨ a) == a +:= (or_comm false a) ⋈ (or_falsel a) -theorem or::truel (a : Bool) : (true ∨ a) == true -:= eqt::intro (case (λ x : Bool, true ∨ x) trivial trivial a) +theorem or_truel (a : Bool) : (true ∨ a) == true +:= eqt_intro (case (λ x : Bool, true ∨ x) trivial trivial a) -theorem or::truer (a : Bool) : (a ∨ true) == true -:= (or::comm a true) ⋈ (or::truel a) +theorem or_truer (a : Bool) : (a ∨ true) == true +:= (or_comm a true) ⋈ (or_truel a) -theorem or::tauto (a : Bool) : (a ∨ ¬ a) == true -:= eqt::intro (em a) +theorem or_tauto (a : Bool) : (a ∨ ¬ a) == true +:= eqt_intro (em a) -theorem and::comm (a b : Bool) : (a ∧ b) == (b ∧ a) -:= boolext (λ H, and::intro (and::elimr H) (and::eliml H)) - (λ H, and::intro (and::elimr H) (and::eliml H)) +theorem and_comm (a b : Bool) : (a ∧ b) == (b ∧ a) +:= boolext (λ H, and_intro (and_elimr H) (and_eliml H)) + (λ H, and_intro (and_elimr H) (and_eliml H)) -theorem and::id (a : Bool) : (a ∧ a) == a -:= boolext (λ H, and::eliml H) - (λ H, and::intro H H) +theorem and_id (a : Bool) : (a ∧ a) == a +:= boolext (λ H, and_eliml H) + (λ H, and_intro H H) -theorem and::assoc (a b c : Bool) : ((a ∧ b) ∧ c) == (a ∧ (b ∧ c)) -:= boolext (λ H, and::intro (and::eliml (and::eliml H)) (and::intro (and::elimr (and::eliml H)) (and::elimr H))) - (λ H, and::intro (and::intro (and::eliml H) (and::eliml (and::elimr H))) (and::elimr (and::elimr H))) +theorem and_assoc (a b c : Bool) : ((a ∧ b) ∧ c) == (a ∧ (b ∧ c)) +:= boolext (λ H, and_intro (and_eliml (and_eliml H)) (and_intro (and_elimr (and_eliml H)) (and_elimr H))) + (λ H, and_intro (and_intro (and_eliml H) (and_eliml (and_elimr H))) (and_elimr (and_elimr H))) -theorem and::truer (a : Bool) : (a ∧ true) == a -:= boolext (λ H : a ∧ true, and::eliml H) - (λ H : a, and::intro H trivial) +theorem and_truer (a : Bool) : (a ∧ true) == a +:= boolext (λ H : a ∧ true, and_eliml H) + (λ H : a, and_intro H trivial) -theorem and::truel (a : Bool) : (true ∧ a) == a -:= trans (and::comm true a) (and::truer a) +theorem and_truel (a : Bool) : (true ∧ a) == a +:= trans (and_comm true a) (and_truer a) -theorem and::falsel (a : Bool) : (a ∧ false) == false -:= boolext (λ H, and::elimr H) - (λ H, false::elim (a ∧ false) H) +theorem and_falsel (a : Bool) : (a ∧ false) == false +:= boolext (λ H, and_elimr H) + (λ H, false_elim (a ∧ false) H) -theorem and::falser (a : Bool) : (false ∧ a) == false -:= (and::comm false a) ⋈ (and::falsel a) +theorem and_falser (a : Bool) : (false ∧ a) == false +:= (and_comm false a) ⋈ (and_falsel a) -theorem and::absurd (a : Bool) : (a ∧ ¬ a) == false -:= boolext (λ H, absurd (and::eliml H) (and::elimr H)) - (λ H, false::elim (a ∧ ¬ a) H) +theorem and_absurd (a : Bool) : (a ∧ ¬ a) == false +:= boolext (λ H, absurd (and_eliml H) (and_elimr H)) + (λ H, false_elim (a ∧ ¬ a) H) -theorem not::true : (¬ true) == false +theorem not_true : (¬ true) == false := trivial -theorem not::false : (¬ false) == true +theorem not_false : (¬ false) == true := trivial -theorem not::and (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b) +theorem not_and (a b : Bool) : (¬ (a ∧ b)) == (¬ a ∨ ¬ b) := case (λ x, (¬ (x ∧ b)) == (¬ x ∨ ¬ b)) (case (λ y, (¬ (true ∧ y)) == (¬ true ∨ ¬ y)) trivial trivial b) (case (λ y, (¬ (false ∧ y)) == (¬ false ∨ ¬ y)) trivial trivial b) a -theorem not::and::elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b -:= (not::and a b) ◂ H +theorem not_and_elim {a b : Bool} (H : ¬ (a ∧ b)) : ¬ a ∨ ¬ b +:= (not_and a b) ◂ H -theorem not::or (a b : Bool) : (¬ (a ∨ b)) == (¬ a ∧ ¬ b) +theorem not_or (a b : Bool) : (¬ (a ∨ b)) == (¬ a ∧ ¬ b) := case (λ x, (¬ (x ∨ b)) == (¬ x ∧ ¬ b)) (case (λ y, (¬ (true ∨ y)) == (¬ true ∧ ¬ y)) trivial trivial b) (case (λ y, (¬ (false ∨ y)) == (¬ false ∧ ¬ y)) trivial trivial b) a -theorem not::or::elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b -:= (not::or a b) ◂ H +theorem not_or_elim {a b : Bool} (H : ¬ (a ∨ b)) : ¬ a ∧ ¬ b +:= (not_or a b) ◂ H -theorem not::iff (a b : Bool) : (¬ (a == b)) == ((¬ a) == b) +theorem not_iff (a b : Bool) : (¬ (a == b)) == ((¬ a) == b) := case (λ x, (¬ (x == b)) == ((¬ x) == b)) (case (λ y, (¬ (true == y)) == ((¬ true) == y)) trivial trivial b) (case (λ y, (¬ (false == y)) == ((¬ false) == y)) trivial trivial b) a -theorem not::iff::elim {a b : Bool} (H : ¬ (a == b)) : (¬ a) == b -:= (not::iff a b) ◂ H +theorem not_iff_elim {a b : Bool} (H : ¬ (a == b)) : (¬ a) == b +:= (not_iff a b) ◂ H -theorem not::implies (a b : Bool) : (¬ (a → b)) == (a ∧ ¬ b) +theorem not_implies (a b : Bool) : (¬ (a → b)) == (a ∧ ¬ b) := case (λ x, (¬ (x → b)) == (x ∧ ¬ b)) (case (λ y, (¬ (true → y)) == (true ∧ ¬ y)) trivial trivial b) (case (λ y, (¬ (false → y)) == (false ∧ ¬ y)) trivial trivial b) a -theorem not::implies::elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b -:= (not::implies a b) ◂ H +theorem not_implies_elim {a b : Bool} (H : ¬ (a → b)) : a ∧ ¬ b +:= (not_implies a b) ◂ H -theorem not::congr {a b : Bool} (H : a == b) : (¬ a) == (¬ b) +theorem not_congr {a b : Bool} (H : a == b) : (¬ a) == (¬ b) := congr2 not H -theorem eq::exists::intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x == Q x) : (∃ x : A, P x) == (∃ x : A, Q x) +theorem eq_exists_intro {A : (Type U)} {P Q : A → Bool} (H : ∀ x : A, P x == Q x) : (∃ x : A, P x) == (∃ x : A, Q x) := congr2 (Exists A) (funext H) -theorem not::forall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (∃ x : A, ¬ P x) -:= calc (¬ ∀ x : A, P x) = (¬ ∀ x : A, ¬ ¬ P x) : not::congr (allext (λ x : A, symm (not::not::eq (P x)))) +theorem not_forall (A : (Type U)) (P : A → Bool) : (¬ (∀ x : A, P x)) == (∃ x : A, ¬ P x) +:= calc (¬ ∀ x : A, P x) = (¬ ∀ x : A, ¬ ¬ P x) : not_congr (allext (λ x : A, symm (not_not_eq (P x)))) ... = (∃ x : A, ¬ P x) : refl (∃ x : A, ¬ P x) -theorem not::forall::elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x -:= (not::forall A P) ◂ H +theorem not_forall_elim {A : (Type U)} {P : A → Bool} (H : ¬ (∀ x : A, P x)) : ∃ x : A, ¬ P x +:= (not_forall A P) ◂ H -theorem not::exists (A : (Type U)) (P : A → Bool) : (¬ ∃ x : A, P x) == (∀ x : A, ¬ P x) +theorem not_exists (A : (Type U)) (P : A → Bool) : (¬ ∃ x : A, P x) == (∀ x : A, ¬ P x) := calc (¬ ∃ x : A, P x) = (¬ ¬ ∀ x : A, ¬ P x) : refl (¬ ∃ x : A, P x) - ... = (∀ x : A, ¬ P x) : not::not::eq (∀ x : A, ¬ P x) + ... = (∀ x : A, ¬ P x) : not_not_eq (∀ x : A, ¬ P x) -theorem not::exists::elim {A : (Type U)} {P : A → Bool} (H : ¬ ∃ x : A, P x) : ∀ x : A, ¬ P x -:= (not::exists A P) ◂ H +theorem not_exists_elim {A : (Type U)} {P : A → Bool} (H : ¬ ∃ x : A, P x) : ∀ x : A, ¬ P x +:= (not_exists A P) ◂ H -theorem exists::unfold1 {A : TypeU} {P : A → Bool} (a : A) (H : ∃ x : A, P x) : P a ∨ (∃ x : A, x ≠ a ∧ P x) -:= exists::elim H +theorem exists_unfold1 {A : TypeU} {P : A → Bool} (a : A) (H : ∃ x : A, P x) : P a ∨ (∃ x : A, x ≠ a ∧ P x) +:= exists_elim H (λ (w : A) (H1 : P w), - or::elim (em (w = a)) - (λ Heq : w = a, or::introl (subst H1 Heq) (∃ x : A, x ≠ a ∧ P x)) - (λ Hne : w ≠ a, or::intror (P a) (exists::intro w (and::intro Hne H1)))) + or_elim (em (w = a)) + (λ Heq : w = a, or_introl (subst H1 Heq) (∃ x : A, x ≠ a ∧ P x)) + (λ Hne : w ≠ a, or_intror (P a) (exists_intro w (and_intro Hne H1)))) -theorem exists::unfold2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x : A, x ≠ a ∧ P x)) : ∃ x : A, P x -:= or::elim H - (λ H1 : P a, exists::intro a H1) +theorem exists_unfold2 {A : TypeU} {P : A → Bool} (a : A) (H : P a ∨ (∃ x : A, x ≠ a ∧ P x)) : ∃ x : A, P x +:= or_elim H + (λ H1 : P a, exists_intro a H1) (λ H2 : (∃ x : A, x ≠ a ∧ P x), - exists::elim H2 + exists_elim H2 (λ (w : A) (Hw : w ≠ a ∧ P w), - exists::intro w (and::elimr Hw))) + exists_intro w (and_elimr Hw))) -theorem exists::unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) = (P a ∨ (∃ x : A, x ≠ a ∧ P x)) -:= boolext (λ H : (∃ x : A, P x), exists::unfold1 a H) - (λ H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists::unfold2 a H) +theorem exists_unfold {A : TypeU} (P : A → Bool) (a : A) : (∃ x : A, P x) = (P a ∨ (∃ x : A, x ≠ a ∧ P x)) +:= boolext (λ H : (∃ x : A, P x), exists_unfold1 a H) + (λ H : (P a ∨ (∃ x : A, x ≠ a ∧ P x)), exists_unfold2 a H) -set::opaque exists true -set::opaque not true -set::opaque or true -set::opaque and true -set::opaque implies true \ No newline at end of file +set_opaque exists true +set_opaque not true +set_opaque or true +set_opaque and true +set_opaque implies true \ No newline at end of file diff --git a/src/builtin/macros.lua b/src/builtin/macros.lua index 82a231ab5d..409f46c82a 100644 --- a/src/builtin/macros.lua +++ b/src/builtin/macros.lua @@ -92,7 +92,7 @@ macro("obtain", { macro_arg.Parameters, macro_arg.Comma, macro_arg.Id, macro_arg if fromid ~= name("from") then error("invalid 'obtain' expression, 'from' keyword expected, got '" .. tostring(fromid) .. "'") end - local exElim = mk_constant({"exists", "elim"}) + local exElim = mk_constant("exists_elim") local H_name = bindings[n][1] local H_type = bindings[n][2] local a_name = bindings[n-1][1] diff --git a/src/builtin/obj/Nat.olean b/src/builtin/obj/Nat.olean index e07e061551..38c2125bad 100644 Binary files a/src/builtin/obj/Nat.olean and b/src/builtin/obj/Nat.olean differ diff --git a/src/builtin/obj/cast.olean b/src/builtin/obj/cast.olean index 5d0d947928..e5d578d430 100644 Binary files a/src/builtin/obj/cast.olean and b/src/builtin/obj/cast.olean differ diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean index 32c4614025..e2d592365f 100644 Binary files a/src/builtin/obj/kernel.olean and b/src/builtin/obj/kernel.olean differ diff --git a/src/frontends/lean/parser_calc.cpp b/src/frontends/lean/parser_calc.cpp index 1b44629022..2d5d7f2a5b 100644 --- a/src/frontends/lean/parser_calc.cpp +++ b/src/frontends/lean/parser_calc.cpp @@ -44,11 +44,11 @@ void calc_proof_parser::add_trans_step(expr const & op1, expr const & op2, trans m_trans_ops.emplace_front(op1, op2, d); } -static name g_eq_imp_trans({"eq", "imp", "trans"}); -static name g_imp_eq_trans({"imp", "eq", "trans"}); -static name g_imp_trans({"imp", "trans"}); -static name g_eq_ne_trans({"eq", "ne", "trans"}); -static name g_ne_eq_trans({"ne", "eq", "trans"}); +static name g_eq_imp_trans("eq_imp_trans"); +static name g_imp_eq_trans("imp_eq_trans"); +static name g_imp_trans("imp_trans"); +static name g_eq_ne_trans("eq_ne_trans"); +static name g_ne_eq_trans("ne_eq_trans"); static name g_neq("neq"); calc_proof_parser::calc_proof_parser() { diff --git a/src/frontends/lean/parser_cmds.cpp b/src/frontends/lean/parser_cmds.cpp index 8a615cda96..b56257f4eb 100644 --- a/src/frontends/lean/parser_cmds.cpp +++ b/src/frontends/lean/parser_cmds.cpp @@ -37,8 +37,8 @@ static name g_infix_kwd("infix"); static name g_infixl_kwd("infixl"); static name g_infixr_kwd("infixr"); static name g_notation_kwd("notation"); -static name g_set_option_kwd("set", "option"); -static name g_set_opaque_kwd("set", "opaque"); +static name g_set_option_kwd("set_option"); +static name g_set_opaque_kwd("set_opaque"); static name g_options_kwd("options"); static name g_env_kwd("environment"); static name g_import_kwd("import"); @@ -46,7 +46,7 @@ static name g_help_kwd("help"); static name g_coercion_kwd("coercion"); static name g_exit_kwd("exit"); static name g_print_kwd("print"); -static name g_pop_kwd("pop", "scope"); +static name g_pop_kwd("pop_scope"); static name g_scope_kwd("scope"); static name g_builtin_kwd("builtin"); static name g_namespace_kwd("namespace"); diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index 8d26d339f1..3f33cd439d 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -137,35 +137,35 @@ MK_CONSTANT(hsymm_fn, name("hsymm")); MK_CONSTANT(eta_fn, name("eta")); MK_CONSTANT(imp_antisym_fn, name("iffintro")); MK_CONSTANT(trivial, name("trivial")); -MK_CONSTANT(false_elim_fn, name({"false", "elim"})); +MK_CONSTANT(false_elim_fn, name("false_elim")); MK_CONSTANT(absurd_fn, name("absurd")); MK_CONSTANT(em_fn, name("em")); MK_CONSTANT(double_neg_fn, name("doubleneg")); -MK_CONSTANT(double_neg_elim_fn, name({"doubleneg", "elim"})); +MK_CONSTANT(double_neg_elim_fn, name("doubleneg_elim")); MK_CONSTANT(mt_fn, name("mt")); MK_CONSTANT(contrapos_fn, name("contrapos")); -MK_CONSTANT(absurd_elim_fn, name({"absurd", "elim"})); +MK_CONSTANT(absurd_elim_fn, name("absurd_elim")); MK_CONSTANT(eq_mp_fn, name("eqmp")); -MK_CONSTANT(not_imp1_fn, name({"not", "imp", "eliml"})); -MK_CONSTANT(not_imp2_fn, name({"not", "imp", "elimr"})); -MK_CONSTANT(conj_fn, name({"and", "intro"})); -MK_CONSTANT(conjunct1_fn, name({"and", "eliml"})); -MK_CONSTANT(conjunct2_fn, name({"and", "elimr"})); -MK_CONSTANT(disj1_fn, name({"or", "introl"})); -MK_CONSTANT(disj2_fn, name({"or", "intror"})); -MK_CONSTANT(disj_cases_fn, name({"or", "elim"})); +MK_CONSTANT(not_imp1_fn, name("not_imp_eliml")); +MK_CONSTANT(not_imp2_fn, name("not_imp_elimr")); +MK_CONSTANT(conj_fn, name("and_intro")); +MK_CONSTANT(conjunct1_fn, name("and_eliml")); +MK_CONSTANT(conjunct2_fn, name("and_elimr")); +MK_CONSTANT(disj1_fn, name("or_introl")); +MK_CONSTANT(disj2_fn, name("or_intror")); +MK_CONSTANT(disj_cases_fn, name("or_elim")); MK_CONSTANT(refute_fn, name("refute")); MK_CONSTANT(symm_fn, name("symm")); MK_CONSTANT(trans_fn, name("trans")); MK_CONSTANT(congr1_fn, name("congr1")); MK_CONSTANT(congr2_fn, name("congr2")); MK_CONSTANT(congr_fn, name("congr")); -MK_CONSTANT(eqt_elim_fn, name({"eqt", "elim"})); -MK_CONSTANT(eqt_intro_fn, name({"eqt", "intro"})); -MK_CONSTANT(forall_elim_fn, name({"forall", "elim"})); -MK_CONSTANT(forall_intro_fn, name({"forall", "intro"})); -MK_CONSTANT(exists_elim_fn, name({"exists", "elim"})); -MK_CONSTANT(exists_intro_fn, name({"exists", "intro"})); +MK_CONSTANT(eqt_elim_fn, name("eqt_elim")); +MK_CONSTANT(eqt_intro_fn, name("eqt_intro")); +MK_CONSTANT(forall_elim_fn, name("forall_elim")); +MK_CONSTANT(forall_intro_fn, name("forall_intro")); +MK_CONSTANT(exists_elim_fn, name("exists_elim")); +MK_CONSTANT(exists_intro_fn, name("exists_intro")); void import_kernel(environment const & env, io_state const & ios) { env->import("kernel", ios); diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index bf1ecabf0f..cbf1a48786 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -34,7 +34,7 @@ class set_opaque_command : public neutral_object_cell { public: set_opaque_command(name const & n, bool opaque):m_obj_name(n), m_opaque(opaque) {} virtual ~set_opaque_command() {} - virtual char const * keyword() const { return "set::opaque"; } + virtual char const * keyword() const { return "set_opaque"; } virtual void write(serializer & s) const { s << "Opa" << m_obj_name << m_opaque; } name const & get_obj_name() const { return m_obj_name; } bool get_flag() const { return m_opaque; } diff --git a/src/tests/frontends/lean/parser.cpp b/src/tests/frontends/lean/parser.cpp index 8f9d2fcc27..e1336fa134 100644 --- a/src/tests/frontends/lean/parser.cpp +++ b/src/tests/frontends/lean/parser.cpp @@ -94,11 +94,11 @@ static void tst3() { parse_error(env, ios, "check U"); parse(env, ios, "variable h : Real -> Real -> Real. notation 10 [ _ ; _ ] : h. check [ 10.3 ; 20.1 ]."); parse_error(env, ios, "variable h : Real -> Real -> Real. notation 10 [ _ ; _ ] : h. check [ 10.3 | 20.1 ]."); - parse_error(env, ios, "set::option pp::indent true"); - parse(env, ios, "set::option pp::indent 10"); - parse_error(env, ios, "set::option pp::colors foo"); - parse_error(env, ios, "set::option pp::colors \"foo\""); - parse(env, ios, "set::option pp::colors true"); + parse_error(env, ios, "set_option pp::indent true"); + parse(env, ios, "set_option pp::indent 10"); + parse_error(env, ios, "set_option pp::colors foo"); + parse_error(env, ios, "set_option pp::colors \"foo\""); + parse(env, ios, "set_option pp::colors true"); parse_error(env, ios, "notation 10 : Int::add"); parse_error(env, ios, "notation 10 _ : Int::add"); parse(env, ios, "notation 10 _ ++ _ : Int::add. eval 10 ++ 20."); diff --git a/tests/lean/abst.lean b/tests/lean/abst.lean index 5206046738..d06359e9b7 100644 --- a/tests/lean/abst.lean +++ b/tests/lean/abst.lean @@ -2,5 +2,5 @@ import Int. axiom PlusComm(a b : Int) : a + b == b + a. variable a : Int. check (funext (fun x : Int, (PlusComm a x))). -set::option pp::implicit true. +set_option pp::implicit true. check (funext (fun x : Int, (PlusComm a x))). diff --git a/tests/lean/alias2.lean b/tests/lean/alias2.lean index d625f6f6cd..86da252676 100644 --- a/tests/lean/alias2.lean +++ b/tests/lean/alias2.lean @@ -3,14 +3,14 @@ scope alias ℕℕ : Natural. variable x : Natural. print environment 1. - set::option pp::unicode false. + set_option pp::unicode false. print environment 1. - set::option pp::unicode true. + set_option pp::unicode true. print environment 1. alias NN : Natural. print environment 2. alias ℕℕℕ : Natural. print environment 3. - set::option pp::unicode false. + set_option pp::unicode false. print environment 3. -pop::scope \ No newline at end of file +pop_scope \ No newline at end of file diff --git a/tests/lean/arith1.lean b/tests/lean/arith1.lean index fbb92abceb..704defe8fa 100644 --- a/tests/lean/arith1.lean +++ b/tests/lean/arith1.lean @@ -10,9 +10,9 @@ variable n : Nat variable m : Nat print n + m print n + x + m -set::option lean::pp::coercion true +set_option lean::pp::coercion true print n + x + m + 10 print x + n + m + 10 print n + m + 10 + x -set::option lean::pp::notation false +set_option lean::pp::notation false print n + m + 10 + x diff --git a/tests/lean/arith2.lean b/tests/lean/arith2.lean index 668e812d81..740659f251 100644 --- a/tests/lean/arith2.lean +++ b/tests/lean/arith2.lean @@ -7,7 +7,7 @@ variable x : Real variable i : Int variable n : Nat print x + i + 1 + n -set::option lean::pp::coercion true +set_option lean::pp::coercion true print x + i + 1 + n print x * i + x print x - i + x - x >= 0 diff --git a/tests/lean/arith3.lean b/tests/lean/arith3.lean index 3721ab4996..df8d471bc1 100644 --- a/tests/lean/arith3.lean +++ b/tests/lean/arith3.lean @@ -4,7 +4,7 @@ eval 8 div 4 eval 7 div 3 eval 7 mod 3 print -8 mod 3 -set::option lean::pp::notation false +set_option lean::pp::notation false print -8 mod 3 eval -8 mod 3 eval (-8 div 3)*3 + (-8 mod 3) \ No newline at end of file diff --git a/tests/lean/arith6.lean b/tests/lean/arith6.lean index 0b09644a64..227572837c 100644 --- a/tests/lean/arith6.lean +++ b/tests/lean/arith6.lean @@ -1,5 +1,5 @@ import Int. -set::option pp::unicode false +set_option pp::unicode false print 3 | 6 eval 3 | 6 eval 3 | 7 @@ -9,5 +9,5 @@ variable x : Int eval x | 3 eval 3 | x eval 6 | 3 -set::option pp::notation false +set_option pp::notation false print 3 | x \ No newline at end of file diff --git a/tests/lean/arith7.lean b/tests/lean/arith7.lean index bc3c370952..9a36066150 100644 --- a/tests/lean/arith7.lean +++ b/tests/lean/arith7.lean @@ -11,6 +11,6 @@ eval |x + 1| > 0 variable y : Int eval |x + y| print |x + y| > x -set::option pp::notation false +set_option pp::notation false print |x + y| > x print |x + y| + |y + x| > x \ No newline at end of file diff --git a/tests/lean/bad10.lean b/tests/lean/bad10.lean index 0a8028457e..da7a672740 100644 --- a/tests/lean/bad10.lean +++ b/tests/lean/bad10.lean @@ -1,5 +1,5 @@ -set::option pp::implicit true. -set::option pp::colors false. +set_option pp::implicit true. +set_option pp::colors false. variable N : Type. definition T (a : N) (f : _ -> _) (H : f a == a) : f (f _) == f _ := diff --git a/tests/lean/bad2.lean b/tests/lean/bad2.lean index e3f0c580b3..4213e300ab 100644 --- a/tests/lean/bad2.lean +++ b/tests/lean/bad2.lean @@ -8,6 +8,6 @@ definition n3 : list Int := cons 10 nil definition n4 : list Int := nil definition n5 : _ := cons 10 nil -set::option pp::coercion true -set::option pp::implicit true +set_option pp::coercion true +set_option pp::implicit true print environment 1. \ No newline at end of file diff --git a/tests/lean/bad9.lean b/tests/lean/bad9.lean index e60bd69cdd..7c2d62dd70 100644 --- a/tests/lean/bad9.lean +++ b/tests/lean/bad9.lean @@ -1,5 +1,5 @@ -set::option pp::implicit true. -set::option pp::colors false. +set_option pp::implicit true. +set_option pp::colors false. variable N : Type. check diff --git a/tests/lean/cast4.lean b/tests/lean/cast4.lean index e06e196156..ab3423e828 100644 --- a/tests/lean/cast4.lean +++ b/tests/lean/cast4.lean @@ -1,5 +1,5 @@ import cast -set::option pp::colors false +set_option pp::colors false check fun (A A': TypeM) (B : A -> TypeM) diff --git a/tests/lean/coercion2.lean b/tests/lean/coercion2.lean index 0af2afa342..634b019cb3 100644 --- a/tests/lean/coercion2.lean +++ b/tests/lean/coercion2.lean @@ -8,25 +8,25 @@ print g a a variable b : R print g a b print g b a -set::option lean::pp::coercion true +set_option lean::pp::coercion true print g a a print g a b print g b a -set::option lean::pp::coercion false +set_option lean::pp::coercion false variable S : Type variable s : S variable r : S variable h : S -> S -> S infixl 10 ++ : g infixl 10 ++ : h -set::option lean::pp::notation false +set_option lean::pp::notation false print a ++ b ++ a print r ++ s ++ r check a ++ b ++ a check r ++ s ++ r -set::option lean::pp::coercion true +set_option lean::pp::coercion true print a ++ b ++ a print r ++ s ++ r -set::option lean::pp::notation true +set_option lean::pp::notation true print a ++ b ++ a print r ++ s ++ r diff --git a/tests/lean/config.lean b/tests/lean/config.lean index f5980302c4..9a35fa712a 100644 --- a/tests/lean/config.lean +++ b/tests/lean/config.lean @@ -1,3 +1,3 @@ --- set::option default configuration for tests -set::option pp::colors false -set::option pp::unicode true +-- set_option default configuration for tests +set_option pp::colors false +set_option pp::unicode true diff --git a/tests/lean/disj1.lean.expected.out b/tests/lean/disj1.lean.expected.out index aac263c313..4ef5421c7e 100644 --- a/tests/lean/disj1.lean.expected.out +++ b/tests/lean/disj1.lean.expected.out @@ -3,4 +3,4 @@ Imported 'tactic' Proved: T1 Proved: T2 -theorem T2 (a b : Bool) (H : a ∨ b) : b ∨ a := or::elim H (λ H : a, or::intror b H) (λ H : b, or::introl H a) +theorem T2 (a b : Bool) (H : a ∨ b) : b ∨ a := or_elim H (λ H : a, or_intror b H) (λ H : b, or_introl H a) diff --git a/tests/lean/disjcases.lean b/tests/lean/disjcases.lean index 4cbe446dc1..81d8968c5d 100644 --- a/tests/lean/disjcases.lean +++ b/tests/lean/disjcases.lean @@ -2,9 +2,9 @@ variables a b c : Bool axiom H : a \/ b theorem T (a b : Bool) : a \/ b → b \/ a. - apply (or::elim H). - apply or::intror. + apply (or_elim H). + apply or_intror. exact. - apply or::introl. + apply or_introl. exact. done. \ No newline at end of file diff --git a/tests/lean/elab1.lean b/tests/lean/elab1.lean index f36ff722b1..762407cfef 100644 --- a/tests/lean/elab1.lean +++ b/tests/lean/elab1.lean @@ -15,13 +15,13 @@ check fun (A B : Type) (a : _) (b : _) (C : Type), my_eq C a b. variable a : Bool variable b : Bool variable H : a /\ b -theorem t1 : b := (fun H1, and::intro H1 (and::eliml H)). +theorem t1 : b := (fun H1, and_intro H1 (and_eliml H)). theorem t2 : a = b := trans (refl a) (refl b). check f Bool Bool. theorem pierce (a b : Bool) : ((a -> b) -> a) -> a := - λ H, or::elim (EM a) + λ H, or_elim (EM a) (λ H_a, H) (λ H_na, NotImp1 (MT H H_na)) diff --git a/tests/lean/elab1.lean.expected.out b/tests/lean/elab1.lean.expected.out index dc491adacd..351e678464 100644 --- a/tests/lean/elab1.lean.expected.out +++ b/tests/lean/elab1.lean.expected.out @@ -54,4 +54,4 @@ Failed to solve ?M::0 Bool Bool -Error (line: 25, pos: 19) unknown identifier 'EM' +Error (line: 25, pos: 18) unknown identifier 'EM' diff --git a/tests/lean/elab4.lean b/tests/lean/elab4.lean index 7463c13377..54b12ee959 100644 --- a/tests/lean/elab4.lean +++ b/tests/lean/elab4.lean @@ -8,5 +8,5 @@ variable R {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (forall x : A, B theorem R2 : forall (A1 A2 B1 B2 : Type) (H : (A1 -> B1) = (A2 -> B2)) (a : A1), B1 = B2 := fun A1 A2 B1 B2 H a, R H a -set::option pp::implicit true +set_option pp::implicit true print environment 7. diff --git a/tests/lean/elab5.lean b/tests/lean/elab5.lean index 2494e5028c..2435609661 100644 --- a/tests/lean/elab5.lean +++ b/tests/lean/elab5.lean @@ -8,5 +8,5 @@ variable R {A A' : Type} {B : A -> Type} {B' : A' -> Type} (H : (forall x : A, B theorem R2 : forall (A1 A2 B1 B2 : Type), ((A1 -> B1) = (A2 -> B2)) -> A1 -> (B1 = B2) := fun A1 A2 B1 B2 H a, R H a -set::option pp::implicit true +set_option pp::implicit true print environment 7. diff --git a/tests/lean/elab7.lean b/tests/lean/elab7.lean index b7dedc3a77..bc90085ba3 100644 --- a/tests/lean/elab7.lean +++ b/tests/lean/elab7.lean @@ -17,5 +17,5 @@ theorem T2 : (fun (x1 : A) (x2 : B), F1 x1 x2) = F2 := funext (fun a, (funext (f theorem T3 : F1 = (fun (x1 : A) (x2 : B), F2 x1 x2) := funext (fun a, (funext (fun b, H a b))) theorem T4 : (fun (x1 : A) (x2 : B), F1 x1 x2) = (fun (x1 : A) (x2 : B), F2 x1 x2) := funext (fun a, (funext (fun b, H a b))) print environment 4 -set::option pp::implicit true +set_option pp::implicit true print environment 4 \ No newline at end of file diff --git a/tests/lean/env_errors.lean b/tests/lean/env_errors.lean index fd677bee02..bb38e0d41f 100644 --- a/tests/lean/env_errors.lean +++ b/tests/lean/env_errors.lean @@ -1,7 +1,6 @@ - variable x : Nat -set::opaque x true. +set_opaque x true. print "before import" (* @@ -26,4 +25,3 @@ print "before load3" local env = get_environment() env:load("fake2.olean") *) - diff --git a/tests/lean/env_errors.lean.expected.out b/tests/lean/env_errors.lean.expected.out index 4f70b45e33..2f63bdc47d 100644 --- a/tests/lean/env_errors.lean.expected.out +++ b/tests/lean/env_errors.lean.expected.out @@ -1,12 +1,12 @@ Set: pp::colors Set: pp::unicode Assumed: x -Error (line: 4, pos: 0) set_opaque failed, 'x' is not a definition +Error (line: 3, pos: 0) set_opaque failed, 'x' is not a definition before import -Error (line: 12, pos: 0) file 'tstblafoo.lean' not found in the LEAN_PATH +Error (line: 11, pos: 0) file 'tstblafoo.lean' not found in the LEAN_PATH before load1 -Error (line: 18, pos: 0) failed to open file 'tstblafoo.lean' +Error (line: 17, pos: 0) failed to open file 'tstblafoo.lean' before load2 -Error (line: 24, pos: 0) corrupted binary file +Error (line: 23, pos: 0) corrupted binary file before load3 -Error (line: 30, pos: 0) file 'fake2.olean' does not seem to be a valid object Lean file +Error (line: 28, pos: 0) file 'fake2.olean' does not seem to be a valid object Lean file diff --git a/tests/lean/eq1.lean b/tests/lean/eq1.lean index 4f543346ef..5d3f426e6f 100644 --- a/tests/lean/eq1.lean +++ b/tests/lean/eq1.lean @@ -1,5 +1,5 @@ import Int. variable i : Int check i = 0 -set::option pp::coercion true +set_option pp::coercion true check i = 0 diff --git a/tests/lean/eq2.lean b/tests/lean/eq2.lean index cc1671051e..7d0b566e12 100644 --- a/tests/lean/eq2.lean +++ b/tests/lean/eq2.lean @@ -4,5 +4,5 @@ variable nil {A : Type} : List A variable cons {A : Type} (head : A) (tail : List A) : List A variable l : List Int. check l = nil. -set::option pp::implicit true +set_option pp::implicit true check l = nil. diff --git a/tests/lean/eq3.lean b/tests/lean/eq3.lean index 605b47339a..95e37cf596 100644 --- a/tests/lean/eq3.lean +++ b/tests/lean/eq3.lean @@ -7,5 +7,5 @@ variable v3 : Vector (0 + n) axiom H1 : v1 == v2 axiom H2 : v2 == v3 check htrans H1 H2 -set::option pp::implicit true +set_option pp::implicit true check htrans H1 H2 diff --git a/tests/lean/ex2.lean b/tests/lean/ex2.lean index 87662216eb..15656a7752 100644 --- a/tests/lean/ex2.lean +++ b/tests/lean/ex2.lean @@ -1,8 +1,8 @@ -- comment print true -set::option lean::pp::notation false +set_option lean::pp::notation false print true && false -set::option pp::unicode false +set_option pp::unicode false print true && false variable a : Bool variable a : Bool @@ -12,7 +12,7 @@ variable A : Type check a && A print environment 1 print options -set::option lean::p::notation true -set::option lean::pp::notation 10 -set::option lean::pp::notation true +set_option lean::p::notation true +set_option lean::pp::notation 10 +set_option lean::pp::notation true print a && b diff --git a/tests/lean/ex2.lean.expected.out b/tests/lean/ex2.lean.expected.out index 6ff1cac5b3..faa3e3168c 100644 --- a/tests/lean/ex2.lean.expected.out +++ b/tests/lean/ex2.lean.expected.out @@ -19,7 +19,7 @@ Arguments types: A : Type variable A : Type (lean::pp::notation := false, pp::unicode := false, pp::colors := false) -Error (line: 15, pos: 12) unknown option 'lean::p::notation', type 'Help Options.' for list of available options -Error (line: 16, pos: 31) invalid option value, given option is not an integer +Error (line: 15, pos: 11) unknown option 'lean::p::notation', type 'Help Options.' for list of available options +Error (line: 16, pos: 30) invalid option value, given option is not an integer Set: lean::pp::notation a /\ b diff --git a/tests/lean/ex3.lean b/tests/lean/ex3.lean index 9186daa05a..4e22291d39 100644 --- a/tests/lean/ex3.lean +++ b/tests/lean/ex3.lean @@ -5,5 +5,5 @@ variable a : T check myeq _ true a variable myeq2 {A:Type} (a b : A) : Bool infix 50 === : myeq2 -set::option lean::pp::implicit true +set_option lean::pp::implicit true check true === a \ No newline at end of file diff --git a/tests/lean/exists1.lean b/tests/lean/exists1.lean index ccee5ea9ff..d830f00ca5 100644 --- a/tests/lean/exists1.lean +++ b/tests/lean/exists1.lean @@ -2,5 +2,5 @@ import Int. variable a : Int variable P : Int -> Int -> Bool axiom H : P a a -theorem T : exists x : Int, P a a := exists::intro a H. +theorem T : exists x : Int, P a a := exists_intro a H. print environment 1. \ No newline at end of file diff --git a/tests/lean/exists1.lean.expected.out b/tests/lean/exists1.lean.expected.out index 93e414f680..7aae4efda0 100644 --- a/tests/lean/exists1.lean.expected.out +++ b/tests/lean/exists1.lean.expected.out @@ -5,4 +5,4 @@ Assumed: P Assumed: H Proved: T -theorem T : ∃ x : ℤ, P a a := exists::intro a H +theorem T : ∃ x : ℤ, P a a := exists_intro a H diff --git a/tests/lean/exists2.lean b/tests/lean/exists2.lean index 0b172240fe..aa6ad409cf 100644 --- a/tests/lean/exists2.lean +++ b/tests/lean/exists2.lean @@ -6,13 +6,13 @@ variable g : Int -> Int axiom H1 : P (f a (g a)) (f a (g a)) axiom H2 : P (f (g a) (g a)) (f (g a) (g a)) axiom H3 : P (f (g a) (g a)) (g a) -theorem T1 : exists x y : Int, P (f y x) (f y x) := exists::intro _ (exists::intro _ H1) -theorem T2 : exists x : Int, P (f x (g x)) (f x (g x)) := exists::intro _ H1 -theorem T3 : exists x : Int, P (f x x) (f x x) := exists::intro _ H2 -theorem T4 : exists x : Int, P (f (g a) x) (f x x) := exists::intro _ H2 -theorem T5 : exists x : Int, P x x := exists::intro _ H2 -theorem T6 : exists x y : Int, P x y := exists::intro _ (exists::intro _ H3) -theorem T7 : exists x : Int, P (f x x) x := exists::intro _ H3 -theorem T8 : exists x y : Int, P (f x x) y := exists::intro _ (exists::intro _ H3) +theorem T1 : exists x y : Int, P (f y x) (f y x) := exists_intro _ (exists_intro _ H1) +theorem T2 : exists x : Int, P (f x (g x)) (f x (g x)) := exists_intro _ H1 +theorem T3 : exists x : Int, P (f x x) (f x x) := exists_intro _ H2 +theorem T4 : exists x : Int, P (f (g a) x) (f x x) := exists_intro _ H2 +theorem T5 : exists x : Int, P x x := exists_intro _ H2 +theorem T6 : exists x y : Int, P x y := exists_intro _ (exists_intro _ H3) +theorem T7 : exists x : Int, P (f x x) x := exists_intro _ H3 +theorem T8 : exists x y : Int, P (f x x) y := exists_intro _ (exists_intro _ H3) print environment 8. \ No newline at end of file diff --git a/tests/lean/exists2.lean.expected.out b/tests/lean/exists2.lean.expected.out index 7f50c23f25..b4418fd8d0 100644 --- a/tests/lean/exists2.lean.expected.out +++ b/tests/lean/exists2.lean.expected.out @@ -16,11 +16,11 @@ Proved: T6 Proved: T7 Proved: T8 -theorem T1 : ∃ x y : ℤ, P (f y x) (f y x) := exists::intro (g a) (exists::intro a H1) -theorem T2 : ∃ x : ℤ, P (f x (g x)) (f x (g x)) := exists::intro a H1 -theorem T3 : ∃ x : ℤ, P (f x x) (f x x) := exists::intro (g a) H2 -theorem T4 : ∃ x : ℤ, P (f (g a) x) (f x x) := exists::intro (g a) H2 -theorem T5 : ∃ x : ℤ, P x x := exists::intro (f (g a) (g a)) H2 -theorem T6 : ∃ x y : ℤ, P x y := exists::intro (f (g a) (g a)) (exists::intro (g a) H3) -theorem T7 : ∃ x : ℤ, P (f x x) x := exists::intro (g a) H3 -theorem T8 : ∃ x y : ℤ, P (f x x) y := exists::intro (g a) (exists::intro (g a) H3) +theorem T1 : ∃ x y : ℤ, P (f y x) (f y x) := exists_intro (g a) (exists_intro a H1) +theorem T2 : ∃ x : ℤ, P (f x (g x)) (f x (g x)) := exists_intro a H1 +theorem T3 : ∃ x : ℤ, P (f x x) (f x x) := exists_intro (g a) H2 +theorem T4 : ∃ x : ℤ, P (f (g a) x) (f x x) := exists_intro (g a) H2 +theorem T5 : ∃ x : ℤ, P x x := exists_intro (f (g a) (g a)) H2 +theorem T6 : ∃ x y : ℤ, P x y := exists_intro (f (g a) (g a)) (exists_intro (g a) H3) +theorem T7 : ∃ x : ℤ, P (f x x) x := exists_intro (g a) H3 +theorem T8 : ∃ x y : ℤ, P (f x x) y := exists_intro (g a) (exists_intro (g a) H3) diff --git a/tests/lean/exists3.lean b/tests/lean/exists3.lean index 22f6cbbb04..6630b6b056 100644 --- a/tests/lean/exists3.lean +++ b/tests/lean/exists3.lean @@ -1,25 +1,25 @@ import Int. variable P : Int -> Int -> Bool -set::opaque exists false. +set_opaque exists false. theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) := fun a b, - not::not::elim (not::not::elim R1 a) b + not_not_elim (not_not_elim R1 a) b axiom Ax : forall x, exists y, P x y theorem T2 : exists x y, P x y := refute (fun R : not (exists x y, P x y), - let L1 : forall x y, not (P x y) := fun a b, (not::not::elim ((not::not::elim R) a)) b, + let L1 : forall x y, not (P x y) := fun a b, (not_not_elim ((not_not_elim R) a)) b, L2 : exists y, P 0 y := Ax 0 - in exists::elim L2 (fun (w : Int) (H : P 0 w), + in exists_elim L2 (fun (w : Int) (H : P 0 w), absurd H (L1 0 w))). theorem T3 (A : (Type U)) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y := refute (fun R : not (exists x y, P x y), let L1 : forall x y, not (P x y) := fun a b, - (not::not::elim ((not::not::elim R) a)) b, + (not_not_elim ((not_not_elim R) a)) b, L2 : exists y, P a y := H1 a - in exists::elim L2 (fun (w : A) (H : P a w), + in exists_elim L2 (fun (w : A) (H : P a w), absurd H (L1 a w))). diff --git a/tests/lean/exists4.lean b/tests/lean/exists4.lean index 887be720bd..a1dbeb15f7 100644 --- a/tests/lean/exists4.lean +++ b/tests/lean/exists4.lean @@ -3,14 +3,14 @@ variables a b c : N variables P : N -> N -> N -> Bool axiom H3 : P a b c -theorem T1 : exists x y z : N, P x y z := exists::@intro N (fun x : N, exists y z : N, P x y z) a - (exists::@intro N _ b - (exists::@intro N (fun z : N, P a b z) c H3)) +theorem T1 : exists x y z : N, P x y z := @exists_intro N (fun x : N, exists y z : N, P x y z) a + (@exists_intro N _ b + (@exists_intro N (fun z : N, P a b z) c H3)) -theorem T2 : exists x y z : N, P x y z := exists::intro a (exists::intro b (exists::intro c H3)) +theorem T2 : exists x y z : N, P x y z := exists_intro a (exists_intro b (exists_intro c H3)) -theorem T3 : exists x y z : N, P x y z := exists::intro _ (exists::intro _ (exists::intro _ H3)) +theorem T3 : exists x y z : N, P x y z := exists_intro _ (exists_intro _ (exists_intro _ H3)) -theorem T4 (H : P a a b) : exists x y z, P x y z := exists::intro _ (exists::intro _ (exists::intro _ H)) +theorem T4 (H : P a a b) : exists x y z, P x y z := exists_intro _ (exists_intro _ (exists_intro _ H)) print environment 4 \ No newline at end of file diff --git a/tests/lean/exists4.lean.expected.out b/tests/lean/exists4.lean.expected.out index 63c0c00698..c9cbd477e9 100644 --- a/tests/lean/exists4.lean.expected.out +++ b/tests/lean/exists4.lean.expected.out @@ -11,11 +11,11 @@ Proved: T3 Proved: T4 theorem T1 : ∃ x y z : N, P x y z := - exists::@intro + @exists_intro N (λ x : N, ∃ y z : N, P x y z) a - (exists::@intro N (λ y : N, ∃ z : N, P a y z) b (exists::@intro N (λ z : N, P a b z) c H3)) -theorem T2 : ∃ x y z : N, P x y z := exists::intro a (exists::intro b (exists::intro c H3)) -theorem T3 : ∃ x y z : N, P x y z := exists::intro a (exists::intro b (exists::intro c H3)) -theorem T4 (H : P a a b) : ∃ x y z : N, P x y z := exists::intro a (exists::intro a (exists::intro b H)) + (@exists_intro N (λ y : N, ∃ z : N, P a y z) b (@exists_intro N (λ z : N, P a b z) c H3)) +theorem T2 : ∃ x y z : N, P x y z := exists_intro a (exists_intro b (exists_intro c H3)) +theorem T3 : ∃ x y z : N, P x y z := exists_intro a (exists_intro b (exists_intro c H3)) +theorem T4 (H : P a a b) : ∃ x y z : N, P x y z := exists_intro a (exists_intro a (exists_intro b H)) diff --git a/tests/lean/exists5.lean b/tests/lean/exists5.lean index 44a71e9e80..1f4bf34a2c 100644 --- a/tests/lean/exists5.lean +++ b/tests/lean/exists5.lean @@ -2,6 +2,6 @@ variable N : Type variables a b c : N variables P : N -> N -> N -> Bool -theorem T1 (f : N -> N) (H : P (f a) b (f (f c))) : exists x y z, P x y z := exists::intro _ (exists::intro _ (exists::intro _ H)) +theorem T1 (f : N -> N) (H : P (f a) b (f (f c))) : exists x y z, P x y z := exists_intro _ (exists_intro _ (exists_intro _ H)) print environment 1. diff --git a/tests/lean/exists5.lean.expected.out b/tests/lean/exists5.lean.expected.out index 315e876378..58c5921a15 100644 --- a/tests/lean/exists5.lean.expected.out +++ b/tests/lean/exists5.lean.expected.out @@ -7,4 +7,4 @@ Assumed: P Proved: T1 theorem T1 (f : N → N) (H : P (f a) b (f (f c))) : ∃ x y z : N, P x y z := - exists::intro (f a) (exists::intro b (exists::intro (f (f c)) H)) + exists_intro (f a) (exists_intro b (exists_intro (f (f c)) H)) diff --git a/tests/lean/exists6.lean b/tests/lean/exists6.lean index 162520625c..0204a8c2bb 100644 --- a/tests/lean/exists6.lean +++ b/tests/lean/exists6.lean @@ -3,6 +3,6 @@ variable P : Int -> Int -> Int -> Bool axiom Ax1 : exists x y z, P x y z axiom Ax2 : forall x y z, not (P x y z) theorem T : false := - exists::elim Ax1 (fun a H1, exists::elim H1 (fun b H2, exists::elim H2 (fun (c : Int) (H3 : P a b c), + exists_elim Ax1 (fun a H1, exists_elim H1 (fun b H2, exists_elim H2 (fun (c : Int) (H3 : P a b c), let notH3 : not (P a b c) := Ax2 a b c in absurd H3 notH3))) diff --git a/tests/lean/exists7.lean b/tests/lean/exists7.lean index fe6b0ba965..116678c3b4 100644 --- a/tests/lean/exists7.lean +++ b/tests/lean/exists7.lean @@ -1,11 +1,11 @@ -set::option pp::colors false +set_option pp::colors false variable N : Type variables a b c : N variables P : N -> N -> N -> Bool -set::opaque exists false. -set::opaque not false. +set_opaque exists false. +set_opaque not false. -theorem T1 (f : N -> N) (H : P (f a) b (f (f c))) : exists x y z, P x y z := exists::intro _ (exists::intro _ (exists::intro _ H)) +theorem T1 (f : N -> N) (H : P (f a) b (f (f c))) : exists x y z, P x y z := exists_intro _ (exists_intro _ (exists_intro _ H)) print environment 1. diff --git a/tests/lean/exists7.lean.expected.out b/tests/lean/exists7.lean.expected.out index 7a003b38e9..1f98f86cc4 100644 --- a/tests/lean/exists7.lean.expected.out +++ b/tests/lean/exists7.lean.expected.out @@ -8,4 +8,4 @@ Assumed: P Proved: T1 theorem T1 (f : N → N) (H : P (f a) b (f (f c))) : ∃ x y z : N, P x y z := - exists::intro (f a) (exists::intro b (exists::intro (f (f c)) H)) + exists_intro (f a) (exists_intro b (exists_intro (f (f c)) H)) diff --git a/tests/lean/exists8.lean b/tests/lean/exists8.lean index 20cb0f461b..725cceaed9 100644 --- a/tests/lean/exists8.lean +++ b/tests/lean/exists8.lean @@ -3,22 +3,22 @@ variable P : Int -> Int -> Bool theorem T1 (R1 : not (exists x y, P x y)) : forall x y, not (P x y) := fun a b, - (not::exists::elim (not::exists::elim R1 a)) b + (not_exists_elim (not_exists_elim R1 a)) b axiom Ax : forall x, exists y, P x y theorem T2 : exists x y, P x y := refute (fun R : not (exists x y, P x y), let L1 : forall x y, not (P x y) := fun a b, - (not::exists::elim ((not::exists::elim R) a)) b, + (not_exists_elim ((not_exists_elim R) a)) b, L2 : exists y, P 0 y := Ax 0 - in exists::elim L2 (fun (w : Int) (H : P 0 w), + in exists_elim L2 (fun (w : Int) (H : P 0 w), absurd H (L1 0 w))). theorem T3 (A : (Type U)) (P : A -> A -> Bool) (a : A) (H1 : forall x, exists y, P x y) : exists x y, P x y := refute (fun R : not (exists x y, P x y), let L1 : forall x y, not (P x y) := fun a b, - (not::exists::elim ((not::exists::elim R) a)) b, + (not_exists_elim ((not_exists_elim R) a)) b, L2 : exists y, P a y := H1 a - in exists::elim L2 (fun (w : A) (H : P a w), + in exists_elim L2 (fun (w : A) (H : P a w), absurd H ((L1 a) w))). diff --git a/tests/lean/implicit1.lean b/tests/lean/implicit1.lean index a105760461..c067ef0488 100644 --- a/tests/lean/implicit1.lean +++ b/tests/lean/implicit1.lean @@ -6,7 +6,7 @@ print forall a b, f a b > 0 variable g : Int -> Real -> Int print forall a b, g a b > 0 print forall a b, g a (f a b) > 0 -set::option pp::coercion true +set_option pp::coercion true print forall a b, g a (f a b) > 0 print fun a, a + 1 print fun a b, a + b diff --git a/tests/lean/implicit2.lean b/tests/lean/implicit2.lean index 0f071888bd..b6fc8c1e77 100644 --- a/tests/lean/implicit2.lean +++ b/tests/lean/implicit2.lean @@ -8,6 +8,6 @@ check g 10 20 true check let r : Real -> Real -> Real := g 10 20 in r check g 10 -set::option pp::implicit true +set_option pp::implicit true check let r : Real -> Real -> Real := g 10 20 in r diff --git a/tests/lean/implicit3.lean b/tests/lean/implicit3.lean index b6e79879bd..6270f578bb 100644 --- a/tests/lean/implicit3.lean +++ b/tests/lean/implicit3.lean @@ -5,7 +5,7 @@ variable f : Int -> Int -> Int variable g : Int -> Int -> Int -> Int notation 10 _ ++ _ : f notation 10 _ ++ _ : g -set::option pp::implicit true -set::option pp::notation false +set_option pp::implicit true +set_option pp::notation false print (10 ++ 20) print (10 ++ 20) 10 diff --git a/tests/lean/implicit6.lean b/tests/lean/implicit6.lean index 6ebf3bee87..9776ad0f3a 100644 --- a/tests/lean/implicit6.lean +++ b/tests/lean/implicit6.lean @@ -4,8 +4,8 @@ infixl 65 + : f print true + false print 10 + 20 print 10 + (- 20) -set::option pp::notation false -set::option pp::coercion true +set_option pp::notation false +set_option pp::coercion true print true + false print 10 + 20 print 10 + (- 20) diff --git a/tests/lean/implicit7.lean b/tests/lean/implicit7.lean index d38a2a179a..b1f76468c1 100644 --- a/tests/lean/implicit7.lean +++ b/tests/lean/implicit7.lean @@ -4,9 +4,9 @@ notation 100 _ ; _ ; _ : f notation 100 _ ; _ ; _ : g check 10 ; true ; false check 10 ; 10 ; true -set::option pp::notation false +set_option pp::notation false check 10 ; true ; false check 10 ; 10 ; true -set::option pp::implicit true +set_option pp::implicit true check 10 ; true ; false check 10 ; 10 ; true diff --git a/tests/lean/induction1.lean b/tests/lean/induction1.lean index 72aaa9501f..7b32970ee3 100644 --- a/tests/lean/induction1.lean +++ b/tests/lean/induction1.lean @@ -10,14 +10,14 @@ theorem Comm1 : ∀ n m, n + m = m + n := Induction _ -- I use a placeholder because I do not want to write the P (λ m, -- Base case - calc 0 + m = m : add::zerol m - ... = m + 0 : symm (add::zeror m)) + calc 0 + m = m : add_zerol m + ... = m + 0 : symm (add_zeror m)) (λ n, -- Inductive case λ (iH : ∀ m, n + m = m + n), λ m, - calc n + 1 + m = (n + m) + 1 : add::succl n m + calc n + 1 + m = (n + m) + 1 : add_succl n m ... = (m + n) + 1 : { iH m } - ... = m + (n + 1) : symm (add::succr m n)) + ... = m + (n + 1) : symm (add_succr m n)) -- indunction on m @@ -25,13 +25,13 @@ theorem Comm2 : ∀ n m, n + m = m + n := λ n, Induction _ - (calc n + 0 = n : add::zeror n - ... = 0 + n : symm (add::zerol n)) + (calc n + 0 = n : add_zeror n + ... = 0 + n : symm (add_zerol n)) (λ m, λ (iH : n + m = m + n), - calc n + (m + 1) = (n + m) + 1 : add::succr n m + calc n + (m + 1) = (n + m) + 1 : add_succr n m ... = (m + n) + 1 : { iH } - ... = (m + 1) + n : symm (add::succl m n)) + ... = (m + 1) + n : symm (add_succl m n)) print environment 1 \ No newline at end of file diff --git a/tests/lean/induction1.lean.expected.out b/tests/lean/induction1.lean.expected.out index f7532df89b..e47a80122c 100644 --- a/tests/lean/induction1.lean.expected.out +++ b/tests/lean/induction1.lean.expected.out @@ -9,6 +9,6 @@ theorem Comm2 : ∀ n m : ℕ, n + m = m + n := λ n : ℕ, Induction (λ x : ℕ, n + x == x + n) - (Nat::add::zeror n ⋈ symm (Nat::add::zerol n)) + (Nat::add_zeror n ⋈ symm (Nat::add_zerol n)) (λ (m : ℕ) (iH : n + m = m + n), - Nat::add::succr n m ⋈ subst (refl (n + m + 1)) iH ⋈ symm (Nat::add::succl m n)) + Nat::add_succr n m ⋈ subst (refl (n + m + 1)) iH ⋈ symm (Nat::add_succl m n)) diff --git a/tests/lean/induction2.lean b/tests/lean/induction2.lean index 1febcba769..b8f4136e6f 100644 --- a/tests/lean/induction2.lean +++ b/tests/lean/induction2.lean @@ -10,9 +10,9 @@ theorem Comm1 : ∀ n m, n + m = m + n := Induction _ -- I use a placeholder because I do not want to write the P (λ m, -- Base case - calc 0 + m = m : add::zerol m - ... = m + 0 : symm (add::zeror m)) + calc 0 + m = m : add_zerol m + ... = m + 0 : symm (add_zeror m)) (λ n iH m, -- Inductive case - calc n + 1 + m = (n + m) + 1 : add::succl n m + calc n + 1 + m = (n + m) + 1 : add_succl n m ... = (m + n) + 1 : { iH } -- Error is here - ... = m + (n + 1) : symm (add::succr m n)) + ... = m + (n + 1) : symm (add_succr m n)) diff --git a/tests/lean/induction2.lean.expected.out b/tests/lean/induction2.lean.expected.out index c16f7e28c3..cc275e97ef 100644 --- a/tests/lean/induction2.lean.expected.out +++ b/tests/lean/induction2.lean.expected.out @@ -9,6 +9,6 @@ Failed to solve Induction with arguments: ?M::3 - λ m : ℕ, Nat::add::zerol m ⋈ symm (Nat::add::zeror m) + λ m : ℕ, Nat::add_zerol m ⋈ symm (Nat::add_zeror m) λ (n : ℕ) (iH : ?M::3 n) (m : ℕ), - Nat::add::succl n m ⋈ subst (refl (n + m + 1)) iH ⋈ symm (Nat::add::succr m n) + Nat::add_succl n m ⋈ subst (refl (n + m + 1)) iH ⋈ symm (Nat::add_succr m n) diff --git a/tests/lean/interactive/config.lean b/tests/lean/interactive/config.lean index f5980302c4..9a35fa712a 100644 --- a/tests/lean/interactive/config.lean +++ b/tests/lean/interactive/config.lean @@ -1,3 +1,3 @@ --- set::option default configuration for tests -set::option pp::colors false -set::option pp::unicode true +-- set_option default configuration for tests +set_option pp::colors false +set_option pp::unicode true diff --git a/tests/lean/interactive/t12.lean b/tests/lean/interactive/t12.lean index a56720c61f..0a77c70ab9 100644 --- a/tests/lean/interactive/t12.lean +++ b/tests/lean/interactive/t12.lean @@ -28,7 +28,7 @@ theorem T3 (A B : Bool) : A /\ B -> B /\ A := in _. conj_hyp. exact. done. conj_hyp. exact. done. - apply and::intro. exact. done. + apply and_intro. exact. done. theorem T4 (A B : Bool) : A /\ B -> B /\ A := fun assumption : A /\ B, diff --git a/tests/lean/interactive/t12.lean.expected.out b/tests/lean/interactive/t12.lean.expected.out index a895f6f3e4..68434ffe87 100644 --- a/tests/lean/interactive/t12.lean.expected.out +++ b/tests/lean/interactive/t12.lean.expected.out @@ -2,7 +2,7 @@ Set: pp::unicode Proved: T1 theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A := - let lemma1 : A := and::eliml assumption, lemma2 : B := and::elimr assumption in and::intro lemma2 lemma1 + let lemma1 : A := and_eliml assumption, lemma2 : B := and_elimr assumption in and_intro lemma2 lemma1 # Proof state: A : Bool, B : Bool, assumption : A ∧ B ⊢ A ## Proof state: diff --git a/tests/lean/interactive/t13.lean.expected.out b/tests/lean/interactive/t13.lean.expected.out index bb7cda099c..44d68d1e50 100644 --- a/tests/lean/interactive/t13.lean.expected.out +++ b/tests/lean/interactive/t13.lean.expected.out @@ -2,5 +2,5 @@ Set: pp::unicode Proved: T1 theorem T1 (A B : Bool) (assumption : A ∧ B) : B ∧ A := - let lemma1 := and::eliml assumption, lemma2 := and::elimr assumption in and::intro lemma2 lemma1 + let lemma1 := and_eliml assumption, lemma2 := and_elimr assumption in and_intro lemma2 lemma1 # \ No newline at end of file diff --git a/tests/lean/interactive/t3.lean.expected.out b/tests/lean/interactive/t3.lean.expected.out index 6a1df92848..be347473ae 100644 --- a/tests/lean/interactive/t3.lean.expected.out +++ b/tests/lean/interactive/t3.lean.expected.out @@ -12,5 +12,5 @@ a : Bool, b : Bool, H : b ⊢ b ## Proof state: no goals ## Proved: T2 -# theorem T2 (a b : Bool) (H : b) : a ∨ b := or::intror a H +# theorem T2 (a b : Bool) (H : b) : a ∨ b := or_intror a H # \ No newline at end of file diff --git a/tests/lean/interactive/t6.lean b/tests/lean/interactive/t6.lean index c4ff76e2bf..1211d45a55 100644 --- a/tests/lean/interactive/t6.lean +++ b/tests/lean/interactive/t6.lean @@ -1,5 +1,5 @@ (* import("tactic.lua") *) theorem T1 (a b : Bool) : a → b → a /\ b. - apply and::intro. + apply and_intro. exact. done. diff --git a/tests/lean/interactive/t8.lean b/tests/lean/interactive/t8.lean index f90c641f28..4083982d88 100644 --- a/tests/lean/interactive/t8.lean +++ b/tests/lean/interactive/t8.lean @@ -1,6 +1,6 @@ (* import("tactic.lua") *) -set::option tactic::proof_state::goal_names true. +set_option tactic::proof_state::goal_names true. theorem T (a : Bool) : a → a /\ a. - apply and::intro. + apply and_intro. exact. done. diff --git a/tests/lean/interactive/t9.lean b/tests/lean/interactive/t9.lean index f8da56ea96..f83b0d405a 100644 --- a/tests/lean/interactive/t9.lean +++ b/tests/lean/interactive/t9.lean @@ -12,7 +12,7 @@ theorem T1 (A B : Bool) : A /\ B → B /\ A := conj_hyp. exact. done. - apply and::intro. + apply and_intro. exact. done. diff --git a/tests/lean/let1.lean b/tests/lean/let1.lean index 8ad56a11d6..e988e596d3 100644 --- a/tests/lean/let1.lean +++ b/tests/lean/let1.lean @@ -6,5 +6,5 @@ check let a : Nat := 10 in a + 1 eval let a : Nat := 20 in a + 10 eval let a := 20 in a + 10 check let a : Int := 20 in a + 10 -set::option pp::coercion true +set_option pp::coercion true print let a : Int := 20 in a + 10 diff --git a/tests/lean/let2.lean b/tests/lean/let2.lean index cc10f337af..b923584cad 100644 --- a/tests/lean/let2.lean +++ b/tests/lean/let2.lean @@ -2,8 +2,8 @@ theorem simple (p q r : Bool) : (p → q) ∧ (q → r) → p → r := λ H_pq_qr H_p, - let P_pq : (p → q) := and::eliml H_pq_qr, - P_qr : (q → r) := and::elimr H_pq_qr, + let P_pq : (p → q) := and_eliml H_pq_qr, + P_qr : (q → r) := and_elimr H_pq_qr, P_q : q := P_pq H_p in P_qr P_q diff --git a/tests/lean/let2.lean.expected.out b/tests/lean/let2.lean.expected.out index a786aa1eea..587185a7cd 100644 --- a/tests/lean/let2.lean.expected.out +++ b/tests/lean/let2.lean.expected.out @@ -2,4 +2,4 @@ Set: pp::unicode Proved: simple theorem simple (p q r : Bool) (H_pq_qr : (p → q) ∧ (q → r)) (H_p : p) : r := - let P_pq : p → q := and::eliml H_pq_qr, P_qr : q → r := and::elimr H_pq_qr, P_q : q := P_pq H_p in P_qr P_q + let P_pq : p → q := and_eliml H_pq_qr, P_qr : q → r := and_elimr H_pq_qr, P_q : q := P_pq H_p in P_qr P_q diff --git a/tests/lean/let3.lean b/tests/lean/let3.lean index 857de32180..a6d7d62dec 100644 --- a/tests/lean/let3.lean +++ b/tests/lean/let3.lean @@ -2,8 +2,8 @@ import Int. variable magic : forall (H : Bool), H -set::option pp::notation false -set::option pp::coercion true +set_option pp::notation false +set_option pp::coercion true print let a : Int := 1, H : a > 0 := magic (a > 0) in H \ No newline at end of file diff --git a/tests/lean/let4.lean b/tests/lean/let4.lean index 8ce9363df9..b97e79608b 100644 --- a/tests/lean/let4.lean +++ b/tests/lean/let4.lean @@ -41,7 +41,7 @@ let a := 10, v2 : vector Int a := v1 in v2 -set::option pp::coercion true +set_option pp::coercion true print let a := 10, diff --git a/tests/lean/lua6.lean b/tests/lean/lua6.lean index 3745198afc..5f3bc1e5dc 100644 --- a/tests/lean/lua6.lean +++ b/tests/lean/lua6.lean @@ -1,6 +1,6 @@ import Int. variable x : Int -set::option pp::notation false +set_option pp::notation false (* print(get_options()) *) diff --git a/tests/lean/norm_bug1.lean b/tests/lean/norm_bug1.lean index 3e4c737bd4..71cac8fa1a 100644 --- a/tests/lean/norm_bug1.lean +++ b/tests/lean/norm_bug1.lean @@ -1,12 +1,12 @@ import cast -set::option pp::colors false +set_option pp::colors false check fun (A A': TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, - L3 : b == b' := cast::eq L2 b + L3 : b == b' := cast_eq L2 b in L3 check fun (A A': TypeM) @@ -18,10 +18,10 @@ check fun (A A': TypeM) (b : A') (H2 : f == g) (H3 : a == b), - let L1 : A == A' := type::eq H3, + let L1 : A == A' := type_eq H3, L2 : A' == A := symm L1, b' : A := cast L2 b, - L3 : b == b' := cast::eq L2 b, + L3 : b == b' := cast_eq L2 b, L4 : a == b' := htrans H3 L3, L5 : f a == f b' := congr2 f L4 in L5 diff --git a/tests/lean/norm_bug1.lean.expected.out b/tests/lean/norm_bug1.lean.expected.out index e44b52a128..88450f4e53 100644 --- a/tests/lean/norm_bug1.lean.expected.out +++ b/tests/lean/norm_bug1.lean.expected.out @@ -2,7 +2,7 @@ Set: pp::unicode Imported 'cast' Set: pp::colors -λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast::eq L2 b in L3 : +λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast_eq L2 b in L3 : ∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b λ (A A' : TypeM) (B : A → TypeM) @@ -13,10 +13,10 @@ (b : A') (H2 : f == g) (H3 : a == b), - let L1 : A == A' := type::eq H3, + let L1 : A == A' := type_eq H3, L2 : A' == A := symm L1, b' : A := cast L2 b, - L3 : b == b' := cast::eq L2 b, + L3 : b == b' := cast_eq L2 b, L4 : a == b' := htrans H3 L3, L5 : f a == f b' := congr2 f L4 in L5 : @@ -29,4 +29,4 @@ (b : A') (H2 : f == g) (H3 : a == b), - f a == f (cast (symm (type::eq H3)) b) + f a == f (cast (symm (type_eq H3)) b) diff --git a/tests/lean/norm_tac.lean b/tests/lean/norm_tac.lean index 63c436f527..49367f8701 100644 --- a/tests/lean/norm_tac.lean +++ b/tests/lean/norm_tac.lean @@ -1,8 +1,8 @@ import Int import tactic -set::option pp::implicit true -set::option pp::coercion true -set::option pp::notation false +set_option pp::implicit true +set_option pp::coercion true +set_option pp::notation false variable vector (A : Type) (sz : Nat) : Type variable read {A : Type} {sz : Nat} (v : vector A sz) (i : Nat) (H : i < sz) : A variable V1 : vector Int 10 diff --git a/tests/lean/overload1.lean b/tests/lean/overload1.lean index 1374ad19f4..e43be27344 100644 --- a/tests/lean/overload1.lean +++ b/tests/lean/overload1.lean @@ -4,7 +4,7 @@ variable g : N -> N -> N infixl 10 ++ : f infixl 10 ++ : g print true ++ false ++ true -set::option lean::pp::notation false +set_option lean::pp::notation false print true ++ false ++ true variable a : N variable b : N diff --git a/tests/lean/overload2.lean b/tests/lean/overload2.lean index d2c699feb8..08feb3d502 100644 --- a/tests/lean/overload2.lean +++ b/tests/lean/overload2.lean @@ -10,8 +10,8 @@ coercion t2r variable f : T -> R -> T variable a : T variable b : R -set::option lean::pp::coercion true -set::option lean::pp::notation false +set_option lean::pp::coercion true +set_option lean::pp::notation false print f a b print f b a variable g : R -> T -> R diff --git a/tests/lean/push.lean b/tests/lean/push.lean index 1387f97495..f90a58cca7 100644 --- a/tests/lean/push.lean +++ b/tests/lean/push.lean @@ -6,7 +6,7 @@ scope variables a b c : Int variable f : Int -> Int eval f a -pop::scope +pop_scope eval f a -- should produce an error @@ -15,8 +15,8 @@ print environment 1 scope infixl 100 ++ : Int::add check 10 ++ 20 -pop::scope +pop_scope check 10 ++ 20 -- should produce an error -pop::scope -- should produce an error \ No newline at end of file +pop_scope -- should produce an error \ No newline at end of file diff --git a/tests/lean/refute1.lean b/tests/lean/refute1.lean index 20c8cd9d7f..148af23d5d 100644 --- a/tests/lean/refute1.lean +++ b/tests/lean/refute1.lean @@ -1,3 +1,3 @@ variables a b : Bool axiom H : a /\ b -theorem T : a := refute (fun R, absurd (and::eliml H) R) +theorem T : a := refute (fun R, absurd (and_eliml H) R) diff --git a/tests/lean/showenv.l b/tests/lean/showenv.l index c18bd02aac..24df3df1fe 100644 --- a/tests/lean/showenv.l +++ b/tests/lean/showenv.l @@ -1,3 +1,3 @@ -set::option pp::colors false +set_option pp::colors false print "===BEGIN ENVIRONMENT===" print environment diff --git a/tests/lean/slow/config.lean b/tests/lean/slow/config.lean index f5980302c4..9a35fa712a 100644 --- a/tests/lean/slow/config.lean +++ b/tests/lean/slow/config.lean @@ -1,3 +1,3 @@ --- set::option default configuration for tests -set::option pp::colors false -set::option pp::unicode true +-- set_option default configuration for tests +set_option pp::colors false +set_option pp::unicode true diff --git a/tests/lean/slow/deep.lean b/tests/lean/slow/deep.lean index 3e03171b36..51f935b00d 100644 --- a/tests/lean/slow/deep.lean +++ b/tests/lean/slow/deep.lean @@ -3,6 +3,6 @@ definition f1 (f : Int -> Int) (x : Int) : Int := f (f (f (f x))) definition f2 (f : Int -> Int) (x : Int) : Int := f1 (f1 (f1 (f1 f))) x definition f3 (f : Int -> Int) (x : Int) : Int := f1 (f2 (f2 f)) x variable f : Int -> Int. -set::option pp::width 80. -set::option lean::pp::max_depth 2000. +set_option pp::width 80. +set_option lean::pp::max_depth 2000. eval f3 f 0. \ No newline at end of file diff --git a/tests/lean/subst.lean b/tests/lean/subst.lean index ac2c17e8dc..a9e5e414f2 100644 --- a/tests/lean/subst.lean +++ b/tests/lean/subst.lean @@ -4,7 +4,7 @@ variable n : Nat axiom H1 : a + a + a = 10 axiom H2 : a = n theorem T : a + n + a = 10 := subst H1 H2 -set::option pp::coercion true -set::option pp::notation false -set::option pp::implicit true +set_option pp::coercion true +set_option pp::notation false +set_option pp::implicit true print environment 1. diff --git a/tests/lean/tactic1.lean.expected.out b/tests/lean/tactic1.lean.expected.out index 4f3276d2bc..58f909e761 100644 --- a/tests/lean/tactic1.lean.expected.out +++ b/tests/lean/tactic1.lean.expected.out @@ -3,4 +3,4 @@ Assumed: p Assumed: q Assumed: r -theorem T1 (H : p) (H::1 : q) : p ∧ q := and::intro H H::1 +theorem T1 (H : p) (H::1 : q) : p ∧ q := and_intro H H::1 diff --git a/tests/lean/tactic10.lean.expected.out b/tests/lean/tactic10.lean.expected.out index 1d28c4c9ce..8e5b9f5789 100644 --- a/tests/lean/tactic10.lean.expected.out +++ b/tests/lean/tactic10.lean.expected.out @@ -5,4 +5,4 @@ Proved: T1 Defined: h Proved: T2 -theorem T2 (a b : Bool) (H : h a b) (H::1 : f b) : a := or::elim H (λ H : a, H) (λ H : b, absurd::elim a H H::1) +theorem T2 (a b : Bool) (H : h a b) (H::1 : f b) : a := or_elim H (λ H : a, H) (λ H : b, absurd_elim a H H::1) diff --git a/tests/lean/tactic2.lean b/tests/lean/tactic2.lean index 1ade0a10d2..007ff3c8d3 100644 --- a/tests/lean/tactic2.lean +++ b/tests/lean/tactic2.lean @@ -5,7 +5,7 @@ theorem T1 : p → q → p /\ q := (fun H1 H2, let H1 : p := _, H2 : q := _ - in and::intro H1 H2 + in and_intro H1 H2 ). exact -- solve first metavar done @@ -30,7 +30,7 @@ theorem T3 : p → p /\ q → r → q /\ r /\ p := _. print environment 1 theorem T4 : p → p /\ q → r → q /\ r /\ p := _. - Repeat (OrElse (apply and::intro) conj_hyp exact) + Repeat (OrElse (apply and_intro) conj_hyp exact) done -- Display proof term generated by previous tac -- diff --git a/tests/lean/tactic2.lean.expected.out b/tests/lean/tactic2.lean.expected.out index 642db319fc..438c013294 100644 --- a/tests/lean/tactic2.lean.expected.out +++ b/tests/lean/tactic2.lean.expected.out @@ -5,8 +5,8 @@ Assumed: r Proved: T1 Proved: T2 -theorem T2 (H : p) (H::1 : q) : p ∧ q ∧ p := and::intro H (and::intro H::1 H) +theorem T2 (H : p) (H::1 : q) : p ∧ q ∧ p := and_intro H (and_intro H::1 H) Proved: T3 -theorem T3 (H : p) (H::1 : p ∧ q) (H::2 : r) : q ∧ r ∧ p := and::intro (and::elimr H::1) (and::intro H::2 H) +theorem T3 (H : p) (H::1 : p ∧ q) (H::2 : r) : q ∧ r ∧ p := and_intro (and_elimr H::1) (and_intro H::2 H) Proved: T4 -theorem T4 (H : p) (H::1 : p ∧ q) (H::2 : r) : q ∧ r ∧ p := and::intro (and::elimr H::1) (and::intro H::2 H) +theorem T4 (H : p) (H::1 : p ∧ q) (H::2 : r) : q ∧ r ∧ p := and_intro (and_elimr H::1) (and_intro H::2 H) diff --git a/tests/lean/tactic3.lean.expected.out b/tests/lean/tactic3.lean.expected.out index bfcc442704..9f38123019 100644 --- a/tests/lean/tactic3.lean.expected.out +++ b/tests/lean/tactic3.lean.expected.out @@ -4,4 +4,4 @@ Assumed: q Assumed: r Proved: T1 -theorem T1 (H : p) (H::1 : p ∧ q) (H::2 : r) : q ∧ r ∧ p := and::intro (and::elimr H::1) (and::intro H::2 H) +theorem T1 (H : p) (H::1 : p ∧ q) (H::2 : r) : q ∧ r ∧ p := and_intro (and_elimr H::1) (and_intro H::2 H) diff --git a/tests/lean/tactic4.lean.expected.out b/tests/lean/tactic4.lean.expected.out index 8e9fca0329..b3572ed655 100644 --- a/tests/lean/tactic4.lean.expected.out +++ b/tests/lean/tactic4.lean.expected.out @@ -1,4 +1,4 @@ Set: pp::colors Set: pp::unicode Proved: T4 -theorem T4 (a b : Bool) (H : a) (H::1 : b) : a ∧ b := and::intro H H::1 +theorem T4 (a b : Bool) (H : a) (H::1 : b) : a ∧ b := and_intro H H::1 diff --git a/tests/lean/tactic5.lean.expected.out b/tests/lean/tactic5.lean.expected.out index 1f95d54122..f31926c27f 100644 --- a/tests/lean/tactic5.lean.expected.out +++ b/tests/lean/tactic5.lean.expected.out @@ -1,4 +1,4 @@ Set: pp::colors Set: pp::unicode Proved: T4 -theorem T4 (a b : Bool) (H : a) (H::1 : b) : a ∧ b ∧ a := and::intro H (and::intro H::1 H) +theorem T4 (a b : Bool) (H : a) (H::1 : b) : a ∧ b ∧ a := and_intro H (and_intro H::1 H) diff --git a/tests/lean/tactic6.lean b/tests/lean/tactic6.lean index c61e31265a..1a6121158d 100644 --- a/tests/lean/tactic6.lean +++ b/tests/lean/tactic6.lean @@ -1,14 +1,14 @@ (* import("tactic.lua") *) theorem T (a b c : Bool): a → b /\ c → c /\ a /\ b := _. conj_hyp - apply and::intro + apply and_intro (* Focus(Then(show_tac(), conj_tac(), show_tac(), assumption_tac()), 2) *) exact done theorem T2 (a b c : Bool): a → b /\ c → c /\ a /\ b := _. conj_hyp - apply and::intro + apply and_intro (* show_tac() *) (* Focus(Then(show_tac(), conj_tac(), Focus(assumption_tac(), 1)), 2) *) (* show_tac() *) diff --git a/tests/lean/tactic8.lean.expected.out b/tests/lean/tactic8.lean.expected.out index 2f702c1d26..0235df481a 100644 --- a/tests/lean/tactic8.lean.expected.out +++ b/tests/lean/tactic8.lean.expected.out @@ -1,4 +1,4 @@ Set: pp::colors Set: pp::unicode Proved: T -theorem T (a b : Bool) (H : a ∨ b) (H::1 : ¬ b) : a := or::elim H (λ H : a, H) (λ H : b, absurd::elim a H H::1) +theorem T (a b : Bool) (H : a ∨ b) (H::1 : ¬ b) : a := or_elim H (λ H : a, H) (λ H : b, absurd_elim a H H::1) diff --git a/tests/lean/tactic9.lean.expected.out b/tests/lean/tactic9.lean.expected.out index 3da17962ca..03a82a6542 100644 --- a/tests/lean/tactic9.lean.expected.out +++ b/tests/lean/tactic9.lean.expected.out @@ -2,4 +2,4 @@ Set: pp::unicode Defined: f Proved: T -theorem T (a b : Bool) (H : a ∨ b) (H::1 : f b) : a := or::elim H (λ H : a, H) (λ H : b, absurd::elim a H H::1) +theorem T (a b : Bool) (H : a ∨ b) (H::1 : f b) : a := or_elim H (λ H : a, H) (λ H : b, absurd_elim a H H::1) diff --git a/tests/lean/tst10.lean b/tests/lean/tst10.lean index f825b758d3..c0221bb8b4 100644 --- a/tests/lean/tst10.lean +++ b/tests/lean/tst10.lean @@ -1,6 +1,6 @@ variable a : Bool variable b : Bool --- and::introunctions +-- Conjunctions print a && b print a && b && a print a /\ b diff --git a/tests/lean/tst2.lean b/tests/lean/tst2.lean index 961ec465f7..f35c213c93 100644 --- a/tests/lean/tst2.lean +++ b/tests/lean/tst2.lean @@ -2,10 +2,10 @@ print options variable a : Bool variable b : Bool print a/\b -set::option lean::pp::notation false +set_option lean::pp::notation false print options print a/\b print environment 2 -set::option lean::pp::notation true +set_option lean::pp::notation true print options print a/\b diff --git a/tests/lean/tst3.lean b/tests/lean/tst3.lean index b2ee389bec..c2bd48ba5e 100644 --- a/tests/lean/tst3.lean +++ b/tests/lean/tst3.lean @@ -1,10 +1,10 @@ -set::option lean::parser::verbose false. +set_option lean::parser::verbose false. notation 10 if _ then _ : implies. print environment 1. print if true then false. variable a : Bool. print if true then if a then false. -set::option lean::pp::notation false. +set_option lean::pp::notation false. print if true then if a then false. variable A : Type. variable f : A -> A -> A -> Bool. @@ -14,29 +14,29 @@ variable c : A. variable d : A. variable e : A. print c |- d ; e. -set::option lean::pp::notation true. +set_option lean::pp::notation true. print c |- d ; e. variable fact : A -> A. notation 20 _ ! : fact. print c! !. -set::option lean::pp::notation false. +set_option lean::pp::notation false. print c! !. -set::option lean::pp::notation true. +set_option lean::pp::notation true. variable g : A -> A -> A. notation 30 [ _ ; _ ] : g print [c;d]. print [c ; [d;e] ]. -set::option lean::pp::notation false. +set_option lean::pp::notation false. print [c ; [d;e] ]. -set::option lean::pp::notation true. +set_option lean::pp::notation true. variable h : A -> A -> A. notation 40 _ << _ >> : h. print environment 1. print d << e >>. print [c ; d << e >> ]. -set::option lean::pp::notation false. +set_option lean::pp::notation false. print [c ; d << e >> ]. -set::option lean::pp::notation true. +set_option lean::pp::notation true. variable r : A -> A -> A. infixl 30 ++ : r. variable s : A -> A -> A. @@ -46,13 +46,13 @@ variable p1 : Bool. variable p2 : Bool. variable p3 : Bool. print p1 || p2 && p3. -set::option lean::pp::notation false. +set_option lean::pp::notation false. print c ** d ++ e ** c. print p1 || p2 && p3. -set::option lean::pp::notation true. +set_option lean::pp::notation true. print c = d || d = c. print not p1 || p2. print p1 && p3 || p2 && p3. -set::option lean::pp::notation false. +set_option lean::pp::notation false. print not p1 || p2. print p1 && p3 || p2 && p3. diff --git a/tests/lean/tst4.lean b/tests/lean/tst4.lean index 17f097cce7..93104e72c8 100644 --- a/tests/lean/tst4.lean +++ b/tests/lean/tst4.lean @@ -2,7 +2,7 @@ variable f {A : Type} (a b : A) : A variable N : Type variable n1 : N variable n2 : N -set::option lean::pp::implicit true +set_option lean::pp::implicit true print f n1 n2 print f (fun x : N -> N, x) (fun y : _, y) variable EqNice {A : Type} (lhs rhs : A) : Bool @@ -17,5 +17,5 @@ variable c : N variable g : N -> N axiom H1 : a = b && b = c theorem Pr : (g a) = (g c) := - congr (refl g) (trans (and::eliml H1) (and::elimr H1)) + congr (refl g) (trans (and_eliml H1) (and_elimr H1)) print environment 2 diff --git a/tests/lean/tst4.lean.expected.out b/tests/lean/tst4.lean.expected.out index e9365109c9..710e25d826 100644 --- a/tests/lean/tst4.lean.expected.out +++ b/tests/lean/tst4.lean.expected.out @@ -27,4 +27,4 @@ theorem Pr : @eq N (g a) (g c) := a c (@refl (N → N) g) - (@trans N a b c (and::@eliml (@eq N a b) (@eq N b c) H1) (and::@elimr (@eq N a b) (@eq N b c) H1)) + (@trans N a b c (@and_eliml (@eq N a b) (@eq N b c) H1) (@and_elimr (@eq N a b) (@eq N b c) H1)) diff --git a/tests/lean/tst5.lean b/tests/lean/tst5.lean index 0f1b6fa5c0..454055b2cf 100644 --- a/tests/lean/tst5.lean +++ b/tests/lean/tst5.lean @@ -4,7 +4,7 @@ variable a : N variable b : N print a = b check a = b -set::option lean::pp::implicit true +set_option lean::pp::implicit true print a = b print (Type 1) = (Type 1) print true = false diff --git a/tests/lean/tst6.lean b/tests/lean/tst6.lean index 2a100f81be..dc6d3eb663 100644 --- a/tests/lean/tst6.lean +++ b/tests/lean/tst6.lean @@ -5,54 +5,54 @@ theorem congrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h congr (congr (refl h) H1) H2 -- Display the theorem showing implicit arguments -set::option lean::pp::implicit true +set_option lean::pp::implicit true print environment 2 -- Display the theorem hiding implicit arguments -set::option lean::pp::implicit false +set_option lean::pp::implicit false print environment 2 theorem Example1 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) := - or::elim H + or_elim H (fun H1 : a = b ∧ b = c, - congrH (trans (and::eliml H1) (and::elimr H1)) (refl b)) + congrH (trans (and_eliml H1) (and_elimr H1)) (refl b)) (fun H1 : a = d ∧ d = c, - congrH (trans (and::eliml H1) (and::elimr H1)) (refl b)) + congrH (trans (and_eliml H1) (and_elimr H1)) (refl b)) -- print proof of the last theorem with all implicit arguments -set::option lean::pp::implicit true +set_option lean::pp::implicit true print environment 1 -- Using placeholders to hide the type of H1 theorem Example2 (a b c d : N) (H: (a = b ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) := - or::elim H + or_elim H (fun H1 : _, - congrH (trans (and::eliml H1) (and::elimr H1)) (refl b)) + congrH (trans (and_eliml H1) (and_elimr H1)) (refl b)) (fun H1 : _, - congrH (trans (and::eliml H1) (and::elimr H1)) (refl b)) + congrH (trans (and_eliml H1) (and_elimr H1)) (refl b)) -set::option lean::pp::implicit true +set_option lean::pp::implicit true print environment 1 -- Same example but the first conjuct has unnecessary stuff theorem Example3 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a b) = (h c b) := - or::elim H + or_elim H (fun H1 : _, - congrH (trans (and::eliml H1) (and::elimr (and::elimr H1))) (refl b)) + congrH (trans (and_eliml H1) (and_elimr (and_elimr H1))) (refl b)) (fun H1 : _, - congrH (trans (and::eliml H1) (and::elimr H1)) (refl b)) + congrH (trans (and_eliml H1) (and_elimr H1)) (refl b)) -set::option lean::pp::implicit false +set_option lean::pp::implicit false print environment 1 theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a c) = (h c a) := - or::elim H + or_elim H (fun H1 : _, - let AeqC := trans (and::eliml H1) (and::elimr (and::elimr H1)) + let AeqC := trans (and_eliml H1) (and_elimr (and_elimr H1)) in congrH AeqC (symm AeqC)) (fun H1 : _, - let AeqC := trans (and::eliml H1) (and::elimr H1) + let AeqC := trans (and_eliml H1) (and_elimr H1) in congrH AeqC (symm AeqC)) -set::option lean::pp::implicit false +set_option lean::pp::implicit false print environment 1 diff --git a/tests/lean/tst6.lean.expected.out b/tests/lean/tst6.lean.expected.out index 2d830f6fb8..157b2fd57d 100644 --- a/tests/lean/tst6.lean.expected.out +++ b/tests/lean/tst6.lean.expected.out @@ -13,57 +13,55 @@ theorem congrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : h a1 a2 = h b1 Proved: Example1 Set: lean::pp::implicit theorem Example1 (a b c d : N) (H : @eq N a b ∧ @eq N b c ∨ @eq N a d ∧ @eq N d c) : @eq N (h a b) (h c b) := - or::@elim - (@eq N a b ∧ @eq N b c) - (@eq N a d ∧ @eq N d c) - (h a b == h c b) - H - (λ H1 : @eq N a b ∧ @eq N b c, - @congrH a - b - c - b - (@trans N a b c (and::@eliml (@eq N a b) (@eq N b c) H1) (and::@elimr (@eq N a b) (@eq N b c) H1)) - (@refl N b)) - (λ H1 : @eq N a d ∧ @eq N d c, - @congrH a - b - c - b - (@trans N a d c (and::@eliml (@eq N a d) (@eq N d c) H1) (and::@elimr (@eq N a d) (@eq N d c) H1)) - (@refl N b)) + @or_elim (@eq N a b ∧ @eq N b c) + (@eq N a d ∧ @eq N d c) + (h a b == h c b) + H + (λ H1 : @eq N a b ∧ @eq N b c, + @congrH a + b + c + b + (@trans N a b c (@and_eliml (@eq N a b) (@eq N b c) H1) (@and_elimr (@eq N a b) (@eq N b c) H1)) + (@refl N b)) + (λ H1 : @eq N a d ∧ @eq N d c, + @congrH a + b + c + b + (@trans N a d c (@and_eliml (@eq N a d) (@eq N d c) H1) (@and_elimr (@eq N a d) (@eq N d c) H1)) + (@refl N b)) Proved: Example2 Set: lean::pp::implicit theorem Example2 (a b c d : N) (H : @eq N a b ∧ @eq N b c ∨ @eq N a d ∧ @eq N d c) : @eq N (h a b) (h c b) := - or::@elim - (@eq N a b ∧ @eq N b c) - (@eq N a d ∧ @eq N d c) - (@eq N (h a b) (h c b)) - H - (λ H1 : @eq N a b ∧ @eq N b c, - @congrH a - b - c - b - (@trans N a b c (and::@eliml (a == b) (@eq N b c) H1) (and::@elimr (@eq N a b) (b == c) H1)) - (@refl N b)) - (λ H1 : @eq N a d ∧ @eq N d c, - @congrH a - b - c - b - (@trans N a d c (and::@eliml (a == d) (@eq N d c) H1) (and::@elimr (@eq N a d) (d == c) H1)) - (@refl N b)) + @or_elim (@eq N a b ∧ @eq N b c) + (@eq N a d ∧ @eq N d c) + (@eq N (h a b) (h c b)) + H + (λ H1 : @eq N a b ∧ @eq N b c, + @congrH a + b + c + b + (@trans N a b c (@and_eliml (a == b) (@eq N b c) H1) (@and_elimr (@eq N a b) (b == c) H1)) + (@refl N b)) + (λ H1 : @eq N a d ∧ @eq N d c, + @congrH a + b + c + b + (@trans N a d c (@and_eliml (a == d) (@eq N d c) H1) (@and_elimr (@eq N a d) (d == c) H1)) + (@refl N b)) Proved: Example3 Set: lean::pp::implicit theorem Example3 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : h a b = h c b := - or::elim H - (λ H1 : a = b ∧ b = e ∧ b = c, congrH (and::eliml H1 ⋈ and::elimr (and::elimr H1)) (refl b)) - (λ H1 : a = d ∧ d = c, congrH (and::eliml H1 ⋈ and::elimr H1) (refl b)) + or_elim H + (λ H1 : a = b ∧ b = e ∧ b = c, congrH (and_eliml H1 ⋈ and_elimr (and_elimr H1)) (refl b)) + (λ H1 : a = d ∧ d = c, congrH (and_eliml H1 ⋈ and_elimr H1) (refl b)) Proved: Example4 Set: lean::pp::implicit theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : h a c = h c a := - or::elim H - (λ H1 : a = b ∧ b = e ∧ b = c, - let AeqC := and::eliml H1 ⋈ and::elimr (and::elimr H1) in congrH AeqC (symm AeqC)) - (λ H1 : a = d ∧ d = c, let AeqC := and::eliml H1 ⋈ and::elimr H1 in congrH AeqC (symm AeqC)) + or_elim H + (λ H1 : a = b ∧ b = e ∧ b = c, + let AeqC := and_eliml H1 ⋈ and_elimr (and_elimr H1) in congrH AeqC (symm AeqC)) + (λ H1 : a = d ∧ d = c, let AeqC := and_eliml H1 ⋈ and_elimr H1 in congrH AeqC (symm AeqC)) diff --git a/tests/lean/type_inf_bug1.lean b/tests/lean/type_inf_bug1.lean index e81e5a60c6..034596783a 100644 --- a/tests/lean/type_inf_bug1.lean +++ b/tests/lean/type_inf_bug1.lean @@ -1,12 +1,12 @@ import cast -set::option pp::colors false +set_option pp::colors false check fun (A A': TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, - L3 : b == b' := cast::eq L2 b + L3 : b == b' := cast_eq L2 b in L3 check fun (A A': TypeM) @@ -19,15 +19,15 @@ check fun (A A': TypeM) (H1 : (forall x : A, B x) == (forall x : A', B' x)) (H2 : f == g) (H3 : a == b), - let L1 : A == A' := type::eq H3, + let L1 : A == A' := type_eq H3, L2 : A' == A := symm L1, b' : A := cast L2 b, - L3 : b == b' := cast::eq L2 b, + L3 : b == b' := cast_eq L2 b, L4 : a == b' := htrans H3 L3, L5 : f a == f b' := congr2 f L4, S1 : (forall x : A', B' x) == (forall x : A, B x) := symm H1, g' : (forall x : A, B x) := cast S1 g, - L6 : g == g' := cast::eq S1 g, + L6 : g == g' := cast_eq S1 g, L7 : f == g' := htrans H2 L6, L8 : f b' == g' b' := congr1 b' L7, L9 : f a == g' b' := htrans L5 L8 diff --git a/tests/lean/type_inf_bug1.lean.expected.out b/tests/lean/type_inf_bug1.lean.expected.out index 4bb4b5dba2..83a7a90ef2 100644 --- a/tests/lean/type_inf_bug1.lean.expected.out +++ b/tests/lean/type_inf_bug1.lean.expected.out @@ -2,7 +2,7 @@ Set: pp::unicode Imported 'cast' Set: pp::colors -λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast::eq L2 b in L3 : +λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := cast_eq L2 b in L3 : ∀ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b λ (A A' : TypeM) (B : A → TypeM) @@ -14,15 +14,15 @@ (H1 : (∀ x : A, B x) == (∀ x : A', B' x)) (H2 : f == g) (H3 : a == b), - let L1 : A == A' := type::eq H3, + let L1 : A == A' := type_eq H3, L2 : A' == A := symm L1, b' : A := cast L2 b, - L3 : b == b' := cast::eq L2 b, + L3 : b == b' := cast_eq L2 b, L4 : a == b' := htrans H3 L3, L5 : f a == f b' := congr2 f L4, S1 : (∀ x : A', B' x) == (∀ x : A, B x) := symm H1, g' : ∀ x : A, B x := cast S1 g, - L6 : g == g' := cast::eq S1 g, + L6 : g == g' := cast_eq S1 g, L7 : f == g' := htrans H2 L6, L8 : f b' == g' b' := congr1 b' L7, L9 : f a == g' b' := htrans L5 L8 @@ -37,4 +37,4 @@ (H1 : (∀ x : A, B x) == (∀ x : A', B' x)) (H2 : f == g) (H3 : a == b), - f a == cast (symm H1) g (cast (symm (type::eq H3)) b) + f a == cast (symm H1) g (cast (symm (type_eq H3)) b) diff --git a/tests/lean/unicode.lean b/tests/lean/unicode.lean index c8287a5935..1c7b9b9b50 100644 --- a/tests/lean/unicode.lean +++ b/tests/lean/unicode.lean @@ -1,8 +1,8 @@ print true /\ false -set::option pp::unicode false +set_option pp::unicode false print true /\ false -set::option pp::unicode true -set::option lean::pp::notation false +set_option pp::unicode true +set_option lean::pp::notation false print true /\ false -set::option pp::unicode false +set_option pp::unicode false print true /\ false diff --git a/tests/lean/univ.lean b/tests/lean/univ.lean index 16397efc9c..f956c5ef9a 100644 --- a/tests/lean/univ.lean +++ b/tests/lean/univ.lean @@ -1,4 +1,3 @@ - universe M >= 1 universe U >= M + 1 definition TypeM := (Type M) @@ -18,7 +17,7 @@ scope env:get_universe_distance("Z", "U") + env:get_universe_distance("U", "M")) *) -pop::scope +pop_scope (* local env = get_environment() diff --git a/tests/lean/univ.lean.expected.out b/tests/lean/univ.lean.expected.out index 2b668484ba..7f48b94fc9 100644 --- a/tests/lean/univ.lean.expected.out +++ b/tests/lean/univ.lean.expected.out @@ -1,5 +1,5 @@ Set: pp::colors Set: pp::unicode Defined: TypeM -Error (line: 30, pos: 0) universe constraint produces an integer overflow: Z2 >= Z1 + 1073741824 -Error (line: 43, pos: 0) universe constraint inconsistency: U1 >= U4 + 0 +Error (line: 29, pos: 0) universe constraint produces an integer overflow: Z2 >= Z1 + 1073741824 +Error (line: 42, pos: 0) universe constraint inconsistency: U1 >= U4 + 0 diff --git a/tests/lua/env4.lua b/tests/lua/env4.lua index 06df329ff3..8fb58abc76 100644 --- a/tests/lua/env4.lua +++ b/tests/lua/env4.lua @@ -1,6 +1,7 @@ assert(not pcall(function() get_environment() end)) local env = environment() env:import("Int") +env:add_uvar_cnstr("M", level(level(), 1)) env:add_uvar_cnstr("Z", level(level("M"), 1)) assert(env:is_ge(level("Z"), level("M"))) local child = env:mk_child() diff --git a/tests/lua/front.lua b/tests/lua/front.lua index f230e11d75..26b595a4f7 100644 --- a/tests/lua/front.lua +++ b/tests/lua/front.lua @@ -10,8 +10,8 @@ variables i j : Int variables p q : Bool notation 100 _ ++ _ : f notation 100 _ ++ _ : g -set::option pp::colors true -set::option pp::width 300 +set_option pp::colors true +set_option pp::width 300 ]], env) print(get_options()) assert(get_options():get{"pp", "colors"}) diff --git a/tests/lua/parser2.lua b/tests/lua/parser2.lua index 3a238ccb2d..707c698217 100644 --- a/tests/lua/parser2.lua +++ b/tests/lua/parser2.lua @@ -4,14 +4,14 @@ parse_lean_cmds([[ variable N : Type variables x y : N variable f : N -> N -> N - set::option pp::colors false + set_option pp::colors false ]], env) local f, x, y = Consts("f, x, y") print(env:type_check(f(x, y))) assert(env:type_check(f(x, y)) == Const("N")) assert(not get_options():get{"pp", "colors"}) parse_lean_cmds([[ - set::option pp::colors true + set_option pp::colors true ]], env) assert(get_options():get{"pp", "colors"}) local o = get_options() @@ -19,7 +19,7 @@ o:update({"lean", "pp", "notation"}, false) assert(not o:get{"lean", "pp", "notation"}) o = parse_lean_cmds([[ check fun x : N, y - set::option pp::notation true + set_option pp::notation true check fun x : N, y ]], env, o) print(o)