Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
chore(*): upgrade to Lean 3.27.0c (#6411)
Browse files Browse the repository at this point in the history


Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
  • Loading branch information
2 people authored and b-mehta committed Apr 2, 2021
1 parent 6835a81 commit 30865d9
Show file tree
Hide file tree
Showing 13 changed files with 28 additions and 22 deletions.
2 changes: 1 addition & 1 deletion leanpkg.toml
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
[package]
name = "mathlib"
version = "0.1"
lean_version = "leanprover-community/lean:3.26.0"
lean_version = "leanprover-community/lean:3.27.0"
path = "src"

[dependencies]
5 changes: 2 additions & 3 deletions src/algebraic_geometry/presheafed_space.lean
Original file line number Diff line number Diff line change
Expand Up @@ -225,9 +225,8 @@ def restrict_top_iso (X : PresheafedSpace C) :
dsimp only [nat_trans.comp_app, comp_c_app, of_restrict, to_restrict_top,
whisker_right_app, comp_base, nat_trans.op_app, opens.map_iso_inv_app],
erw [← X.presheaf.map_comp, ← X.presheaf.map_comp, ← X.presheaf.map_comp, id_c_app],
convert eq_to_hom_map X.presheaf _, swap,
{ erw [op_obj, id_base, opens.map_id_obj], refl },
{ refine has_hom.hom.unop_inj _, exact subsingleton.elim _ _ } } }
convert eq_to_hom_map X.presheaf _,
erw [op_obj, id_base, opens.map_id_obj], refl } }

/--
The global sections, notated Gamma.
Expand Down
6 changes: 6 additions & 0 deletions src/category_theory/opposites.lean
Original file line number Diff line number Diff line change
Expand Up @@ -406,6 +406,12 @@ rfl
lemma op_equiv_symm_apply (A B : Cᵒᵖ) (f : B.unop ⟶ A.unop) : (op_equiv _ _).symm f = f.op :=
rfl

instance subsingleton_of_unop (A B : Cᵒᵖ) [subsingleton (unop B ⟶ unop A)] : subsingleton (A ⟶ B) :=
(op_equiv A B).subsingleton

instance decidable_eq_of_unop (A B : Cᵒᵖ) [decidable_eq (unop B ⟶ unop A)] : decidable_eq (A ⟶ B) :=
(op_equiv A B).decidable_eq

universes v
variables {α : Type v} [preorder α]

