max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
10886 commits 1 branch 0 tags 5.3 GiB
Commit graph

3592 commits

Author SHA1 Message Date
Leonardo de Moura
80670abb8f fix(library/tactic/congruence/congruence_closure): assertion violation 2016-12-28 08:55:24 -08:00
Leonardo de Moura
1d519e4c7b feat(library/tactic/congruence): add theory AC skeleton 2016-12-27 21:38:03 -08:00
Leonardo de Moura
4d0404bd6d chore(library): define rb_expr_tree and rb_expr_map 2016-12-27 20:29:31 -08:00
Leonardo de Moura
b5c1b429e7 feat(library/tactic/ac_tactics): add ac_manager helper class 2016-12-27 17:57:56 -08:00
Leonardo de Moura
7c06306154 chore(library/type_context): reduce redundancy 2016-12-27 17:19:19 -08:00
Leonardo de Moura
d3795b20dd feat(library/defeq_canonizer): remove thread local cache 
The goal is to avoid hard to debug behavior because any tactic (e.g., simp/dsimp/cc) using
defeq_canonize was breaking referential transparency.
 2016-12-27 12:56:39 -08:00
Daniel Selsam
1af202f816 feat(library/tactic/simp_lemmas.cpp): tracing for invalid simp_lemmas 2016-12-27 11:45:07 -08:00
Leonardo de Moura
fb54126d08 fix(library/tactic/congruence/congruence_closure): do not assume instances have been canonized. 2016-12-27 11:19:45 -08:00
Leonardo de Moura
773389f9df feat(library/init/meta/congruence_tactics): add cc_state.gmt and cc_state.inc_gmt 2016-12-27 10:49:20 -08:00
Leonardo de Moura
f719991c71 feat(library/tactic/congruence/congruence_closure): propagate projection over constructor equality 2016-12-26 19:47:29 -08:00
Leonardo de Moura
941bbd3e96 fix(library/tactic/congruence/congruence_closure): crash when processing partially applied constructors 2016-12-26 18:51:03 -08:00
Leonardo de Moura
15f1c6bab2 chore(library/tactic/congruence/ematch): style 2016-12-26 18:23:57 -08:00
Leonardo de Moura
6661faf3da fix(library/tactic/congruence/congruence_closure): but at add_occurrence 2016-12-26 18:13:06 -08:00
Leonardo de Moura
8419219ca6 feat(library/tactic/congruence/congruence_closure): add trace.debug.cc option 2016-12-26 18:13:02 -08:00
Leonardo de Moura
148d34b3bf feat(library/tactic/congruence/congruence_closure): merge annotated term with term being annotated 2016-12-26 16:30:18 -08:00
Leonardo de Moura
9e46818563 feat(library/tactic/congruence): ematching 2016-12-26 15:52:18 -08:00
Leonardo de Moura
6a5f6a84cd feat(library/tactic/congruence/hinst_lemma): add heuristic instantiation lemmas 2016-12-25 20:11:58 -08:00
Leonardo de Moura
9b35adfc8c feat(library/tactic/congruence/congruence_closure): add support for constructor equalities 2016-12-25 12:47:17 -08:00
Leonardo de Moura
7f4160bb4b feat(library/constructions): add helper procedures for building injection and inconsistency proofs for constructor equalities 2016-12-25 12:44:33 -08:00
Leonardo de Moura
a30081a715 feat(library/tactic/congruence/congruence_closure): interpreted values in the same equivalence class 2016-12-25 11:09:55 -08:00
Leonardo de Moura
b313328cb9 feat(library/equations_compiler): int constants 2016-12-25 10:00:18 -08:00
Leonardo de Moura
f9fb041e04 fix(library/comp_val): mk_int_val_ne_proof 
There was a typo in the proof generation. The weird part is that the
proof was valid, but it was very inefficient to check.
The proof was valid because ((n:int) ≥ m) reduces to true/false if n and
m are integer numerals. Thus, if ((n:int) ≥ m) holds then `trivial` is a
valid proof.
However, the reduction is extremely inefficient since it relies on
computations in unary.

In the buggy version, we provided a proof for (a >= 0) where (b >= 0)
was expected. However, both types are definitionally equal to true.
This is why the proof worked.
 2016-12-24 15:54:48 -08:00
