Upgrade to latest mathlib

leanpkg.toml

@@ -1,8 +1,8 @@
 [package]
 name = "lean-humanproof"
 version = "0.1"
-lean_version = "leanprover-community/lean:3.19.0"
+lean_version = "leanprover-community/lean:3.33.0"
 path = "src"
 
 [dependencies]
-mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "329393a78d910d4e347d2abe0905bd72bda9c2bf"}
+mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "075ff371481316d01bc4785d3f803af6f90a3171"}

src/basic/binder.lean

@@ -1,6 +1,10 @@
 /- © E.W.Ayers 2019 -/
 import meta.expr
 
+def binder_info.is_explicit : binder_info → bool
+| binder_info.default := tt
+| _ := ff
+
 namespace binder
 
 meta def push_local : binder → tactic.unsafe.type_context expr
@@ -25,4 +29,10 @@ meta def to_lam : binder → expr → expr
 meta def mk_local : binder → tactic expr
 | ⟨n, i, y⟩ := tactic.mk_local' n i y
 
+meta def is_explicit : binder → bool
+| ⟨n, i, y⟩ := i.is_explicit
+
+meta def mk_default : _root_.name → expr → binder
+| n y := ⟨n,binder_info.default,y⟩
+
 end binder

src/basic/pattern_table.lean

@@ -111,4 +111,7 @@ meta def get : pattern_table α → expr → tactic (list α)
 meta def of_list : list (entry α) → pattern_table α
 | l := list.foldr insert ∅ l
 
+meta instance pt_has_append : has_append (pattern_table α ) :=
+show has_append (listdict _ _), by apply_instance
+
 end pattern_table

src/basic/queue.lean

@@ -106,7 +106,7 @@ meta def dequeue : pqueue p → option (α × pqueue p)
 | pq := do
   q ← dict.min pq,
   (a,q) ← q.dequeue, -- should not be empty
-  if is_empty q then pure (a, dict.erase (p a) pq) else
+  if queue.is_empty q then pure (a, dict.erase (p a) pq) else
   pure (a, dict.insert (p a) q pq)
 
 meta def of_list : list α → pqueue p

src/basic/table.lean

@@ -91,23 +91,28 @@ namespace dict
     := rb_map.fold r l $ λ k a acc, acc.modify (λ o, option.rec_on o a $ merger k a) k
     meta instance : has_append (dict k α) := ⟨merge⟩
     meta def fold {β} (r : β → k → α → β) (z : β) (d : dict k α) : β := rb_map.fold d z (λ k a b, r b k a)
-    meta def mfold {T} [monad T] {β} (f : β → k → α → T β) (z : β) (d : dict k α) : T β := rb_map.mfold d z (λ k a b, f b k a)
+    meta def mfold {T} [monad T] {β} (f : β → k → α → T β) (z : β) (d : dict k α) : T β :=
+    rb_map.mfold d z (λ k a b, f b k a)
     meta def map {β} (f : α → β) (d : dict k α) : dict k β := rb_map.map f d
-    meta def filter (p : k → α → bool) (d : dict k α) := fold (λ d k a, if p k a then insert k a d else d) empty d
+    meta def filter (p : k → α → bool) (d : dict k α) :=
+    fold (λ d k a, if p k a then insert k a d else d) empty d
     meta def collect {β} (f : k → α → dict k β) := fold (λ d k a, d ++ f k a) empty
-    meta def choose {β} (f : k → α → option β) := fold (λ d k a, match f k a with (some b) := insert k b d | none := d end) empty
+    meta def choose {β} (f : k → α → option β) :=
+    fold (λ d k a, match f k a with (some b) := insert k b d | none := d end) empty
     meta def keys : dict k α → table k := fold (λ acc k v, table.insert k acc) ∅
     meta def to_list : dict k α → list (k×α) := rb_map.to_list
     meta def min : dict k α → option α := rb_map.min
     meta def max : dict k α → option α := rb_map.max
