From 08b4ce2db9cc3095f0a9197bf20e2c50e96e614c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 3 Nov 2014 22:40:08 -0800 Subject: [PATCH] feat(frontends/lean/structure_cmd): use 'mk' as constructor name when it is not provided --- src/frontends/lean/structure_cmd.cpp | 22 ++-- tests/lean/run/group5.lean | 146 +++++++++++++++++++++++++++ 2 files changed, 162 insertions(+), 6 deletions(-) create mode 100644 tests/lean/run/group5.lean diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 1cdadeaa1f..572261c125 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -39,6 +39,10 @@ Author: Leonardo de Moura #include "frontends/lean/type_util.h" #include "frontends/lean/class.h" +#ifndef LEAN_DEFAULT_STRUCTURE_INTRO +#define LEAN_DEFAULT_STRUCTURE_INTRO "mk" +#endif + namespace lean { static name * g_tmp_prefix = nullptr; @@ -693,14 +697,20 @@ struct structure_cmd_fn { if (m_p.curr_is_token(get_assign_tk())) { m_p.check_token_next(get_assign_tk(), "invalid 'structure', ':=' expected"); m_mk_pos = m_p.pos(); - m_mk = m_p.check_atomic_id_next("invalid 'structure', identifier expected"); - m_mk = m_name + m_mk; - m_mk_infer = parse_implicit_infer_modifier(m_p); - m_p.check_token_next(get_dcolon_tk(), "invalid 'structure', '::' expected"); + if (m_p.curr_is_token(get_lparen_tk()) || m_p.curr_is_token(get_lcurly_tk()) || m_p.curr_is_token(get_lbracket_tk())) { + m_mk = m_name + LEAN_DEFAULT_STRUCTURE_INTRO; + m_mk_infer = implicit_infer_kind::Implicit; + } else { + m_mk = m_p.check_atomic_id_next("invalid 'structure', identifier expected"); + m_mk = m_name + m_mk; + m_mk_infer = parse_implicit_infer_modifier(m_p); + m_p.check_token_next(get_dcolon_tk(), "invalid 'structure', '::' expected"); + } process_new_fields(); } else { - m_mk_pos = m_name_pos; - m_mk = m_name + "mk"; + m_mk_pos = m_name_pos; + m_mk = m_name + LEAN_DEFAULT_STRUCTURE_INTRO; + m_mk_infer = implicit_infer_kind::Implicit; process_empty_new_fields(); } infer_resultant_universe(); diff --git a/tests/lean/run/group5.lean b/tests/lean/run/group5.lean new file mode 100644 index 0000000000..a8c9deec33 --- /dev/null +++ b/tests/lean/run/group5.lean @@ -0,0 +1,146 @@ +-- Copyright (c) 2014 Jeremy Avigad. All rights reserved. +-- Released under Apache 2.0 license as described in the file LICENSE. +-- Authors: Jeremy Avigad, Leonardo de Moura + +-- algebra.group +-- ============= + +-- Various structures with 1, *, inv, including groups. + +import logic.eq logic.connectives +import data.unit data.sigma data.prod +import algebra.function algebra.binary + +open eq + +namespace algebra + +structure has_mul [class] (A : Type) := +(mul : A → A → A) + +structure has_one [class] (A : Type) := +(one : A) + +structure has_inv [class] (A : Type) := +(inv : A → A) + +infixl `*` := has_mul.mul +postfix `⁻¹` := has_inv.inv +notation 1 := has_one.one + +structure semigroup [class] (A : Type) extends has_mul A := +(assoc : ∀ a b c, mul (mul a b) c = mul a (mul b c)) + +set_option pp.notation false +-- set_option pp.implicit true +-- set_option pp.coercions true +print instances has_mul + +section + variables {A : Type} [s : semigroup A] + include s + variables a b : A + + example : a * b = semigroup.mul a b := + rfl + + theorem mul_assoc (a b c : A) : a * b * c = a * (b * c) := + semigroup.assoc a b c +end + +structure comm_semigroup [class] (A : Type) extends semigroup A := +(comm : ∀a b, mul a b = mul b a) + +namespace comm_semigroup + variables {A : Type} [s : comm_semigroup A] + include s + variables a b c : A + theorem mul_comm : a * b = b * a := !comm_semigroup.comm + + theorem mul_left_comm : a * (b * c) = b * (a * c) := + binary.left_comm mul_comm mul_assoc a b c +end comm_semigroup + +structure monoid [class] (A : Type) extends semigroup A, has_one A := +(right_id : ∀a, mul a one = a) (left_id : ∀a, mul one a = a) + +section + variables {A : Type} [s : monoid A] + variable a : A + include s + + theorem mul_right_id : a * 1 = a := !monoid.right_id + theorem mul_left_id : 1 * a = a := !monoid.left_id +end + +structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A + +structure Semigroup := +(carrier : Type) (struct : semigroup carrier) + +coercion Semigroup.carrier +instance Semigroup.struct + +structure CommSemigroup := +(carrier : Type) (struct : comm_semigroup carrier) + +coercion CommSemigroup.carrier +instance CommSemigroup.struct + +structure Monoid := +(carrier : Type) (struct : monoid carrier) + +coercion Monoid.carrier +instance Monoid.struct + +structure CommMonoid := +(carrier : Type) (struct : comm_monoid carrier) + +coercion CommMonoid.carrier +instance CommMonoid.struct + +end algebra + +open algebra + +section examples + +theorem test1 {S : Semigroup} (a b c d : S) : a * (b * c) * d = a * b * (c * d) := +calc + a * (b * c) * d = a * b * c * d : {symm !mul_assoc} + ... = a * b * (c * d) : !mul_assoc + +theorem test2 {M : CommSemigroup} (a b : M) : a * b = a * b := rfl + +theorem test3 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) := +calc + a * (b * c) * d = a * b * c * d : {symm !mul_assoc} + ... = a * b * (c * d) : !mul_assoc + +-- for test4b to work, we need instances at the level of the bundled structures as well +definition Monoid_Semigroup [coercion] (M : Monoid) : Semigroup := +Semigroup.mk (Monoid.carrier M) _ + +theorem test4 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) := +test1 a b c d + +theorem test5 {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) := +calc + a * 1 * b * c = a * b * c : {!mul_right_id} + ... = a * (b * c) : !mul_assoc + +theorem test5a {M : Monoid} (a b c : M) : a * 1 * b * c = a * (b * c) := +calc + a * 1 * b * c = a * b * c : {!mul_right_id} + ... = a * (b * c) : !mul_assoc + +theorem test5b {A : Type} {M : monoid A} (a b c : A) : a * 1 * b * c = a * (b * c) := +calc + a * 1 * b * c = a * b * c : {!mul_right_id} + ... = a * (b * c) : !mul_assoc + +theorem test6 {M : CommMonoid} (a b c : M) : a * 1 * b * c = a * (b * c) := +calc + a * 1 * b * c = a * b * c : {!mul_right_id} + ... = a * (b * c) : !mul_assoc +end examples