michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(frontends/lean): add 'attribute' command

Browse source 
The new command provides a uniform way to set declaration attributes.
It replaces the commands: class, instance, coercion, multiple_instances,
reducible, irreducible
This commit is contained in:
Leonardo de Moura 2015-01-24 20:23:21 -08:00
parent b5c4e603db
commit 4f2e0c6d7f
89 changed files with 313 additions and 408 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
doc/lean/reducible.org
View file

@ -58,42 +58,28 @@ The following command declares a transparent definition =pr= and mark it as redu
definition pr1 [reducible] (A : Type) (a b : A) : A := a
#+END_SRC
The =reducible= mark is saved in the compiled .olean files. The user
can temporarily change the =reducible= and =irreducible= marks using
the following commands. The temporary modification is effective only in the
The =reducible= attribute is saved in the compiled .olean files. The user
can temporarily change the =reducible= and =irreducible= attributes using
the =attribute= command. The temporary modification is effective only in the
current file, and is not saved in the produced .olean file.
#+BEGIN_SRC lean
definition id (A : Type) (a : A) : A := a
definition pr2 (A : Type) (a b : A) : A := b
-- mark pr2 as reducible
reducible pr2
attribute pr2 [reducible]
-- ...
-- mark id and pr2 as irreducible
irreducible id pr2
attribute id [irreducible]
attribute pr2 [irreducible]
#+END_SRC
The annotation =[persistent]= can be used to instruct Lean to make the
The command =persistent attribute= can be used to instruct Lean to make the
modification permanent, and save it in the .olean file.
#+BEGIN_SRC lean
definition pr2 (A : Type) (a b : A) : A := b
-- Mark pr2 as irreducible.
-- The modification will affect modules that import this one.
irreducible [persistent] pr2
persistent attribute pr2 [irreducible]
#+END_SRC
The reducible and irreducible annotations can be removed using the modifier =[none]=.
#+BEGIN_SRC lean
definition pr2 (A : Type) (a b : A) : A := b
-- temporarily remove any reducible and irreducible annotation from pr2
reducible [none] pr2
-- permanently remove any reducible and irreducible annotation from pr2
reducible [persistent] [none] pr2
#+END_SRC
Finally, the command =irreducible= is syntax sugar for =reducible [off]=.
The commands =reducible= and =reducible [on]= are equivalent.

4
hott/algebra/category/basic.hlean
View file

@ -12,7 +12,7 @@ open precategory morphism is_equiv eq truncation nat sigma sigma.ops
structure category [class] (ob : Type) extends (precategory ob) :=
(iso_of_path_equiv : Π {a b : ob}, is_equiv (@iso_of_path ob (precategory.mk hom _ comp ID assoc id_left id_right) a b))
multiple_instances [persistent] category
persistent attribute category [multiple-instances]
namespace category
variables {ob : Type} {C : category ob} {a b : ob}
@ -20,7 +20,7 @@ namespace category
-- Make iso_of_path_equiv a class instance
-- TODO: Unsafe class instance?
instance [persistent] iso_of_path_equiv
persistent attribute iso_of_path_equiv [instance]
definition path_of_iso {a b : ob} : a ≅ b → a = b :=
iso_of_path⁻¹

2
hott/algebra/category/set.hlean
View file

@ -29,7 +29,7 @@ end precategory
namespace category
universe variable l
instance precategory.set_precategory.{l+1 l}
attribute precategory.set_precategory.{l+1 l} [instance]
definition set_category_equiv_iso (a b : (Σ (A : Type.{l}), is_hset A))
: (a ≅ b) = (a.1 ≃ b.1) :=

49
hott/algebra/group.hlean
View file

@ -490,77 +490,76 @@ end add_comm_group
/- bundled structures -/
structure Semigroup :=
(carrier : Type) (struct : semigroup carrier)
coercion Semigroup.carrier
instance Semigroup.struct
persistent attribute Semigroup.carrier [coercion]
persistent attribute Semigroup.struct [instance]
structure CommSemigroup :=
(carrier : Type) (struct : comm_semigroup carrier)
coercion CommSemigroup.carrier
instance CommSemigroup.struct
persistent attribute CommSemigroup.carrier [coercion]
persistent attribute CommSemigroup.struct [instance]
structure Monoid :=
(carrier : Type) (struct : monoid carrier)
coercion Monoid.carrier
instance Monoid.struct
persistent attribute Monoid.carrier [coercion]
persistent attribute Monoid.struct [instance]
structure CommMonoid :=
(carrier : Type) (struct : comm_monoid carrier)
coercion CommMonoid.carrier
instance CommMonoid.struct
persistent attribute CommMonoid.carrier [coercion]
persistent attribute CommMonoid.struct [instance]
structure Group :=
(carrier : Type) (struct : group carrier)
coercion Group.carrier
instance Group.struct
persistent attribute Group.carrier [coercion]
persistent attribute Group.struct [instance]
structure CommGroup :=
(carrier : Type) (struct : comm_group carrier)
coercion CommGroup.carrier
instance CommGroup.struct
persistent attribute CommGroup.carrier [coercion]
persistent attribute CommGroup.struct [instance]
structure AddSemigroup :=
(carrier : Type) (struct : add_semigroup carrier)
coercion AddSemigroup.carrier
instance AddSemigroup.struct
persistent attribute AddSemigroup.carrier [coercion]
persistent attribute AddSemigroup.struct [instance]
structure AddCommSemigroup :=
(carrier : Type) (struct : add_comm_semigroup carrier)
coercion AddCommSemigroup.carrier
instance AddCommSemigroup.struct
persistent attribute AddCommSemigroup.carrier [coercion]
persistent attribute AddCommSemigroup.struct [instance]
structure AddMonoid :=
(carrier : Type) (struct : add_monoid carrier)
coercion AddMonoid.carrier
instance AddMonoid.struct
persistent attribute AddMonoid.carrier [coercion]
persistent attribute AddMonoid.struct [instance]
structure AddCommMonoid :=
(carrier : Type) (struct : add_comm_monoid carrier)
coercion AddCommMonoid.carrier
instance AddCommMonoid.struct
persistent attribute AddCommMonoid.carrier [coercion]
persistent attribute AddCommMonoid.struct [instance]
structure AddGroup :=
(carrier : Type) (struct : add_group carrier)
coercion AddGroup.carrier
instance AddGroup.struct
persistent attribute AddGroup.carrier [coercion]
persistent attribute AddGroup.struct [instance]
structure AddCommGroup :=
(carrier : Type) (struct : add_comm_group carrier)
coercion AddCommGroup.carrier
instance AddCommGroup.struct
persistent attribute AddCommGroup.carrier [coercion]
persistent attribute AddCommGroup.struct [instance]
end path_algebra

2
hott/algebra/groupoid.hlean
View file

@ -14,7 +14,7 @@ structure groupoid [class] (ob : Type) extends precategory ob :=
namespace groupoid
instance [persistent] all_iso
persistent attribute all_iso [instance]
--set_option pp.universes true
--set_option pp.implicit true

4
hott/algebra/precategory/basic.hlean
View file

@ -14,13 +14,13 @@ structure precategory [class] (ob : Type) : Type :=
(id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f)
(id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f)
multiple_instances [persistent] precategory
persistent attribute precategory [multiple-instances]
namespace precategory
variables {ob : Type} [C : precategory ob]
variables {a b c d : ob}
include C
instance [persistent] homH
persistent attribute homH [instance]
definition compose := comp

2
hott/algebra/precategory/constructions.hlean
View file

@ -110,7 +110,7 @@ namespace precategory
infixr `×c`:30 := product.Prod_precategory
--instance [persistent] type_category category_one
-- category_two product.prod_category
instance [persistent] product.prod_precategory
persistent attribute product.prod_precategory [instance]
end ops

6
hott/algebra/precategory/functor.hlean
View file