-    /--[HACK] not efficient, don't use in perf critical code. Use min.-/
-    meta def first : dict k α → option (k×α) := fold (λ o k a, option.rec_on o (some (k,a)) some) none
+    /--[HACK] not efficient. Use min if you don't need the key.-/
+    meta def first : dict k α → option (k×α) :=
+    fold (λ o k a, option.rec_on o (some (k,a)) some) none
     meta def any (f : k → α → bool) : dict k α → bool := fold (λ o k a, o || f k a) ff
     meta def all (f : k → α → bool) : dict k α → bool := fold (λ o k a, o && f k a) tt
     meta instance dict_has_union [has_union α] : has_union (dict k α) := ⟨dict.merge_with (λ _, (∪))⟩
     section formatting
         open format
-        meta instance [has_to_string α] [has_to_string k] : has_to_string (dict k α) := ⟨λ d,  (λ s, "{" ++ s ++ "}") $ list.to_string $ dict.to_list $ d⟩
+        meta instance [has_to_string α] [has_to_string k] : has_to_string (dict k α) :=
+        ⟨λ d,  (λ s, "{" ++ s ++ "}") $ list.to_string $ dict.to_list $ d⟩
         -- meta instance has_to_format [has_to_format α] [has_to_format k] : has_to_format (dict k α) := ⟨λ d,
         --     to_fmt "{" ++ group (nest 1 $ join $ list.intersperse ("," ++ line) $ list.map (λ (p:k×α), to_fmt p.1 ++ " ↦ " ++ to_fmt p.2) $ dict.to_list d) ++ to_fmt "}"
         -- ⟩
@@ -118,7 +123,7 @@ namespace dict
     end formatting
 end dict
 
-/--dictionary with a default if it doesn't exist. You define the default when you make the dictionary. -/
+/-- dictionary with a default if it doesn't exist. You define the default when you make the dictionary. -/
 meta structure dictd (k : Type) (α : Type) : Type :=
 (val : dict k α)
 (default : k → α)
@@ -128,7 +133,8 @@ namespace dictd
   meta instance [inhabited α] : has_emptyc (dictd k α) := ⟨empty (λ _, inhabited.default α)⟩
   meta def get (key : k) (dd : dictd k α) : α := dict.get_default (dd.2 key) key dd.1
   meta def insert (key : k) (a : α) (dd : dictd k α) : dictd k α := ⟨dict.insert key a dd.1, dd.2⟩
-  meta def modify (f : α → α) (key : k) (dd : dictd k α) : dictd k α := ⟨dict.modify (λ o, f $ option.get_or_else o (dd.2 key)) key dd.1, dd.2⟩
+  meta def modify (f : α → α) (key : k) (dd : dictd k α) : dictd k α :=
+  ⟨dict.modify (λ o, f $ option.get_or_else o (dd.2 key)) key dd.1, dd.2⟩
   meta def of_dict (default : k → α) : dict k α → dictd k α := λ d, ⟨d, default⟩
 end dictd
 
@@ -140,11 +146,16 @@ namespace tabledict
     variables {κ α : Type} [has_lt κ] [decidable_rel ((<) : κ → κ → Prop)] [has_lt α] [decidable_rel ((<) : α → α → Prop)]
     meta def empty : tabledict κ α := dict.empty
     meta instance : has_emptyc (tabledict κ α) := ⟨empty⟩
-    meta def insert : κ → α → tabledict κ α → tabledict κ α := λ k a d, dict.modify_default ∅ (λ t, t.insert a) k d
-    meta def erase : κ → α → tabledict κ α → tabledict κ α := λ k a d, dict.modify_when_present (λ t, t.erase a) k d
-    meta def get : κ → tabledict κ α → table α := λ k t, dict.get_default ∅ k t
-    meta def contains : κ → α → tabledict κ α → bool := λ k a d,  match dict.get k d with |(some t) := t.contains a | none := ff end
-    meta instance [has_to_tactic_format κ] [has_to_tactic_format α] : has_to_tactic_format (tabledict κ α) := ⟨λ (d : dict κ (table α)), tactic.pp d⟩
+    meta def insert : κ → α → tabledict κ α → tabledict κ α :=
+    λ k a d, dict.modify_default ∅ (λ t, t.insert a) k d
+    meta def erase : κ → α → tabledict κ α → tabledict κ α :=
+    λ k a d, dict.modify_when_present (λ t, t.erase a) k d
+    meta def get : κ → tabledict κ α → table α :=
+    λ k t, dict.get_default ∅ k t
+    meta def contains : κ → α → tabledict κ α → bool :=
+    λ k a d,  match dict.get k d with |(some t) := t.contains a | none := ff end
+    meta instance [has_to_tactic_format κ] [has_to_tactic_format α] : has_to_tactic_format (tabledict κ α) :=
+    ⟨λ (d : dict κ (table α)), tactic.pp d⟩
     meta def fold {β} (f : β → κ → α → β) : β → tabledict κ α → β := dict.fold (λ b k, table.fold (λ b, f b k) b)
     meta def mfold {T} [monad T] {β} (f : β → κ → α → T β) : β → tabledict κ α → T β := dict.mfold (λ b k, table.mfold (λ b, f b k) b)
     meta def to_list : tabledict κ α → list α := list.collect (table.to_list ∘ prod.snd) ∘ dict.to_list
