chore(library/init/core): declare and using structure

This change was requested by several users.

doc/changes.md

@@ -131,6 +131,12 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
 * `injection` and `injections` tactics generate fresh names when user does not provide names.
   The fresh names are of the form `h_<idx>`. See discussion [here](https://github.com/leanprover/lean/issues/1805).
 
+* Use `structure` to declare `and`. This change allows us to use `h.1` and `h.2` as shorthand for `h.left` and `h.right`.
+
+* Add attribute `[pp_using_anonymous_constructor]` to `and`. Now, `and.intro h1 h2` is pretty printed as
+  `⟨h1, h2⟩`. This change is motivated by the previous one. Without it, `and.intro h1 h2` would be
+  pretty printed as `{left := h1, right := h2}`.
+
 *API name changes*
 
 * `list.dropn` => `list.drop`

library/init/core.lean

@@ -146,18 +146,12 @@ structure prod (α : Type u) (β : Type v) :=
 structure pprod (α : Sort u) (β : Sort v) :=
 (fst : α) (snd : β)
 
-inductive and (a b : Prop) : Prop
-| intro : a → b → and
+structure and (a b : Prop) : Prop :=
+intro :: (left : a) (right : b)
 
-def and.elim_left {a b : Prop} (h : and a b) : a :=
-and.rec (λ ha hb, ha) h
+def and.elim_left {a b : Prop} (h : and a b) : a := h.1
 
-def and.left := @and.elim_left
-
-def and.elim_right {a b : Prop} (h : and a b) : b :=
-and.rec (λ ha hb, hb) h
-
-def and.right := @and.elim_right
+def and.elim_right {a b : Prop} (h : and a b) : b := h.2
 
 /- eq basic support -/
 
@@ -239,7 +233,7 @@ inductive bool : Type
 structure subtype {α : Sort u} (p : α → Prop) :=
 (val : α) (property : p val)
 
-attribute [pp_using_anonymous_constructor] sigma psigma subtype pprod
+attribute [pp_using_anonymous_constructor] sigma psigma subtype pprod and
 
 class inductive decidable (p : Prop)
 | is_false : ¬p → decidable

src/frontends/lean/structure_cmd.cpp

@@ -47,6 +47,7 @@ Author: Leonardo de Moura
 #include "library/constructions/projection.h"
 #include "library/constructions/no_confusion.h"
 #include "library/constructions/injective.h"
+#include "library/constructions/drec.h"
 #include "library/equations_compiler/util.h"
 #include "library/inductive_compiler/add_decl.h"
 #include "library/tactic/elaborator_exception.h"
@@ -1128,6 +1129,8 @@ struct structure_cmd_fn {
         name cases_on_name(m_name, "cases_on");
         add_rec_on_alias(cases_on_name);
         m_env = add_aux_recursor(m_env, cases_on_name);
+        if (is_inductive_predicate(m_env, m_name))
+            m_env = mk_drec(m_env, m_name);
     }
 
     // Return the parent names without namespace prefix

tests/lean/anc1.lean.expected.out

@@ -1,26 +1,24 @@
 (1, 2) : ℕ × ℕ
-and.intro trivial trivial : true ∧ true
+⟨trivial, trivial⟩ : true ∧ true
 anc1.lean:5:0: warning: declaration '[anonymous]' uses sorry
 ⟨1, _⟩ : Σ' (x : ℕ), x > 0
 show true, from true.intro : true
 Exists.intro 1 (id_locked (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0
-λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A, from and.intro Hb Ha :
+λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A, from ⟨Hb, Ha⟩ :
   ∀ (A B C : Prop), A → B → C → B ∧ A
-λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C),
-  show B ∧ A ∧ C ∧ A, from and.intro Hb (and.intro Ha (and.intro Hc Ha)) :
+λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A ∧ C ∧ A, from ⟨Hb, ⟨Ha, ⟨Hc, Ha⟩⟩⟩ :
+  ∀ (A B C : Prop), A → B → C → B ∧ A ∧ C ∧ A
+λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A ∧ C ∧ A, from ⟨Hb, ⟨Ha, ⟨Hc, Ha⟩⟩⟩ :
   ∀ (A B C : Prop), A → B → C → B ∧ A ∧ C ∧ A
 λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C),
-  show B ∧ A ∧ C ∧ A, from and.intro Hb (and.intro Ha (and.intro Hc Ha)) :
-  ∀ (A B C : Prop), A → B → C → B ∧ A ∧ C ∧ A
-λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C),
-  show ((B ∧ true) ∧ A) ∧ C ∧ A, from and.intro (and.intro (and.intro Hb true.intro) Ha) (and.intro Hc Ha) :
+  show ((B ∧ true) ∧ A) ∧ C ∧ A, from ⟨⟨⟨Hb, true.intro⟩, Ha⟩, ⟨Hc, Ha⟩⟩ :
   ∀ (A B C : Prop), A → B → C → ((B ∧ true) ∧ A) ∧ C ∧ A
 λ (A : Type u) (P Q : A → Prop) (a : A) (H1 : P a) (H2 : Q a),
