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

feat(library/init/meta/comp_value_tactics): add support for char/string/fin at comp_val tactic

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-23 13:19:54 -08:00
parent 98fbe76f30
commit 21bad7cb97
3 changed files with 66 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

51
library/init/meta/comp_value_tactics.lean
View file

@ -9,6 +9,9 @@ import init.meta.tactic
meta constant mk_nat_val_ne_proof : expr → expr → option expr
meta constant mk_nat_val_lt_proof : expr → expr → option expr
meta constant mk_nat_val_le_proof : expr → expr → option expr
meta constant mk_fin_val_ne_proof : expr → expr → option expr
meta constant mk_char_val_ne_proof : expr → expr → option expr
meta constant mk_string_val_ne_proof : expr → expr → option expr
namespace tactic
open expr
@ -16,27 +19,43 @@ meta def comp_val : tactic unit :=
do t ← target,
guard (is_app t),
type ← infer_type t^.app_arg,
guard (type = const `nat []),
(do (a, b) ← returnopt (is_ne t),
pr ← returnopt (mk_nat_val_ne_proof a b),
(do is_def_eq type (const `nat []),
(do (a, b) ← returnopt (is_ne t),
pr ← returnopt (mk_nat_val_ne_proof a b),
exact pr)
<|>
(do (a, b) ← returnopt (is_lt t),
pr ← returnopt (mk_nat_val_lt_proof a b),
exact pr)
<|>
(do (a, b) ← returnopt (is_gt t),
pr ← returnopt (mk_nat_val_lt_proof b a),
exact pr)
<|>
(do (a, b) ← returnopt (is_le t),
pr ← returnopt (mk_nat_val_le_proof a b),
exact pr)
<|>
(do (a, b) ← returnopt (is_ge t),
pr ← returnopt (mk_nat_val_le_proof b a),
exact pr))
<|>
(do is_def_eq type (const `char []),
(a, b) ← returnopt (is_ne t),
pr ← returnopt (mk_char_val_ne_proof a b),
exact pr)
<|>
(do (a, b) ← returnopt (is_lt t),
pr ← returnopt (mk_nat_val_lt_proof a b),
(do is_def_eq type (const `string []),
(a, b) ← returnopt (is_ne t),
pr ← returnopt (mk_string_val_ne_proof a b),
exact pr)
<|>
(do (a, b) ← returnopt (is_gt t),
pr ← returnopt (mk_nat_val_lt_proof b a),
exact pr)
<|>
(do (a, b) ← returnopt (is_le t),
pr ← returnopt (mk_nat_val_le_proof a b),
exact pr)
<|>
(do (a, b) ← returnopt (is_ge t),
pr ← returnopt (mk_nat_val_le_proof b a),
(do type ← whnf type,
guard (is_app_of type `fin),
(a, b) ← returnopt (is_ne t),
pr ← returnopt (mk_fin_val_ne_proof a b),
exact pr)
<|>
(do (a, b) ← returnopt (is_eq t),
unify a b, to_expr `(eq.refl %%a) >>= exact)
unify a b, to_expr `(eq.refl %%a) >>= exact)
end tactic

15
src/library/vm/vm_expr.cpp
View file

@ -336,6 +336,18 @@ vm_obj vm_mk_nat_val_le_proof(vm_obj const & a, vm_obj const & b) {
return to_obj(mk_nat_val_le_proof(to_expr(a), to_expr(b)));
}
vm_obj vm_mk_fin_val_ne_proof(vm_obj const & a, vm_obj const & b) {
return to_obj(mk_fin_val_ne_proof(to_expr(a), to_expr(b)));
}
vm_obj vm_mk_char_val_ne_proof(vm_obj const & a, vm_obj const & b) {
return to_obj(mk_char_val_ne_proof(to_expr(a), to_expr(b)));
}
vm_obj vm_mk_string_val_ne_proof(vm_obj const & a, vm_obj const & b) {
return to_obj(mk_string_val_ne_proof(to_expr(a), to_expr(b)));
}
void initialize_vm_expr() {
DECLARE_VM_BUILTIN(name({"expr", "var"}), expr_var);
DECLARE_VM_BUILTIN(name({"expr", "sort"}), expr_sort);
@ -373,6 +385,9 @@ void initialize_vm_expr() {
DECLARE_VM_BUILTIN(name("mk_nat_val_ne_proof"), vm_mk_nat_val_ne_proof);
DECLARE_VM_BUILTIN(name("mk_nat_val_lt_proof"), vm_mk_nat_val_lt_proof);
DECLARE_VM_BUILTIN(name("mk_nat_val_le_proof"), vm_mk_nat_val_le_proof);
DECLARE_VM_BUILTIN(name("mk_fin_val_ne_proof"), vm_mk_fin_val_ne_proof);
DECLARE_VM_BUILTIN(name("mk_char_val_ne_proof"), vm_mk_char_val_ne_proof);
DECLARE_VM_BUILTIN(name("mk_string_val_ne_proof"), vm_mk_string_val_ne_proof);
}
void finalize_vm_expr() {

16
tests/lean/run/comp_val2.lean Normal file
View file

@ -0,0 +1,16 @@
open tactic
example : #"a" ≠ #"b" := by comp_val
example : #"0" ≠ #"a" := by comp_val
example : "hello worlg" ≠ "hhello world" := by comp_val
example : "hello world" ≠ "hhello world" := by comp_val
example : "abc" ≠ "cde" := by comp_val
example : "abc" ≠ "" := by comp_val
example : "" ≠ "cde" := by comp_val
example : @fin.mk 5 3 dec_trivial ≠ @fin.mk 5 4 dec_trivial :=
by comp_val
example : @fin.mk 5 4 dec_trivial ≠ @fin.mk 5 1 dec_trivial :=
by comp_val