Leonardo de Moura
3061d8b9a3 feat(library): add mk_int_val_ne_proof 2016-12-24 15:22:31 -08:00
Leonardo de Moura
8f401c8752 chore(library/tactic/congruence/congruence_closure): remove unnecessary field 2016-12-24 09:14:25 -08:00
Leonardo de Moura
0906d84c92 fix(library/tactic/congruence/congruence_closure): proof generation for congruence with different arity 2016-12-24 09:12:10 -08:00
Leonardo de Moura
424a6acb68 fix(library/tactic/congruence/congruence_closure): missing proof construction step 2016-12-24 08:43:04 -08:00
Leonardo de Moura
a176bd324d fix(library/tactic/congruence/congruence_closure): check_eq_true 2016-12-23 22:24:39 -08:00
Leonardo de Moura
a13d3c83c9 fix(library/tactic/congruence/congruence_closure): heq bug and add more tests 2016-12-23 21:57:49 -08:00
Leonardo de Moura
b1b694a532 fix(library/tactic/congruence/congruence_closure): bugs, and add basic cc tactic 2016-12-23 19:30:45 -08:00
Leonardo de Moura
ca261b7fa8 feat(library/init/meta/congruence_tactics): add option for retrieving only non-singleton equivalence classes, add auxiliary functions 2016-12-23 18:35:44 -08:00
Leonardo de Moura
a2850ac050 fix(library/tactic/congruence/congruence_closure): bugs in the fo-approx mode, and debug mode compilation errors 2016-12-23 17:31:20 -08:00
Leonardo de Moura
1aa92c7d7d fix(library/tactic/congruence/congruence_closure): add entries for 'true' and 'false' 2016-12-23 15:54:09 -08:00
Leonardo de Moura
d431d7274a feat(library/tactic/congruence/congruence_closure): hard code support for ne 2016-12-23 15:37:05 -08:00
Leonardo de Moura
6eb81d2472 feat(library/tactic/congruence/congruence_closure): add new configuration options for minimizing the number of entries and occurrences 2016-12-23 15:18:10 -08:00
Leonardo de Moura
a4173467c4 feat(library/app_builder): use Semireducible if caller did not specify a transparency_mode and ctx.mode() is Reducible or None 
see discussion at #1265
 2016-12-23 14:41:22 -08:00
Leonardo de Moura
17cc40b35e feat(library/tactic/congruence/congruence_closure): do not recurse on values and instances when internalizing terms 2016-12-23 13:24:43 -08:00
Gabriel Ebner
15157bdf0b feat(frontends/lean/parser): keep going after failed imports 2016-12-23 10:53:47 +01:00
Gabriel Ebner
e3b3de5cf3 fix(module_mgr): guard all accesses to m_mod_info 2016-12-23 18:01:44 +01:00
Leonardo de Moura
104ee1b120 fix(library/tactic/congruence/congruence_tactics): stupid mistake 2016-12-22 20:54:20 -08:00
Leonardo de Moura
6329afc121 chore(library/tactic/congruence/congruence_closure): fix typo 2016-12-22 20:05:02 -08:00
Leonardo de Moura
77737a621d fix(library/tactic/congruence/congruence_closure): name collision, we had congr_lemma_cache in two different modules 2016-12-22 19:35:38 -08:00
Leonardo de Moura
94e6fbcbbf perf(library/vm/vm): make sure builtin cases_on recursors are assigned ids first 
This will minimize the size of the m_builtin_cases_vector.
It also indirectly prevents the crash decribed at 144d9096e2.
However, the fix used there is more robust.
 2016-12-22 18:46:51 -08:00
Leonardo de Moura
144d9096e2 fix(library/vm/vm): serialization/deserialization of builtin cases_on instruction 
We generate internal ids for builtin cases_on recursors.
These ids were being saved in the .olean files.
This was fine before commit 41e8a1712e because we had a separate
mapping for builtin cases_on recursors. Now, all ids are stored in the
same mapping. Thus, minor changes in the set of VM builtin operations
make lean crash when importing .olean files because they will change the
internal id for the builtin cases_on.
The problem can be reproduced in the following way:

0- Go to build/release

1- make clean-olean

2- make
Everything is fine after step 2

3- Comment the following line at tactic_state.cpp

    DECLARE_VM_BUILTIN(name({"tactic", "open_namespaces"}),      tactic_open_namespaces);

4- make

5- Lean will crash when executing the following command

   ../../bin/lean ../../library/init/meta/tactic.lean

I believe this bug is reponsible by the crash that @jroesch reported on Slack.

This commit fixes the problem by storing the name of the builtin
cases_on recursor in the .olean file.
 2016-12-22 18:35:30 -08:00
Leonardo de Moura
e5c4231248 fix(library/vm/vm): bug at vm_index_manager? 
@gebner, I have been experiencing crashes that are hard to reproduce.
I think one of the problems was that get_vm_name was returning a `name const &`.
I think this may produce a memory access violation in the following
scenario:

1- Thread 1 invokes get_vm_name, and gets a reference R. This is a
   reference to a memory cell in the vector m_idx2name.
2- Thread 2 invokes get_vm_index, and it triggers a vector resize
   operation. After the resize, reference R is invalid.
3- Thread 1 crashes trying to access R.
 2016-12-22 18:19:33 -08:00
Leonardo de Moura
eefd4cd6ab feat(library/tactic/congruence/congruence_tactics): add missing functions 2016-12-22 18:11:01 -08:00
Leonardo de Moura
f777aafa4e feat(library/init/meta,library/tactic/congruence): add congruence closure lean API 2016-12-22 16:26:17 -08:00
Leonardo de Moura
d16a3df7a3 feat(library/tactic/congruence): initialization and pretty printing 2016-12-22 15:18:52 -08:00
Leonardo de Moura
6bc0952dbc feat(library/tactic/congruence/congruence_closure): generate lazy eq_true proofs 2016-12-22 14:44:38 -08:00
Leonardo de Moura
f7dce940b6 feat(library/tactic/congruence/congruence_closure): proof generation 2016-12-22 14:23:33 -08:00
Daniel Selsam
49de5313fa chore(library/tactic/change_tactic.cpp): better formatting for error message 2016-12-22 11:13:54 -08:00