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

feat(frontends/lean): make the 'expression template' argument in Subst implicit because higher-order matching can infer it.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-30 10:45:34 -07:00
parent bc92671ae4
commit 032f5cd7b3
7 changed files with 33 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/frontends/lean/notation.cpp
View file

@ -11,6 +11,11 @@ Author: Leonardo de Moura
#include "frontends/lean/frontend.h"
namespace lean {
void add_alias(frontend & f, name const & n, name const & m) {
object const & obj = f.get_object(n);
f.add_definition(m, obj.get_type(), mk_constant(n));
}
/**
\brief Initialize builtin notation.
*/
@ -80,7 +85,9 @@ void init_builtin_notation(frontend & f) {
f.mark_implicit_arguments(mk_mp_fn(), {true, true, false, false});
f.mark_implicit_arguments(mk_discharge_fn(), {true, true, false});
f.mark_implicit_arguments(mk_refl_fn(), {true, false});
f.mark_implicit_arguments(mk_subst_fn(), {true, true, true, false, false, false});
f.mark_implicit_arguments(mk_subst_fn(), {true, true, true, true, false, false});
add_alias(f, "Subst", "SubstP");
f.mark_implicit_arguments("SubstP", {true, true, true, false, false, false});
f.mark_implicit_arguments(mk_trans_ext_fn(), {true, true, true, true, true, true, false, false});
f.mark_implicit_arguments(mk_eta_fn(), {true, true, false});
f.mark_implicit_arguments(mk_imp_antisym_fn(), {true, true, false, false});

2
tests/lean/bad5.lean
View file

@ -3,5 +3,5 @@ Variable a : Int
Variable b : Int
Axiom H1 : a = b
Axiom H2 : (g a) > 0
Theorem T1 : (g b) > 0 := Subst (λ x, (g x) > 0) H2 H1
Theorem T1 : (g b) > 0 := SubstP (λ x, (g x) > 0) H2 H1
Show Environment 2

2
tests/lean/bad5.lean.expected.out
View file

@ -7,4 +7,4 @@
Assumed: H2
Proved: T1
Axiom H2 : (g a) > 0
Theorem T1 : (g b) > 0 := Subst (λ x : ℤ, (g x) > 0) H2 H1
Theorem T1 : (g b) > 0 := SubstP (λ x : ℤ, (g x) > 0) H2 H1

2
tests/lean/ho.lean
View file

@ -3,5 +3,5 @@ Variable a : Int
Variable b : Int
Axiom H1 : a = b
Axiom H2 : (g a) > 0
Theorem T1 : (g b) > 0 := Subst _ H2 H1
Theorem T1 : (g b) > 0 := Subst H2 H1
Show Environment 2

2
tests/lean/ho.lean.expected.out
View file

@ -7,4 +7,4 @@
Assumed: H2
Proved: T1
Axiom H2 : (g a) > 0
Theorem T1 : (g b) > 0 := Subst (λ x : ℤ, if ((g x) ≤ 0) ⊥ ⊤) H2 H1
Theorem T1 : (g b) > 0 := Subst H2 H1

9
tests/lean/subst.lean Normal file
View file

@ -0,0 +1,9 @@
Variable a : Int
Variable n : Nat
Axiom H1 : a + a + a = 10
Axiom H2 : a = n
Theorem T : a + n + a = 10 := Subst H1 H2
Set pp::coercion true
Set pp::notation false
Set pp::implicit true
Show Environment 1.

12
tests/lean/subst.lean.expected.out Normal file
View file

@ -0,0 +1,12 @@
Set: pp::colors
Set: pp::unicode
Assumed: a
Assumed: n
Assumed: H1
Assumed: H2
Proved: T
Set: lean::pp::coercion
Set: lean::pp::notation
Set: lean::pp::implicit
Theorem T : eq::explicit ℤ (Int::add (Int::add a (nat_to_int n)) a) (nat_to_int 10) :=
Subst::explicit ℤ a (nat_to_int n) (λ x : ℤ, Int::add (Int::add a x) a == 10) H1 H2