feat(frontends/lean): add coercion modifier
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
08465f049a
commit
bd1873f6b1
3 changed files with 120 additions and 1 deletions
|
@ -13,6 +13,7 @@ Author: Leonardo de Moura
|
|||
#include "library/placeholder.h"
|
||||
#include "library/locals.h"
|
||||
#include "library/explicit.h"
|
||||
#include "library/coercion.h"
|
||||
#include "frontends/lean/parser.h"
|
||||
#include "frontends/lean/util.h"
|
||||
#include "frontends/lean/class.h"
|
||||
|
@ -25,6 +26,7 @@ static name g_assign(":=");
|
|||
static name g_private("[private]");
|
||||
static name g_inline("[inline]");
|
||||
static name g_instance("[instance]");
|
||||
static name g_coercion("[coercion]");
|
||||
|
||||
environment universe_cmd(parser & p) {
|
||||
name n = p.check_id_next("invalid universe declaration, identifier expected");
|
||||
|
@ -167,10 +169,12 @@ struct decl_modifiers {
|
|||
bool m_is_private;
|
||||
bool m_is_opaque;
|
||||
bool m_is_instance;
|
||||
bool m_is_coercion;
|
||||
decl_modifiers() {
|
||||
m_is_private = false;
|
||||
m_is_opaque = true;
|
||||
m_is_instance = false;
|
||||
m_is_coercion = false;
|
||||
}
|
||||
|
||||
void parse(parser & p) {
|
||||
|
@ -184,6 +188,9 @@ struct decl_modifiers {
|
|||
} else if (p.curr_is_token(g_instance)) {
|
||||
m_is_instance = true;
|
||||
p.next();
|
||||
} else if (p.curr_is_token(g_coercion)) {
|
||||
m_is_coercion = true;
|
||||
p.next();
|
||||
} else {
|
||||
break;
|
||||
}
|
||||
|
@ -281,6 +288,8 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) {
|
|||
}
|
||||
if (modifiers.m_is_instance)
|
||||
env = add_instance(env, real_n);
|
||||
if (modifiers.m_is_coercion)
|
||||
env = add_coercion(env, real_n, p.ios());
|
||||
return env;
|
||||
}
|
||||
environment definition_cmd(parser & p) {
|
||||
|
|
|
@ -73,7 +73,7 @@ token_table init_token_table() {
|
|||
{"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
|
||||
|
||||
char const * commands[] = {"theorem", "axiom", "variable", "definition", "coercion",
|
||||
"variables", "[private]", "[inline]", "[fact]", "[instance]", "[class]", "[module]",
|
||||
"variables", "[private]", "[inline]", "[fact]", "[instance]", "[class]", "[module]", "[coercion]",
|
||||
"abbreviation", "opaque_hint", "evaluate", "check", "print", "end", "namespace", "section", "import",
|
||||
"abbreviation", "inductive", "record", "structure", "module", "universe",
|
||||
"precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
|
||||
|
|
110
tests/lean/run/algebra1.lean
Normal file
110
tests/lean/run/algebra1.lean
Normal file
|
@ -0,0 +1,110 @@
|
|||
import standard
|
||||
using num
|
||||
|
||||
abbreviation Type1 := Type.{1}
|
||||
|
||||
section
|
||||
parameter {A : Type}
|
||||
parameter f : A → A → A
|
||||
parameter one : A
|
||||
parameter inv : A → A
|
||||
infixl `*`:75 := f
|
||||
postfix `^-1`:100 := inv
|
||||
definition is_assoc := ∀ a b c, (a*b)*c = a*b*c
|
||||
definition is_id := ∀ a, a*one = a
|
||||
definition is_inv := ∀ a, a*a^-1 = one
|
||||
end
|
||||
|
||||
namespace algebra
|
||||
inductive mul_struct (A : Type) : Type :=
|
||||
| mk_mul_struct : (A → A → A) → mul_struct A
|
||||
|
||||
inductive add_struct (A : Type) : Type :=
|
||||
| mk_add_struct : (A → A → A) → add_struct A
|
||||
|
||||
definition mul [inline] {A : Type} {s : mul_struct A} (a b : A)
|
||||
:= mul_struct_rec (fun f, f) s a b
|
||||
|
||||
infixl `*`:75 := mul
|
||||
|
||||
definition add [inline] {A : Type} {s : add_struct A} (a b : A)
|
||||
:= add_struct_rec (fun f, f) s a b
|
||||
|
||||
infixl `+`:65 := add
|
||||
end
|
||||
|
||||
namespace nat
|
||||
inductive nat : Type :=
|
||||
| zero : nat
|
||||
| succ : nat → nat
|
||||
|
||||
variable add : nat → nat → nat
|
||||
variable mul : nat → nat → nat
|
||||
|
||||
definition is_mul_struct [inline] [instance] : algebra.mul_struct nat
|
||||
:= algebra.mk_mul_struct mul
|
||||
|
||||
definition is_add_struct [inline] [instance] : algebra.add_struct nat
|
||||
:= algebra.mk_add_struct add
|
||||
|
||||
definition to_nat (n : num) : nat
|
||||
:= #algebra
|
||||
num_rec zero (λ n, pos_num_rec (succ zero) (λ n r, r + r) (λ n r, r + r + succ zero) n) n
|
||||
end
|
||||
|
||||
namespace algebra
|
||||
namespace semigroup
|
||||
inductive semigroup_struct (A : Type) : Type :=
|
||||
| mk_semigroup_struct : Π (mul : A → A → A), is_assoc mul → semigroup_struct A
|
||||
|
||||
definition mul [inline] {A : Type} (s : semigroup_struct A) (a b : A)
|
||||
:= semigroup_struct_rec (fun f h, f) s a b
|
||||
|
||||
definition assoc [inline] {A : Type} (s : semigroup_struct A) : is_assoc (mul s)
|
||||
:= semigroup_struct_rec (fun f h, h) s
|
||||
|
||||
definition is_mul_struct [inline] [instance] (A : Type) (s : semigroup_struct A) : mul_struct A
|
||||
:= mk_mul_struct (mul s)
|
||||
|
||||
inductive semigroup : Type :=
|
||||
| mk_semigroup : Π (A : Type), semigroup_struct A → semigroup
|
||||
|
||||
definition carrier [inline] [coercion] (g : semigroup)
|
||||
:= semigroup_rec (fun c s, c) g
|
||||
|
||||
definition is_semigroup [inline] [instance] (g : semigroup) : semigroup_struct (carrier g)
|
||||
:= semigroup_rec (fun c s, s) g
|
||||
end
|
||||
|
||||
namespace monoid
|
||||
inductive monoid_struct (A : Type) : Type :=
|
||||
| mk_monoid_struct : Π (mul : A → A → A) (id : A), is_assoc mul → is_id mul id → monoid_struct A
|
||||
|
||||
definition mul [inline] {A : Type} (s : monoid_struct A) (a b : A)
|
||||
:= monoid_struct_rec (fun mul id a i, mul) s a b
|
||||
|
||||
definition assoc [inline] {A : Type} (s : monoid_struct A) : is_assoc (mul s)
|
||||
:= monoid_struct_rec (fun mul id a i, a) s
|
||||
|
||||
using algebra.semigroup -- Fix: allow user to write just semigroup
|
||||
definition is_semigroup_struct [inline] [instance] (A : Type) (s : monoid_struct A) : semigroup_struct A
|
||||
:= mk_semigroup_struct (mul s) (assoc s)
|
||||
|
||||
inductive monoid : Type :=
|
||||
| mk_monoid : Π (A : Type), monoid_struct A → monoid
|
||||
|
||||
definition carrier [inline] [coercion] (m : monoid)
|
||||
:= monoid_rec (fun c s, c) m
|
||||
|
||||
definition is_monoid [inline] [instance] (m : monoid) : monoid_struct (carrier m)
|
||||
:= monoid_rec (fun c s, s) m
|
||||
end
|
||||
end
|
||||
|
||||
section
|
||||
using algebra algebra.semigroup algebra.monoid
|
||||
variable M : monoid
|
||||
variables a b c : M
|
||||
check a*b*c*a*b*c*a*b*a*b*c*a
|
||||
check a*b
|
||||
end
|
Loading…
Reference in a new issue