@@ -161,7 +172,8 @@ namespace listdict
     meta instance : has_emptyc (listdict κ α) := ⟨empty⟩
     meta def insert : κ → α → listdict κ α → listdict κ α | k a d := dict.modify_default [] (λ t, a :: t) k d
     meta def inserts: κ → list α → listdict κ α → listdict κ α | k as d := dict.modify_default [] (λ t, as ++ t) k d
-    meta def pop : κ → listdict κ α → option (α × listdict κ α) | k d := match dict.get_default [] k d with |[] := none |(h::t) := some (h, dict.insert k t d)  end
+    meta def pop : κ → listdict κ α → option (α × listdict κ α) | k d :=
+    match dict.get_default [] k d with |[] := none |(h::t) := some (h, dict.insert k t d)  end
     meta def get : κ → listdict κ α → list α | k d := dict.get_default [] k d
     meta def fold {β} (f : β → κ → α → β) : β → listdict κ α → β := dict.fold (λ b k, list.foldl (λ b, f b k) b)
     meta def mfold {T} [monad T] {β} (f:β → κ → α → T β) : β → listdict κ α → T β := dict.mfold (λ b k, list.mfoldl (λ b, f b k) b)
@@ -170,9 +182,11 @@ namespace listdict
     meta instance has_pp [has_to_tactic_format κ] [has_to_tactic_format α] : has_to_tactic_format (listdict κ α) := ⟨λ (d : dict κ (list α)), tactic.pp d⟩
     meta def of : list (κ × list α) → listdict κ α := list.foldl (λ acc p, prod.rec inserts p acc) ∅
     meta def map {β} (f : α → β) : listdict κ α → listdict κ β := dict.map (list.map f)
+    meta def append : listdict κ α → listdict κ α → listdict κ α := dict.merge_with (λ k, (++))
+    meta instance ld_has_append : has_append (listdict κ α) := ⟨append⟩
 end listdict
 
-/--A table which tracks the number of times that a given key has been inserted. -/
+/-- A table which tracks the number of times that a given key has been inserted. -/
 meta def mtable (κ : Type) [has_lt κ] [decidable_rel ((<) : κ → κ → Prop)] : Type := dict κ ℕ
 
 namespace mtable

src/basic/tactic.lean

@@ -118,4 +118,10 @@ meta def with_state {α} : tactic_state → tactic α → tactic α
     write tso,
     pure a
 
+meta def return_except {α ε} [has_to_format ε] : except ε α → tactic α
+| (except.ok a) := pure a
+| (except.error e) := tactic.fail e
+
+
+
 end tactic

src/basic/telescope.lean

@@ -76,4 +76,23 @@ meta def to_cotelescope : telescope → cotelescope := list.reverse
 
 meta instance : has_coe telescope nat := ⟨list.length⟩
 
+meta def length : telescope → nat := list.length
+
+/-- Finds the index of the deepest binder that satisfies the given predicate.
+Note that the indexing scheme gives the shallowest binder the index zero. -/
+meta def find_index (predicate : binder → Prop) [decidable_pred predicate] : telescope → option ℕ
+| [] := none
+| (h :: t) := if predicate h then some t.length else find_index t
+
+
+meta def reverse_beta : telescope → expr → expr
+| Γ f := Γ.to_lams $ expr.mk_app f $ list.map expr.var $ list.reverse $ list.range Γ.length
+
 end telescope