@ -19,8 +19,8 @@ infixl `⇒`:25 := functor
namespace functor
variables {C D E : Precategory}
coercion [persistent] obF
coercion [persistent] homF
persistent attribute obF [coercion]
persistent attribute homF [coercion]
-- "functor C D" is equivalent to a certain sigma type
set_option unifier.max_steps 38500
@ -156,7 +156,7 @@ namespace precategory
namespace ops
notation `PreCat`:max := Precat_of_strict_cats
instance [persistent] precat_of_strict_precats
persistent attribute precat_of_strict_precats [instance]
end ops

4
hott/algebra/precategory/morphism.hlean
View file

@ -16,7 +16,7 @@ namespace morphism
inductive is_iso [class] (f : a ⟶ b) : Type
:= mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
multiple_instances [persistent] is_iso
persistent attribute is_iso [multiple-instances]
definition retraction_of (f : a ⟶ b) [H : is_section f] : hom b a :=
is_section.rec (λg h, g) H
@ -133,7 +133,7 @@ namespace morphism
namespace isomorphic
-- openrelation
instance [persistent] is_iso
persistent attribute is_iso [instance]
definition refl (a : ob) : a ≅ a :=
mk id

2
hott/init/axioms/funext_varieties.hlean
View file

@ -85,7 +85,7 @@ context
@transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f idhtpy) (sigma.mk g h)
(@path_contr _ contr_basedhtpy _ _) d
reducible htpy_ind
attribute htpy_ind [reducible]
definition htpy_ind_beta : htpy_ind f idhtpy = d :=
(@path2_contr _ _ _ _ !path_contr idp)⁻¹ ▹ idp

2
hott/init/equiv.hlean
View file

@ -212,7 +212,7 @@ end is_equiv
namespace equiv
instance [persistent] to_is_equiv
persistent attribute to_is_equiv [instance]
infix `≃`:25 := equiv

2
hott/init/hedberg.hlean
View file

@ -43,4 +43,4 @@ context
... = q : aux)
end
instance [persistent] is_hset_of_decidable_eq
persistent attribute is_hset_of_decidable_eq [instance]

2
hott/init/nat.hlean
View file

@ -296,7 +296,7 @@ namespace nat
notation a * b := mul a b
reducible sub
attribute sub [reducible]
definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b :=
rec_on b
rfl

2
hott/init/trunc.hlean
View file

@ -188,7 +188,7 @@ namespace truncation
structure trunctype (n : trunc_index) :=
(trunctype_type : Type) (is_trunc_trunctype_type : is_trunc n trunctype_type)
coercion trunctype.trunctype_type
attribute trunctype.trunctype_type [coercion]
notation n `-Type` := trunctype n
notation `hprop` := -1-Type

5
hott/types/sigma.hlean
View file

