From a26618e0f2dff4a7c2a2c8e9fda894cf9d037454 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 12 Oct 2014 13:06:00 -0700 Subject: [PATCH] feat(frontends/lean): add '[]' notation for marking arguments where class-instance resolution should be applied --- library/algebra/category/adjoint.lean | 5 ++ library/algebra/category/basic.lean | 2 +- library/algebra/category/constructions.lean | 4 +- library/algebra/category/morphism.lean | 66 ++++++++++----------- library/algebra/relation.lean | 10 ++-- library/data/list/basic.lean | 4 +- library/logic/axioms/hilbert.lean | 2 +- library/logic/axioms/piext.lean | 2 +- library/logic/decidable.lean | 12 ++-- library/logic/identities.lean | 20 +++---- library/logic/if.lean | 14 ++--- library/logic/inhabited.lean | 2 +- library/logic/instances.lean | 4 +- library/logic/quantifiers.lean | 4 +- src/frontends/lean/elaborator.cpp | 45 +++++++++----- src/frontends/lean/elaborator.h | 2 +- src/frontends/lean/parser.cpp | 6 +- src/frontends/lean/pp.cpp | 8 +-- src/frontends/lean/server.cpp | 2 +- src/kernel/expr.cpp | 5 +- src/kernel/expr.h | 17 ++++-- src/library/kernel_bindings.cpp | 2 + src/library/kernel_serializer.cpp | 4 +- src/library/print.cpp | 4 +- tests/lean/cls_err.lean | 2 +- tests/lean/const.lean | 4 +- tests/lean/pp.lean.expected.out | 2 +- tests/lean/run/algebra1.lean | 4 +- tests/lean/run/class11.lean | 2 +- tests/lean/run/class5.lean | 2 +- tests/lean/run/elab_bug1.lean | 2 +- tests/lean/run/group2.lean | 2 +- tests/lean/run/group3.lean | 22 +++---- tests/lean/run/univ_bug2.lean | 2 +- 34 files changed, 162 insertions(+), 128 deletions(-) diff --git a/library/algebra/category/adjoint.lean b/library/algebra/category/adjoint.lean index b8b2fa735..ec6cb8c84 100644 --- a/library/algebra/category/adjoint.lean +++ b/library/algebra/category/adjoint.lean @@ -21,6 +21,11 @@ namespace adjoint variables {obC obD : Type} (C : category obC) {D : category obD} + variables (f : Cᵒᵖ ×c C ⇒ C ×c C) (g : C ×c C ⇒ C ×c C) + check g ∘f f + + check natural_transformation (Hom D) + definition adjoint (F : C ⇒ D) (G : D ⇒ C) := natural_transformation (@functor.compose _ _ _ _ _ _ (Hom D) sorry) --(Hom C ∘f sorry) diff --git a/library/algebra/category/basic.lean b/library/algebra/category/basic.lean index 33bfcda9d..84cf20719 100644 --- a/library/algebra/category/basic.lean +++ b/library/algebra/category/basic.lean @@ -17,7 +17,7 @@ mk : Π (hom : ob → ob → Type) category ob namespace category - variables {ob : Type} {C : category ob} + variables {ob : Type} [C : category ob] variables {a b c d : ob} include C definition hom [reducible] : ob → ob → Type := rec (λ hom compose id assoc idr idl, hom) C diff --git a/library/algebra/category/constructions.lean b/library/algebra/category/constructions.lean index f14930f31..efaf4a043 100644 --- a/library/algebra/category/constructions.lean +++ b/library/algebra/category/constructions.lean @@ -58,7 +58,7 @@ namespace category section open decidable unit empty - variables {A : Type} {H : decidable_eq A} + variables {A : Type} [H : decidable_eq A] include H definition set_hom (a b : A) := decidable.rec_on (H a b) (λh, unit) (λh, empty) theorem set_hom_subsingleton [instance] (a b : A) : subsingleton (set_hom a b) := _ @@ -71,7 +71,7 @@ namespace category (λh f, empty.rec _ f) f) (λh (g : empty), empty.rec _ g) g - definition set_category (A : Type) {H : decidable_eq A} : category A := + definition set_category (A : Type) [H : decidable_eq A] : category A := mk (λa b, set_hom a b) (λ a b c g f, set_compose g f) (λ a, rec_on_true rfl ⋆) diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean index c1ced7a9a..9f5334e48 100644 --- a/library/algebra/category/morphism.lean +++ b/library/algebra/category/morphism.lean @@ -8,7 +8,7 @@ open eq eq.ops category namespace morphism section - variables {ob : Type} {C : category ob} include C + variables {ob : Type} [C : category ob] include C variables {a b c d : ob} {h : @hom ob C c d} {g : @hom ob C b c} {f : @hom ob C a b} {i : @hom ob C b a} inductive is_section [class] (f : @hom ob C a b) : Type := mk : ∀{g}, g ∘ f = id → is_section f @@ -17,37 +17,37 @@ namespace morphism inductive is_iso [class] (f : @hom ob C a b) : Type := mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f --remove implicit arguments in above lines - definition retraction_of (f : hom a b) {H : is_section f} : hom b a := + definition retraction_of (f : hom a b) [H : is_section f] : hom b a := is_section.rec (λg h, g) H - definition section_of (f : hom a b) {H : is_retraction f} : hom b a := + definition section_of (f : hom a b) [H : is_retraction f] : hom b a := is_retraction.rec (λg h, g) H - definition inverse (f : hom a b) {H : is_iso f} : hom b a := + definition inverse (f : hom a b) [H : is_iso f] : hom b a := is_iso.rec (λg h1 h2, g) H postfix `⁻¹` := inverse - theorem inverse_compose (f : hom a b) {H : is_iso f} : f⁻¹ ∘ f = id := + theorem inverse_compose (f : hom a b) [H : is_iso f] : f⁻¹ ∘ f = id := is_iso.rec (λg h1 h2, h1) H - theorem compose_inverse (f : hom a b) {H : is_iso f} : f ∘ f⁻¹ = id := + theorem compose_inverse (f : hom a b) [H : is_iso f] : f ∘ f⁻¹ = id := is_iso.rec (λg h1 h2, h2) H - theorem retraction_compose (f : hom a b) {H : is_section f} : retraction_of f ∘ f = id := + theorem retraction_compose (f : hom a b) [H : is_section f] : retraction_of f ∘ f = id := is_section.rec (λg h, h) H - theorem compose_section (f : hom a b) {H : is_retraction f} : f ∘ section_of f = id := + theorem compose_section (f : hom a b) [H : is_retraction f] : f ∘ section_of f = id := is_retraction.rec (λg h, h) H - theorem iso_imp_retraction [instance] (f : hom a b) {H : is_iso f} : is_section f := + theorem iso_imp_retraction [instance] (f : hom a b) [H : is_iso f] : is_section f := is_section.mk !inverse_compose - theorem iso_imp_section [instance] (f : hom a b) {H : is_iso f} : is_retraction f := + theorem iso_imp_section [instance] (f : hom a b) [H : is_iso f] : is_retraction f := is_retraction.mk !compose_inverse theorem id_is_iso [instance] : is_iso (ID a) := is_iso.mk !id_compose !id_compose - theorem inverse_is_iso [instance] (f : a ⟶ b) {H : is_iso f} : is_iso (f⁻¹) := + theorem inverse_is_iso [instance] (f : a ⟶ b) [H : is_iso f] : is_iso (f⁻¹) := is_iso.mk !compose_inverse !inverse_compose theorem left_inverse_eq_right_inverse {f : hom a b} {g g' : hom b a} @@ -59,30 +59,30 @@ namespace morphism ... = id ∘ g' : {Hl} ... = g' : !id_left - theorem retraction_eq_intro {H : is_section f} (H2 : f ∘ i = id) : retraction_of f = i + theorem retraction_eq_intro [H : is_section f] (H2 : f ∘ i = id) : retraction_of f = i := left_inverse_eq_right_inverse !retraction_compose H2 - theorem section_eq_intro {H : is_retraction f} (H2 : i ∘ f = id) : section_of f = i + theorem section_eq_intro [H : is_retraction f] (H2 : i ∘ f = id) : section_of f = i := symm (left_inverse_eq_right_inverse H2 !compose_section) - theorem inverse_eq_intro_right {H : is_iso f} (H2 : f ∘ i = id) : f⁻¹ = i + theorem inverse_eq_intro_right [H : is_iso f] (H2 : f ∘ i = id) : f⁻¹ = i := left_inverse_eq_right_inverse !inverse_compose H2 - theorem inverse_eq_intro_left {H : is_iso f} (H2 : i ∘ f = id) : f⁻¹ = i + theorem inverse_eq_intro_left [H : is_iso f] (H2 : i ∘ f = id) : f⁻¹ = i := symm (left_inverse_eq_right_inverse H2 !compose_inverse) - theorem section_eq_retraction (f : a ⟶ b) {Hl : is_section f} {Hr : is_retraction f} : + theorem section_eq_retraction (f : a ⟶ b) [Hl : is_section f] [Hr : is_retraction f] : retraction_of f = section_of f := retraction_eq_intro !compose_section - theorem section_retraction_imp_iso (f : a ⟶ b) {Hl : is_section f} {Hr : is_retraction f} + theorem section_retraction_imp_iso (f : a ⟶ b) [Hl : is_section f] [Hr : is_retraction f] : is_iso f := is_iso.mk (subst (section_eq_retraction f) (retraction_compose f)) (compose_section f) theorem inverse_unique (H H' : is_iso f) : @inverse _ _ _ _ f H = @inverse _ _ _ _ f H' := inverse_eq_intro_left !inverse_compose - theorem inverse_involutive (f : a ⟶ b) {H : is_iso f} : (f⁻¹)⁻¹ = f := + theorem inverse_involutive (f : a ⟶ b) [H : is_iso f] : (f⁻¹)⁻¹ = f := inverse_eq_intro_right !inverse_compose theorem retraction_of_id : retraction_of (ID a) = id := @@ -94,7 +94,7 @@ namespace morphism theorem iso_of_id : ID a⁻¹ = id := inverse_eq_intro_left !id_compose - theorem composition_is_section [instance] {Hf : is_section f} {Hg : is_section g} + theorem composition_is_section [instance] [Hf : is_section f] [Hg : is_section g] : is_section (g ∘ f) := is_section.mk (calc @@ -118,7 +118,7 @@ namespace morphism theorem composition_is_inverse [instance] (Hf : is_iso f) (Hg : is_iso g) : is_iso (g ∘ f) := !section_retraction_imp_iso - inductive isomorphic (a b : ob) : Type := mk : ∀(g : a ⟶ b) {H : is_iso g}, isomorphic a b + inductive isomorphic (a b : ob) : Type := mk : ∀(g : a ⟶ b) [H : is_iso g], isomorphic a b end -- remove namespace isomorphic @@ -150,12 +150,12 @@ namespace morphism inductive is_epi [class] (f : @hom ob C a b) : Prop := mk : (∀c (g h : hom b c), g ∘ f = h ∘ f → g = h) → is_epi f - theorem mono_elim {H : is_mono f} {g h : c ⟶ a} (H2 : f ∘ g = f ∘ h) : g = h + theorem mono_elim [H : is_mono f] {g h : c ⟶ a} (H2 : f ∘ g = f ∘ h) : g = h := is_mono.rec (λH3, H3 c g h H2) H - theorem epi_elim {H : is_epi f} {g h : b ⟶ c} (H2 : g ∘ f = h ∘ f) : g = h + theorem epi_elim [H : is_epi f] {g h : b ⟶ c} (H2 : g ∘ f = h ∘ f) : g = h := is_epi.rec (λH3, H3 c g h H2) H - theorem section_is_mono [instance] (f : hom a b) {H : is_section f} : is_mono f := + theorem section_is_mono [instance] (f : hom a b) [H : is_section f] : is_mono f := is_mono.mk (λ c g h H, calc @@ -167,7 +167,7 @@ namespace morphism ... = id ∘ h : {retraction_compose f} ... = h : !id_left) - theorem retraction_is_epi [instance] (f : hom a b) {H : is_retraction f} : is_epi f := + theorem retraction_is_epi [instance] (f : hom a b) [H : is_retraction f] : is_epi f := is_epi.mk (λ c g h H, calc @@ -184,13 +184,13 @@ namespace morphism theorem id_is_mono : is_mono (ID a) theorem id_is_epi : is_epi (ID a) - theorem composition_is_mono [instance] {Hf : is_mono f} {Hg : is_mono g} : is_mono (g ∘ f) := + theorem composition_is_mono [instance] [Hf : is_mono f] [Hg : is_mono g] : is_mono (g ∘ f) := is_mono.mk (λ d h₁ h₂ H, have H2 : g ∘ (f ∘ h₁) = g ∘ (f ∘ h₂), from symm (assoc g f h₁) ▸ symm (assoc g f h₂) ▸ H, mono_elim (mono_elim H2)) - theorem composition_is_epi [instance] {Hf : is_epi f} {Hg : is_epi g} : is_epi (g ∘ f) := + theorem composition_is_epi [instance] [Hf : is_epi f] [Hg : is_epi g] : is_epi (g ∘ f) := is_epi.mk (λ d h₁ h₂ H, have H2 : (h₁ ∘ g) ∘ f = (h₂ ∘ g) ∘ f, from assoc h₁ g f ▸ assoc h₂ g f ▸ H, @@ -202,11 +202,11 @@ namespace morphism namespace iso section - variables {ob : Type} {C : category ob} include C + variables {ob : Type} [C : category ob] include C variables {a b c d : ob} (f : @hom ob C b a) (r : @hom ob C c d) (q : @hom ob C b c) (p : @hom ob C a b) (g : @hom ob C d c) - variable {Hq : is_iso q} include Hq + variable [Hq : is_iso q] include Hq theorem compose_pV : q ∘ q⁻¹ = id := !compose_inverse theorem compose_Vp : q⁻¹ ∘ q = id := !inverse_compose theorem compose_V_pp : q⁻¹ ∘ (q ∘ p) = p := @@ -230,7 +230,7 @@ namespace morphism ... = f ∘ id : {inverse_compose q} ... = f : id_right f - theorem inv_pp {H' : is_iso p} : (q ∘ p)⁻¹ = p⁻¹ ∘ q⁻¹ := + theorem inv_pp [H' : is_iso p] : (q ∘ p)⁻¹ = p⁻¹ ∘ q⁻¹ := have H1 : (p⁻¹ ∘ q⁻¹) ∘ q ∘ p = p⁻¹ ∘ (q⁻¹ ∘ (q ∘ p)), from assoc (p⁻¹) (q⁻¹) (q ∘ p)⁻¹, have H2 : (p⁻¹) ∘ (q⁻¹ ∘ (q ∘ p)) = p⁻¹ ∘ p, from congr_arg _ (compose_V_pp q p), have H3 : p⁻¹ ∘ p = id, from inverse_compose p, @@ -241,9 +241,9 @@ namespace morphism -- (p⁻¹ ∘ (q⁻¹)) ∘ q ∘ p = p⁻¹ ∘ (q⁻¹ ∘ (q ∘ p)) : assoc (p⁻¹) (q⁻¹) (q ∘ p)⁻¹ -- ... = (p⁻¹) ∘ p : congr_arg (λx, p⁻¹ ∘ x) (compose_V_pp q p) -- ... = id : inverse_compose p) - theorem inv_Vp {H' : is_iso g} : (q⁻¹ ∘ g)⁻¹ = g⁻¹ ∘ q := inverse_involutive q ▸ inv_pp (q⁻¹) g - theorem inv_pV {H' : is_iso f} : (q ∘ f⁻¹)⁻¹ = f ∘ q⁻¹ := inverse_involutive f ▸ inv_pp q (f⁻¹) - theorem inv_VV {H' : is_iso r} : (q⁻¹ ∘ r⁻¹)⁻¹ = r ∘ q := inverse_involutive r ▸ inv_Vp q (r⁻¹) + theorem inv_Vp [H' : is_iso g] : (q⁻¹ ∘ g)⁻¹ = g⁻¹ ∘ q := inverse_involutive q ▸ inv_pp (q⁻¹) g + theorem inv_pV [H' : is_iso f] : (q ∘ f⁻¹)⁻¹ = f ∘ q⁻¹ := inverse_involutive f ▸ inv_pp q (f⁻¹) + theorem inv_VV [H' : is_iso r] : (q⁻¹ ∘ r⁻¹)⁻¹ = r ∘ q := inverse_involutive r ▸ inv_Vp q (r⁻¹) end section @@ -254,7 +254,7 @@ namespace morphism {g : @hom ob C d c} {h : @hom ob C c b} {x : @hom ob C b d} {z : @hom ob C a c} {y : @hom ob C d b} {w : @hom ob C c a} - variable {Hq : is_iso q} include Hq + variable [Hq : is_iso q] include Hq theorem moveR_Mp (H : y = q⁻¹ ∘ g) : q ∘ y = g := H⁻¹ ▸ compose_p_Vp q g theorem moveR_pM (H : w = f ∘ q⁻¹) : w ∘ q = f := H⁻¹ ▸ compose_pV_p f q diff --git a/library/algebra/relation.lean b/library/algebra/relation.lean index bda2e0bf7..b2d56b32c 100644 --- a/library/algebra/relation.lean +++ b/library/algebra/relation.lean @@ -26,7 +26,7 @@ namespace is_reflexive definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_reflexive R) : reflexive R := is_reflexive.rec (λu, u) C - definition infer ⦃T : Type⦄ (R : T → T → Prop) {C : is_reflexive R} : reflexive R := + definition infer ⦃T : Type⦄ (R : T → T → Prop) [C : is_reflexive R] : reflexive R := is_reflexive.rec (λu, u) C end is_reflexive @@ -40,7 +40,7 @@ namespace is_symmetric definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_symmetric R) : symmetric R := is_symmetric.rec (λu, u) C - definition infer ⦃T : Type⦄ (R : T → T → Prop) {C : is_symmetric R} : symmetric R := + definition infer ⦃T : Type⦄ (R : T → T → Prop) [C : is_symmetric R] : symmetric R := is_symmetric.rec (λu, u) C end is_symmetric @@ -54,7 +54,7 @@ namespace is_transitive definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_transitive R) : transitive R := is_transitive.rec (λu, u) C - definition infer ⦃T : Type⦄ (R : T → T → Prop) {C : is_transitive R} : transitive R := + definition infer ⦃T : Type⦄ (R : T → T → Prop) [C : is_transitive R] : transitive R := is_transitive.rec (λu, u) C end is_transitive @@ -107,7 +107,7 @@ namespace congruence rec (λu, u) C x y theorem infer {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop) - (f : T1 → T2) {C : congruence R1 R2 f} ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) := + (f : T1 → T2) [C : congruence R1 R2 f] ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) := rec (λu, u) C x y definition app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop} @@ -149,7 +149,7 @@ end congruence -- using congruence. theorem congruence_const [instance] {T2 : Type} (R2 : T2 → T2 → Prop) - {C : is_reflexive R2} ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) : + [C : is_reflexive R2] ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) : congruence R1 R2 (λu : T1, c) := congruence.const R2 (is_reflexive.app C) R1 c diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 49bbe3d2d..3fe07adbb 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -195,7 +195,7 @@ induction_on l from H3 ▸ rfl, !exists_intro (!exists_intro H4))) -definition mem.is_decidable [instance] {H : decidable_eq T} (x : T) (l : list T) : decidable (x ∈ l) := +definition mem.is_decidable [instance] (H : decidable_eq T) (x : T) (l : list T) : decidable (x ∈ l) := rec_on l (decidable.inr (iff.false_elim !mem.nil)) (take (h : T) (l : list T) (iH : decidable (x ∈ l)), @@ -223,7 +223,7 @@ rec_on l -- Find -- ---- section -variable {H : decidable_eq T} +variable [H : decidable_eq T] include H definition find (x : T) : list T → nat := diff --git a/library/logic/axioms/hilbert.lean b/library/logic/axioms/hilbert.lean index 90ee81068..23c0e2f65 100644 --- a/library/logic/axioms/hilbert.lean +++ b/library/logic/axioms/hilbert.lean @@ -38,7 +38,7 @@ nonempty_imp_inhabited (obtain w Hw, from H, nonempty.intro w) -- the Hilbert epsilon function -- ---------------------------- -opaque definition epsilon {A : Type} {H : nonempty A} (P : A → Prop) : A := +opaque definition epsilon {A : Type} [H : nonempty A] (P : A → Prop) : A := let u : {x : A, (∃y, P y) → P x} := strong_indefinite_description P H in elt_of u diff --git a/library/logic/axioms/piext.lean b/library/logic/axioms/piext.lean index b80110a38..44e5985b6 100644 --- a/library/logic/axioms/piext.lean +++ b/library/logic/axioms/piext.lean @@ -7,7 +7,7 @@ import logic.inhabited logic.cast open inhabited -- Pi extensionality -axiom piext {A : Type} {B B' : A → Type} {H : inhabited (Π x, B x)} : +axiom piext {A : Type} {B B' : A → Type} [H : inhabited (Π x, B x)] : (Π x, B x) = (Π x, B' x) → B = B' theorem cast_app {A : Type} {B B' : A → Type} (H : (Π x, B x) = (Π x, B' x)) (f : Π x, B x) diff --git a/library/logic/decidable.lean b/library/logic/decidable.lean index b27bb6b4d..966adc2ff 100644 --- a/library/logic/decidable.lean +++ b/library/logic/decidable.lean @@ -24,11 +24,11 @@ namespace decidable C H := decidable.rec H1 H2 H - definition rec_on_true {H : decidable p} {H1 : p → Type} {H2 : ¬p → Type} (H3 : p) (H4 : H1 H3) + definition rec_on_true [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type} (H3 : p) (H4 : H1 H3) : rec_on H H1 H2 := rec_on H (λh, H4) (λh, false.rec_type _ (h H3)) - definition rec_on_false {H : decidable p} {H1 : p → Type} {H2 : ¬p → Type} (H3 : ¬p) (H4 : H2 H3) + definition rec_on_false [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type} (H3 : ¬p) (H4 : H2 H3) : rec_on H H1 H2 := rec_on H (λh, false.rec_type _ (H3 h)) (λh, H4) @@ -45,13 +45,13 @@ namespace decidable d2) d1) - theorem em (p : Prop) {H : decidable p} : p ∨ ¬p := + theorem em (p : Prop) [H : decidable p] : p ∨ ¬p := induction_on H (λ Hp, or.inl Hp) (λ Hnp, or.inr Hnp) - definition by_cases {q : Type} {C : decidable p} (Hpq : p → q) (Hnpq : ¬p → q) : q := + definition by_cases {q : Type} [C : decidable p] (Hpq : p → q) (Hnpq : ¬p → q) : q := rec_on C (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp) - theorem by_contradiction {Hp : decidable p} (H : ¬p → false) : p := + theorem by_contradiction [Hp : decidable p] (H : ¬p → false) : p := or.elim (em p) (assume H1 : p, H1) (assume H1 : ¬p, false_elim (H H1)) @@ -92,7 +92,7 @@ namespace decidable definition decidable_eq_equiv (Hp : decidable p) (H : p = q) : decidable q := decidable_iff_equiv Hp (eq_to_iff H) - protected theorem rec_subsingleton [instance] {H : decidable p} {H1 : p → Type} {H2 : ¬p → Type} + protected theorem rec_subsingleton [instance] [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type} (H3 : Π(h : p), subsingleton (H1 h)) (H4 : Π(h : ¬p), subsingleton (H2 h)) : subsingleton (rec_on H H1 H2) := rec_on H (λh, H3 h) (λh, H4 h) --this can be proven using dependent version of "by_cases" diff --git a/library/logic/identities.lean b/library/logic/identities.lean index 61e8ea4c0..0e609a931 100644 --- a/library/logic/identities.lean +++ b/library/logic/identities.lean @@ -37,13 +37,13 @@ calc ... ↔ b ∧ (a ∧ c) : and.assoc -theorem not_not_iff {a : Prop} {D : decidable a} : (¬¬a) ↔ a := +theorem not_not_iff {a : Prop} [D : decidable a] : (¬¬a) ↔ a := iff.intro (assume H : ¬¬a, by_cases (assume H' : a, H') (assume H' : ¬a, absurd H' H)) (assume H : a, assume H', H' H) -theorem not_not_elim {a : Prop} {D : decidable a} (H : ¬¬a) : a := +theorem not_not_elim {a : Prop} [D : decidable a] (H : ¬¬a) : a := iff.mp not_not_iff H theorem not_true : (¬true) ↔ false := @@ -52,7 +52,7 @@ iff.intro (assume H, H trivial) false_elim theorem not_false : (¬false) ↔ true := iff.intro (assume H, trivial) (assume H H', H') -theorem not_or {a b : Prop} {Da : decidable a} {Db : decidable b} : (¬(a ∨ b)) ↔ (¬a ∧ ¬b) := +theorem not_or {a b : Prop} [Da : decidable a] [Db : decidable b] : (¬(a ∨ b)) ↔ (¬a ∧ ¬b) := iff.intro (assume H, or.elim (em a) (assume Ha, absurd (or.inl Ha) H) @@ -64,7 +64,7 @@ iff.intro (assume Ha, absurd Ha (and.elim_left H)) (assume Hb, absurd Hb (and.elim_right H))) -theorem not_and {a b : Prop} {Da : decidable a} {Db : decidable b} : (¬(a ∧ b)) ↔ (¬a ∨ ¬b) := +theorem not_and {a b : Prop} [Da : decidable a] [Db : decidable b] : (¬(a ∧ b)) ↔ (¬a ∨ ¬b) := iff.intro (assume H, or.elim (em a) (assume Ha, or.elim (em b) @@ -76,7 +76,7 @@ iff.intro (assume Hna, absurd (and.elim_left N) Hna) (assume Hnb, absurd (and.elim_right N) Hnb)) -theorem imp_or {a b : Prop} {Da : decidable a} : (a → b) ↔ (¬a ∨ b) := +theorem imp_or {a b : Prop} [Da : decidable a] : (a → b) ↔ (¬a ∨ b) := iff.intro (assume H : a → b, (or.elim (em a) (assume Ha : a, or.inr (H Ha)) @@ -84,24 +84,24 @@ iff.intro (assume (H : ¬a ∨ b) (Ha : a), or.resolve_right H (not_not_iff⁻¹ ▸ Ha)) -theorem not_implies {a b : Prop} {Da : decidable a} {Db : decidable b} : (¬(a → b)) ↔ (a ∧ ¬b) := +theorem not_implies {a b : Prop} [Da : decidable a] [Db : decidable b] : (¬(a → b)) ↔ (a ∧ ¬b) := calc (¬(a → b)) ↔ (¬(¬a ∨ b)) : {imp_or} ... ↔ (¬¬a ∧ ¬b) : not_or ... ↔ (a ∧ ¬b) : {not_not_iff} -theorem peirce {a b : Prop} {D : decidable a} : ((a → b) → a) → a := +theorem peirce {a b : Prop} [D : decidable a] : ((a → b) → a) → a := assume H, by_contradiction (assume Hna : ¬a, have Hnna : ¬¬a, from not_implies_left (mt H Hna), absurd (not_not_elim Hnna) Hna) -theorem not_exists_forall {A : Type} {P : A → Prop} {D : ∀x, decidable (P x)} +theorem not_exists_forall {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)] (H : ¬∃x, P x) : ∀x, ¬P x := take x, or.elim (em (P x)) (assume Hp : P x, absurd (exists_intro x Hp) H) (assume Hn : ¬P x, Hn) -theorem not_forall_exists {A : Type} {P : A → Prop} {D : ∀x, decidable (P x)} - {D' : decidable (∃x, ¬P x)} (H : ¬∀x, P x) : +theorem not_forall_exists {A : Type} {P : A → Prop} [D : ∀x, decidable (P x)] + [D' : decidable (∃x, ¬P x)] (H : ¬∀x, P x) : ∃x, ¬P x := @by_contradiction _ D' (assume H1 : ¬∃x, ¬P x, have H2 : ∀x, ¬¬P x, from @not_exists_forall _ _ (take x, not_decidable (D x)) H1, diff --git a/library/logic/if.lean b/library/logic/if.lean index e11b4a26e..b271ebc8d 100644 --- a/library/logic/if.lean +++ b/library/logic/if.lean @@ -7,24 +7,24 @@ import logic.decidable tools.tactic open decidable tactic eq.ops -definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A := +definition ite (c : Prop) [H : decidable c] {A : Type} (t e : A) : A := decidable.rec_on H (assume Hc, t) (assume Hnc, e) notation `if` c `then` t `else` e:45 := ite c t e -theorem if_pos {c : Prop} {H : decidable c} (Hc : c) {A : Type} {t e : A} : (if c then t else e) = t := +theorem if_pos {c : Prop} [H : decidable c] (Hc : c) {A : Type} {t e : A} : (if c then t else e) = t := decidable.rec (assume Hc : c, eq.refl (@ite c (inl Hc) A t e)) (assume Hnc : ¬c, absurd Hc Hnc) H -theorem if_neg {c : Prop} {H : decidable c} (Hnc : ¬c) {A : Type} {t e : A} : (if c then t else e) = e := +theorem if_neg {c : Prop} [H : decidable c] (Hnc : ¬c) {A : Type} {t e : A} : (if c then t else e) = e := decidable.rec (assume Hc : c, absurd Hc Hnc) (assume Hnc : ¬c, eq.refl (@ite c (inr Hnc) A t e)) H -theorem if_t_t (c : Prop) {H : decidable c} {A : Type} (t : A) : (if c then t else t) = t := +theorem if_t_t (c : Prop) [H : decidable c] {A : Type} (t : A) : (if c then t else t) = t := decidable.rec (assume Hc : c, eq.refl (@ite c (inl Hc) A t t)) (assume Hnc : ¬c, eq.refl (@ite c (inr Hnc) A t t)) @@ -36,7 +36,7 @@ if_pos trivial theorem if_false {A : Type} (t e : A) : (if false then t else e) = e := if_neg not_false_trivial -theorem if_cond_congr {c₁ c₂ : Prop} {H₁ : decidable c₁} {H₂ : decidable c₂} (Heq : c₁ ↔ c₂) {A : Type} (t e : A) +theorem if_cond_congr {c₁ c₂ : Prop} [H₁ : decidable c₁] [H₂ : decidable c₂] (Heq : c₁ ↔ c₂) {A : Type} (t e : A) : (if c₁ then t else e) = (if c₂ then t else e) := decidable.rec_on H₁ (assume Hc₁ : c₁, decidable.rec_on H₂ @@ -46,12 +46,12 @@ decidable.rec_on H₁ (assume Hc₂ : c₂, absurd (iff.elim_right Heq Hc₂) Hnc₁) (assume Hnc₂ : ¬c₂, if_neg Hnc₁ ⬝ (if_neg Hnc₂)⁻¹)) -theorem if_congr_aux {c₁ c₂ : Prop} {H₁ : decidable c₁} {H₂ : decidable c₂} {A : Type} {t₁ t₂ e₁ e₂ : A} +theorem if_congr_aux {c₁ c₂ : Prop} [H₁ : decidable c₁] [H₂ : decidable c₂] {A : Type} {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) : (if c₁ then t₁ else e₁) = (if c₂ then t₂ else e₂) := Ht ▸ He ▸ (if_cond_congr Hc t₁ e₁) -theorem if_congr {c₁ c₂ : Prop} {H₁ : decidable c₁} {A : Type} {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) : +theorem if_congr {c₁ c₂ : Prop} [H₁ : decidable c₁] {A : Type} {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂) (He : e₁ = e₂) : (if c₁ then t₁ else e₁) = (@ite c₂ (decidable_iff_equiv H₁ Hc) A t₂ e₂) := have H2 [visible] : decidable c₂, from (decidable_iff_equiv H₁ Hc), if_congr_aux Hc Ht He diff --git a/library/logic/inhabited.lean b/library/logic/inhabited.lean index 7b3b771d1..0ddb60662 100644 --- a/library/logic/inhabited.lean +++ b/library/logic/inhabited.lean @@ -22,6 +22,6 @@ definition dfun_inhabited [instance] (A : Type) {B : A → Type} (H : Πx, inhab inhabited (Πx, B x) := mk (λa, destruct (H a) (λb, b)) -definition default (A : Type) {H : inhabited A} : A := destruct H (take a, a) +definition default (A : Type) [H : inhabited A] : A := destruct H (take a, a) end inhabited diff --git a/library/logic/instances.lean b/library/logic/instances.lean index 5d92f55a3..30cb9779a 100644 --- a/library/logic/instances.lean +++ b/library/logic/instances.lean @@ -68,7 +68,7 @@ definition congruence_iff_compose [instance] := congruence.compose21 congruence_ namespace general_operations -theorem subst {T : Type} (R : T → T → Prop) ⦃P : T → Prop⦄ {C : congruence R iff P} +theorem subst {T : Type} (R : T → T → Prop) ⦃P : T → Prop⦄ [C : congruence R iff P] {a b : T} (H : R a b) (H1 : P a) : P b := iff.elim_left (congruence.app C H) H1 end general_operations @@ -113,7 +113,7 @@ relation.mp_like.mk (iff.elim_left H) -- Substition for iff -- ------------------ namespace iff -theorem subst {P : Prop → Prop} {C : congruence iff iff P} {a b : Prop} (H : a ↔ b) (H1 : P a) : +theorem subst {P : Prop → Prop} [C : congruence iff iff P] {a b : Prop} (H : a ↔ b) (H1 : P a) : P b := @general_operations.subst Prop iff P C a b H H1 end iff diff --git a/library/logic/quantifiers.lean b/library/logic/quantifiers.lean index dd77e4a82..97b4de116 100644 --- a/library/logic/quantifiers.lean +++ b/library/logic/quantifiers.lean @@ -55,10 +55,10 @@ iff.intro theorem forall_true_iff_true (A : Type) : (∀x : A, true) ↔ true := iff.intro (assume H, trivial) (assume H, take x, trivial) -theorem forall_p_iff_p (A : Type) {H : inhabited A} (p : Prop) : (∀x : A, p) ↔ p := +theorem forall_p_iff_p (A : Type) [H : inhabited A] (p : Prop) : (∀x : A, p) ↔ p := iff.intro (assume Hl, inhabited.destruct H (take x, Hl x)) (assume Hr, take x, Hr) -theorem exists_p_iff_p (A : Type) {H : inhabited A} (p : Prop) : (∃x : A, p) ↔ p := +theorem exists_p_iff_p (A : Type) [H : inhabited A] (p : Prop) : (∃x : A, p) ↔ p := iff.intro (assume Hl, obtain a Hp, from Hl, Hp) (assume Hr, inhabited.destruct H (take a, exists_intro a Hr)) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index d1d66058d..e8a3dd9e8 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -204,13 +204,20 @@ void elaborator::copy_info_to_manager(substitution s) { /** \brief Create a metavariable, and attach choice constraint for generating solutions using class-instances and tactic-hints. */ -expr elaborator::mk_placeholder_meta(optional const & type, tag g, bool is_strict, constraint_seq & cs) { - auto ec = mk_placeholder_elaborator(env(), ios(), m_context, - m_ngen.next(), m_relax_main_opaque, use_local_instances(), - is_strict, type, g, m_unifier_config); - register_meta(ec.first); - cs += ec.second; - return ec.first; +expr elaborator::mk_placeholder_meta(optional const & type, tag g, bool is_strict, + bool is_inst_implicit, constraint_seq & cs) { + if (is_inst_implicit) { + auto ec = mk_placeholder_elaborator(env(), ios(), m_context, + m_ngen.next(), m_relax_main_opaque, use_local_instances(), + is_strict, type, g, m_unifier_config); + register_meta(ec.first); + cs += ec.second; + return ec.first; + } else { + expr m = m_context.mk_meta(m_ngen, type, g); + register_meta(m); + return m; + } } expr elaborator::visit_expecting_type(expr const & e, constraint_seq & cs) { @@ -225,7 +232,8 @@ expr elaborator::visit_expecting_type(expr const & e, constraint_seq & cs) { expr elaborator::visit_expecting_type_of(expr const & e, expr const & t, constraint_seq & cs) { if (is_placeholder(e) && !placeholder_type(e)) { - expr r = mk_placeholder_meta(some_expr(t), e.get_tag(), is_strict_placeholder(e), cs); + bool inst_imp = true; + expr r = mk_placeholder_meta(some_expr(t), e.get_tag(), is_strict_placeholder(e), inst_imp, cs); save_placeholder_info(e, r); return r; } else if (is_choice(e)) { @@ -283,7 +291,7 @@ static bool is_implicit_pi(expr const & e) { if (!is_pi(e)) return false; binder_info bi = binding_info(e); - return bi.is_strict_implicit() || bi.is_implicit(); + return bi.is_strict_implicit() || bi.is_implicit() || bi.is_inst_implicit(); } /** \brief Auxiliary function for adding implicit arguments to coercions to function-class */ @@ -298,7 +306,8 @@ expr elaborator::add_implict_args(expr e, constraint_seq & cs, bool relax) { lean_assert(is_pi(type)); tag g = e.get_tag(); bool is_strict = true; - expr imp_arg = mk_placeholder_meta(some_expr(binding_domain(type)), g, is_strict, cs); + bool inst_imp = binding_info(type).is_inst_implicit(); + expr imp_arg = mk_placeholder_meta(some_expr(binding_domain(type)), g, is_strict, inst_imp, cs); e = mk_app(e, imp_arg, g); type = instantiate(binding_body(type), imp_arg); constraint_seq new_cs; @@ -522,10 +531,13 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) { lean_assert(is_pi(f_type)); if (!expl) { bool first = true; - while (binding_info(f_type).is_strict_implicit() || (!first && binding_info(f_type).is_implicit())) { + while (binding_info(f_type).is_strict_implicit() || + (!first && binding_info(f_type).is_implicit()) || + (!first && binding_info(f_type).is_inst_implicit())) { tag g = f.get_tag(); bool is_strict = true; - expr imp_arg = mk_placeholder_meta(some_expr(binding_domain(f_type)), g, is_strict, f_cs); + bool inst_imp = binding_info(f_type).is_inst_implicit(); + expr imp_arg = mk_placeholder_meta(some_expr(binding_domain(f_type)), g, is_strict, inst_imp, f_cs); f = mk_app(f, imp_arg, g); auto f_t = ensure_fun(f, f_cs); f = f_t.first; @@ -551,7 +563,8 @@ expr elaborator::visit_app(expr const & e, constraint_seq & cs) { } expr elaborator::visit_placeholder(expr const & e, constraint_seq & cs) { - expr r = mk_placeholder_meta(placeholder_type(e), e.get_tag(), is_strict_placeholder(e), cs); + bool inst_implicit = true; + expr r = mk_placeholder_meta(placeholder_type(e), e.get_tag(), is_strict_placeholder(e), inst_implicit, cs); save_placeholder_info(e, r); return r; } @@ -826,7 +839,8 @@ pair elaborator::visit(expr const & e) { expr imp_arg; bool is_strict = true; while (is_pi(r_type)) { - if (!binding_info(r_type).is_implicit()) { + binder_info bi = binding_info(r_type); + if (!bi.is_implicit() && !bi.is_inst_implicit()) { if (!consume_args) break; if (!has_free_var(binding_body(r_type), 0)) { @@ -835,7 +849,8 @@ pair elaborator::visit(expr const & e) { break; } } - imp_arg = mk_placeholder_meta(some_expr(binding_domain(r_type)), g, is_strict, cs); + bool inst_imp = bi.is_inst_implicit(); + imp_arg = mk_placeholder_meta(some_expr(binding_domain(r_type)), g, is_strict, inst_imp, cs); r = mk_app(r, imp_arg, g); r_type = whnf(instantiate(binding_body(r_type), imp_arg), cs); } diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h index 3c8f589a1..382be3818 100644 --- a/src/frontends/lean/elaborator.h +++ b/src/frontends/lean/elaborator.h @@ -84,7 +84,7 @@ class elaborator : public coercion_info_manager { virtual void save_coercion_info(expr const & e, expr const & c); virtual void erase_coercion_info(expr const & e); void copy_info_to_manager(substitution s); - expr mk_placeholder_meta(optional const & type, tag g, bool is_strict, constraint_seq & cs); + expr mk_placeholder_meta(optional const & type, tag g, bool is_strict, bool inst_implicit, constraint_seq & cs); expr visit_expecting_type(expr const & e, constraint_seq & cs); expr visit_expecting_type_of(expr const & e, expr const & t, constraint_seq & cs); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 57f099237..7684925f8 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -689,7 +689,7 @@ optional parser::parse_optional_binder_info() { } } else if (curr_is_token(get_lbracket_tk())) { next(); - return some(mk_cast_binder_info()); + return some(mk_inst_implicit_binder_info()); } else if (curr_is_token(get_ldcurly_tk())) { next(); return some(mk_strict_implicit_binder_info()); @@ -719,14 +719,14 @@ binder_info parser::parse_binder_info() { - default : consume ')' - implicit : consume '}' - strict implicit : consume '}}' or '⦄' - - cast : consume ']' + - inst implicit : consume ']' */ void parser::parse_close_binder_info(optional const & bi) { if (!bi) { return; } else if (bi->is_implicit()) { check_token_next(get_rcurly_tk(), "invalid declaration, '}' expected"); - } else if (bi->is_cast()) { + } else if (bi->is_inst_implicit()) { check_token_next(get_rbracket_tk(), "invalid declaration, ']' expected"); } else if (bi->is_strict_implicit()) { if (curr_is_token(get_rcurly_tk())) { diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 55dea6202..dbe65a8e0 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -189,7 +189,7 @@ bool pretty_fn::is_implicit(expr const & f) { } try { binder_info bi = binding_info(m_tc.ensure_pi(m_tc.infer(f).first).first); - return bi.is_implicit() || bi.is_strict_implicit(); + return bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit(); } catch (exception &) { return false; } @@ -346,7 +346,7 @@ bool pretty_fn::has_implicit_args(expr const & f) { expr type = m_tc.whnf(m_tc.infer(f).first).first; while (is_pi(type)) { binder_info bi = binding_info(type); - if (bi.is_implicit() || bi.is_strict_implicit()) + if (bi.is_implicit() || bi.is_strict_implicit() || bi.is_inst_implicit()) return true; expr local = mk_local(ngen.next(), binding_name(type), binding_domain(type), binding_info(type)); type = m_tc.whnf(instantiate(binding_body(type), local)).first; @@ -370,7 +370,7 @@ auto pretty_fn::pp_app(expr const & e) -> result { format pretty_fn::pp_binder_block(buffer const & names, expr const & type, binder_info const & bi) { format r; if (bi.is_implicit()) r += format("{"); - else if (bi.is_cast()) r += format("["); + else if (bi.is_inst_implicit()) r += format("["); else if (bi.is_strict_implicit() && m_unicode) r += format("⦃"); else if (bi.is_strict_implicit() && !m_unicode) r += format("{{"); else r += format("("); @@ -380,7 +380,7 @@ format pretty_fn::pp_binder_block(buffer const & names, expr const & type, } r += compose(colon(), nest(m_indent, compose(line(), pp_child(type, 0).first))); if (bi.is_implicit()) r += format("}"); - else if (bi.is_cast()) r += format("]"); + else if (bi.is_inst_implicit()) r += format("]"); else if (bi.is_strict_implicit() && m_unicode) r += format("⦄"); else if (bi.is_strict_implicit() && !m_unicode) r += format("}}"); else r += format(")"); diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index 9eaca1d02..01d79eaa8 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -549,7 +549,7 @@ void server::display_decl(name const & short_name, name const & long_name, envir while (true) { if (!is_pi(type)) break; - if (!binding_info(type).is_implicit()) + if (!binding_info(type).is_implicit() && !binding_info(type).is_inst_implicit()) break; std::string q("?"); q += binding_name(type).to_string(); diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index dda693d42..01cbc5a71 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -134,7 +134,7 @@ void expr_const::dealloc() { } unsigned binder_info::hash() const { - return (m_implicit << 3) | (m_cast << 2) | (m_contextual << 1) | m_strict_implicit; + return (m_implicit << 4) | (m_cast << 3) | (m_contextual << 2) | (m_strict_implicit << 1) | m_inst_implicit; } // Expr metavariables and local variables @@ -196,7 +196,8 @@ bool operator==(binder_info const & i1, binder_info const & i2) { i1.is_implicit() == i2.is_implicit() && i1.is_cast() == i2.is_cast() && i1.is_contextual() == i2.is_contextual() && - i1.is_strict_implicit() == i2.is_strict_implicit(); + i1.is_strict_implicit() == i2.is_strict_implicit() && + i1.is_inst_implicit() == i2.is_inst_implicit(); } // Expr binders (Lambda, Pi) diff --git a/src/kernel/expr.h b/src/kernel/expr.h index b518fee89..dee56a4cf 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -229,21 +229,30 @@ public: class binder_info { unsigned m_implicit:1; //! if true, binder argument is an implicit argument unsigned m_cast:1; //! if true, binder argument is a target for using cast - unsigned m_contextual:1; //! if true, binder argument is assumed to be part of the context, and may be argument for metavariables. + /** if m_contextual is true, binder argument is assumed to be part of the context, + and may be argument for metavariables. */ + unsigned m_contextual:1; unsigned m_strict_implicit:1; //! if true, binder argument is assumed to be a strict implicit argument + /** \brief if m_inst_implicit is true, binder argument is an implicit argument, and should be + inferred by class-instance resolution. */ + unsigned m_inst_implicit:1; public: - binder_info(bool implicit = false, bool cast = false, bool contextual = true, bool strict_implicit = false): - m_implicit(implicit), m_cast(cast), m_contextual(contextual), m_strict_implicit(strict_implicit) {} + binder_info(bool implicit = false, bool cast = false, bool contextual = true, bool strict_implicit = false, + bool inst_implicit = false): + m_implicit(implicit), m_cast(cast), m_contextual(contextual), m_strict_implicit(strict_implicit), + m_inst_implicit(inst_implicit) {} bool is_implicit() const { return m_implicit; } bool is_cast() const { return m_cast; } bool is_contextual() const { return m_contextual; } bool is_strict_implicit() const { return m_strict_implicit; } + bool is_inst_implicit() const { return m_inst_implicit; } unsigned hash() const; - binder_info update_contextual(bool f) const { return binder_info(m_implicit, m_cast, f, m_strict_implicit); } + binder_info update_contextual(bool f) const { return binder_info(m_implicit, m_cast, f, m_strict_implicit, m_inst_implicit); } }; inline binder_info mk_implicit_binder_info() { return binder_info(true); } inline binder_info mk_strict_implicit_binder_info() { return binder_info(false, false, true, true); } +inline binder_info mk_inst_implicit_binder_info() { return binder_info(false, false, true, false, true); } inline binder_info mk_cast_binder_info() { return binder_info(false, true); } inline binder_info mk_contextual_info(bool f) { return binder_info(false, false, f); } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 222fe7cd2..b79a1f7a4 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -285,12 +285,14 @@ static int binder_info_is_implicit(lua_State * L) { return push_boolean(L, to_bi static int binder_info_is_cast(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_cast()); } static int binder_info_is_contextual(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_contextual()); } static int binder_info_is_strict_implicit(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_strict_implicit()); } +static int binder_info_is_inst_implicit(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_inst_implicit()); } static const struct luaL_Reg binder_info_m[] = { {"__gc", binder_info_gc}, {"is_implicit", safe_function}, {"is_cast", safe_function}, {"is_contextual", safe_function}, {"is_strict_implicit", safe_function}, + {"is_inst_implicit", safe_function}, {0, 0} }; static void open_binder_info(lua_State * L) { diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index 149f2b925..cbdcccfbd 100644 --- a/src/library/kernel_serializer.cpp +++ b/src/library/kernel_serializer.cpp @@ -121,6 +121,7 @@ serializer & operator<<(serializer & s, binder_info const & i) { s.write_bool(i.is_cast()); s.write_bool(i.is_contextual()); s.write_bool(i.is_strict_implicit()); + s.write_bool(i.is_inst_implicit()); return s; } @@ -129,7 +130,8 @@ static binder_info read_binder_info(deserializer & d) { bool cast = d.read_bool(); bool ctx = d.read_bool(); bool s_imp = d.read_bool(); - return binder_info(imp, cast, ctx, s_imp); + bool i_imp = d.read_bool(); + return binder_info(imp, cast, ctx, s_imp, i_imp); } static name * g_binder_name = nullptr; diff --git a/src/library/print.cpp b/src/library/print.cpp index f81047b3d..ab334c9bf 100644 --- a/src/library/print.cpp +++ b/src/library/print.cpp @@ -148,7 +148,7 @@ struct print_expr_fn { expr const & n = p.second; if (binding_info(e).is_implicit()) out() << "{"; - else if (binding_info(e).is_cast()) + else if (binding_info(e).is_inst_implicit()) out() << "["; else if (!binding_info(e).is_contextual()) out() << "[["; @@ -160,7 +160,7 @@ struct print_expr_fn { print(binding_domain(e)); if (binding_info(e).is_implicit()) out() << "}"; - else if (binding_info(e).is_cast()) + else if (binding_info(e).is_inst_implicit()) out() << "]"; else if (!binding_info(e).is_contextual()) out() << "]]"; diff --git a/tests/lean/cls_err.lean b/tests/lean/cls_err.lean index 3d21d57a4..7f5b3132d 100644 --- a/tests/lean/cls_err.lean +++ b/tests/lean/cls_err.lean @@ -3,7 +3,7 @@ import logic inductive H [class] (A : Type) := mk : A → H A -definition foo {A : Type} {h : H A} : A := +definition foo {A : Type} [h : H A] : A := H.rec (λa, a) h context diff --git a/tests/lean/const.lean b/tests/lean/const.lean index 70df5fc54..98d844398 100644 --- a/tests/lean/const.lean +++ b/tests/lean/const.lean @@ -1,10 +1,10 @@ import logic -definition foo {A : Type} {H : inhabited A} : A := +definition foo {A : Type} [H : inhabited A] : A := inhabited.rec (λa, a) H -constant bla {A : Type} {H : inhabited A} : Type.{1} +constant bla {A : Type} [H : inhabited A] : Type.{1} set_option pp.implicit true diff --git a/tests/lean/pp.lean.expected.out b/tests/lean/pp.lean.expected.out index fa9299df1..2f4a648f8 100644 --- a/tests/lean/pp.lean.expected.out +++ b/tests/lean/pp.lean.expected.out @@ -2,6 +2,6 @@ λ {A B : Type} (a : A) (b : B), a : ?M_1 → ?M_2 → ?M_1 λ (A : Type) {B : Type} (a : A) (b : B), a : Π (A : Type) {B : Type}, A → B → A λ (A B : Type) (a : A) (b : B), a : Π (A B : Type), A → B → A -λ [A : Type] (B : Type) (a : A) (b : B), a : Π [A : Type] (B : Type), A → B → A +λ [A : Type] (B : Type) (a : A) (b : B), a : Π (B : Type), ?M_1 → B → ?M_1 λ ⦃A : Type⦄ {B : Type} (a : A) (b : B), a : Π ⦃A : Type⦄ {B : Type}, A → B → A λ ⦃A B : Type⦄ (a : A) (b : B), a : Π ⦃A B : Type⦄, A → B → A diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean index 633e3d232..ed22f6ce3 100644 --- a/tests/lean/run/algebra1.lean +++ b/tests/lean/run/algebra1.lean @@ -21,12 +21,12 @@ namespace algebra inductive add_struct [class] (A : Type) : Type := mk : (A → A → A) → add_struct A - definition mul {A : Type} {s : mul_struct A} (a b : A) + definition mul {A : Type} [s : mul_struct A] (a b : A) := mul_struct.rec (fun f, f) s a b infixl `*`:75 := mul - definition add {A : Type} {s : add_struct A} (a b : A) + definition add {A : Type} [s : add_struct A] (a b : A) := add_struct.rec (fun f, f) s a b infixl `+`:65 := add diff --git a/tests/lean/run/class11.lean b/tests/lean/run/class11.lean index 3dc8f54d7..faf7b9fa6 100644 --- a/tests/lean/run/class11.lean +++ b/tests/lean/run/class11.lean @@ -3,7 +3,7 @@ import logic constant C {A : Type} : A → Prop class C -constant f {A : Type} (a : A) {H : C a} : Prop +constant f {A : Type} (a : A) [H : C a] : Prop definition g {A : Type} (a b : A) {H1 : C a} {H2 : C b} : Prop := f a ∧ f b diff --git a/tests/lean/run/class5.lean b/tests/lean/run/class5.lean index 8c10d2827..bbb197123 100644 --- a/tests/lean/run/class5.lean +++ b/tests/lean/run/class5.lean @@ -4,7 +4,7 @@ namespace algebra inductive mul_struct [class] (A : Type) : Type := mk : (A → A → A) → mul_struct A - definition mul {A : Type} {s : mul_struct A} (a b : A) + definition mul {A : Type} [s : mul_struct A] (a b : A) := mul_struct.rec (λ f, f) s a b infixl `*`:75 := mul diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean index d0e5a768e..e1421fffa 100644 --- a/tests/lean/run/elab_bug1.lean +++ b/tests/lean/run/elab_bug1.lean @@ -57,7 +57,7 @@ theorem congr_not [instance] (T : Type) (R : T → T → Prop) (f : T → Prop) (H : congruence R iff f) : congruence R iff (λx, ¬ f x) := sorry -theorem subst_iff {T : Type} {R : T → T → Prop} {P : T → Prop} {C : congruence R iff P} +theorem subst_iff {T : Type} {R : T → T → Prop} {P : T → Prop} [C : congruence R iff P] {a b : T} (H : R a b) (H1 : P a) : P b := -- iff_mp_left (congruence.rec id C a b H) H1 iff.elim_left (@congr_app _ _ R iff P C a b H) H1 diff --git a/tests/lean/run/group2.lean b/tests/lean/run/group2.lean index b08451b46..5c45ff341 100644 --- a/tests/lean/run/group2.lean +++ b/tests/lean/run/group2.lean @@ -28,7 +28,7 @@ definition group_to_struct [instance] (g : group) : group_struct (carrier g) check group_struct -definition mul {A : Type} {s : group_struct A} (a b : A) : A +definition mul {A : Type} [s : group_struct A] (a b : A) : A := group_struct.rec (λ mul one inv h1 h2 h3, mul) s a b infixl `*`:75 := mul diff --git a/tests/lean/run/group3.lean b/tests/lean/run/group3.lean index 854a96b3e..b48e0da12 100644 --- a/tests/lean/run/group3.lean +++ b/tests/lean/run/group3.lean @@ -22,9 +22,9 @@ inductive has_mul [class] (A : Type) : Type := mk : (A → A → A) → has_mul inductive has_one [class] (A : Type) : Type := mk : A → has_one A inductive has_inv [class] (A : Type) : Type := mk : (A → A) → has_inv A -definition mul {A : Type} {s : has_mul A} (a b : A) : A := has_mul.rec (λf, f) s a b -definition one {A : Type} {s : has_one A} : A := has_one.rec (λo, o) s -definition inv {A : Type} {s : has_inv A} (a : A) : A := has_inv.rec (λi, i) s a +definition mul {A : Type} [s : has_mul A] (a b : A) : A := has_mul.rec (λf, f) s a b +definition one {A : Type} [s : has_one A] : A := has_one.rec (λo, o) s +definition inv {A : Type} [s : has_inv A] (a : A) : A := has_inv.rec (λi, i) s a infix `*` := mul postfix `⁻¹` := inv @@ -40,7 +40,7 @@ mk : Π mul: A → A → A, namespace semigroup section - variables {A : Type} {s : semigroup A} + variables {A : Type} [s : semigroup A] variables a b c : A definition mul := semigroup.rec (λmul assoc, mul) s a b context @@ -52,7 +52,7 @@ end end semigroup section - variables {A : Type} {s : semigroup A} + variables {A : Type} [s : semigroup A] include s definition semigroup_has_mul [instance] : has_mul A := has_mul.mk semigroup.mul @@ -72,7 +72,7 @@ mk : Π (mul: A → A → A) namespace comm_semigroup section - variables {A : Type} {s : comm_semigroup A} + variables {A : Type} [s : comm_semigroup A] variables a b c : A definition mul (a b : A) : A := comm_semigroup.rec (λmul assoc comm, mul) s a b definition assoc : mul (mul a b) c = mul a (mul b c) := @@ -83,7 +83,7 @@ end end comm_semigroup section - variables {A : Type} {s : comm_semigroup A} + variables {A : Type} [s : comm_semigroup A] variables a b c : A include s definition comm_semigroup_semigroup [instance] : semigroup A := @@ -108,7 +108,7 @@ mk : Π (mul: A → A → A) (one : A) namespace monoid section - variables {A : Type} {s : monoid A} + variables {A : Type} [s : monoid A] variables a b c : A include s context @@ -127,7 +127,7 @@ namespace monoid end monoid section - variables {A : Type} {s : monoid A} + variables {A : Type} [s : monoid A] variable a : A include s definition monoid_has_one [instance] : has_one A := has_one.mk (monoid.one) @@ -153,7 +153,7 @@ mk : Π (mul: A → A → A) (one : A) namespace comm_monoid section - variables {A : Type} {s : comm_monoid A} + variables {A : Type} [s : comm_monoid A] variables a b c : A definition mul := comm_monoid.rec (λmul one assoc right_id left_id comm, mul) s a b definition one := comm_monoid.rec (λmul one assoc right_id left_id comm, one) s @@ -169,7 +169,7 @@ namespace comm_monoid end comm_monoid section - variables {A : Type} {s : comm_monoid A} + variables {A : Type} [s : comm_monoid A] include s definition comm_monoid_monoid [instance] : monoid A := monoid.mk comm_monoid.mul comm_monoid.one comm_monoid.assoc diff --git a/tests/lean/run/univ_bug2.lean b/tests/lean/run/univ_bug2.lean index cb12a4a14..d4ce5c812 100644 --- a/tests/lean/run/univ_bug2.lean +++ b/tests/lean/run/univ_bug2.lean @@ -16,7 +16,7 @@ namespace simplifies_to theorem get_eq {T : Type} {t1 t2 : T} (C : simplifies_to t1 t2) : t1 = t2 := simplifies_to.rec (λx, x) C -theorem infer_eq {T : Type} (t1 t2 : T) {C : simplifies_to t1 t2} : t1 = t2 := +theorem infer_eq {T : Type} (t1 t2 : T) [C : simplifies_to t1 t2] : t1 = t2 := simplifies_to.rec (λx, x) C theorem simp_app [instance] (S : Type) (T : Type) (f1 f2 : S → T) (s1 s2 : S)