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

1138 commits

Author SHA1 Message Date
Leonardo de Moura
7ac6b14d2a chore(library/init/data/int/basic): use abstract when transfering in an instance declaration 
@johoelzl I'm using `abstract` tactic because instances are
automatically marked as [reducible], and they will be unfolded when
solving unification constraints. This cannot be avoided since we need to
solve unification constraints such as

      int.has_add =?= comm_ring.to_has_add int.comm_ring

The `abstract tac` tactic creates an auxiliary lemma to store the proof
generated by `tac`. If we use `print int.comm_ring` we can see that
the definition is much smaller. The proofs are irrelevant. So, this has
no drawbacks, and gives us a good performance boost.
 2017-03-07 19:57:43 -08:00
Johannes Hölzl
d6eae3265c feat(library/data/dlist): setup transfer for dlist 2017-03-07 19:30:51 -08:00
Johannes Hölzl
9d62638e9a chore(library/init/meta/transfer): short documentation of transfer rules 2017-03-07 19:30:51 -08:00
Johannes Hölzl
1f45995c16 feat(library/init/meta/transfer): add transfer and use for int 
This commit introduces the transfer method. As application it is
used it to prove that the integers form a commutative ring.
 2017-03-07 19:30:51 -08:00
Johannes Hölzl
ca0fe37c41 feat(library/init/meta/tactic): add mk_local_pis 2017-03-07 19:30:51 -08:00
Johannes Hölzl
da4f552a7a feat(library/init/meta): add decidable_eq for binder_info 2017-03-07 19:30:51 -08:00
Johannes Hölzl
69ed20f656 feat(library/init/meta/match_tactic): add tactic_format for pattern 2017-03-07 19:30:51 -08:00
Johannes Hölzl
0ad5f5bc89 feat(library/init/meta/expr): add instantiate_local(s) 2017-03-07 19:30:51 -08:00
Johannes Hölzl
9e9b289031 feat(library/init/data/prod): add prod.map 2017-03-07 19:30:51 -08:00
Johannes Hölzl
b593d090f2 feat(library/init/data/list): add remove_all 2017-03-07 19:30:51 -08:00
Johannes Hölzl
1c30a593c1 feat(library/init/data/list): add enum 2017-03-07 19:30:51 -08:00
Johannes Hölzl
16aaa9b88e feat(library/init/data/list): add unzip 2017-03-07 19:30:51 -08:00
Johannes Hölzl
4c88e2c5b0 feat(library/init/data/int): use relators for proof of int is a ring 2017-03-07 19:30:51 -08:00
Leonardo de Moura
0c6108ce7a chore(library/init/data/quot): use Sort instead of Type 
Remark: The kernel was already using Sort. So, the limitation was
artificial. Moreover, it may seem unnecessary to have quotients of
proofs in a proof irrelevant system, but this is useful for proving
a more general funext lemma. This more general version is needed in
the new tested contributed by @digama0.
 2017-03-07 14:29:57 -08:00
Mario Carneiro
793017b190 feat(library/init/logic.lean): add Sort -> Prop universe lift 2017-03-07 14:01:59 -08:00
Leonardo de Moura
51958df84b chore(frontends/lean/token_table): remove dead keywords 2017-03-07 14:00:49 -08:00
Leonardo de Moura
9a263a2766 chore(library/init): instances are reducible and are inlined by the compiler 
So, these instances would create two copies of `p` after inlining
 2017-03-07 10:58:09 -08:00
Jeremy Avigad
803e1958fa refactor(library/init/classical.lean): move definition of some 2017-03-06 10:54:42 -08:00
Leonardo de Moura
4608782669 fix(init/logic): eq.mpr and eq.mp can be use for type casting 
So, they should be `def`. Otherwise code generation will fail.
 2017-03-06 09:13:39 -08:00
Leonardo de Moura
156e5603d6 feat(library/init/category/combinators): put list combinators in the namespace list 
In this way we can use them with the ^. notation
 2017-03-05 21:30:30 -08:00
