fix(tests,doc): adjust tests and documentation

doc/lean/declarations.org

@@ -5,7 +5,7 @@
 The command =definition= declares a new constant/function. The identity function is defined as
 
 #+BEGIN_SRC lean
-  definition id {A : Type} (a : A) : A := a
+  definition identity {A : Type} (a : A) : A := a
 #+END_SRC
 
 We say definitions are "transparent", because the type checker can
@@ -21,13 +21,13 @@ _definitionally equal_.
   check λ (v : tuple nat (2+3)) (w : tuple nat 5), v = w
 #+END_SRC
 
-Similarly, the following definition only type checks because =id= is transparent, and the type checker can establish that
+Similarly, the following definition only type checks because =identity= is transparent, and the type checker can establish that
 =nat= and =id nat= are definitionally equal, that is, they are the "same".
 
 #+BEGIN_SRC lean
   import data.nat
-  definition id {A : Type} (a : A) : A := a
+  definition identity {A : Type} (a : A) : A := a
-  check λ (x : nat) (y : id nat), x = y
+  check λ (x : nat) (y : identity nat), x = y
 #+END_SRC
 
 ** Theorems
@@ -38,7 +38,7 @@ really care about the actual proof, only about its existence.  As
 described in previous sections, =Prop= (the type of all propositions)
 is _proof irrelevant_.  If we had defined =id= using a theorem the
 previous example would produce a typing error because the type checker
-would be unable to unfold =id= and establish that =nat= and =id nat=
+would be unable to unfold =identity= and establish that =nat= and =identity nat=
 are definitionally equal.
 
 ** Private definitions and theorems

doc/lean/reducible.org

@@ -64,13 +64,13 @@ the =attribute= command. The modification is saved in the
 produced .olean file.
 
 #+BEGIN_SRC lean
-  definition id (A : Type) (a : A) : A := a
+  definition identity (A : Type) (a : A) : A := a
   definition pr2 (A : Type) (a b : A) : A := b
   -- mark pr2 as reducible
   attribute pr2 [reducible]
   -- ...
   -- mark id and pr2 as irreducible
-  attribute id [irreducible]
+  attribute identity [irreducible]
   attribute pr2 [irreducible]
 #+END_SRC
 

doc/lean/tutorial.org

@@ -267,9 +267,9 @@ explicitly.
 #+BEGIN_SRC lean
   import logic
 
-  definition id.{l} {A : Type.{l}} (a : A) : A := a
+  definition identity.{l} {A : Type.{l}} (a : A) : A := a
 
-  check id true
+  check identity true
 #+END_SRC
 
 The universes can be explicitly provided for each constant and =Type=

tests/lean/550.lean.expected.out

@@ -3,36 +3,32 @@
 term
   linv
 has type
-  finv ∘ func = function.id
+  finv ∘ func = id
 but is expected to have type
-  x = function.id
+  x = id
 rewrite step failed using pattern
   finv_1 ∘ func_1
 proof state:
 A : Type,
 f : bijection A,
 func finv : A → A,
