Commit graph

17 commits

Author SHA1 Message Date
Leonardo de Moura
7a3aab60c6 chore(builtin/kernel): remove \bowtie as notation for transitivity
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-18 21:11:12 -08:00
Leonardo de Moura
a43020b31b refactor(kernel): remove heterogeneous equality
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-16 17:39:12 -08:00
Leonardo de Moura
57e58c598c fix(tests/lean): adjust tests to reflect recent changes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-15 16:35:33 -08:00
Leonardo de Moura
57c0006916 chore(*): cleanup lean builtin symbols, replace :: with _
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-09 08:33:52 -08:00
Leonardo de Moura
935c2a03a3 feat(*): change name conventions for Lean builtin libraries
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 19:21:44 -08:00
Leonardo de Moura
4ba097a141 feat(frontends/lean): use lowercase commands, replace 'endscope' and 'endnamespace' with 'end'
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-01-05 13:06:36 -08:00
Leonardo de Moura
df58eb132e feat(frontends/lean): simplify explicit version names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-21 17:05:25 -08:00
Leonardo de Moura
812c1a2960 feat(library/elaborator): only expand definitions that are not marked as hidden
The elaborator produces better proof terms. This is particularly important when we have to prove the remaining holes using tactics.
For example, in one of the tests, the elaborator was producing the sub-expression

 (λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤)

After, this commit it produces

 (λ x : N, ¬ ∀ x::1 : N, ¬ P a x x::1)

The expressions above are definitionally equal, but the second is easier to work with.

Question: do we really need hidden definitions?
Perhaps, we can use only the opaque flag.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-20 02:16:49 -08:00
Leonardo de Moura
ad3f771b1d feat(frontends/lean): hide 'explicit' version of objects with implicit arguments
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 13:12:39 -08:00
Leonardo de Moura
bff5a6bfb2 fix(frontends/lean/pp): make sure pp and parser are using the same precedences
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-12-19 12:46:14 -08:00
Leonardo de Moura
20a36e98ec feat(library/elaborator): modify how elaborator handles constraints of the form ?M << P and P << ?M, where P is a proposition.
Before this commit, the elaborator would only assign ?M <- P, if P was normalized. This is bad since normalization may "destroy" the structure of P.

For example, consider the constraint
[a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ implies a (implies b (and a b))

Before this, ?M::1 will not be assigned to the "implies-term" because the "implies-term" is not normalized yet.
So, the elaborator would continue to process the constraint, and convert it into:

[a : Bool; b : Bool; c : Bool] ⊢ ?M::1 ≺ if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true

Now, ?M::1 is assigned to the term
     if Bool a (if Bool b (if Bool (if Bool a (if Bool b false true) true) false true) true) true

This is bad, since the original structure was lost.

This commit also contains an example that only works after the commit is applied.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-11-29 09:15:01 -08:00
Leonardo de Moura
4dd6cead83 refactor(equality): make homogeneous equality the default equality
It was not a good idea to use heterogeneous equality as the default equality in Lean.
It creates the following problems.

- Heterogeneous equality does not propagate constraints in the elaborator.
For example, suppose that l has type (List Int), then the expression
     l = nil
will not propagate the type (List Int) to nil.

- It is easy to write false. For example, suppose x has type Real, and the user
writes x = 0. This is equivalent to false, since 0 has type Nat. The elaborator cannot introduce
the coercion since x = 0 is a type correct expression.

Homogeneous equality does not suffer from the problems above.
We keep heterogeneous equality because it is useful for generating proof terms.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-10-29 16:20:06 -07:00
Leonardo de Moura
b62816cc25 Fix problem with pretty printer. Add another test for elaborator
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-06 18:01:11 -07:00
Leonardo de Moura
a341643335 Fix unit tests for Windows
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-03 10:44:51 -07:00
Leonardo de Moura
e218b92a9d Modify verbose message for Set command
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-02 12:29:21 -07:00
Leonardo de Moura
a3bbd9fbb5 Minimize use the colors in tests. The colors make the diff hard to read
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 10:34:57 -07:00
Leonardo de Moura
51640ecff8 Move files in examples directory to tests directory. They are not real examples
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-08-31 19:16:30 -07:00