+
+/-- Given a constant function name `f`, infers the type of `f` and returns `f` as a pi_type telescope. -/
+meta def tactic.fn_type_of_pis : name → tactic (telescope × expr)
+| n := do
+    f ← tactic.mk_const n,
+    y ← tactic.infer_type f,
+    pure $ telescope.of_pis y

src/examples/analysis.lean

@@ -9,6 +9,8 @@ class met_space (X : Type) extends has_dist X :=
 (dist_comm : ∀ x y, dist x y = dist y x)
 (dist_triangle : ∀ x y z, dist x z ≤ dist x y + dist y z)
 
+attribute [classnoun "metric space"] met_space
+
 open met_space
 
 variables {X Y: Type} [met_space X] [met_space Y] {A B : set X}
@@ -23,7 +25,6 @@ def is_uniform_limit (f : ℕ → X → Y) (g : X → Y) :=
 
 def continuous (f : X → Y) :=
 ∀ (x : X), ∀ (ε : ℝ), (ε > 0) → ∃ (δ : ℝ), (δ > 0) ∧ ∀ (y : X), dist x y < δ → dist (f x) (f y) < ε
-
 @[reducible]
 def sequence (X : Type) := ℕ → X
 

src/examples/groups.lean

@@ -1,4 +1,5 @@
 import group_theory.group_action group_theory.coset
+import hp.tactic.hp_interactive
 
 namespace examples
 
@@ -11,7 +12,8 @@ attribute [class] is_hom
 variables [is_hom f]
 lemma is_hom.one : f 1 = 1 :=
 begin
-  apply eq_one_of_mul_self_left_cancel,
+  apply mul_right_eq_self.1,
+  show (f 1) * (f 1) = (f 1),
   rw ←‹is_hom f›,
   simp,
 end
@@ -70,26 +72,29 @@ begin
                    ... = 1                 : by simp
 end
 
-#check subgroup.normal
-
 end
 
 section
 
 variables {G : Type} [group G]
-variables {H : subgroup G} {a b : G}
 
-#check left_coset
+lemma test_1 (x : G) : x = x :=
+begin [hp]
+
+end
+
+variables {H : subgroup G} {a b : G}
 
 lemma mem_own_left_coset : a ∈ left_coset a H :=
-begin
-  show ∃ (h : G), (h ∈ H) ∧ a * h = a,
-  use (1 : G),
-  split,
-  show (1 : G) ∈ H,
-    apply subgroup.one_mem,
-  show a * (1 : G) = a,
-    simp
+begin [hp]
+
+  -- show ∃ (h : G), (h ∈ H) ∧ a * h = a,
+  -- use (1 : G),
+  -- split,
+  -- show (1 : G) ∈ H,
+  --   apply subgroup.one_mem,
+  -- show a * (1 : G) = a,
+  --   simp
 end
 
 theorem G1 : (left_coset a H = left_coset b H) ↔ b⁻¹ * a ∈ H :=
@@ -133,19 +138,19 @@ end
 
 /- Every kernel is a normal subgroup -/
 
-def kernel {H G : Type} [group H] [group G] (f : H → G) [group_hom]
+-- def kernel {H G : Type} [group H] [group G] (f : H → G) [group_hom]
 
-example :
+-- example :
 
-/- This one is too classical.
+-- /- This one is too classical.
 
- -/
--- example : (¬ disjoint (left_coset a H) (left_coset b H)) → left_coset a H = left_coset b H :=
--- begin
---   intros h₁,
---   refine (G1 ).2 _,
---   apply set.disjoint.union_left
--- end
+--  -/
+-- -- example : (¬ disjoint (left_coset a H) (left_coset b H)) → left_coset a H = left_coset b H :=
+-- -- begin
+-- --   intros h₁,
+-- --   refine (G1 ).2 _,
+-- --   apply set.disjoint.union_left
+-- -- end
 
 end
 

src/hp/core/hyp.lean

@@ -4,7 +4,7 @@ namespace hp
 
 open tactic
 
-/-- Just a helper type for local_constant so I don't have to error handle all the time. -/
+/-- A helper type for local_constant. [todo] rename from hyp -/
 @[derive decidable_eq]
 meta structure hyp :=
 (uniq_name : name)

src/hp/core/labeller.lean

@@ -1,7 +1,28 @@
 import basic hp.core.source
 