Expand Down
4 changes: 2 additions & 2 deletions src/computability/language.lean
Original file line number Diff line number Diff line change
Expand Up @@ -204,11 +204,11 @@ begin
{ use 0,
tauto },
{ specialize ih _,
{ exact λ y hy, hS _ (list.mem_cons_of_mem _ hy) },
{ cases ih with i ih,
use i.succ,
rw [pow_succ, mem_mul],
exact ⟨ x, S.join, hS x (list.mem_cons_self _ _), ih, rfl ⟩ },
{ exact λ y hy, hS _ (list.mem_cons_of_mem _ hy) } } },
exact ⟨ x, S.join, hS x (list.mem_cons_self _ _), ih, rfl ⟩ } } },
{ rintro ⟨ i, hx ⟩,
induction i with i ih generalizing x,
{ rw [pow_zero, mem_one] at hx,
Expand Down
2 changes: 1 addition & 1 deletion src/computability/regular_expressions.lean
Original file line number Diff line number Diff line change
Expand Up @@ -228,9 +228,9 @@ begin
{ finish },
refine ⟨ t, U.join, by finish, _, _ ⟩,
{ specialize helem (b :: t) _,
{ finish },
rw rmatch at helem,
convert helem.2,
finish,
finish },
{ have hwf : U.join.length < (list.cons a x).length,
{ rw hsum,
Expand Down
4 changes: 2 additions & 2 deletions src/computability/tm_computable.lean
Original file line number Diff line number Diff line change
Expand Up @@ -74,15 +74,15 @@ end fin_tm2
def init_list (tm : fin_tm2) (s : list (tm.Γ tm.k₀)) : tm.cfg :=
{ l := option.some tm.main,
var := tm.initial_state,
stk := λ k, @dite (k = tm.k₀) (tm.K_decidable_eq k tm.k₀) (list (tm.Γ k))
stk := λ k, @dite (list (tm.Γ k)) (k = tm.k₀) (tm.K_decidable_eq k tm.k₀)
(λ h, begin rw h, exact s, end)
(λ _,[]) }

/-- The final configuration corresponding to a list in the output alphabet. -/
def halt_list (tm : fin_tm2) (s : list (tm.Γ tm.k₁)) : tm.cfg :=
{ l := option.none,
var := tm.initial_state,
stk := λ k, @dite (k = tm.k₁) (tm.K_decidable_eq k tm.k₁) (list (tm.Γ k))
stk := λ k, @dite (list (tm.Γ k)) (k = tm.k₁) (tm.K_decidable_eq k tm.k₁)
(λ h, begin rw h, exact s, end)
(λ _,[]) }

Expand Down
2 changes: 1 addition & 1 deletion src/data/polynomial/degree/definitions.lean
Original file line number Diff line number Diff line change
Expand Up @@ -215,7 +215,7 @@ coeff_eq_zero_of_nat_degree_lt (lt_add_one _)

-- We need the explicit `decidable` argument here because an exotic one shows up in a moment!
lemma ite_le_nat_degree_coeff (p : polynomial R) (n : ℕ) (I : decidable (n < 1 + nat_degree p)) :
@ite (n < 1 + nat_degree p) I _ (coeff p n) 0 = coeff p n :=
@ite _ (n < 1 + nat_degree p) I (coeff p n) 0 = coeff p n :=
begin
split_ifs,
{ refl },
Expand Down
2 changes: 1 addition & 1 deletion src/linear_algebra/dual.lean
Original file line number Diff line number Diff line change
Expand Up @@ -234,7 +234,7 @@ h.to_dual_apply_right i v
(h.dual_basis_is_basis.to_dual _).comp (h.to_dual B) = eval K V :=
begin
refine h.ext (λ i, h.dual_basis_is_basis.ext (λ j, _)),
suffices : @ite _ (classical.prop_decidable _) K 1 0 = @ite _ (de j i) K 1 0,
suffices : @ite K _ (classical.prop_decidable _) 1 0 = @ite K _ (de j i) 1 0,
by simpa [h.dual_basis_is_basis.to_dual_apply_left, h.dual_basis_repr, h.to_dual_apply_right],
split_ifs; refl
end
Expand Down
4 changes: 2 additions & 2 deletions src/tactic/split_ifs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,8 @@ open interactive
meta def find_if_cond : expr → option expr | e :=
e.fold none $ λ e _ acc, acc <|> do
c ← match e with
| `(@ite %%c %%_ _ _ _) := some c
| `(@dite %%c %%_ _ _ _) := some c
| `(@ite _ %%c %%_ _ _) := some c
| `(@dite _ %%c %%_ _ _) := some c
| _ := none
end,
guard ¬c.has_var,
Expand Down
2 changes: 1 addition & 1 deletion src/tactic/unfold_cases.lean
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,7 @@ namespace unfold_cases
(e.g. `whnf` or `dsimp`).
-/
meta def find_splitting_expr : expr → tactic expr
| `(@ite %%cond %%dec_inst _ _ _ = _) := pure `(@decidable.em %%cond %%dec_inst)
| `(@ite _ %%cond %%dec_inst _ _ = _) := pure `(@decidable.em %%cond %%dec_inst)
| `(%%(app x y) = _) := pure y
| e := fail!"expected an expression of the form: f x = y. Got:\n{e}"

Expand Down
4 changes: 2 additions & 2 deletions src/topology/locally_constant/basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -127,8 +127,8 @@ begin
suffices : x ∉ Uᶜ, from not_not.1 this,
intro hxV,
specialize hs U Uᶜ (hf {f y}) (hf {f y}ᶜ) _ ⟨y, ⟨hy, rfl⟩⟩ ⟨x, ⟨hx, hxV⟩⟩,
{ simpa only [inter_empty, not_nonempty_empty, inter_compl_self] using hs },
{ simp only [union_compl_self, subset_univ] }
{ simp only [union_compl_self, subset_univ] },
{ simpa only [inter_empty, not_nonempty_empty, inter_compl_self] using hs }
end

lemma iff_is_const [preconnected_space X] {f : X → Y} :
Expand Down
4 changes: 2 additions & 2 deletions src/topology/omega_complete_partial_order.lean
Original file line number Diff line number Diff line change
Expand Up @@ -68,10 +68,10 @@ begin
dsimp [is_open] at *,
apply complete_lattice.Sup_continuous' _,
introv ht, specialize h₀ { x | t x } _,
{ simpa using h₀ },
{ simp only [flip, set.mem_image] at *,
rcases ht with ⟨x,h₀,h₁⟩, subst h₁,
simpa, }
simpa, },
{ simpa using h₀ }
end

end Scott
Expand Down
9 changes: 5 additions & 4 deletions test/qpf.lean
Original file line number Diff line number Diff line change
Expand Up @@ -175,14 +175,15 @@ end
lemma supp_mk_tt' {α} (x : α) : qpf.supp' (foo.mk tt x) = {x} :=
begin
dsimp [qpf.supp'], ext, simp, dsimp [qpf.box], split; intro h,
{ specialize h {x} _, { simp at h, assumption },
clear h, introv hfg, simp, rw hfg, simp },
{ specialize h {x} _,
{ clear h, introv hfg, simp, rw hfg, simp },
{ simp at h, assumption }, },
{ introv hfg, subst x_1, classical,
let f : α → α ⊕ bool := λ x, if x ∈ i then sum.inl x else sum.inr tt,
let g : α → α ⊕ bool := λ x, if x ∈ i then sum.inl x else sum.inr ff,
specialize hfg _ f g _,
{ intros, simp [*,f,g,if_pos] },
{ simp [f,g] at hfg, split_ifs at hfg,
assumption, cases hfg },
{ intros, simp [*,f,g,if_pos] } }
assumption, cases hfg } }
end
end ex

0 comments on commit 30865d9

Please sign in to comment.