michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
lean2/tests/lean/tst6.lean.expected.out

119 lines
4.2 KiB
Text
Raw Normal View History

Modify verbose message for Set command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-02 19:29:21 +00:00
Set: pp::colors
Fix unit tests for Windows Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-03 17:44:51 +00:00
Set: pp::unicode
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
Assumed: N
Assumed: h
Proved: CongrH
Modify verbose message for Set command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-02 19:29:21 +00:00
Set: lean::pp::implicit
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 23:20:02 +00:00
Theorem CongrH {a1 a2 b1 b2 : N} (H1 : eq::explicit N a1 b1) (H2 : eq::explicit N a2 b2) : eq::explicit
N
(h a1 a2)
(h b1 b2) :=
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
Congr::explicit
N
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 17:34:57 +00:00
(λ x : N, N)
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
(h a1)
(h b1)
a2
b2
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 17:34:57 +00:00
(Congr::explicit N (λ x : N, N → N) h h a1 b1 (Refl::explicit (N → N → N) h) H1)
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
H2
Fix problem with pretty printer. Add another test for elaborator Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-07 00:58:45 +00:00
Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := CongrH H1 H2
Modify verbose message for Set command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-02 19:29:21 +00:00
Set: lean::pp::implicit
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 17:34:57 +00:00
Theorem CongrH {a1 a2 b1 b2 : N} (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := Congr (Congr (Refl h) H1) H2
Theorem CongrH::explicit (a1 a2 b1 b2 : N) (H1 : a1 = b1) (H2 : a2 = b2) : (h a1 a2) = (h b1 b2) := CongrH H1 H2
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
Proved: Example1
Modify verbose message for Set command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-02 19:29:21 +00:00
Set: lean::pp::implicit
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 23:20:02 +00:00
Theorem Example1 (a b c d : N)
(H : eq::explicit N a b ∧ eq::explicit N b c ∨ eq::explicit N a d ∧ eq::explicit N d c) : eq::explicit
N
(h a b)
(h c b) :=
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
DisjCases::explicit
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 23:20:02 +00:00
(eq::explicit N a b ∧ eq::explicit N b c)
(eq::explicit N a d ∧ eq::explicit N d c)
((h a b) == (h c b))
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
H
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 23:20:02 +00:00
(λ H1 : eq::explicit N a b ∧ eq::explicit N b c,
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
CongrH::explicit
a
b
c
b
(Trans::explicit
N
a
b
c
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 23:20:02 +00:00
(Conjunct1::explicit (eq::explicit N a b) (eq::explicit N b c) H1)
(Conjunct2::explicit (eq::explicit N a b) (eq::explicit N b c) H1))
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
(Refl::explicit N b))
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 23:20:02 +00:00
(λ H1 : eq::explicit N a d ∧ eq::explicit N d c,
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
CongrH::explicit
a
b
c
b
(Trans::explicit
N
a
d
c
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 23:20:02 +00:00
(Conjunct1::explicit (eq::explicit N a d) (eq::explicit N d c) H1)
(Conjunct2::explicit (eq::explicit N a d) (eq::explicit N d c) H1))
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
(Refl::explicit N b))
Proved: Example2
Modify verbose message for Set command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-02 19:29:21 +00:00
Set: lean::pp::implicit
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 23:20:02 +00:00
Theorem Example2 (a b c d : N)
(H : eq::explicit N a b ∧ eq::explicit N b c ∨ eq::explicit N a d ∧ eq::explicit N d c) : eq::explicit
N
(h a b)
(h c b) :=
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
DisjCases::explicit
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 23:20:02 +00:00
(eq::explicit N a b ∧ eq::explicit N b c)
(eq::explicit N a d ∧ eq::explicit N d c)
((h a b) == (h c b))
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
H
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 23:20:02 +00:00
(λ H1 : eq::explicit N a b ∧ eq::explicit N b c,
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
CongrH::explicit
a
b
c
b
(Trans::explicit
N
a
b
c
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 23:20:02 +00:00
(Conjunct1::explicit (a == b) (b == c) H1)
(Conjunct2::explicit (a == b) (b == c) H1))
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
(Refl::explicit N b))
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 23:20:02 +00:00
(λ H1 : eq::explicit N a d ∧ eq::explicit N d c,
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
CongrH::explicit
a
b
c
b
(Trans::explicit
N
a
d
c
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 23:20:02 +00:00
(Conjunct1::explicit (a == d) (d == c) H1)
(Conjunct2::explicit (a == d) (d == c) H1))
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
(Refl::explicit N b))
Proved: Example3
Modify verbose message for Set command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-02 19:29:21 +00:00
Set: lean::pp::implicit
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 17:34:57 +00:00
Theorem Example3 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a b) = (h c b) :=
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
DisjCases
H
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 17:34:57 +00:00
(λ H1 : a = b ∧ b = e ∧ b = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))) (Refl b))
(λ H1 : a = d ∧ d = c, CongrH (Trans (Conjunct1 H1) (Conjunct2 H1)) (Refl b))
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
Proved: Example4
Modify verbose message for Set command Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-02 19:29:21 +00:00
Set: lean::pp::implicit
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 17:34:57 +00:00
Theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a c) = (h c a) :=
Move files in examples directory to tests directory. They are not real examples Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-09-01 02:15:48 +00:00
DisjCases
H
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 17:34:57 +00:00
(λ H1 : a = b ∧ b = e ∧ b = c,
let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1)) in CongrH AeqC (Symm AeqC))
(λ H1 : a = d ∧ d = c, let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) in CongrH AeqC (Symm AeqC))
Reference in a new issue Copy permalink