-  show ∃ (x : A), P x ∧ Q x, from Exists.intro a (and.intro H1 H2) :
+  show ∃ (x : A), P x ∧ Q x, from Exists.intro a ⟨H1, H2⟩ :
   ∀ (A : Type u) (P Q : A → Prop) (a : A), P a → Q a → (∃ (x : A), P x ∧ Q x)
 λ (A : Type u) (P Q : A → Prop) (a b : A) (H1 : P a) (H2 : Q b),
-  show ∃ (x y : A), P x ∧ Q y, from Exists.intro a (Exists.intro b (and.intro H1 H2)) :
+  show ∃ (x y : A), P x ∧ Q y, from Exists.intro a (Exists.intro b ⟨H1, H2⟩) :
   ∀ (A : Type u) (P Q : A → Prop) (a b : A), P a → Q b → (∃ (x y : A), P x ∧ Q y)
 λ (A : Type u) (P Q : A → Prop) (a b : A) (H1 : P a) (H2 : Q b),
-  show ∃ (x y : A), P x ∧ Q y, from Exists.intro a (Exists.intro b (and.intro H1 H2)) :
+  show ∃ (x y : A), P x ∧ Q y, from Exists.intro a (Exists.intro b ⟨H1, H2⟩) :
   ∀ (A : Type u) (P Q : A → Prop) (a b : A), P a → Q b → (∃ (x y : A), P x ∧ Q y)

tests/lean/cases_induction_fresh.lean.expected.out

@@ -1,25 +1,25 @@
 p q r s : Prop,
-a : p,
-a_1 : q,
-a_2 : r,
-a_3 : s
+left : p,
+right : q,
+left_1 : r,
+right_1 : s
 ⊢ s ∧ q
 p q r s : Prop,
-a : p,
-a_2 : q,
-a_1 : r,
-a_3 : s
+left : p,
+right : q,
+left_1 : r,
+right_1 : s
 ⊢ s ∧ q
 ------------
 p q r s : Prop,
-a : p,
-a_1 : q,
-a_2 : r,
-a_3 : s
+left : p,
+right : q,
+left_1 : r,
+right_1 : s
 ⊢ s ∧ q
 p q r s : Prop,
-a : p,
-a_2 : q,
-a_1 : r,
-a_3 : s
+left : p,
+right : q,
+left_1 : r,
+right_1 : s
 ⊢ s ∧ q

tests/lean/interactive/rb_map_ts.lean.expected.out

@@ -1,7 +1,7 @@
 {"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"}],"response":"all_messages"}
-{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":77,"file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"}
-{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":77,"file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":81,"severity":"information","text":"test\n"}],"response":"all_messages"}
-{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":77,"file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":81,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":10,"end_pos_line":89,"file_name":"f","pos_col":0,"pos_line":89,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":77,"file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":77,"file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":81,"severity":"information","text":"test\n"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":66,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":0,"end_pos_line":77,"file_name":"f","pos_col":0,"pos_line":75,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":81,"severity":"information","text":"test\n"},{"caption":"print result","end_pos_col":10,"end_pos_line":89,"file_name":"f","pos_col":0,"pos_line":89,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), ⟨a, a_1⟩"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"record":{"source":,"state":"Custom state: ⟨x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p ∧ q","tactic_params":["(string)"],"text":"trace","type":"string → mytac unit"},"response":"ok","seq_num":67}
 {"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":71}