max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/noncomputable): improve is_noncomputable

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-08 14:02:23 -07:00
parent 14d009ce92
commit dcc314c109
48 changed files with 151 additions and 113 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/CMakeLists.txt
View file

@ -14,7 +14,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp
fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp scope_pos_info_provider.cpp
inductive.cpp mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp
aux_definition.cpp inverse.cpp
aux_definition.cpp inverse.cpp library_system.cpp
# Legacy -- The following files will be eventually deleted
normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp

12
src/library/constants.cpp
View file

@ -77,6 +77,7 @@ name const * g_fin = nullptr;
name const * g_fin_mk = nullptr;
name const * g_funext = nullptr;
name const * g_ge = nullptr;
name const * g_get_line = nullptr;
name const * g_gt = nullptr;
name const * g_has_add = nullptr;
name const * g_has_div = nullptr;
@ -265,6 +266,8 @@ name const * g_prod_pr2 = nullptr;
name const * g_propext = nullptr;
name const * g_pexpr = nullptr;
name const * g_pexpr_subst = nullptr;
name const * g_put_str = nullptr;
name const * g_put_nat = nullptr;
name const * g_to_pexpr = nullptr;
name const * g_quot_mk = nullptr;
name const * g_quot_lift = nullptr;
@ -415,6 +418,7 @@ void initialize_constants() {
g_fin_mk = new name{"fin", "mk"};
g_funext = new name{"funext"};
g_ge = new name{"ge"};
g_get_line = new name{"get_line"};
g_gt = new name{"gt"};
g_has_add = new name{"has_add"};
g_has_div = new name{"has_div"};
@ -603,6 +607,8 @@ void initialize_constants() {
g_propext = new name{"propext"};
g_pexpr = new name{"pexpr"};
g_pexpr_subst = new name{"pexpr", "subst"};
g_put_str = new name{"put_str"};
g_put_nat = new name{"put_nat"};
g_to_pexpr = new name{"to_pexpr"};
g_quot_mk = new name{"quot", "mk"};
g_quot_lift = new name{"quot", "lift"};
@ -754,6 +760,7 @@ void finalize_constants() {
delete g_fin_mk;
delete g_funext;
delete g_ge;
delete g_get_line;
delete g_gt;
delete g_has_add;
delete g_has_div;
@ -942,6 +949,8 @@ void finalize_constants() {
delete g_propext;
delete g_pexpr;
delete g_pexpr_subst;
delete g_put_str;
delete g_put_nat;
delete g_to_pexpr;
delete g_quot_mk;
delete g_quot_lift;
@ -1092,6 +1101,7 @@ name const & get_fin_name() { return *g_fin; }
name const & get_fin_mk_name() { return *g_fin_mk; }
name const & get_funext_name() { return *g_funext; }
name const & get_ge_name() { return *g_ge; }
name const & get_get_line_name() { return *g_get_line; }
name const & get_gt_name() { return *g_gt; }
name const & get_has_add_name() { return *g_has_add; }
name const & get_has_div_name() { return *g_has_div; }
@ -1280,6 +1290,8 @@ name const & get_prod_pr2_name() { return *g_prod_pr2; }
name const & get_propext_name() { return *g_propext; }
name const & get_pexpr_name() { return *g_pexpr; }
name const & get_pexpr_subst_name() { return *g_pexpr_subst; }
name const & get_put_str_name() { return *g_put_str; }
name const & get_put_nat_name() { return *g_put_nat; }
name const & get_to_pexpr_name() { return *g_to_pexpr; }
name const & get_quot_mk_name() { return *g_quot_mk; }
name const & get_quot_lift_name() { return *g_quot_lift; }

3
src/library/constants.h
View file

@ -79,6 +79,7 @@ name const & get_fin_name();
name const & get_fin_mk_name();
name const & get_funext_name();
name const & get_ge_name();
name const & get_get_line_name();
name const & get_gt_name();
name const & get_has_add_name();
name const & get_has_div_name();
@ -267,6 +268,8 @@ name const & get_prod_pr2_name();
name const & get_propext_name();
name const & get_pexpr_name();
name const & get_pexpr_subst_name();
name const & get_put_str_name();
name const & get_put_nat_name();
name const & get_to_pexpr_name();
name const & get_quot_mk_name();
name const & get_quot_lift_name();

3
src/library/constants.txt
View file

@ -72,6 +72,7 @@ fin
fin.mk
funext
ge
get_line
gt
has_add
has_div
@ -260,6 +261,8 @@ prod.pr2
propext
pexpr
pexpr.subst
put_str
put_nat
to_pexpr
quot.mk
quot.lift

20
src/library/library_system.cpp Normal file
View file

@ -0,0 +1,20 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/name.h"
#include "library/constants.h"
namespace lean {
bool is_system_builtin(name const & n) {
return
n == get_IO_name() ||
n == get_functorIO_name() ||
n == get_monadIO_name() ||
n == get_put_str_name() ||
n == get_put_nat_name() ||
n == get_get_line_name();
}
}

13
src/library/library_system.h Normal file
View file

@ -0,0 +1,13 @@
/*
Copyright (c) 2016 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"
namespace lean {
/** \brief Return true iff \c n is the name of a builtin constant from the library.system folder. */
bool is_system_builtin(name const & n);
}

24
src/library/noncomputable.cpp
View file

@ -8,10 +8,11 @@ Author: Leonardo de Moura
#include <string>
#include "util/sstream.h"
#include "kernel/for_each_fn.h"
#include "kernel/type_checker.h"
#include "library/module.h"
#include "library/util.h"
#include "library/fingerprint.h"
#include "library/old_type_checker.h"
#include "library/library_system.h"
namespace lean {
struct noncomputable_ext : public environment_extension {
@ -49,15 +50,24 @@ static void noncomputable_reader(deserializer & d, shared_environment & senv,
});
}
static bool is_noncomputable(old_type_checker & tc, noncomputable_ext const & ext, name const & n) {
static bool is_noncomputable(type_checker & tc, noncomputable_ext const & ext, name const & n) {
environment const & env = tc.env();
if (ext.m_noncomputable.contains(n))
return true;
declaration const & d = tc.env().get(n);
return d.is_axiom() && !tc.is_prop(d.get_type()).first;
declaration const & d = env.get(n);
if (!d.is_trusted()) {
return false; /* ignore nontrusted definitions */
} else if (d.is_axiom() && !tc.is_prop(d.get_type())) {
return true;
} else if (d.is_constant_assumption()) {
return !env.is_builtin(d.get_name()) && !is_system_builtin(d.get_name()) && !tc.is_prop(d.get_type());
} else {
return false;
}
}
bool is_noncomputable(environment const & env, name const & n) {
old_type_checker tc(env);
type_checker tc(env);
auto ext = get_extension(env);
return is_noncomputable(tc, ext, n);
}
@ -80,8 +90,8 @@ optional<name> get_noncomputable_reason(environment const & env, name const & n)
declaration const & d = env.get(n);
if (!d.is_definition())
return optional<name>();
old_type_checker tc(env);
if (tc.is_prop(d.get_type()).first)
type_checker tc(env);
if (tc.is_prop(d.get_type()))
return optional<name>(); // definition is a proposition, then do nothing
expr const & v = d.get_value();
auto ext = get_extension(env);

2
tests/lean/def_ite_value.lean
View file

@ -1,5 +1,5 @@
set_option new_elaborator true
set_option eqn_compiler.lemmas false -- TODO(Leo): remove
definition f : string → nat → nat
| "hello world" 1 := 0
| "hello world" _ := 1

10
tests/lean/defeq_simp_lemmas1.lean
View file

@ -2,11 +2,11 @@ namespace foo
universe l
constants (A : Type.{l})
definition q (x : A) := x
definition h (x : A) : A := q x
definition g (x y : A) := h y
definition f (x y z : A) := g (g x y) z
definition d (x y z w : A) := f (f x y z) (f y z w) (f x w z)
noncomputable definition q (x : A) := x
noncomputable definition h (x : A) : A := q x
noncomputable definition g (x y : A) := h y
noncomputable definition f (x y z : A) := g (g x y) z
noncomputable definition d (x y z w : A) := f (f x y z) (f y z w) (f x w z)
attribute [defeq]
definition h.def (x : A) : h x = q x := rfl

10
tests/lean/defeq_simp_lemmas2.lean
View file

@ -2,11 +2,11 @@ namespace foo
universe l
constants (A : Type.{l})
definition q (x : A) := x
definition h (x : A) : A := q x
definition g (x y : A) := h y
definition f (x y z : A) := g (g x y) z
definition d (x y z w : A) := f (f x y z) (f y z w) (f x w z)
noncomputable definition q (x : A) := x
noncomputable definition h (x : A) : A := q x
noncomputable definition g (x y : A) := h y
noncomputable definition f (x y z : A) := g (g x y) z
noncomputable definition d (x y z w : A) := f (f x y z) (f y z w) (f x w z)
attribute [defeq]
definition h.rfl (x : A) : h x = x := rfl

4
tests/lean/inst.lean
View file

@ -9,7 +9,7 @@ C.rec (λa, a) c
constant magic (A : Type) : A
attribute [instance, priority std.priority.max]
definition C_magic (A : Type) : C A :=
noncomputable definition C_magic (A : Type) : C A :=
C.mk (magic A)
attribute [instance]
@ -21,6 +21,6 @@ definition C_prod {A B : Type} (Ha : C A) (Hb : C B) : C (prod A B) :=
C.mk (prod.mk (val Ha) (val Hb))
-- C_magic will be used because it has max priority
definition test : C (prod Prop Prop) := _
noncomputable definition test : C (prod Prop Prop) := _
eval test

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

@ -1,5 +1 @@
inst.lean:12:11:failed to generate bytecode for 'C_magic'
code generation failed, VM does not have code for 'magic'
inst.lean:24:11:failed to generate bytecode for 'test'
code generation failed, VM does not have code for 'magic'
C.mk (magic (prod Prop Prop))

2
tests/lean/nested1.lean
View file

@ -5,7 +5,7 @@ namespace test
constant foo (a : nat) : a > 0 → nat
definition bla (a : nat) :=
noncomputable definition bla (a : nat) :=
foo
(succ (succ a))
abstract as foo.prf lt.step (zero_lt_succ a) end

6
tests/lean/nested1.lean.expected.out
View file

@ -1,11 +1,9 @@
nested1.lean:8:11:failed to generate bytecode for 'test.bla'
code generation failed, VM does not have code for 'test.foo'
attribute [irreducible]
definition test.foo.prf : ∀ (x : ℕ), 0 < succ (succ x) :=
λ x, lt.step (zero_lt_succ x)
definition test.bla : ℕ → ℕ :=
noncomputable definition test.bla : ℕ → ℕ :=
λ a, foo (succ (succ a)) (foo.prf a)
definition test.bla : ℕ → ℕ :=
noncomputable definition test.bla : ℕ → ℕ :=
λ a, test.foo (succ (succ a)) (test.foo.prf a)
attribute [irreducible]
definition test.foo.prf : ∀ (x : ℕ), 0 < succ (succ x) :=

2
tests/lean/pattern_pp.lean
View file

@ -1,4 +1,4 @@
definition Sum : nat → (nat → nat) → nat := sorry
noncomputable definition Sum : nat → (nat → nat) → nat := sorry
attribute [forward]
definition Sum_weird (f g h : nat → nat) (n : nat) : (Sum n (λ x, f (g (h x)))) = 1 := sorry
print Sum_weird

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

@ -1,5 +1,3 @@
pattern_pp.lean:1:11:failed to generate bytecode for 'Sum'
code generation failed, VM does not have code for 'sorry'
attribute [forward]
definition Sum_weird : ∀ (f g h : ℕ → ℕ) (n : ℕ), Sum n (λ (x : ℕ), f (g (h x))) = 1 :=
λ f g h n, sorry

2
tests/lean/pp_no_proofs.lean
View file

@ -5,7 +5,7 @@ constants (P : ∀ {t:true}, ℕ → Prop) (P0 : @P trivial 0)
(Ps : ∀ {n}, @P trivial n → @P trivial (succ n))
(f : Π {n}, @P trivial n → ℕ)
definition messy := f (Ps (Ps (Ps (Ps (Ps (Ps P0))))))
noncomputable definition messy := f (Ps (Ps (Ps (Ps (Ps (Ps P0))))))
eval messy
set_option pp.proofs false

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

@ -1,5 +1,3 @@
pp_no_proofs.lean:8:11:failed to generate bytecode for 'messy'
code generation failed, VM does not have code for 'f'
f (Ps (Ps (Ps (Ps (Ps (Ps P0))))))
f ⌞P 6⌟
@f 6 ⌞@P ⌞true⌟ 6⌟

2
tests/lean/red.lean
View file

@ -1,6 +1,6 @@
constant g : nat → nat
definition f := g
noncomputable definition f := g
example : f = g := rfl

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

@ -1,5 +1,3 @@
red.lean:3:11:failed to generate bytecode for 'f'
code generation failed, VM does not have code for 'g'
red.lean:9:19: error: type mismatch at definition 'example', has type
f = f
but is expected to have type

14
tests/lean/run/basic.lean
View file

@ -5,7 +5,7 @@ definition tst.{l} (A : Type) (B : Type) (C : Type.{l}) : Type := A → B → C
check tst
constant group.{l} : Type.{l+1}
constant carrier.{l} : group.{l} → Type.{l}
definition to_carrier (g : group) := carrier g
noncomputable definition to_carrier (g : group) := carrier g
check to_carrier.{1}
@ -44,8 +44,8 @@ section
variable {T2 : Type.{l}}
variable {T3 : Type.{u}}
variable f : T1 → T2 → T2
definition is_proj2 := ∀ x y, f x y = y
definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z
noncomputable definition is_proj2 := ∀ x y, f x y = y
noncomputable definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z
end
check @is_proj2.{1}
@ -56,8 +56,8 @@ section
variables {T1 T2 : Type}
variable {T3 : Type}
variable f : T1 → T2 → T2
definition is_proj2 := ∀ x y, f x y = y
definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z
noncomputable definition is_proj2 := ∀ x y, f x y = y
noncomputable definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z
end
check @foo.is_proj2.{1}
check @foo.is_proj3.{1 2}
@ -69,8 +69,8 @@ section
variable {T2 : Type}
variable {T3 : Type}
variable f : T1 → T2 → T2
definition is_proj2 := ∀ x y, f x y = y
definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z
noncomputable definition is_proj2 := ∀ x y, f x y = y
noncomputable definition is_proj3 (f : T1 → T2 → T3 → T3) := ∀ x y z, f x y z = z
end
check @bla.is_proj2.{1 2}
check @bla.is_proj3.{1 2 3}

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

@ -2,5 +2,5 @@ inductive [class] C {A : Type} : 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 :=
noncomputable definition g {A : Type} (a b : A) {H1 : C a} {H2 : C b} : Prop :=
f a ∧ f b

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

@ -2,7 +2,7 @@ open tactic
constants (A : Type.{1}) (x y : A)
definition f (z : A) : A := z
noncomputable definition f (z : A) : A := z
attribute [defeq]
definition f.def (z:A) : f z = z := rfl

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

@ -1,7 +1,7 @@
open tactic
set_option pp.binder_types true
definition foo (A : Type) : A → A :=
noncomputable definition foo (A : Type) : A → A :=
sorry
example (a : nat) (H : foo unit () = ()) : true :=

18
tests/lean/run/imp.lean
View file

@ -8,10 +8,10 @@ check @f a
check @f a b
check @f a b c
definition l1 : N → N → N → N := @f
definition l2 : N → N → N := @f a
definition l3 : N → N := @f a b
definition l4 : N := @f a b c
noncomputable definition l1 : N → N → N → N := @f
noncomputable definition l2 : N → N → N := @f a
noncomputable definition l3 : N → N := @f a b
noncomputable definition l4 : N := @f a b c
constant g : forall ⦃a b : N⦄, N → N
@ -22,8 +22,8 @@ check @g a
check @g a b
check @g a b c
definition l5 : N → N → N → N := @g
definition l6 : N → N → N := @g a
definition l7 : N → N := @g a b
definition l8 : N := @g a b c
definition l9 : N → N → N → N := g
noncomputable definition l5 : N → N → N → N := @g
noncomputable definition l6 : N → N → N := @g a
noncomputable definition l7 : N → N := @g a b
noncomputable definition l8 : N := @g a b c
noncomputable definition l9 : N → N → N → N := g

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

@ -9,7 +9,7 @@ inductive category (ob : Type) (mor : ob → ob → Type) : Type
| mk : Π (id : Π (A : ob), mor A A),
(Π (A B : ob) (f : mor A A), id A = f) → category
definition id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat
noncomputable definition id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat
attribute id [reducible]
theorem id_left (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) (A : ob) (f : mor A A) :

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

@ -9,7 +9,7 @@ inductive category (ob : Type) (mor : ob → ob → Type) : Type
| mk : Π (id : Π (A : ob), mor A A),
(Π (A B : ob) (f : mor A A), id A = f) → category
definition id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat
noncomputable definition id (ob : Type) (mor : ob → ob → Type) (Cat : category ob mor) := category.rec (λ id idl, id) Cat
constant ob : Type.{1}
constant mor : ob → ob → Type.{1}
constant Cat : category ob mor

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

@ -12,7 +12,7 @@ inductive category : Type
| mk : Π (id : Π (A : ob), mor A A),
(Π (A B : ob) (f : mor A A), id A = f) → category
definition id (Cat : category) := category.rec (λ id idl, id) Cat
noncomputable definition id (Cat : category) := category.rec (λ id idl, id) Cat
constant Cat : category
attribute id [reducible]

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

@ -12,7 +12,7 @@ inductive category : Type
| mk : Π (id : Π (A : ob), mor A A),
(Π (A B : ob) (f : mor A A), id A = f) → category
definition id (Cat : category) := category.rec (λ id idl, id) Cat
noncomputable definition id (Cat : category) := category.rec (λ id idl, id) Cat
constant Cat : category
print "-----------------"

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

@ -16,7 +16,7 @@ check λ H : a = a, H₂
inductive to_type {B : Type} : B → Type
| mk : Π (b : B), to_type b
definition tst1 : to_type (λ H : a = a, H₂) := to_type.mk (@eq.rec A a P H₂ a)
noncomputable definition tst1 : to_type (λ H : a = a, H₂) := to_type.mk (@eq.rec A a P H₂ a)
check to_type.mk(λ H : a = a, H₂)
check to_type.mk(@eq.rec A a P H₂ a)
check to_type.mk(λ H : a = a, H₂) = to_type.mk(@eq.rec A a P H₂ a)

12
tests/lean/run/match_convoy.lean
View file

@ -27,21 +27,21 @@ end
constant bag_setoid : ∀ A, setoid (list A)
attribute [instance] bag_setoid
definition bag (A : Type) : Type :=
noncomputable definition bag (A : Type) : Type :=
quot (bag_setoid A)
constant subcount : ∀ {A}, list A → list A → bool
constant list.count : ∀ {A}, A → list A → nat
constant all_of_subcount_eq_tt : ∀ {A} {l₁ l₂ : list A}, subcount l₁ l₂ = tt → ∀ a, list.count a l₁ ≤ list.count a l₂
constant ex_of_subcount_eq_ff : ∀ {A} {l₁ l₂ : list A}, subcount l₁ l₂ = ff → ∃ a, ¬ list.count a l₁ ≤ list.count a l₂
definition count {A} (a : A) (b : bag A) : nat :=
noncomputable definition count {A} (a : A) (b : bag A) : nat :=
quot.lift_on b (λ l, list.count a l)
(λ l₁ l₂ h, sorry)
definition subbag {A} (b₁ b₂ : bag A) := ∀ a, count a b₁ ≤ count a b₂
noncomputable definition subbag {A} (b₁ b₂ : bag A) := ∀ a, count a b₁ ≤ count a b₂
infix ⊆ := subbag
attribute [instance]
definition decidable_subbag {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) :=
noncomputable definition decidable_subbag {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) :=
quot.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂,
match subcount l₁ l₂, rfl : ∀ (b : _), subcount l₁ l₂ = b → _ with
| tt, H := decidable.tt (all_of_subcount_eq_tt H)
@ -51,7 +51,7 @@ quot.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂,
end)
attribute [instance]
definition decidable_subbag2 {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) :=
noncomputable definition decidable_subbag2 {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) :=
quot.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂,
match sigma.mk (subcount l₁ l₂) rfl : (Σ (b : _), subcount l₁ l₂ = b) → _ with
| sigma.mk tt H := decidable.tt (all_of_subcount_eq_tt H)
@ -63,7 +63,7 @@ quot.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂,
local notation ⟦ a , b ⟧ := sigma.mk a b
attribute [instance]
definition decidable_subbag3 {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) :=
noncomputable definition decidable_subbag3 {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) :=
quot.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂,
match ⟦subcount l₁ l₂, rfl⟧ : (Σ (b : _), subcount l₁ l₂ = b) → _ with
| ⟦tt, H⟧ := decidable.tt (all_of_subcount_eq_tt H)

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

@ -6,7 +6,7 @@ infixl `mod`:70 := modulo1
constant gcd_aux : ℕ × ℕ → ℕ
definition gcd (x y : ℕ) : ℕ := gcd_aux (x, y)
noncomputable definition gcd (x y : ℕ) : ℕ := gcd_aux (x, y)
theorem gcd_def (x y : ℕ) : gcd x y = @ite (y = 0) (nat.has_decidable_eq (pr2 (x, y)) 0) nat x (gcd y (x mod y)) :=
sorry

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

@ -19,7 +19,7 @@ infixl `+` := add
infix `≤` := le
axiom add_assoc (a b c : int) : (a + b) + c = a + (b + c)
axiom add_le_left {a b : int} (H : a ≤ b) (c : int) : c + a ≤ c + b
definition lt (a b : int) := a + one1 ≤ b
noncomputable definition lt (a b : int) := a + one1 ≤ b
infix `<` := lt
end int

5
tests/lean/run/pack_unpack1.lean
View file

@ -61,10 +61,13 @@ constant P {A : Type} : tree A → Type₁
constant mk1 {A : Type} (a : A) : P (tree.leaf a)
constant mk2 {A : Type} (l : list (tree A)) : P (tree.node l)
definition bla {A : Type} : ∀ n : tree A, P n
noncomputable definition bla {A : Type} : ∀ n : tree A, P n
| (tree.leaf a) := mk1 a
| (tree.node l) := mk2 l
check bla._main.equations.eqn_1
check bla._main.equations.eqn_2
definition foo {A : Type} : nat → tree A → nat
| 0 _ := 0
| (n+1) (tree.leaf a) := 0

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

@ -31,7 +31,7 @@ have aux : ∀ (P : pquot R → Prop), P (pquot.abs R a) → P (pquot.abs R b),
pquot.eqv R H,
aux (λ x : pquot R, pquot.abs R a = x) rfl
definition pquot.rec_on {A : Type} {R : A → A → Prop} {C : pquot R → Type}
noncomputable definition pquot.rec_on {A : Type} {R : A → A → Prop} {C : pquot R → Type}
(q : pquot R)
(f : Π a, C (pquot.abs R a))
(sound : ∀ (a b : A), R a b → f a == f b)
@ -48,7 +48,7 @@ pquot.rec f
aux₄ (f a) (f b) aux₁ Ha)
q
definition pquot.lift {A : Type} {R : A → A → Prop} {B : Type}
noncomputable definition pquot.lift {A : Type} {R : A → A → Prop} {B : Type}
(f : A → B)
(sound : ∀ (a b : A), R a b → f a = f b)
(q : pquot R)
@ -69,7 +69,7 @@ pquot.rec_on q f (λ (a b : A) (H : R a b),
theorem pquot.abs.surjective {A : Type} {R : A → A → Prop} : ∀ q : pquot R, ∃ x : A, pquot.abs R x = q :=
take q, pquot.induction_on q (take a, exists.intro a rfl)
definition pquot.exact {A : Type} (R : A → A → Prop) :=
noncomputable definition pquot.exact {A : Type} (R : A → A → Prop) :=
∀ a b : A, pquot.abs R a = pquot.abs R b → R a b
-- Definable quotient

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

@ -1,6 +1,6 @@
section
parameter (A : Type)
definition foo := A
theorem bar {X : Type} {A : X} : foo :=
noncomputable definition bar {X : Type} {A : X} : foo :=
sorry
end

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

@ -3,18 +3,18 @@ open sigma
constant hom.{l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} (a : A) (b : B) : Type.{max l₁ l₂}
attribute [reducible]
definition arrow_ob (A B : Type) : Type :=
noncomputable definition arrow_ob (A B : Type) : Type :=
Σ (a : A) (b : B), hom a b
definition src1 {A B : Type} (x : arrow_ob A B) : A :=
noncomputable definition src1 {A B : Type} (x : arrow_ob A B) : A :=
match x with
(sigma.mk a (sigma.mk b h)) := a
end
definition src2 {A B : Type} : arrow_ob A B → A
noncomputable definition src2 {A B : Type} : arrow_ob A B → A
| src2 (sigma.mk a (sigma.mk b c)) := a
definition src3 {A B : Type} (x : arrow_ob A B) : A :=
noncomputable definition src3 {A B : Type} (x : arrow_ob A B) : A :=
match x with
(sigma.mk a (sigma.mk b c)) := a
end

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

@ -3,7 +3,7 @@ open tactic
constants (A : Type.{1}) (x y z : A) (g : A → A) (Hg : g y = z)
attribute Hg [simp]
definition f (a : A) := y
noncomputable definition f (a : A) := y
lemma f.def : ∀ (a), f a = y := λ a, rfl
meta_definition simp_f_to_y : tactic unit := mk_eq_simp_ext $

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

@ -18,8 +18,8 @@ constants (f₁ : Π (X : Type) (X_grp : group X), X)
constants (f₂ : Π (X : Type) [X_grp : group X], X)
constants (A : Type.{l}) (A_grp₁ : group A)
attribute [irreducible] definition A_grp₂ : group A := A_grp₁
attribute [irreducible] definition A_grp₃ (t : true) : group A := A_grp₁
attribute [irreducible] noncomputable definition A_grp₂ : group A := A_grp₁
attribute [irreducible] noncomputable definition A_grp₃ (t : true) : group A := A_grp₁
set_option simplify.canonize_instances_fixed_point true
example : @f₂ A A_grp₁ = @f₂ A A_grp₂ := by simplify_goal_force

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

@ -24,8 +24,8 @@ attribute H₂ [simp]
example : f A ss_A a₁ a₂ ss_a₁ ss_a₂ = f A ss_A a₁' a₂' ss_a₁' ss_a₂' := by simp
attribute [reducible] definition c₁' := a₁'
attribute [reducible] definition c₂' := a₂'
attribute [reducible] noncomputable definition c₁' := a₁'
attribute [reducible] noncomputable definition c₂' := a₂'
example : f A ss_A a₁' a₂' ss_a₁' ss_a₂' = f A ss_A c₁' c₂' ss_a₁' ss_a₂' := by simp
example : f A ss_A a₁ a₂ ss_a₁ ss_a₂ = f A ss_A c₁' c₂' ss_a₁' ss_a₂' := by simp

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

@ -31,7 +31,7 @@ example : w = z := by simp
set_option simplify.topdown false
example : w = f y := by simp
attribute [reducible] definition u := f (f x)
attribute [reducible] noncomputable definition u := f (f x)
set_option simplify.topdown true
example : u = z := by simp

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

@ -1,4 +1,4 @@
definition b : Prop :=
noncomputable definition b : Prop :=
sorry
theorem tst : true = false :=

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

@ -6,10 +6,10 @@ structure unification_hint := (pattern : unification_constraint) (constraints :
namespace toy
constants (A : Type.{1}) (f h : A → A) (x y z : A)
attribute [irreducible]
definition g (x y : A) : A := f z
noncomputable definition g (x y : A) : A := f z
attribute [unify]
definition toy_hint (x y : A) : unification_hint :=
noncomputable definition toy_hint (x y : A) : unification_hint :=
unification_hint.mk (unification_constraint.mk (g x y) (f z)) []
open tactic

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

@ -6,14 +6,14 @@ inductive ifin : ℕ → Type -- inductively defined fin-type
open ifin
definition foo {N : Type} : Π{n : ℕ}, N → ifin n → (N × ifin n)
noncomputable definition foo {N : Type} : Π{n : ℕ}, N → ifin n → (N × ifin n)
| (succ k) n (fz .k) := sorry
| (succ k) n (fs x) := sorry
definition bar {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
noncomputable definition bar {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
| (succ k) (n, fz .k) := sorry
| (succ k) (n, fs x) := sorry
definition bar2 {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
noncomputable definition bar2 {N : Type} : Π{n : ℕ}, (N × ifin n) → (N × ifin n)
| (succ k) (n, fz .k) := sorry
| (succ k) (n, fs x) := sorry

6
tests/lean/t5.lean
View file

@ -1,12 +1,12 @@
constant N : Type.{1}
constant f : N → N
constant a : N
definition g (a : N) : N := f a
noncomputable definition g (a : N) : N := f a
check g
namespace foo
definition h : N := f a
noncomputable definition h : N := f a
check h
private definition q : N := f a
private noncomputable definition q : N := f a
check q
end foo
check foo.h

6
tests/lean/t5.lean.expected.out
View file

@ -1,11 +1,5 @@
t5.lean:4:11:failed to generate bytecode for 'g'
code generation failed, VM does not have code for 'f'
g : N → N
t5.lean:7:13:failed to generate bytecode for 'foo.h'
code generation failed, VM does not have code for 'f'
h : N
t5.lean:9:21:failed to generate bytecode for 'private.106392691.q'
code generation failed, VM does not have code for 'f'
q : N
foo.h : N
t5.lean:13:6: error: unknown identifier 'q'

8
tests/lean/unification_hints1.lean
View file

@ -7,12 +7,12 @@ structure unification_hint := (pattern : unification_constraint) (constraints :
namespace toy
constants (A : Type.{1}) (f h : A → A) (x y z : A)
attribute [irreducible]
definition g (x y : A) : A := f z
noncomputable definition g (x y : A) : A := f z
#unify (g x y), (f z)
attribute [unify]
definition toy_hint (x y : A) : unification_hint :=
noncomputable definition toy_hint (x y : A) : unification_hint :=
unification_hint.mk (unification_constraint.mk (g x y) (f z)) []
#unify (g x y), (f z)
@ -44,12 +44,12 @@ definition Canonical.carrier (s : Canonical) : Type :=
Canonical.rec_on s (λ c op, c)
constants (A : Type.{1}) (f : A → A) (x : A)
definition A_canonical : Canonical := Canonical.mk A f
noncomputable definition A_canonical : Canonical := Canonical.mk A f
#unify (Canonical.carrier A_canonical), A
attribute [unify]
definition Canonical_hint (C : Canonical) : unification_hint :=
noncomputable definition Canonical_hint (C : Canonical) : unification_hint :=
unification_hint.mk (unification_constraint.mk (Canonical.carrier C) A) [unification_constraint.mk C A_canonical]
-- TODO(dhs): we mark carrier as irreducible and prove A_canonical explicitly to work around the fact that

8
tests/lean/unification_hints1.lean.expected.out
View file

@ -1,9 +1,5 @@
unification_hints1.lean:10:11:failed to generate bytecode for 'toy.g'
code generation failed, VM does not have code for 'toy.f'
g x y =?= f z
fail
unification_hints1.lean:15:11:failed to generate bytecode for 'toy.toy_hint'
code generation failed, VM does not have code for 'toy.f'
g x y =?= f z
g x y =?= f z
success
@ -17,12 +13,8 @@ success
unification hints:
(add, nat.succ) #4 + 1 =?= succ #3 {#4 =?= #3}
(toy.g, toy.f) toy.g #1 #0 =?= toy.f toy.z {}
unification_hints1.lean:47:11:failed to generate bytecode for 'canonical.A_canonical'
code generation failed, VM does not have code for 'canonical.f'
Canonical.carrier A_canonical =?= A
fail
unification_hints1.lean:52:11:failed to generate bytecode for 'canonical.Canonical_hint'
code generation failed, VM does not have code for 'canonical.f'
Canonical.carrier A_canonical =?= A
Canonical.carrier A_canonical =?= A
success