feat(library/comp_val): add mk_fin_val_ne_proof and mk_char_val_ne_proof

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 :=

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

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

src/library/comp_val.cpp

@@ -105,4 +105,40 @@ optional<expr> 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<expr> 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<expr> 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;
+}
 }

src/library/comp_val.h

@@ -27,4 +27,13 @@ optional<expr> mk_nat_val_ne_proof(expr const & a, expr const & b);
 optional<expr> mk_nat_val_lt_proof(expr const & a, expr const & b);
 /* Same for a <= b */
 optional<expr> mk_nat_val_le_proof(expr const & a, expr const & b);
+
+/* Similar to mk_nat_val_ne_proof, but for fin type */
+optional<expr> mk_fin_val_ne_proof(expr const & a, expr const & b);
+
+/* Similar to mk_char_val_ne_proof, but for char type */
+optional<expr> mk_char_val_ne_proof(expr const & a, expr const & b);
+
+void initialize_comp_val();
+void finalize_comp_val();
 }

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; }

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();

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

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();