Leonardo de Moura
59c0cbd2e4 chore(library): test new '^.' notation in the standard library, and cleanup definitions using it 2017-03-05 21:21:50 -08:00
Leonardo de Moura
7cae7a5b02 feat(library/init/data/fin/ops): add def lemmas 2017-03-05 16:57:36 -08:00
Leonardo de Moura
0049a42336 feat(library/init/data/fin): add div 2017-03-05 16:43:15 -08:00
Leonardo de Moura
1cdf13821c feat(library/init/data/unsigned): add basic unsigned operations 2017-03-05 16:14:16 -08:00
Leonardo de Moura
6134a4a70e feat(library/init): basic operations for (fin n) 2017-03-05 16:00:02 -08:00
Leonardo de Moura
76f989d51c chore(library/init/data/bool/lemmas): add (coe tt) and (coe ff) simp lemmas 2017-03-05 09:50:01 -08:00
Sebastian Ullrich
ddfdca2e57 chore(init/meta): replace some uses of to_expr `(...) with ``(...) 2017-03-05 08:37:16 -08:00
Sebastian Ullrich
5d68938a9c feat(frontends/lean): expr literals ```(...) 2017-03-05 08:37:16 -08:00
Simon Hudon
b34eac6f1d feat(library/init/data/nat): add theorem decomposing numbers into quotient and remainder 2017-03-05 08:29:34 -08:00
Leonardo de Moura
471c3644a3 chore(library/init/data/option/basic): add lift for option_t 2017-03-05 08:17:55 -08:00
Leonardo de Moura
aeb370ac6b feat(library/init/data/bool/lemmas): add more simp lemmas for bool 2017-03-04 17:01:52 -08:00
Leonardo de Moura
c812e12651 chore(library/init/data/list/lemmas): remove old comment 2017-03-04 16:31:31 -08:00
Leonardo de Moura
05962604f1 feat(library/init/data/bool): add basic simp lemmas for bool 2017-03-04 16:31:16 -08:00
Leonardo de Moura
0768bb28f4 chore(library/init/wf): rename parameter 2017-03-03 16:56:40 -08:00
Jeremy Avigad
f460cbdf2e feat(library/init/classical): simpler choice axiom 2017-03-03 12:43:31 -08:00
Leonardo de Moura
525242561a fix(library/init/meta/tactic): use zeta reduction by default in the abstract tactic 
Abstracting let-exprs may produce type errors.
In the future we may consider another strategy for `abstract`.
First, we try to abstract the `let`, then if it fails, we expand.
Not sure if this is a good idea.
 2017-03-02 11:34:28 -08:00
Leonardo de Moura
b1848efbc4 chore(library/init/meta): add head prefix to head reduction tactics, and add zeta tactic (that applies zeta reduction to all subterms) 2017-03-02 10:55:38 -08:00
Leonardo de Moura
d8371a4b0d feat(library/data/hash_map): avoid read' and write' operations that require an extra test 2017-03-01 22:06:48 -08:00
Daniel Selsam
1f6306d068 perf(library/inductive_compiler): simplification with sizeof lemmas 2017-03-01 21:13:20 -08:00
Jeremy Avigad
4108e5c98b feat(library/init/classical): replace strong indefinite description with indefinite description 2017-03-01 21:13:03 -08:00
Leonardo de Moura
04991692bf feat(library/init/data/nat/lemmas): aux lemmas 2017-03-01 20:28:27 -08:00
Leonardo de Moura
2fb5f6a49e feat(library/init/meta): add subst_vars tactic 2017-03-01 15:11:17 -08:00
Leonardo de Moura
7b0a18167b feat(library/constructions/drec): add drec_on and refactor 2017-03-01 14:12:10 -08:00
Leonardo de Moura
17556758cb feat(library/constructions,library/inductive_compiler): automatically generate dependent eliminator for inductive predicates 
The dependent eliminator for an inductive predicate C is called C.drec

TODO: construct dcases_on and drec_on using C.drec

We need this recursor for implementing dependent elimination for
inductive predicates.

We don't need to define acc.drec and eq.drec in the standard library anymore.
 2017-02-28 20:58:04 -08:00
Leonardo de Moura
04e27eb96f feat(library/init/meta/tactic): add applyc tactic 2017-02-25 12:55:28 -08:00
Leonardo de Moura
7ec0505e94 chore(library/init/meta/vm): style 2017-02-25 12:47:58 -08:00
Leonardo de Moura
35acad642c feat(library/init/meta/tactic): add to_string instance 2017-02-25 12:47:46 -08:00
Leonardo de Moura
52221cdbd1 fix(frontends/lean/elaborator): {} elaboration issue 2017-02-24 21:20:39 -08:00
Leonardo de Moura
57c125c60e chore(library/init/meta/expr): unsigned ==> nat 2017-02-24 19:34:11 -08:00
Leonardo de Moura
921d72b6c4 feat(library/init/meta): add helper tactics 2017-02-24 16:26:47 -08:00