From 680bab8bb853341dd88b6a68d27dc092ab68da27 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 23 Nov 2016 10:24:44 -0800 Subject: [PATCH] feat(library/comp_val): add mk_fin_val_ne_proof and mk_char_val_ne_proof --- library/init/char.lean | 3 ++- library/init/char_lemmas.lean | 34 +++++++++++++++++++++++++++++++++ library/init/default.lean | 2 +- src/library/comp_val.cpp | 36 +++++++++++++++++++++++++++++++++++ src/library/comp_val.h | 9 +++++++++ src/library/constants.cpp | 8 ++++++++ src/library/constants.h | 2 ++ src/library/constants.txt | 2 ++ src/library/init_module.cpp | 3 +++ 9 files changed, 97 insertions(+), 2 deletions(-) create mode 100644 library/init/char_lemmas.lean diff --git a/library/init/char.lean b/library/init/char.lean index c5d5ff03d7..b315eb7c52 100644 --- a/library/init/char.lean +++ b/library/init/char.lean @@ -13,7 +13,7 @@ def char := fin char_sz namespace char /- We cannot use tactic dec_trivial here because the tactic framework has not been defined yet. -/ -private lemma zero_lt_char_sz : 0 < char_sz := +lemma zero_lt_char_sz : 0 < char_sz := zero_lt_succ _ @[pattern] def of_nat (n : nat) : char := @@ -21,6 +21,7 @@ if h : n < char_sz then fin.mk n h else fin.mk 0 zero_lt_char_sz def to_nat (c : char) : nat := fin.val c + end char instance : decidable_eq char := diff --git a/library/init/char_lemmas.lean b/library/init/char_lemmas.lean new file mode 100644 index 0000000000..ad99b3fda5 --- /dev/null +++ b/library/init/char_lemmas.lean @@ -0,0 +1,34 @@ +prelude +import init.char init.meta init.logic init.nat_lemmas + +namespace char +lemma of_nat_eq_of_lt {n : nat} : ∀ h : n < char_sz, of_nat n = fin.mk n h := +begin + intro h, + unfold of_nat, + cases (nat.decidable_lt n char_sz), + {contradiction}, + {reflexivity} +end + +lemma of_nat_eq_fin_of_ge {n : nat} : n ≥ char_sz → of_nat n = fin.mk 0 zero_lt_char_sz := +begin + intro h, + unfold of_nat, + cases (nat.decidable_lt n char_sz), + {reflexivity}, + {note h' := not_lt_of_ge h, contradiction} +end + +lemma of_nat_eq_of_ge {n : nat} : n ≥ char_sz → of_nat n = of_nat 0 := +begin + intro h, + rw [of_nat_eq_fin_of_ge h] +end + +lemma of_nat_ne_of_ne {n₁ n₂ : nat} (h₁ : n₁ ≠ n₂) (h₂ : n₁ < char_sz) (h₃ : n₂ < char_sz) : of_nat n₁ ≠ of_nat n₂ := +begin + rw [of_nat_eq_of_lt h₂, of_nat_eq_of_lt h₃], + apply @fin.ne_of_vne _ (fin.mk n₁ h₂) (fin.mk n₂ h₃) h₁ +end +end char diff --git a/library/init/default.lean b/library/init/default.lean index 94ccabe343..1f1ea1bd72 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -12,4 +12,4 @@ import init.monad init.option init.state init.fin init.list init.char init.strin import init.monad_combinators init.set import init.timeit init.trace init.unsigned init.ordering init.list_classes init.coe import init.wf init.nat_div init.meta init.instances init.breakpoint -import init.sigma_lex init.id_locked init.order init.algebra init.nat_lemmas +import init.sigma_lex init.id_locked init.order init.algebra init.nat_lemmas init.char_lemmas diff --git a/src/library/comp_val.cpp b/src/library/comp_val.cpp index a07504a0d3..086a6e378c 100644 --- a/src/library/comp_val.cpp +++ b/src/library/comp_val.cpp @@ -105,4 +105,40 @@ optional mk_nat_val_le_proof(expr const & a, expr const & b) { return some_expr(mk_app(mk_constant(get_nat_le_of_lt_name()), a, b, *pr)); return none_expr(); } + +optional mk_fin_val_ne_proof(expr const & a, expr const & b) { + if (!is_app_of(a, get_fin_mk_name(), 3) || + !is_app_of(b, get_fin_mk_name(), 3)) + return none_expr(); + expr const & n = app_arg(app_fn(app_fn(a))); + expr const & v_a = app_arg(app_fn(a)); + expr const & v_b = app_arg(app_fn(b)); + auto pr = mk_nat_val_lt_proof(v_a, v_b); + if (!pr) return none_expr(); + return some_expr(mk_app(mk_constant(get_fin_ne_of_vne_name()), n, a, b, *pr)); +} + +static expr * g_char_sz = nullptr; + +optional mk_char_val_ne_proof(expr const & a, expr const & b) { + if (is_app_of(a, get_char_of_nat_name(), 1) && + is_app_of(a, get_char_of_nat_name(), 1)) { + expr const & v_a = app_arg(a); + expr const & v_b = app_arg(b); + if (auto h_1 = mk_nat_val_ne_proof(v_a, v_b)) { + if (auto h_2 = mk_nat_val_lt_proof(v_a, *g_char_sz)) { + if (auto h_3 = mk_nat_val_lt_proof(v_b, *g_char_sz)) { + return some_expr(mk_app({mk_constant(get_char_of_nat_ne_of_ne_name()), v_a, v_b, *h_1, *h_2, *h_3})); + }}} + } + return mk_fin_val_ne_proof(a, b); +} + +void initialize_comp_val() { + g_char_sz = new expr(to_nat_expr(mpz(255))); +} + +void finalize_comp_val() { + delete g_char_sz; +} } diff --git a/src/library/comp_val.h b/src/library/comp_val.h index a346824c92..d84b25b198 100644 --- a/src/library/comp_val.h +++ b/src/library/comp_val.h @@ -27,4 +27,13 @@ optional mk_nat_val_ne_proof(expr const & a, expr const & b); optional mk_nat_val_lt_proof(expr const & a, expr const & b); /* Same for a <= b */ optional mk_nat_val_le_proof(expr const & a, expr const & b); + +/* Similar to mk_nat_val_ne_proof, but for fin type */ +optional mk_fin_val_ne_proof(expr const & a, expr const & b); + +/* Similar to mk_char_val_ne_proof, but for char type */ +optional mk_char_val_ne_proof(expr const & a, expr const & b); + +void initialize_comp_val(); +void finalize_comp_val(); } diff --git a/src/library/constants.cpp b/src/library/constants.cpp index d77427d1d4..09206c0fdb 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -27,6 +27,7 @@ name const * g_cast_eq = nullptr; name const * g_cast_heq = nullptr; name const * g_char = nullptr; name const * g_char_of_nat = nullptr; +name const * g_char_of_nat_ne_of_ne = nullptr; name const * g_classical = nullptr; name const * g_classical_prop_decidable = nullptr; name const * g_classical_type_decidable_eq = nullptr; @@ -78,6 +79,7 @@ name const * g_false_rec = nullptr; name const * g_field = nullptr; name const * g_fin = nullptr; name const * g_fin_mk = nullptr; +name const * g_fin_ne_of_vne = nullptr; name const * g_forall_congr = nullptr; name const * g_forall_congr_eq = nullptr; name const * g_funext = nullptr; @@ -444,6 +446,7 @@ void initialize_constants() { g_cast_heq = new name{"cast_heq"}; g_char = new name{"char"}; g_char_of_nat = new name{"char", "of_nat"}; + g_char_of_nat_ne_of_ne = new name{"char", "of_nat_ne_of_ne"}; g_classical = new name{"classical"}; g_classical_prop_decidable = new name{"classical", "prop_decidable"}; g_classical_type_decidable_eq = new name{"classical", "type_decidable_eq"}; @@ -495,6 +498,7 @@ void initialize_constants() { g_field = new name{"field"}; g_fin = new name{"fin"}; g_fin_mk = new name{"fin", "mk"}; + g_fin_ne_of_vne = new name{"fin", "ne_of_vne"}; g_forall_congr = new name{"forall_congr"}; g_forall_congr_eq = new name{"forall_congr_eq"}; g_funext = new name{"funext"}; @@ -862,6 +866,7 @@ void finalize_constants() { delete g_cast_heq; delete g_char; delete g_char_of_nat; + delete g_char_of_nat_ne_of_ne; delete g_classical; delete g_classical_prop_decidable; delete g_classical_type_decidable_eq; @@ -913,6 +918,7 @@ void finalize_constants() { delete g_field; delete g_fin; delete g_fin_mk; + delete g_fin_ne_of_vne; delete g_forall_congr; delete g_forall_congr_eq; delete g_funext; @@ -1279,6 +1285,7 @@ name const & get_cast_eq_name() { return *g_cast_eq; } name const & get_cast_heq_name() { return *g_cast_heq; } name const & get_char_name() { return *g_char; } name const & get_char_of_nat_name() { return *g_char_of_nat; } +name const & get_char_of_nat_ne_of_ne_name() { return *g_char_of_nat_ne_of_ne; } name const & get_classical_name() { return *g_classical; } name const & get_classical_prop_decidable_name() { return *g_classical_prop_decidable; } name const & get_classical_type_decidable_eq_name() { return *g_classical_type_decidable_eq; } @@ -1330,6 +1337,7 @@ name const & get_false_rec_name() { return *g_false_rec; } name const & get_field_name() { return *g_field; } name const & get_fin_name() { return *g_fin; } name const & get_fin_mk_name() { return *g_fin_mk; } +name const & get_fin_ne_of_vne_name() { return *g_fin_ne_of_vne; } name const & get_forall_congr_name() { return *g_forall_congr; } name const & get_forall_congr_eq_name() { return *g_forall_congr_eq; } name const & get_funext_name() { return *g_funext; } diff --git a/src/library/constants.h b/src/library/constants.h index 0321572bdb..5ba90e9cdb 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -29,6 +29,7 @@ name const & get_cast_eq_name(); name const & get_cast_heq_name(); name const & get_char_name(); name const & get_char_of_nat_name(); +name const & get_char_of_nat_ne_of_ne_name(); name const & get_classical_name(); name const & get_classical_prop_decidable_name(); name const & get_classical_type_decidable_eq_name(); @@ -80,6 +81,7 @@ name const & get_false_rec_name(); name const & get_field_name(); name const & get_fin_name(); name const & get_fin_mk_name(); +name const & get_fin_ne_of_vne_name(); name const & get_forall_congr_name(); name const & get_forall_congr_eq_name(); name const & get_funext_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index ef40ac9eed..cf60936215 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -22,6 +22,7 @@ cast_eq cast_heq char char.of_nat +char.of_nat_ne_of_ne classical classical.prop_decidable classical.type_decidable_eq @@ -73,6 +74,7 @@ false.rec field fin fin.mk +fin.ne_of_vne forall_congr forall_congr_eq funext diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 32a3510e5b..7bfbbd748d 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -47,6 +47,7 @@ Author: Leonardo de Moura #include "library/arith_instance_manager.h" #include "library/inverse.h" #include "library/pattern_attribute.h" +#include "library/comp_val.h" namespace lean { void initialize_library_core_module() { @@ -104,9 +105,11 @@ void initialize_library_module() { initialize_arith_instance_manager(); initialize_inverse(); initialize_pattern_attribute(); + initialize_comp_val(); } void finalize_library_module() { + finalize_comp_val(); finalize_pattern_attribute(); finalize_inverse(); finalize_arith_instance_manager();