michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(builtin): move pair definition and theorems to pair.lean

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-06 09:20:52 -08:00
parent daf7075ce4
commit db3bcdba55
5 changed files with 13 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/builtin/CMakeLists.txt
View file

@ -95,7 +95,8 @@ add_theory("Real.lean" "${CMAKE_CURRENT_BINARY_DIR}/Int.olean")
add_theory("specialfn.lean" "${CMAKE_CURRENT_BINARY_DIR}/Real.olean")
add_theory("subtype.lean" "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean")
add_theory("optional.lean" "${CMAKE_CURRENT_BINARY_DIR}/subtype.olean")
add_theory("sum.lean" "${CMAKE_CURRENT_BINARY_DIR}/optional.olean")
add_theory("pair.lean" "${CMAKE_CURRENT_BINARY_DIR}/kernel.olean")
add_theory("sum.lean" "${CMAKE_CURRENT_BINARY_DIR}/optional.olean" "${CMAKE_CURRENT_BINARY_DIR}/pair.olean")
update_interface("kernel.olean" "kernel" "-n")
update_interface("Nat.olean" "library/arith" "-n")

BIN
src/builtin/obj/pair.olean Normal file
View file

Binary file not shown.

BIN
src/builtin/obj/sum.olean
View file

Binary file not shown.

10
src/builtin/pair.lean Normal file
View file

@ -0,0 +1,10 @@
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
definition pair {A : (Type U)} {B : (Type U)} (a : A) (b : B) := tuple a, b
theorem pair_inj1 {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x} (H : a = b) : proj1 a = proj1 b
:= subst (refl (proj1 a)) H
theorem pair_inj2 {A B : (Type U)} {a b : A # B} (H : a = b) : proj2 a = proj2 b
:= subst (refl (proj2 a)) H
theorem pairext_proj {A B : (Type U)} {p : A # B} {a : A} {b : B} (H1 : proj1 p = a) (H2 : proj2 p = b) : p = (pair a b)
:= @pairext A (λ x, B) p (pair a b) H1 (to_heq H2)

10
src/builtin/sum.lean
View file

@ -2,6 +2,7 @@
-- Released under Apache 2.0 license as described in the file LICENSE.
-- Author: Leonardo de Moura
import macros
import pair
import subtype
import optional
using subtype
@ -12,15 +13,6 @@ definition sum_pred (A B : (Type U)) := λ p : (optional A) # (optional B), (pro
definition sum (A B : (Type U)) := subtype ((optional A) # (optional B)) (sum_pred A B)
namespace sum
-- TODO: move pair, pair_inj1 and pair_inj2 to separate file
definition pair {A : (Type U)} {B : (Type U)} (a : A) (b : B) := tuple a, b
theorem pair_inj1 {A : (Type U)} {B : A → (Type U)} {a b : sig x, B x} (H : a = b) : proj1 a = proj1 b
:= subst (refl (proj1 a)) H
theorem pair_inj2 {A B : (Type U)} {a b : A # B} (H : a = b) : proj2 a = proj2 b
:= subst (refl (proj2 a)) H
theorem pairext_proj {A B : (Type U)} {p : A # B} {a : A} {b : B} (H1 : proj1 p = a) (H2 : proj2 p = b) : p = (pair a b)
:= @pairext A (λ x, B) p (pair a b) H1 (to_heq H2)
theorem inl_pred {A : (Type U)} (a : A) (B : (Type U)) : sum_pred A B (pair (some a) none)
:= not_intro
(assume N : (some a = none) = (none = (optional::@none B)),