-/- System for assigning labels to things that is not as bad as the built in one. -/
-
+/-! System for assigning labels to things.
+Labels are chosen from hard-coded sets of letters.
+Which set is used depends on the type of the thing being labelled.
+So for example a group element should be labelled with `g`, `h` etc
+but a point in a metric space should be labelled with `x`, `y` etc.
+
+[todo] Allow adding new suggested name lists with attributes.
+[todo] I think that a lot of non-humanproof tactics would benefit (in terms of user-friendliness) from
+using this kind of labelling system. Perhaps there is some way it can be integrated with Lean.
+
+# Labelling pools
+
+A labelling pool is a dictionary `string ⇀ list string` sending a key string to a set of possible labels.
+A labeller is defined by three pools:
+- Class pool: sending names of classes `𝒞` to labels for types `α` that are instances of `𝒞`.
+  For example a type `_ : Type` implementing `group _` should be labelled `G`.
+  If a class has multiple arguments, the first argument is always bound to.
+- Element pool: Suppose we have `α : Type` and `[𝒞 α]` for some typeclass `𝒞`, then the element pool contains labels for the elements of `α`.
+  For example, `{G : Type} [group G]` causes `_ : G` to be labelled `g` or `h`. While `[metric_space X]` will be labelled `x y : X`
+- Type pool: takes the function constant name of a type as the key and returns element names for that type.
+  Eg terms of type `set α` will be labelled `A`, `B` etc.
+
+-/
 namespace hp
 
 meta def labeller.pool := listdict string string
@@ -26,7 +47,7 @@ meta instance {n} {l : labeller} : decidable (n ∈ l) := by apply_instance
 
 meta def default_labels := ["x", "y", "z", "v", "w", "a", "b", "c"]
 
-meta def default_class_pool : listdict string string :=
+meta def default_class_pool : pool :=
 listdict.of [
   ("category", ["C", "D", "E"]),
   ("group", ["G", "H"]),

src/hp/core/proper.lean

@@ -151,6 +151,8 @@ meta def smallest_absent_composite_subterms (lhs : expr) (rhs : zipper) :=
 
 /-- The pretty printer will automatically instantiate vars which leads to an issue where
 earlier clauses will talk about variables that later get assigned.
+The 'dummifier' solves this by replacing instantiated metavariables with dummy undeclared
+variables before they are pretty printed.
 -/
 meta def dummify {α} [assignable α] : (expr × name) → α → tactic α
 | ⟨ms, n⟩ x := do
@@ -269,6 +271,7 @@ meta def get_distance (outer : expr) (l : expr) (r : expr) : tactic ℕ := do
 meta def get_proper_children (e : expr) : tactic (list expr) := do
     e ← tactic.instantiate_mvars e,
     (list.map cursor <$> prod.snd <$> (down_proper $ zip e)) <|> pure []
+
 meta def get_smallest_complex_subterms (z : zipper) : tactic (list zipper) := do
     minimal_monotone (λ z, do ⟨_,[]⟩ ← down_proper z | failure, pure z) z
 

src/hp/rewrite/equate_attr.lean

@@ -64,7 +64,7 @@ attribute [equate] mul_sub_right_distrib
 namespace set_rules
     universe u
     variables {α : Type u} {A B C : set α}
-    def ext : (∀ a, a ∈ A ↔ a ∈ B) → A = B := begin intro, funext, rw <-iff_eq_eq, apply a x end
+    def ext : (∀ a, a ∈ A ↔ a ∈ B) → A = B := begin intro h, funext, rw <-iff_eq_eq, apply h x end
     @[equate] def A1 : A \ B = A ∩ (Bᶜ) := begin refl end
     @[equate] def A2 : ( B ∩ C )ᶜ = Bᶜ ∪ Cᶜ := ext $ λ a, ⟨λ h, classical.by_cases (λ aB, classical.by_cases (λ aC, absurd (and.intro aB aC) h) or.inr ) or.inl,λ h, or.cases_on h (λ h ⟨ab,_⟩, absurd ab h) (λ h ⟨_,ac⟩, absurd ac h)⟩
     -- @[equate] def A3 :  - ( B ∪ C ) = - B ∩ - C := ext $ λ a, ⟨λ h, ⟨h ∘ or.inl,h ∘ or.inr⟩, λ ⟨x,y⟩ h₂, or.cases_on h₂ x y⟩