@ -142,7 +142,7 @@ namespace sigma
apply dpair_eq_dpair_pp_pp
end
reducible dpair_eq_dpair
attribute dpair_eq_dpair [reducible]
definition dpair_eq_dpair_p1_1p (p : a = a') (q : p ▹ b = b') :
dpair_eq_dpair p q = dpair_eq_dpair p idp ⬝ dpair_eq_dpair idp q :=
begin
@ -285,7 +285,8 @@ namespace sigma
equiv.mk (functor f g) !is_equiv_functor
context --remove
irreducible inv function.compose --remove
attribute inv [irreducible]
attribute function.compose [irreducible] --remove
definition equiv_functor (Hf : A ≃ A') (Hg : Π a, B a ≃ B' (to_fun Hf a)) :
(Σa, B a) ≃ (Σa', B' a') :=
equiv_functor_of_is_equiv (to_fun Hf) (λ a, to_fun (Hg a))

2
library/algebra/category/basic.lean
View file

@ -19,7 +19,7 @@ structure category [class] (ob : Type) : Type :=
(id_left : Π ⦃a b : ob⦄ (f : hom a b), comp !ID f = f)
(id_right : Π ⦃a b : ob⦄ (f : hom a b), comp f !ID = f)
multiple_instances [persistent] category
persistent attribute category [multiple-instances]
namespace category
variables {ob : Type} [C : category ob]

12
library/algebra/category/constructions.lean
View file

@ -77,10 +77,10 @@ namespace category
(λ a b c d h g f, @subsingleton.elim (set_hom a d) _ _ _)
(λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
(λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
reducible discrete_category
attribute discrete_category [reducible]
definition Discrete_category (A : Type) [H : decidable_eq A] := Mk (discrete_category A)
context
instance discrete_category
attribute discrete_category [instance]
include H
theorem dicrete_category.endomorphism {a b : A} (f : a ⟶ b) : a = b :=
decidable.rec_on (H a b) (λh f, h) (λh f, empty.rec _ f) f
@ -125,8 +125,10 @@ namespace category
notation 2 := Category_two
postfix `ᵒᵖ`:max := opposite.Opposite
infixr `×c`:30 := product.Prod_category
instance [persistent] type_category category_one
category_two product.prod_category
persistent attribute type_category [instance]
persistent attribute category_one [instance]
persistent attribute category_two [instance]
persistent attribute product.prod_category [instance]
end ops
open ops
@ -226,7 +228,7 @@ namespace category
definition Slice_category [reducible] (C : Category) (c : C) := Mk (slice_category C c)
open category.ops
instance [persistent] slice_category
persistent attribute slice_category [instance]
variables {D : Category}
definition forgetful (x : D) : (Slice_category D x) ⇒ D :=
functor.mk (λ a, to_ob a)

9
library/algebra/category/functor.lean
View file

@ -21,9 +21,10 @@ structure functor (C D : Category) : Type :=
infixl `⇒`:25 := functor
namespace functor
coercion [persistent] object
coercion [persistent] morphism
irreducible [persistent] respect_id respect_comp
persistent attribute object [coercion]
persistent attribute morphism [coercion]
persistent attribute respect_id [irreducible]
persistent attribute respect_comp [irreducible]
variables {A B C D : Category}
@ -70,7 +71,7 @@ namespace category
namespace ops
notation `Cat`:max := Category_of_categories
instance [persistent] category_of_categories
persistent attribute category_of_categories [instance]
end ops
end category

4
library/algebra/category/morphism.lean
View file

@ -20,7 +20,7 @@ namespace morphism
inductive is_iso [class] (f : a ⟶ b) : Type
:= mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
multiple_instances [persistent] is_iso
persistent attribute is_iso [multiple-instances]
definition retraction_of (f : a ⟶ b) [H : is_section f] : hom b a :=
is_section.rec (λg h, g) H
@ -131,7 +131,7 @@ namespace morphism
namespace isomorphic
open relation
instance [persistent] is_iso
persistent attribute is_iso [instance]
theorem refl (a : ob) : a ≅ a := mk id
theorem symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a := mk (inverse (iso H))

48
library/algebra/group.lean
View file

@ -489,73 +489,73 @@ end add_comm_group
structure Semigroup :=
(carrier : Type) (struct : semigroup carrier)
coercion Semigroup.carrier
instance Semigroup.struct
persistent attribute Semigroup.carrier [coercion]
persistent attribute Semigroup.struct [instance]
structure CommSemigroup :=
(carrier : Type) (struct : comm_semigroup carrier)
coercion CommSemigroup.carrier
instance CommSemigroup.struct
persistent attribute CommSemigroup.carrier [coercion]
persistent attribute CommSemigroup.struct [instance]
structure Monoid :=
(carrier : Type) (struct : monoid carrier)
coercion Monoid.carrier
instance Monoid.struct
persistent attribute Monoid.carrier [coercion]
persistent attribute Monoid.struct [instance]
structure CommMonoid :=
(carrier : Type) (struct : comm_monoid carrier)
coercion CommMonoid.carrier
instance CommMonoid.struct
persistent attribute CommMonoid.carrier [coercion]
persistent attribute CommMonoid.struct [instance]
structure Group :=
(carrier : Type) (struct : group carrier)
coercion Group.carrier
instance Group.struct
persistent attribute Group.carrier [coercion]
persistent attribute Group.struct [instance]
structure CommGroup :=
(carrier : Type) (struct : comm_group carrier)
coercion CommGroup.carrier
instance CommGroup.struct
persistent attribute CommGroup.carrier [coercion]
persistent attribute CommGroup.struct [instance]
structure AddSemigroup :=
(carrier : Type) (struct : add_semigroup carrier)
coercion AddSemigroup.carrier
instance AddSemigroup.struct
persistent attribute AddSemigroup.carrier [coercion]
persistent attribute AddSemigroup.struct [instance]
structure AddCommSemigroup :=
(carrier : Type) (struct : add_comm_semigroup carrier)
coercion AddCommSemigroup.carrier
instance AddCommSemigroup.struct
persistent attribute AddCommSemigroup.carrier [coercion]
persistent attribute AddCommSemigroup.struct [instance]
structure AddMonoid :=
(carrier : Type) (struct : add_monoid carrier)
coercion AddMonoid.carrier
instance AddMonoid.struct
persistent attribute AddMonoid.carrier [coercion]
persistent attribute AddMonoid.struct [instance]
structure AddCommMonoid :=
(carrier : Type) (struct : add_comm_monoid carrier)
coercion AddCommMonoid.carrier
instance AddCommMonoid.struct
persistent attribute AddCommMonoid.carrier [coercion]
persistent attribute AddCommMonoid.struct [instance]
structure AddGroup :=
(carrier : Type) (struct : add_group carrier)
coercion AddGroup.carrier
instance AddGroup.struct
persistent attribute AddGroup.carrier [coercion]
persistent attribute AddGroup.struct [instance]
structure AddCommGroup :=
(carrier : Type) (struct : add_comm_group carrier)
coercion AddCommGroup.carrier
instance AddCommGroup.struct
persistent attribute AddCommGroup.carrier [coercion]
persistent attribute AddCommGroup.struct [instance]
end algebra

3
library/data/bool.lean
View file

@ -10,7 +10,8 @@ import logic.eq
open eq eq.ops decidable
namespace bool
reducible bor band rec_on
attribute bor [reducible]
attribute band [reducible]
theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
cases_on b (or.inl rfl) (or.inr rfl)

9
library/data/int/basic.lean
View file

@ -42,7 +42,7 @@ inductive int : Type :=
neg_succ_of_nat : nat → int
notation `ℤ` := int
coercion [persistent] int.of_nat
persistent attribute int.of_nat [coercion]
definition int.of_num [coercion] [reducible] (n : num) : ℤ := int.of_nat (nat.of_num n)
namespace int
@ -128,7 +128,7 @@ calc
... = of_nat (m - n) : rfl
context
reducible sub_nat_nat
attribute sub_nat_nat [reducible]
theorem sub_nat_nat_of_lt {m n : ℕ} (H : m < n) :
sub_nat_nat m n = neg_succ_of_nat (pred (n - m)) :=
have H1 : n - m = succ (pred (n - m)), from (succ_pred_of_pos (sub_pos_of_lt H))⁻¹,
@ -282,7 +282,8 @@ calc
... = b : abstr_repr
context
reducible abstr dist
attribute abstr [reducible]
attribute dist [reducible]
theorem nat_abs_abstr (p : ℕ × ℕ) : nat_abs (abstr p) = dist (pr1 p) (pr2 p) :=
let m := pr1 p, n := pr2 p in
or.elim (@le_or_gt n m)
@ -463,7 +464,7 @@ have H3 : pabs (padd (repr a) (repr b)) ≤ pabs (repr a) + pabs (repr b),
H⁻¹ ▸ H1⁻¹ ▸ H2⁻¹ ▸ H3
context
reducible nat_abs
attribute nat_abs [reducible]
theorem mul_nat_abs (a b : ℤ) : nat_abs (a * b) = #nat (nat_abs a) * (nat_abs b) :=
cases_on a
(take m,

3
library/data/list/basic.lean
View file

@ -197,7 +197,8 @@ induction_on s
theorem mem_concat (x : T) (s t : list T) : x ∈ s ++ t ↔ x ∈ s ∨ x ∈ t :=
iff.intro mem_concat_imp_or mem_or_imp_concat
reducible mem append
attribute mem [reducible]
attribute append [reducible]
theorem mem_split {x : T} {l : list T} : x ∈ l → ∃s t : list T, l = s ++ (x::t) :=
induction_on l
(take H : x ∈ nil, false.elim (iff.elim_left !mem_nil H))

2
library/data/nat/div.lean
View file

@ -333,7 +333,7 @@ private definition pair_nat.lt : nat × nat → nat × nat → Prop := measure p
private definition pair_nat.lt.wf : well_founded pair_nat.lt :=
intro_k (measure.wf pr₂) 20 -- we use intro_k to be able to execute gcd efficiently in the kernel
instance pair_nat.lt.wf -- instance will not be saved in .olean
attribute pair_nat.lt.wf [instance] -- instance will not be saved in .olean
infixl [local] `≺`:50 := pair_nat.lt
private definition gcd.lt.dec (x y₁ : nat) : (succ y₁, x mod succ y₁) ≺ (x, succ y₁) :=

2
library/init/nat.lean
View file

@ -289,7 +289,7 @@ namespace nat
notation a * b := mul a b
section
reducible sub
attribute sub [reducible]
definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b :=
induction_on b
rfl

9
src/emacs/lean-syntax.el
View file

@ -8,15 +8,16 @@
(require 'rx)
(defconst lean-keywords
'("import" "prelude" "reducible" "irreducible" "tactic_hint" "protected" "private" "opaque" "definition" "renaming"
'("import" "prelude" "tactic_hint" "protected" "private" "opaque" "definition" "renaming"
"hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "constant" "constants"
"hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "example"
"context" "open" "as" "export" "axiom" "inductive" "with" "structure" "record" "universe" "universes"
"alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix"
"calc_trans" "calc_subst" "calc_refl" "calc_symm" "match"
"infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
"using" "namespace" "instance" "class" "multiple_instances" "section" "fields" "find_decl"
"set_option" "add_rewrite" "extends" "include" "omit" "classes" "instances" "coercions" "raw")
"using" "namespace" "section" "fields" "find_decl"
"attribute" "persistent" "set_option" "add_rewrite" "extends" "include" "omit" "classes"
"instances" "coercions" "raw")
"lean keywords")
(defconst lean-syntax-table
@ -116,7 +117,7 @@
(,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
;; modifiers
(,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]"
"\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]" "\[wf\]" "\[whnf\]"
"\[coercion\]" "\[reducible\]" "\[irreducible\]" "\[wf\]" "\[whnf\]" "\[multiple-instances\]"
"\[decls\]" "\[strict\]" "\[local\]" "\[coercions\]" "\[classes\]" "\[notations\]" "\[tactic_hints\]" "\[reduce_hints\]"))
. 'font-lock-doc-face)
(,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)

2
src/frontends/lean/CMakeLists.txt
View file

@ -3,7 +3,7 @@ token_table.cpp scanner.cpp parse_table.cpp parser_config.cpp
parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp
server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp
begin_end_ext.cpp class.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
begin_end_ext.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.cpp
coercion_elaborator.cpp info_tactic.cpp proof_qed_elaborator.cpp
init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp

71
src/frontends/lean/builtin_cmds.cpp
View file

@ -35,7 +35,6 @@ Author: Leonardo de Moura
#include "frontends/lean/find_cmd.h"
#include "frontends/lean/begin_end_ext.h"
#include "frontends/lean/decl_cmds.h"
#include "frontends/lean/class.h"
#include "frontends/lean/tactic_hint.h"
#include "frontends/lean/tokens.h"
#include "frontends/lean/parse_table.h"
@ -536,72 +535,6 @@ environment open_export_cmd(parser & p, bool open) {
environment open_cmd(parser & p) { return open_export_cmd(p, true); }
environment export_cmd(parser & p) { return open_export_cmd(p, false); }
environment coercion_cmd(parser & p) {
if (in_context_or_parametric_section(p))
throw parser_error("invalid 'coercion' command, coercions cannot be defined in contexts or "
"sections containing parameters", p.pos());
bool persistent = false;
parse_persistent(p, persistent);
name f = p.check_constant_next("invalid 'coercion' command, constant expected");
if (p.curr_is_token(get_colon_tk())) {
p.next();
name C = p.check_constant_next("invalid 'coercion' command, constant expected");
return add_coercion(p.env(), f, C, p.ios(), persistent);
} else {
return add_coercion(p.env(), f, p.ios(), persistent);
}
}
static void parse_reducible_modifiers(parser & p, reducible_status & status, bool & persistent) {
while (true) {
if (parse_persistent(p, persistent)) {
} else if (p.curr_is_token_or_id(get_on_tk())) {
p.next();
status = reducible_status::On;
} else if (p.curr_is_token_or_id(get_off_tk())) {
p.next();
status = reducible_status::Off;
} else if (p.curr_is_token_or_id(get_none_tk())) {
p.next();
status = reducible_status::None;
} else {
break;
}
}
}
environment reducible_cmd(parser & p) {
environment env = p.env();
reducible_status status = reducible_status::On;
bool persistent = false;
parse_reducible_modifiers(p, status, persistent);
bool found = false;
while (p.curr_is_identifier()) {
name c = p.check_constant_next("invalid 'reducible' command, constant expected");
found = true;
env = set_reducible(env, c, status, persistent);
}
if (!found)
throw exception("invalid empty 'reducible' command");
return env;
}
environment irreducible_cmd(parser & p) {
environment env = p.env();
reducible_status status = reducible_status::Off;
bool persistent = false;
parse_persistent(p, persistent);
bool found = false;
while (p.curr_is_identifier()) {
name c = p.check_constant_next("invalid 'irreducible' command, constant expected");
found = true;
env = set_reducible(env, c, status, persistent);
}
if (!found)
throw exception("invalid empty 'irreducible' command");
return env;
}
environment erase_cache_cmd(parser & p) {
name n = p.check_id_next("invalid #erase_cache command, identifier expected");
p.erase_cached_definition(n);
@ -656,9 +589,6 @@ void init_cmd_table(cmd_table & r) {
add_cmd(r, cmd_info("end", "close the current namespace/section", end_scoped_cmd));
add_cmd(r, cmd_info("check", "type check given expression, and display its type", check_cmd));
add_cmd(r, cmd_info("eval", "evaluate given expression", eval_cmd));
add_cmd(r, cmd_info("coercion", "add a new coercion", coercion_cmd));
add_cmd(r, cmd_info("reducible", "mark definitions as reducible/irreducible for automation", reducible_cmd));
add_cmd(r, cmd_info("irreducible", "mark definitions as irreducible for automation", irreducible_cmd));
add_cmd(r, cmd_info("find_decl", "find definitions and/or theorems", find_cmd));
add_cmd(r, cmd_info("#erase_cache", "erase cached definition (for debugging purposes)", erase_cache_cmd));
add_cmd(r, cmd_info("#projections", "generate projections for inductive datatype (for debugging purposes)", projections_cmd));
@ -670,7 +600,6 @@ void init_cmd_table(cmd_table & r) {
register_notation_cmds(r);
register_calc_cmds(r);
register_begin_end_cmds(r);
register_class_cmds(r);
register_tactic_hint_cmd(r);
}

92
src/frontends/lean/class.cpp
View file

@ -1,92 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <string>
#include "library/num.h"
#include "library/normalize.h"
#include "library/class.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/util.h"
#include "frontends/lean/tokens.h"
namespace lean {
optional<unsigned> parse_instance_priority(parser & p) {
if (p.curr_is_token(get_priority_tk())) {
p.next();
auto pos = p.pos();
environment env = open_priority_aliases(open_num_notation(p.env()));
parser::local_scope scope(p, env);
expr val = p.parse_expr();
val = normalize(p.env(), val);
if (optional<mpz> mpz_val = to_num(val)) {
if (!mpz_val->is_unsigned_int())
throw parser_error("invalid 'priority', argument does not fit in a machine integer", pos);
p.check_token_next(get_rbracket_tk(), "invalid 'priority', ']' expected");
return optional<unsigned>(mpz_val->get_unsigned_int());
} else {
throw parser_error("invalid 'priority', argument does not evaluate to a numeral", pos);
}
} else {
return optional<unsigned>();
}
}
environment add_instance_cmd(parser & p) {
bool found = false;
bool persistent = false;
parse_persistent(p, persistent);
optional<unsigned> priority = parse_instance_priority(p);
environment env = p.env();
while (p.curr_is_identifier()) {
found = true;
name c = p.check_constant_next("invalid 'class instance' declaration, constant expected");
if (priority)
env = add_instance(env, c, *priority, persistent);
else
env = add_instance(env, c, persistent);
}
if (!found)
throw parser_error("invalid 'class instance' declaration, at least one identifier expected", p.pos());
return env;
}
environment add_class_cmd(parser & p) {
bool found = false;
environment env = p.env();
bool persistent = false;
parse_persistent(p, persistent);
while (p.curr_is_identifier()) {
found = true;
name c = p.check_constant_next("invalid 'class' declaration, constant expected");
env = add_class(env, c, persistent);
}
if (!found)
throw parser_error("invalid 'class' declaration, at least one identifier expected", p.pos());
return env;
}
environment multiple_instances_cmd(parser & p) {
bool found = false;
environment env = p.env();
bool persistent = false;
parse_persistent(p, persistent);
while (p.curr_is_identifier()) {
found = true;
name c = p.check_constant_next("invalid 'multiple_instances' command, constant expected");
env = mark_multiple_instances(env, c, persistent);
}
if (!found)
throw parser_error("invalid 'multiple_instances' command, at least one identifier expected", p.pos());
return env;
}
void register_class_cmds(cmd_table & r) {
add_cmd(r, cmd_info("instance", "add a new instance", add_instance_cmd));
add_cmd(r, cmd_info("class", "add a new class", add_class_cmd));
add_cmd(r, cmd_info("multiple_instances", "mark that Lean must explore multiple instances of the given class", multiple_instances_cmd));
}
}

17
src/frontends/lean/class.h
View file

@ -1,17 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "util/name.h"
#include "util/list.h"
#include "kernel/environment.h"
#include "frontends/lean/cmd_table.h"
namespace lean {
/** \brief Parse priority for an class instance */
optional<unsigned> parse_instance_priority(parser & p);
void register_class_cmds(cmd_table & r);
}

132
src/frontends/lean/decl_cmds.cpp
View file

@ -12,7 +12,9 @@ Author: Leonardo de Moura
#include "kernel/for_each_fn.h"
#include "library/scoped_ext.h"
#include "library/aliases.h"
#include "library/num.h"
#include "library/private.h"
#include "library/normalize.h"
#include "library/protected.h"
#include "library/placeholder.h"
#include "library/locals.h"
@ -23,7 +25,6 @@ Author: Leonardo de Moura
#include "library/unfold_macros.h"
#include "library/definitional/equations.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/class.h"
#include "frontends/lean/util.h"
#include "frontends/lean/tokens.h"
@ -269,15 +270,45 @@ static environment constants_cmd(parser & p) {
return variables_cmd_core(p, variable_kind::Constant);
}
struct decl_modifiers {
struct decl_attributes {
bool m_def_only; // if true only definition attributes are allowed
bool m_is_instance;
bool m_is_coercion;
bool m_is_reducible;
bool m_is_irreducible;
bool m_is_class;
bool m_has_multiple_instances;
optional<unsigned> m_priority;
decl_modifiers():m_priority() {
m_is_instance = false;
m_is_coercion = false;
m_is_reducible = false;
decl_attributes(bool def_only = true):m_priority() {
m_def_only = def_only;
m_is_instance = false;
m_is_coercion = false;
m_is_reducible = false;
m_is_irreducible = false;
m_is_class = false;
m_has_multiple_instances = false;
}
optional<unsigned> parse_instance_priority(parser & p) {
if (p.curr_is_token(get_priority_tk())) {
p.next();
auto pos = p.pos();
environment env = open_priority_aliases(open_num_notation(p.env()));
parser::local_scope scope(p, env);
expr val = p.parse_expr();
val = normalize(p.env(), val);
if (optional<mpz> mpz_val = to_num(val)) {
if (!mpz_val->is_unsigned_int())
throw parser_error("invalid 'priority', argument does not fit in a machine integer", pos);
p.check_token_next(get_rbracket_tk(), "invalid 'priority', ']' expected");
return optional<unsigned>(mpz_val->get_unsigned_int());
} else {
throw parser_error("invalid 'priority', argument does not evaluate to a numeral", pos);
}
} else {
return optional<unsigned>();
}
}
void parse(parser & p) {
@ -290,20 +321,61 @@ struct decl_modifiers {
auto pos = p.pos();
p.next();
if (in_context(p.env()))
throw parser_error("invalid '[coercion]' modifier, coercions cannot be defined in contexts", pos);
throw parser_error("invalid '[coercion]' attribute, coercions cannot be defined in contexts", pos);
m_is_coercion = true;
} else if (p.curr_is_token(get_reducible_tk())) {
if (m_is_irreducible)
throw parser_error("invalid '[reducible]' attribute, '[irreducible]' was already provided", pos);
m_is_reducible = true;
p.next();
} else if (p.curr_is_token(get_irreducible_tk())) {
if (m_is_reducible)
throw parser_error("invalid '[irreducible]' attribute, '[reducible]' was already provided", pos);
m_is_irreducible = true;
p.next();
} else if (p.curr_is_token(get_class_tk())) {
if (m_def_only)
throw parser_error("invalid '[class]' attribute, definitions cannot be marked as classes", pos);
m_is_class = true;
p.next();
} else if (p.curr_is_token(get_multiple_instances_tk())) {
if (m_def_only)
throw parser_error("invalid '[multiple-instances]' attribute, only classes can have this attribute", pos);
m_has_multiple_instances = true;
p.next();
} else if (auto it = parse_instance_priority(p)) {
m_priority = *it;
if (!m_is_instance)
throw parser_error("invalid '[priority]' occurrence, declaration must be marked as an '[instance]'", pos);
throw parser_error("invalid '[priority]' attribute, declaration must be marked as an '[instance]'", pos);
} else {
break;
}
}
}
environment apply(environment env, io_state const & ios, name const & d, bool persistent) {
if (m_is_instance) {
if (m_priority) {
#if defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
#endif
env = add_instance(env, d, *m_priority, persistent);
} else {
env = add_instance(env, d, persistent);
}
}
if (m_is_coercion)
env = add_coercion(env, d, ios, persistent);
if (m_is_reducible)
env = set_reducible(env, d, reducible_status::On, persistent);
if (m_is_irreducible)
env = set_reducible(env, d, reducible_status::Off, persistent);
if (m_is_class)
env = add_class(env, d, persistent);
if (m_has_multiple_instances)
env = mark_multiple_instances(env, d, persistent);
return env;
}
};
static void check_end_of_theorem(parser const & p) {
@ -519,7 +591,7 @@ class definition_cmd_fn {
pos_info m_pos;
name m_name;
decl_modifiers m_modifiers;
decl_attributes m_attributes;
name m_real_name; // real name for this declaration
buffer<name> m_ls_buffer;
buffer<name> m_aux_decls; // user provided names for aux_decls
@ -550,7 +622,7 @@ class definition_cmd_fn {
parse_univ_params(m_p, m_ls_buffer);
// Parse modifiers
m_modifiers.parse(m_p);
m_attributes.parse(m_p);
if (m_p.curr_is_token(get_assign_tk())) {
auto pos = m_p.pos();
@ -702,25 +774,12 @@ class definition_cmd_fn {
// TODO(Leo): register aux_decls
if (!m_is_private)
m_p.add_decl_index(real_n, m_pos, m_p.get_cmd_token(), type);
if (n != real_n)
m_env = add_expr_alias_rec(m_env, n, real_n);
if (m_modifiers.m_is_instance) {
bool persistent = true;
if (m_modifiers.m_priority) {
#if defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
#endif
m_env = add_instance(m_env, real_n, *m_modifiers.m_priority, persistent);
} else {
m_env = add_instance(m_env, real_n, persistent);
}
}
if (m_modifiers.m_is_coercion)
m_env = add_coercion(m_env, real_n, m_p.ios());
if (m_is_protected)
m_env = add_protected(m_env, real_n);
if (m_modifiers.m_is_reducible)
m_env = set_reducible(m_env, real_n, reducible_status::On);
if (n != real_n)
m_env = add_expr_alias_rec(m_env, n, real_n);
bool persistent = true;
m_env = m_attributes.apply(m_env, m_p.ios(), real_n, persistent);
}
}
@ -947,6 +1006,23 @@ static environment omit_cmd(parser & p) {
return include_cmd_core(p, false);
}
static environment attribute_cmd_core(parser & p, bool persistent) {
name d = p.check_constant_next("invalid 'attribute' command, constant expected");
bool decl_only = false;
decl_attributes attributes(decl_only);
attributes.parse(p);
return attributes.apply(p.env(), p.ios(), d, persistent);
}
static environment attribute_cmd(parser & p) {
return attribute_cmd_core(p, false);
}
static environment persistent_attribute_cmd(parser & p) {
p.check_token_next(get_attribute_tk(), "invalid command, 'attribute' expected");
return attribute_cmd_core(p, true);
}
void register_decl_cmds(cmd_table & r) {
add_cmd(r, cmd_info("universe", "declare a universe level", universe_cmd));
add_cmd(r, cmd_info("universes", "declare universe levels", universes_cmd));
@ -964,6 +1040,8 @@ void register_decl_cmds(cmd_table & r) {
add_cmd(r, cmd_info("protected", "add new protected definition/theorem", protected_definition_cmd));
add_cmd(r, cmd_info("theorem", "add new theorem", theorem_cmd));
add_cmd(r, cmd_info("include", "force section parameter/variable to be included", include_cmd));
add_cmd(r, cmd_info("attribute", "set declaration attributes", attribute_cmd));
add_cmd(r, cmd_info("persistent", "set declaration attributes (the value is saved in .olean files)", persistent_attribute_cmd));
add_cmd(r, cmd_info("omit", "undo 'include' command", omit_cmd));
}
}

1
src/frontends/lean/elaborator.cpp
View file

@ -42,7 +42,6 @@ Author: Leonardo de Moura
#include "library/definitional/equations.h"
#include "frontends/lean/local_decls.h"
#include "frontends/lean/structure_cmd.h"
#include "frontends/lean/class.h"
#include "frontends/lean/tactic_hint.h"
#include "frontends/lean/info_manager.h"
#include "frontends/lean/info_annotation.h"

1
src/frontends/lean/tactic_hint.cpp
View file

@ -14,7 +14,6 @@ Author: Leonardo de Moura
#include "frontends/lean/tactic_hint.h"
#include "frontends/lean/cmd_table.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/class.h"
#include "frontends/lean/tokens.h"
namespace lean {

4
src/frontends/lean/token_table.cpp
View file

@ -89,12 +89,12 @@ void init_token_table(token_table & t) {
char const * commands[] =
{"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
"variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
"[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[parsing-only]", "reducible", "irreducible",
"[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[parsing-only]", "[multiple-instances]",
"evaluate", "check", "eval", "[wf]", "[whnf]", "[strict]", "[local]", "[priority", "print", "end", "namespace", "section", "prelude",
"import", "inductive", "record", "structure", "module", "universe", "universes",
"precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
"exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
"add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl",
"add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl", "attribute", "persistent",
"include", "omit", "#erase_cache", "#projections", "#telescope_eq", nullptr};
pair<char const *, char const *> aliases[] =

12
src/frontends/lean/tokens.cpp
View file

@ -81,9 +81,12 @@ static name * g_instance = nullptr;
static name * g_priority = nullptr;
static name * g_coercion = nullptr;
static name * g_reducible = nullptr;
static name * g_irreducible = nullptr;
static name * g_parsing_only = nullptr;
static name * g_with = nullptr;
static name * g_class = nullptr;
static name * g_multiple_instances = nullptr;
static name * g_attribute = nullptr;
static name * g_prev = nullptr;
static name * g_scoped = nullptr;
static name * g_foldr = nullptr;
@ -178,9 +181,12 @@ void initialize_tokens() {
g_priority = new name("[priority");
g_coercion = new name("[coercion]");
g_reducible = new name("[reducible]");
g_irreducible = new name("[irreducible]");
g_parsing_only = new name("[parsing-only]");
g_attribute = new name("attribute");
g_with = new name("with");
g_class = new name("[class]");
g_multiple_instances = new name("[multiple-instances]");
g_prev = new name("prev");
g_scoped = new name("scoped");
g_foldr = new name("foldr");
@ -234,6 +240,9 @@ void finalize_tokens() {
delete g_priority;
delete g_coercion;
delete g_reducible;
delete g_irreducible;
delete g_multiple_instances;
delete g_attribute;
delete g_parsing_only;
delete g_in;
delete g_assign;
@ -373,6 +382,9 @@ name const & get_instance_tk() { return *g_instance; }
name const & get_priority_tk() { return *g_priority; }
name const & get_coercion_tk() { return *g_coercion; }
name const & get_reducible_tk() { return *g_reducible; }
name const & get_irreducible_tk() { return *g_irreducible; }
name const & get_multiple_instances_tk() { return *g_multiple_instances; }
name const & get_attribute_tk() { return *g_attribute; }
name const & get_parsing_only_tk() { return *g_parsing_only; }
name const & get_class_tk() { return *g_class; }
name const & get_with_tk() { return *g_with; }

3
src/frontends/lean/tokens.h
View file

@ -83,6 +83,9 @@ name const & get_instance_tk();
name const & get_priority_tk();
name const & get_coercion_tk();
name const & get_reducible_tk();
name const & get_irreducible_tk();
name const & get_multiple_instances_tk();
name const & get_attribute_tk();
name const & get_parsing_only_tk();
name const & get_class_tk();
name const & get_with_tk();

2
tests/lean/bad_class.lean
View file

@ -1,7 +1,7 @@
import logic
namespace foo
definition subsingleton (A : Type) := ∀⦃a b : A⦄, a = b
class subsingleton
attribute subsingleton [class]
protected definition prop.subsingleton [instance] (P : Prop) : subsingleton P :=
λa b, !proof_irrel

2
tests/lean/bad_coercions.lean
View file

@ -15,5 +15,5 @@ context
definition foo (v : vector A n) : list A :=
nil A
coercion foo
attribute foo [coercion]
end

4
tests/lean/bad_coercions.lean.expected.out
View file

@ -1,2 +1,2 @@
bad_coercions.lean:12:18: error: invalid '[coercion]' modifier, coercions cannot be defined in contexts
bad_coercions.lean:18:11: error: invalid 'coercion' command, coercions cannot be defined in contexts or sections containing parameters
bad_coercions.lean:12:18: error: invalid '[coercion]' attribute, coercions cannot be defined in contexts
bad_coercions.lean:18:16: error: invalid '[coercion]' attribute, coercions cannot be defined in contexts

2
tests/lean/hott/bug_struct_level.hlean
View file

@ -6,7 +6,7 @@ context
parameter {D₀ : Type}
parameter (C : precategory D₀)
parameter (D₂ : Π ⦃a b c d : D₀⦄ (f : hom a b) (g : hom c d) (h : hom a c) (i : hom b d), Type)
reducible compose
attribute compose [reducible]
definition comp₁_type [reducible] : Type :=
Π ⦃a b c₁ d₁ c₂ d₂ : D₀⦄

2
tests/lean/run/alias1.lean
View file

@ -20,7 +20,7 @@ check foo a b
check foo x y
constant f : num → val
coercion f
attribute f [coercion]
check foo a x
check foo x y

2
tests/lean/run/alias2.lean
View file

@ -14,7 +14,7 @@ open N1
open N2
constants a b : num
constant f : num → val
coercion f
attribute f [coercion]
definition aux2 := foo a b
check aux2

2
tests/lean/run/class11.lean
View file

@ -1,7 +1,7 @@
import logic
constant C {A : Type} : A → Prop
class C
attribute C [class]
constant f {A : Type} (a : A) [H : C a] : Prop

8
tests/lean/run/class4.lean
View file

@ -74,20 +74,20 @@ constant dvd : Π (x y : nat) {H : not_zero y}, nat
constants a b : nat
set_option pp.implicit true
reducible add
attribute add [reducible]
check dvd a (succ b)
check (λ H : not_zero b, dvd a b)
check (succ zero)
check a + (succ zero)
check dvd a (a + (succ b))
reducible [off] add
attribute add [irreducible]
check dvd a (a + (succ b))
reducible add
attribute add [reducible]
check dvd a (a + (succ b))
reducible [off] add
attribute add [irreducible]
check dvd a (a + (succ b))
end nat

3
tests/lean/run/class6.lean
View file

@ -13,7 +13,8 @@ theorem inhabited_t1 : inhabited t1
theorem inhabited_t2 : inhabited t2
:= inhabited.mk t2.mk2
instance inhabited_t1 inhabited_t2
attribute inhabited_t1 [instance]
attribute inhabited_t2 [instance]
theorem T : inhabited (t1 × t2)
:= _

2
tests/lean/run/class8.lean
View file

@ -4,7 +4,7 @@ open tactic prod
inductive inh [class] (A : Type) : Prop :=
intro : A -> inh A
instance inh.intro
attribute inh.intro [instance]
theorem inh_elim {A : Type} {B : Prop} (H1 : inh A) (H2 : A → B) : B
:= inh.rec H2 H1

4
tests/lean/run/class_bug1.lean
View file

@ -8,7 +8,7 @@ mk : Π (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
(Π {A B : ob} {f : mor A B}, comp f id = f) →
(Π {A B : ob} {f : mor A B}, comp id f = f) →
category ob mor
class category
attribute category [class]
namespace category
context sec_cat
@ -16,7 +16,7 @@ context sec_cat
inductive foo :=
mk : A → foo
class foo
attribute foo [class]
parameters {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor}
definition compose := rec (λ comp id assoc idr idl, comp) Cat
definition id := rec (λ comp id assoc idr idl, id) Cat

4
tests/lean/run/class_bug2.lean
View file

@ -8,7 +8,7 @@ mk : Π (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
(Π {A B : ob} {f : mor A B}, comp f id = f) →
(Π {A B : ob} {f : mor A B}, comp id f = f) →
category ob mor
class category
attribute category [class]
namespace category
section sec_cat
@ -16,7 +16,7 @@ section sec_cat
inductive foo :=
mk : A → foo
class foo
attribute foo [class]
variables {ob : Type} {mor : ob → ob → Type} {Cat : category ob mor}
definition compose := rec (λ comp id assoc idr idl, comp) Cat
definition id := rec (λ comp id assoc idr idl, id) Cat

6
tests/lean/run/class_coe.lean
View file

@ -24,9 +24,9 @@ constants x y : real
constant num_to_nat : num → nat
constant nat_to_int : nat → int
constant int_to_real : int → real
coercion num_to_nat
coercion nat_to_int
coercion int_to_real
attribute num_to_nat [coercion]
attribute nat_to_int [coercion]
attribute int_to_real [coercion]
set_option pp.implicit true
set_option pp.coercions true

2
tests/lean/run/coe1.lean
View file

@ -3,7 +3,7 @@ prelude
constant A : Type.{1}
constant B : Type.{1}
constant f : A → B
coercion f
attribute f [coercion]
constant g : B → B → B
constants a1 a2 a3 : A
constants b1 b2 b3 : B

2
tests/lean/run/coe11.lean
View file

@ -17,7 +17,7 @@ my_functor.rec (λ obF homF Hid Hcomp, homF) F
constants obC obD : Type
constants a b : obC
constant C : category obC
instance C
attribute C [instance]
constant D : category obD
constant F : my_functor C D
constant m : hom a b

2
tests/lean/run/coe2.lean
View file

@ -12,7 +12,7 @@ namespace setoid
infix `≈` := eqv
coercion carrier
attribute carrier [coercion]
inductive morphism (s1 s2 : setoid) : Type :=
mk_morphism : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2

2
tests/lean/run/coe3.lean
View file

@ -12,7 +12,7 @@ namespace setoid
infix `≈` := eqv
coercion carrier
attribute carrier [coercion]
inductive morphism (s1 s2 : setoid) : Type :=
mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2

2
tests/lean/run/coe4.lean
View file

@ -17,7 +17,7 @@ namespace setoid
infix `≈` := eqv
coercion carrier
attribute carrier [coercion]
inductive morphism (s1 s2 : setoid) : Type :=
mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2

2
tests/lean/run/coe5.lean
View file

@ -17,7 +17,7 @@ namespace setoid
infix `≈` := eqv
coercion carrier
attribute carrier [coercion]
inductive morphism (s1 s2 : setoid) : Type :=
mk : Π (f : s1 → s2), (∀ x y, x ≈ y → f x ≈ f y) → morphism s1 s2

2
tests/lean/run/coe7.lean
View file

@ -3,7 +3,7 @@ namespace experiment
constant nat : Type.{1}
constant int : Type.{1}
constant of_nat : nat → int
coercion of_nat
attribute of_nat [coercion]
theorem tst (n : nat) : n = n :=
have H : true, from trivial,

2
tests/lean/run/coe8.lean
View file

@ -3,7 +3,7 @@ namespace experiment
constant nat : Type.{1}
constant int : Type.{1}
constant of_nat : nat → int
coercion of_nat
attribute of_nat [coercion]
constant nat_add : nat → nat → nat
constant int_add : int → int → int
infixl `+` := int_add

8
tests/lean/run/coe9.lean
View file

@ -11,10 +11,10 @@ constant to_row {A : Type} {n : nat} : vector A n → matrix A 1 n
constant to_col {A : Type} {n : nat} : vector A n → matrix A n 1
constant to_list {A : Type} {n : nat} : vector A n → list A
coercion to_row
coercion to_col
coercion list_to_vec
coercion to_list
attribute to_row [coercion]
attribute to_col [coercion]
attribute list_to_vec [coercion]
attribute to_list [coercion]
constant f {A : Type} {n : nat} (M : matrix A n 1) : nat
constant g {A : Type} {n : nat} (M : matrix A 1 n) : nat

2
tests/lean/run/coesec.lean
View file

@ -5,5 +5,5 @@ section
variables {A B : Type}
definition to_function (F : func A B) : A → B :=
func.rec (λf, f) F
coercion to_function
attribute to_function [coercion]
end

2
tests/lean/run/div2.lean
View file

@ -50,7 +50,7 @@ definition rec_measure {dom codom : Type} (default : codom) (measure : dom →
(rec_val : dom → (dom → codom) → codom) (x : dom) : codom :=
rec_measure_aux default measure rec_val (succ (measure x)) x
multiple_instances decidable
attribute decidable [multiple-instances]
theorem rec_measure_aux_spec {dom codom : Type} (default : codom) (measure : dom → ℕ)
(rec_val : dom → (dom → codom) → codom)

2
tests/lean/run/e10.lean
View file

@ -13,7 +13,7 @@ namespace int
constant add : int → int → int
infixl + := add
constant of_nat : nat → int
coercion of_nat
attribute of_nat [coercion]
end int
section

2
tests/lean/run/e11.lean
View file

@ -13,7 +13,7 @@ namespace int
constant add : int → int → int
infixl + := add
constant of_nat : nat → int
coercion of_nat
attribute of_nat [coercion]
end int
section

2
tests/lean/run/e12.lean
View file

@ -13,7 +13,7 @@ namespace int
constant add : int → int → int
infixl + := add
constant of_nat : nat → int
coercion of_nat
attribute of_nat [coercion]
end int
constants n m : nat.nat

2
tests/lean/run/e13.lean
View file

@ -14,7 +14,7 @@ namespace int
infixl + := add
constant of_nat : nat → int
namespace coercions
coercion of_nat
attribute of_nat [coercion]
end coercions
end int

2
tests/lean/run/e14.lean
View file

@ -31,7 +31,7 @@ check vector.rec
definition vector_to_list {A : Type} {n : nat} (v : vector A n) : list A
:= vector.rec (@nil A) (fun (n : nat) (a : A) (v : vector A n) (l : list A), cons a l) v
coercion vector_to_list
attribute vector_to_list [coercion]
constant f : forall {A : Type}, list A → nat

2
tests/lean/run/e17.lean
View file

@ -11,7 +11,7 @@ inductive int : Type :=
of_nat : nat → int,
neg : nat → int
coercion int.of_nat
attribute int.of_nat [coercion]
constants n m : nat
constants i j : int

2
tests/lean/run/e18.lean
View file

@ -11,7 +11,7 @@ inductive int : Type :=
of_nat : nat → int,
neg : nat → int
coercion int.of_nat
attribute int.of_nat [coercion]
constants n m : nat
constants i j : int

2
tests/lean/run/e6.lean
View file

@ -13,7 +13,7 @@ namespace int
constant add : int → int → int
infixl + := add
constant of_nat : nat → int
coercion [persistent] of_nat
persistent attribute of_nat [coercion]
end int
open int

2
tests/lean/run/e7.lean
View file

@ -13,7 +13,7 @@ namespace int
constant add : int → int → int
infixl + := add
constant of_nat : nat → int
coercion of_nat
attribute of_nat [coercion]
end int
open nat

2
tests/lean/run/e8.lean
View file

@ -13,7 +13,7 @@ namespace int
constant add : int → int → int
infixl + := add
constant of_nat : nat → int
coercion of_nat
attribute of_nat [coercion]
end int
-- Open "only" the notation and declarations from the namespaces nat and int

2
tests/lean/run/e9.lean
View file

@ -16,7 +16,7 @@ namespace int
end int
namespace int_coercions
coercion [persistent] int.of_nat
persistent attribute int.of_nat [coercion]
end int_coercions
-- Open "only" the notation and declarations from the namespaces nat and int

2
tests/lean/run/elab_failure.lean
View file

@ -1,6 +1,6 @@
import data.nat.basic data.bool
open bool nat
reducible nat.rec_on
attribute nat.rec_on [reducible]
definition is_eq (a b : nat) : bool :=
nat.rec_on a
(λ b, nat.cases_on b tt (λb₁, ff))

4
tests/lean/run/fibrant_class1.lean
View file

@ -7,10 +7,10 @@ idpath : path a a
notation a ≈ b := path a b
axiom path_fibrant {A : Type'} [fA : fibrant A] (a b : A) : fibrant (path a b)
instance [persistent] path_fibrant
persistent attribute path_fibrant [instance]
axiom imp_fibrant {A : Type'} {B : Type'} [C1 : fibrant A] [C2 : fibrant B] : fibrant (A → B)
instance imp_fibrant
attribute imp_fibrant [instance]
definition test {A : Type} [fA : fibrant A] {x y : A} :
Π (z : A), y ≈ z → fibrant (x ≈ y → x ≈ z) := _

6
tests/lean/run/fibrant_class2.lean
View file

@ -3,13 +3,13 @@ fibrant_mk : fibrant T
axiom pi_fibrant {A : Type} {B : A → Type} [C1 : fibrant A] [C2 : Πx : A, fibrant (B x)] :
fibrant (Πx : A, B x)
instance pi_fibrant
attribute pi_fibrant [instance]
inductive path {A : Type} [fA : fibrant A] (a : A) : A → Type :=
idpath : path a a
axiom path_fibrant {A : Type} [fA : fibrant A] (a b : A) : fibrant (path a b)
instance [persistent] path_fibrant
persistent attribute path_fibrant [instance]
notation a ≈ b := path a b
@ -26,7 +26,7 @@ definition test4 {A : Type} [fA : fibrant A] {x y z : A} :
fibrant (x ≈ y → x ≈ z) := _
axiom imp_fibrant {A : Type} {B : Type} [C1 : fibrant A] [C2 : fibrant B] : fibrant (A → B)
instance imp_fibrant
attribute imp_fibrant [instance]
definition test5 {A : Type} [fA : fibrant A] {x y : A} :
Π (z : A), y ≈ z → fibrant (x ≈ y → x ≈ z) := _

2
tests/lean/run/group2.lean
View file

@ -21,7 +21,7 @@ mk : Π (A : Type), group_struct A → group
definition carrier (g : group) : Type
:= group.rec (λ c s, c) g
coercion carrier
attribute carrier [coercion]
definition group_to_struct [instance] (g : group) : group_struct (carrier g)
:= group.rec (λ (A : Type) (s : group_struct A), s) g

16
tests/lean/run/group4.lean
View file

@ -80,26 +80,26 @@ print prefix algebra.comm_monoid
structure Semigroup :=
mk :: (carrier : Type) (struct : semigroup carrier)
coercion [persistent] Semigroup.carrier
instance [persistent] Semigroup.struct
persistent attribute Semigroup.carrier [coercion]
persistent attribute Semigroup.struct [instance]
structure CommSemigroup :=
mk :: (carrier : Type) (struct : comm_semigroup carrier)
coercion [persistent] CommSemigroup.carrier
instance [persistent] CommSemigroup.struct
persistent attribute CommSemigroup.carrier [coercion]
persistent attribute CommSemigroup.struct [instance]
structure Monoid :=
mk :: (carrier : Type) (struct : monoid carrier)
coercion [persistent] Monoid.carrier
instance [persistent] Monoid.struct
persistent attribute Monoid.carrier [coercion]
persistent attribute Monoid.struct [instance]
structure CommMonoid :=
mk :: (carrier : Type) (struct : comm_monoid carrier)
coercion [persistent] CommMonoid.carrier
instance [persistent] CommMonoid.struct
persistent attribute CommMonoid.carrier [coercion]
persistent attribute CommMonoid.struct [instance]
end algebra

16
tests/lean/run/group5.lean
View file

@ -78,26 +78,26 @@ structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
structure Semigroup :=
(carrier : Type) (struct : semigroup carrier)
coercion [persistent] Semigroup.carrier
instance [persistent] Semigroup.struct
persistent attribute Semigroup.carrier [coercion]
persistent attribute Semigroup.struct [instance]
structure CommSemigroup :=
(carrier : Type) (struct : comm_semigroup carrier)
coercion [persistent] CommSemigroup.carrier
instance [persistent] CommSemigroup.struct
persistent attribute CommSemigroup.carrier [coercion]
persistent attribute CommSemigroup.struct [instance]
structure Monoid :=
(carrier : Type) (struct : monoid carrier)
coercion [persistent] Monoid.carrier
instance [persistent] Monoid.struct
persistent attribute Monoid.carrier [coercion]
persistent attribute Monoid.struct [instance]
structure CommMonoid :=
(carrier : Type) (struct : comm_monoid carrier)
coercion [persistent] CommMonoid.carrier
instance [persistent] CommMonoid.struct
persistent attribute CommMonoid.carrier [coercion]
persistent attribute CommMonoid.struct [instance]
end algebra

2
tests/lean/run/impbug1.lean
View file

@ -11,7 +11,7 @@ mk : Π (id : Π (A : ob), mor A A),
definition id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat
reducible id
attribute id [reducible]
theorem id_left (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) (A : ob) (f : mor A A) :
@eq (mor A A) (id ob mor Cat A) f :=
@category.rec ob mor (λ (C : category ob mor), @eq (mor A A) (id ob mor C A) f)

2
tests/lean/run/impbug2.lean
View file

@ -14,7 +14,7 @@ constant ob : Type.{1}
constant mor : ob → ob → Type.{1}
constant Cat : category ob mor
reducible id
attribute id [reducible]
theorem id_left (A : ob) (f : mor A A) : @eq (mor A A) (id ob mor Cat A) f :=
@category.rec ob mor (λ (C : category ob mor), @eq (mor A A) (id ob mor C A) f)
(λ (id : Π (T : ob), mor T T)

2
tests/lean/run/impbug3.lean
View file

@ -15,7 +15,7 @@ mk : Π (id : Π (A : ob), mor A A),
definition id (Cat : category) := category.rec (λ id idl, id) Cat
constant Cat : category
reducible id
attribute id [reducible]
theorem id_left (A : ob) (f : mor A A) : @eq (mor A A) (id Cat A) f :=
@category.rec (λ (C : category), @eq (mor A A) (id C A) f)
(λ (id : Π (T : ob), mor T T)

2
tests/lean/run/list_elab1.lean
View file

@ -23,7 +23,7 @@ list.rec Hnil Hind l
definition concat {T : Type} (s t : list T) : list T :=
list.rec t (fun x : T, fun l : list T, fun u : list T, cons x u) s
reducible concat
attribute concat [reducible]
theorem concat_nil {T : Type} (t : list T) : concat t nil = t :=
list_induction_on t (eq.refl (concat nil nil))
(take (x : T) (l : list T) (H : concat l nil = l),

2
tests/lean/run/nat_coe.lean
View file

@ -10,7 +10,7 @@ constant int_add : int → int → int
infixl `+` := int_add
constant of_nat : nat → int
coercion of_nat
attribute of_nat [coercion]
constants a b : nat
constants i j : int

2
tests/lean/run/nateq.lean
View file

@ -1,6 +1,6 @@
import data.nat.basic data.bool
open bool nat eq.ops
reducible nat.rec_on
attribute nat.rec_on [reducible]
definition is_eq (a b : nat) : bool :=
nat.rec_on a

2
tests/lean/run/opaque_hint_bug.lean
View file

@ -9,5 +9,5 @@ section
definition concat (s t : list T) : list T
:= list.rec t (fun x l u, list.cons x u) s
reducible concat
attribute concat [reducible]
end

2
tests/lean/run/private_names.lean
View file

@ -3,7 +3,7 @@ section
private definition foo : inhabited Prop :=
inhabited.mk false
instance [priority 1000] foo
attribute foo [instance] [priority 1000]
example : default Prop = false :=
rfl

2
tests/lean/run/tactic23.lean
View file

@ -17,7 +17,7 @@ definition pos_num_to_nat (n : pos_num) : nat
:= pos_num.rec one (λ n r, r + r) (λ n r, r + r + one) n
definition num_to_nat (n : num) : nat
:= num.rec zero (λ n, pos_num_to_nat n) n
coercion num_to_nat
attribute num_to_nat [coercion]
-- Now we can write 2 + 3, the coercion will be applied
check 2 + 3

2
tests/lean/run/trans.lean
View file

@ -11,7 +11,7 @@ definition transport {A : Type} {a b : A} {P : A → Type} (p : a = b) (H : P a)
theorem transport_refl {A : Type} {a : A} {P : A → Type} (H : P a) : transport (refl a) H = H
:= refl H
reducible [off] transport
attribute transport [irreducible]
theorem transport_proof_irrel {A : Type} {a b : A} {P : A → Type} (p1 p2 : a = b) (H : P a) : transport p1 H = transport p2 H
:= refl (transport p1 H)

4
tests/lean/sec2.lean
View file

@ -5,7 +5,7 @@ constant g : B → B
constant a : A
namespace foo
coercion f
attribute f [coercion]
print coercions
check g a
end foo
@ -13,7 +13,7 @@ end foo
check g a -- Error
section boo
coercion f
attribute f [coercion]
print coercions
check g a
end boo

2
tests/lean/slow/list_elab2.lean
View file

@ -61,7 +61,7 @@ list_induction_on t (refl _)
(take (x : T) (l : list T) (H : concat l nil = l),
H ▸ (refl (cons x (concat l nil))))
reducible concat
attribute concat [reducible]
theorem concat_nil2 (t : list T) : t ++ nil = t :=
list_induction_on t (refl _)
(take (x : T) (l : list T) (H : concat l nil = l),