-linv : finv ∘ func = function.id,
+linv : finv ∘ func = id,
-rinv : func ∘ finv = function.id
+rinv : func ∘ finv = id
 ⊢ mk (finv ∘ func) (finv ∘ func)
     (eq.rec
-       (eq.rec
+       (eq.rec (eq.rec (eq.rec (eq.rec (eq.refl id) (eq.symm linv)) (eq.symm (compose.left_id func))) (eq.symm rinv))
-          (eq.rec (eq.rec (eq.rec (eq.refl function.id) (eq.symm linv)) (eq.symm (compose.left_id func)))
-             (eq.symm rinv))
           (function.compose.assoc func finv func))
        (eq.symm (function.compose.assoc finv func (finv ∘ func))))
     (eq.rec
-       (eq.rec
+       (eq.rec (eq.rec (eq.rec (eq.rec (eq.refl id) (eq.symm linv)) (eq.symm (compose.right_id finv))) (eq.symm rinv))
-          (eq.rec (eq.rec (eq.rec (eq.refl function.id) (eq.symm linv)) (eq.symm (compose.right_id finv)))
-             (eq.symm rinv))
           (eq.symm (function.compose.assoc finv func finv)))
        (function.compose.assoc (finv ∘ func) finv func)) = id
 550.lean:43:44: error: don't know how to synthesize placeholder
 A : Type,
 f : bijection A,
 func finv : A → A,
-linv : finv ∘ func = function.id,
+linv : finv ∘ func = id,
-rinv : func ∘ finv = function.id
+rinv : func ∘ finv = id
 ⊢ inv (mk func finv linv rinv) ∘b mk func finv linv rinv = id
 550.lean:43:2: error: failed to add declaration 'bijection.inv.linv' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term

tests/lean/abbrev1.lean

@@ -12,8 +12,8 @@ set_option pp.abbreviations true
 
 print definition tst
 
-abbreviation id [parsing_only] {A : Type} (a : A) := a
+abbreviation id2 [parsing_only] {A : Type} (a : A) := a
 
-definition tst1 :nat := id 10
+definition tst1 :nat := id2 10
 
 print definition tst1

tests/lean/ctxopt.lean

@@ -1,5 +1,5 @@
 import logic
-definition id {A : Type} (a : A) := a
+-- definition id {A : Type} (a : A) := a
 
 section
   set_option pp.implicit true

tests/lean/interactive/findp.input.expected.out

@@ -2,7 +2,10 @@
 -- ENDWAIT
 -- BEGINFINDP STALE
 false|Prop
+false_or|∀ (a : Prop), false ∨ a ↔ a
 false.rec|Π (C : Type), false → C
+false_iff|∀ (a : Prop), false ↔ a ↔ ¬a
+false_and|∀ (a : Prop), false ∧ a ↔ false
 false.elim|false → ?c
 false_of_ne|?a ≠ ?a → false
 false.rec_on|Π (C : Type), false → C
@@ -12,9 +15,11 @@ false.induction_on|∀ (C : Prop), false → C
 false_of_true_iff_false|(true ↔ false) → false
 true_ne_false|¬true = false
 nat.lt_self_iff_false|∀ (n : ℕ), n < n ↔ false
+iff_false|∀ (a : Prop), a ↔ false ↔ ¬a
 true_iff_false|true ↔ false ↔ false
 ne_self_iff_false|∀ (a : ?A), a ≠ a ↔ false
 not_of_is_false|is_false ?c → ¬?c
+or_false|∀ (a : Prop), a ∨ false ↔ a
 not_of_iff_false|(?a ↔ false) → ¬?a
 is_false|Π (c : Prop) [H : decidable c], Prop
 classical.eq_true_or_eq_false|∀ (a : Prop), a = true ∨ a = false
@@ -29,6 +34,8 @@ not_false_iff|¬false ↔ true
 of_not_is_false|¬is_false ?c → ?c
 classical.cases_true_false|∀ (P : Prop → Prop), P true → P false → (∀ (a : Prop), P a)
 iff_false_intro|¬?a → (?a ↔ false)
+and_false|∀ (a : Prop), a ∧ false ↔ false
+if_false|∀ (t e : ?A), ite false t e = e
 ne_false_of_self|?p → ?p ≠ false
 nat.succ_le_zero_iff_false|∀ (n : ℕ), nat.succ n ≤ 0 ↔ false
 tactic.exfalso|tactic

tests/lean/interactive/mod.input.expected.out

@@ -13,7 +13,7 @@ my_id2 : Π {A : Type}, A → A
 -- BEGINWAIT
 -- ENDWAIT
 -- BEGINEVAL
-EVAL_command:1:7: error: unknown identifier 'my_id'
+my_id : Π {A : Type}, A → A
 -- ENDEVAL
 -- BEGINEVAL
 my_id2 : Π {A : Type}, A → A

tests/lean/mismatch.lean

@@ -1,4 +1,4 @@
-definition id {A : Type} {a : A} := a
+-- definition id {A : Type} {a : A} := a
 definition o : num := 1
 
 check @id nat o

tests/lean/mismatch.lean.expected.out

@@ -1,5 +1,5 @@
 mismatch.lean:4:7: error: type mismatch at application
-  @id ℕ o
+  id o
 term
   o
 has type

tests/lean/param_binder_update.lean

@@ -3,7 +3,7 @@ section
 
   parameter A
 
-  definition id (a : A) := a
+  -- definition id (a : A) := a
 
   parameter {A}
 

tests/lean/param_binder_update.lean.expected.out

@@ -1,4 +1,4 @@
-id : Π (A : Type), A → A
+id : Π {A : Type}, A → A
 id₂ : Π {A : Type}, A → A
 foo1 : A → B → A
 foo2 : A → B → A

tests/lean/run/coe14.lean

@@ -21,10 +21,9 @@ check g (functor.to_fun f) 0
 
 check g f 0
 
-definition id (A : Type) (a : A) := a
 
 constant S : struct
 constant a : S
 
-check id (struct.to_sort S) a
+check @id (struct.to_sort S) a
-check id S a
+check @id S a

tests/lean/run/fold.lean

@@ -1,4 +1,4 @@
-definition id {A : Type} (a : A) := a
+-- definition id {A : Type} (a : A) := a
 
 example (a b c : nat) : id a = id b → a = b :=
 begin

tests/lean/run/id.lean

@@ -1,5 +1,5 @@
 import logic
-definition id {A : Type} (a : A) := a
+
 check id id
 set_option pp.universes true
 check id id

tests/lean/rw_set2.lean.expected.out

@@ -1,17 +1,47 @@
 simplification rules for iff
+#1, ?M_1 ↔ ?M_1 ↦ true
+#1, false ↔ ?M_1 ↦ ¬?M_1
+#1, ?M_1 ↔ false ↦ ¬?M_1
+#1, true ↔ ?M_1 ↦ ?M_1
+#1, ?M_1 ↔ true ↦ ?M_1
+#0, false ↔ true ↦ false
+#0, true ↔ false ↦ false
+#1, ?M_1 ↔ ¬?M_1 ↦ false
 #2, ?M_1 - ?M_2 ≤ ?M_1 ↦ true
 #1, 0 ≤ ?M_1 ↦ true
 #1, succ ?M_1 ≤ ?M_1 ↦ false
 #1, pred ?M_1 ≤ ?M_1 ↦ true
 #1, ?M_1 ≤ succ ?M_1 ↦ true
+#1, ?M_1 ∧ ?M_1 ↦ ?M_1
+#1, false ∧ ?M_1 ↦ false
+#1, ?M_1 ∧ false ↦ false
+#1, true ∧ ?M_1 ↦ ?M_1
+#1, ?M_1 ∧ true ↦ ?M_1
+#3 perm, ?M_1 ∧ ?M_2 ∧ ?M_3 ↦ ?M_2 ∧ ?M_1 ∧ ?M_3
+#3, (?M_1 ∧ ?M_2) ∧ ?M_3 ↦ ?M_1 ∧ ?M_2 ∧ ?M_3
+#2 perm, ?M_1 ∧ ?M_2 ↦ ?M_2 ∧ ?M_1
+#2, ?M_2 == ?M_2 ↦ true
 #2, ?M_1 - ?M_2 < succ ?M_1 ↦ true
 #1, ?M_1 < 0 ↦ false
 #1, ?M_1 < succ ?M_1 ↦ true
 #1, 0 < succ ?M_1 ↦ true
+#1, ?M_1 ∨ ?M_1 ↦ ?M_1
+#1, false ∨ ?M_1 ↦ ?M_1
+#1, ?M_1 ∨ false ↦ ?M_1
+#1, true ∨ ?M_1 ↦ true
+#1, ?M_1 ∨ true ↦ true
+#3 perm, ?M_1 ∨ ?M_2 ∨ ?M_3 ↦ ?M_2 ∨ ?M_1 ∨ ?M_3
+#3, (?M_1 ∨ ?M_2) ∨ ?M_3 ↦ ?M_1 ∨ ?M_2 ∨ ?M_3
+#2 perm, ?M_1 ∨ ?M_2 ↦ ?M_2 ∨ ?M_1
+#2, ?M_2 = ?M_2 ↦ true
+#0, ¬false ↦ true
+#0, ¬true ↦ false
 simplification rules for eq
 #1, g ?M_1 ↦ f ?M_1 + 1
 #2, g ?M_3 ↦ 1
 #2, f ?M_1 ↦ 0
+#3, ite false ?M_2 ?M_3 ↦ ?M_3
+#3, ite true ?M_2 ?M_3 ↦ ?M_2
 #4, ite ?M_1 ?M_4 ?M_4 ↦ ?M_4
 #1, 0 - ?M_1 ↦ 0
 #2, succ ?M_1 - succ ?M_2 ↦ ?M_1 - ?M_2

tests/lean/sec_param_pp.lean

@@ -2,17 +2,17 @@ section
  parameters {A : Type} (a : A)
  variable f : A → A → A
 
- definition id : A := a
+ definition id2 : A := a
- check id
+ check id2
 
 
  definition pr (b : A) : A := f a b
 
- check pr f id
+ check pr f id2
 
  set_option pp.universes true
 
- check pr f id
+ check pr f id2
 
  definition pr2 (B : Type) (b : B) : A := a
 

tests/lean/sec_param_pp.lean.expected.out

@@ -1,4 +1,4 @@
-id : A
+id2 : A
-pr f id : A
+pr f id2 : A
-pr f id : A
+pr f id2 : A
 pr2.{1} num 10 : A

tests/lean/sec_param_pp2.lean

@@ -6,12 +6,12 @@ section
 
    variable f : A → B → A
 
-   definition id := f a b
+   definition id2 := f a b
 
-   check id
+   check id2
    set_option pp.universes true
-   check id
+   check id2
  end
- check id
+ check id2
 end
-check id
+check id2

tests/lean/sec_param_pp2.lean.expected.out

@@ -1,4 +1,4 @@
-id : (A → B → A) → A
+id2 : (A → B → A) → A
-id : (A → B → A) → A
+id2 : (A → B → A) → A
-id.{l_2} : ?B a → (A → ?B a → A) → A
+id2.{l_2} : ?B a → (A → ?B a → A) → A
-id.{l_1 l_2} : ?A → (Π {B : Type.{l_2}}, B → (?A → B → ?A) → ?A)
+id2.{l_1 l_2} : ?A → (Π {B : Type.{l_2}}, B → (?A → B → ?A) → ?A)

tests/lean/simplifier6.lean

@@ -4,8 +4,8 @@ import logic.connectives logic.quantifiers
 namespace pi_congr1
 constants (p1 q1 p2 q2 p3 q3 : Prop) (H1 : p1 ↔ q1) (H2 : p2 ↔ q2) (H3 : p3 ↔ q3)
 
-attribute congr_forall [congr]
+attribute forall_congr [congr]
-attribute congr_imp    [congr]
+attribute imp_congr    [congr]
 attribute H1 [simp]
 attribute H2 [simp]
 attribute H3 [simp]
@@ -19,7 +19,7 @@ end pi_congr1
 namespace pi_congr2
 universe l
 constants (T : Type.{l}) (P Q : T → Prop) (H : ∀ (x : T), P x ↔ Q x)
-attribute congr_forall [congr]
+attribute forall_congr [congr]
 attribute H [simp]
 
 constant (x : T)

tests/lean/simplifier6.lean.expected.out

@@ -1,4 +1,4 @@
 H1
-congr_imp H1 H2
+imp_congr H1 H2
-congr_imp H1 (congr_imp H2 H3)
+imp_congr H1 (imp_congr H2 H3)
-congr_forall (λ (x : T), H x)
+forall_congr (λ (x : T), H x)

tests/lean/simplifier9.lean

@@ -1,8 +1,8 @@
 -- Rewriting with (tmp)-local hypotheses
 import logic.quantifiers
 
-attribute congr_imp [congr]
+attribute imp_congr [congr]
-attribute congr_forall [congr]
+attribute forall_congr [congr]
 
 universe l
 constants (T : Type.{l}) (P Q : T → Prop)

tests/lean/simplifier9.lean.expected.out

@@ -1,14 +1,14 @@
-x = y → y = y
+x = y → true
-T → x = y → y = y
+T → x = y → true
-∀ (x_1 : T), x = x_1 → x_1 = y
+∀ (a : T), x = a → a = y
-∀ (x_1 : T), x_1 = x → x = x
+∀ (a : T), a = x → true
-T → T → x = y → y = y
+T → T → x = y → true
 T → T → x = y → P y
 (∀ (x : T), P x ↔ Q x) → Q x
 Prop → (∀ (x : T), P x ↔ Q x) → Prop → Q x
-∀ (x_1 : Prop), (∀ (x : T), P x ↔ Q x) → x_1 ∨ Q x
+∀ (a : Prop), (∀ (x : T), P x ↔ Q x) → a ∨ Q x
 (∀ (x : T), P x ↔ Q x) → Q x
-∀ (x : T), T → (∀ (x : T), P x ↔ Q x) → Q x
+∀ (a : T), T → (∀ (x : T), P x ↔ Q x) → Q a
-∀ (x x_1 : T), x = x_1 → P x_1
+∀ (a a_1 : T), a = a_1 → P a_1
-∀ (x x_1 x_2 : T), x = x_1 → x_1 = x_2 → P x_2
+∀ (a a_1 a_2 : T), a = a_1 → a_1 = a_2 → P a_2
-∀ (x x_1 : T), x = x_1 → (∀ (w : T), P w ↔ Q w) → Q x_1
+∀ (a a_1 : T), a = a_1 → (∀ (w : T), P w ↔ Q w) → Q a_1

tests/lean/slow/path_groupoids.lean

@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jeremy Avigad
 -- Ported from Coq HoTT
-definition id {A : Type} (a : A) := a
+-- definition id {A : Type} (a : A) := a
 definition compose {A : Type} {B : Type} {C : Type} (g : B → C) (f : A → B) := λ x, g (f x)
 infixr ∘ := compose
 

tests/lean/unfoldf.lean

@@ -1,6 +1,6 @@
 open nat
 
-definition id [unfold_full] {A : Type} (a : A) := a
+-- definition id [unfold_full] {A : Type} (a : A) := a
 definition compose {A B C : Type} (g : B → C) (f : A → B) (a : A) := g (f a)
 notation g ∘ f := compose g f
 

tests/lean/univ.lean

@@ -1,19 +1,19 @@
 import data.num
 
-definition id (A : Type) (a : A) := a
+definition id2 (A : Type) (a : A) := a
 
-check id Type num
+check id2 Type num
 
-check id Type' num
+check id2 Type' num
 
-check id Type.{1} num
+check id2 Type.{1} num
 
-check id _ num
+check id2 _ num
 
-check id Type.{_+1} num
+check id2 Type.{_+1} num
 
-check id Type.{0+1} num
+check id2 Type.{0+1} num
 
-check id Type Type.{1}
+check id2 Type Type.{1}
 
-check id Type' Type.{1}
+check id2 Type' Type.{1}

tests/lean/univ.lean.expected.out

@@ -1,13 +1,13 @@
-univ.lean:5:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is
+univ.lean:5:10: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is
   Type₁
-univ.lean:7:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is
+univ.lean:7:10: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is
   Type₁
-id Type₁ num : Type₁
+id2 Type₁ num : Type₁
-id Type₁ num : Type₁
+id2 Type₁ num : Type₁
-univ.lean:13:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is
+univ.lean:13:10: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is
   Type₁
-id Type₁ num : Type₁
+id2 Type₁ num : Type₁
-univ.lean:17:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is
+univ.lean:17:10: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is
   Type₂
-univ.lean:19:9: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is
+univ.lean:19:10: error: solution computed by the elaborator forces a universe placeholder to be a fixed value, computed sort is
   Type₂

tests/lean/whnf_tac.lean

@@ -1,6 +1,6 @@
 import logic
 
-definition id {A : Type} (a : A) := a
+-- definition id {A : Type} (a : A) := a
 
 theorem tst (a : Prop) : a → id a :=
 begin