refactor(library/cast): use .lean file instead of .cpp file to define casting library

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/CMakeLists.txt

@@ -195,8 +195,6 @@ add_subdirectory(library)
 set(LEAN_LIBS ${LEAN_LIBS} library)
 add_subdirectory(library/arith)
 set(LEAN_LIBS ${LEAN_LIBS} arithlib)
-add_subdirectory(library/cast)
-set(LEAN_LIBS ${LEAN_LIBS} castlib)
 add_subdirectory(library/all)
 set(LEAN_LIBS ${LEAN_LIBS} alllib)
 add_subdirectory(library/rewriter)

src/extra/cast.lean

@@ -0,0 +1,35 @@
+(*
+   "Type casting" library.
+*)
+
+(*
+   The cast operator allows us to cast an element of type A
+   into B if we provide a proof that types A and B are equal.
+*)
+Variable cast {A B : (Type U)} : A == B → A → B.
+(*
+   The CastEq axiom states that for any cast of x is equal to x.
+*)
+Axiom CastEq  {A B : (Type U)} (H : A == B) (x : A) : x == cast H x.
+
+(*
+   The CastApp axiom "propagates" the cast over application
+*)
+Axiom CastApp {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)}
+              (H1 : (Π x : A, B x) == (Π x : A', B' x)) (H2 : A == A')
+              (f : Π x : A, B x) (x : A) :
+    cast H1 f (cast H2 x) == f x.
+
+(*
+   If two (dependent) function spaces are equal, then their domains are equal.
+*)
+Axiom DomInj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)}
+             (H : (Π x : A, B x) == (Π x : A', B' x)) :
+    A == A'.
+
+(*
+   If two (dependent) function spaces are equal, then their ranges are equal.
+*)
+Axiom RanInj {A A' : (Type U)} {B : A → (Type U)} {B' : A' → (Type U)}
+             (H : (Π x : A, B x) == (Π x : A', B' x)) (a : A) :
+    B a == B' (cast (DomInj H) a).

src/frontends/lean/notation.cpp

@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #include "kernel/builtin.h"
 #include "library/basic_thms.h"
 #include "library/arith/arith.h"
-#include "library/cast/cast.h"
 #include "frontends/lean/frontend.h"
 
 namespace lean {
@@ -95,12 +94,6 @@ void init_builtin_notation(environment const & env, io_state & ios) {
     mark_implicit_arguments(env, mk_hsymm_fn(), 4);
     mark_implicit_arguments(env, mk_htrans_fn(), 6);
 
-    mark_implicit_arguments(env, mk_cast_fn(), 2);
-    mark_implicit_arguments(env, mk_cast_eq_fn(), 2);
-    mark_implicit_arguments(env, mk_cast_app_fn(), 4);
-    mark_implicit_arguments(env, mk_dom_inj_fn(), 4);
-    mark_implicit_arguments(env, mk_ran_inj_fn(), 4);
-
     // implicit arguments for basic theorems
     mark_implicit_arguments(env, mk_absurd_fn(), 1);
     mark_implicit_arguments(env, mk_double_neg_elim_fn(), 1);

src/library/all/all.cpp

@@ -7,14 +7,12 @@ Author: Leonardo de Moura
 #include "kernel/builtin.h"
 #include "library/basic_thms.h"
 #include "library/arith/arith.h"
-#include "library/cast/cast.h"
 #include "library/all/all.h"
 
 namespace lean {
 void import_all(environment const & env) {
     import_basic(env);
     import_basic_thms(env);
-    import_cast(env);
     import_arith(env);
 }
 environment mk_toplevel() {

src/library/cast/CMakeLists.txt

@@ -1,2 +0,0 @@
-add_library(castlib cast.cpp)
-target_link_libraries(castlib ${LEAN_LIBS})

src/library/cast/cast.cpp

@@ -1,58 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "kernel/environment.h"
-#include "kernel/abstract.h"
-#include "kernel/builtin.h"
-#include "kernel/instantiate.h"
-#include "library/basic_thms.h"
-#include "library/cast/cast.h"
-
-namespace lean {
-// Cast builtin operator
-MK_CONSTANT(cast_fn,      name("cast"));
-MK_CONSTANT(cast_eq_fn,   name("CastEq"));
-MK_CONSTANT(cast_app_fn,  name("CastApp"));
-MK_CONSTANT(dom_inj_fn,   name("DomInj"));
-MK_CONSTANT(ran_inj_fn,   name("RanInj"));
-
-void import_cast(environment const & env) {
-    if (!env->mark_builtin_imported("cast"))
-        return;
-    expr x         = Const("x");
-    expr A         = Const("A");
-    expr Ap        = Const("A'");
-    expr B         = Const("B");
-    expr Bp        = Const("B'");
-    expr piABx     = Pi({x, A}, B(x));
-    expr piApBpx   = Pi({x, Ap}, Bp(x));
-    expr H         = Const("H");
-    expr H1        = Const("H1");
-    expr H2        = Const("H2");
-    expr a         = Const("a");
-    expr b         = Const("b");
-    expr f         = Const("f");
-
-    env->add_var(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}}, Eq(A, B) >> (A >> B)));
-
-    // DomInj : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A'
-    env->add_axiom(dom_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}}, Eq(A, Ap)));
-
-    // RanInj : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A),
-    //                     B a = B' (cast A A' (DomInj A A' B B' H) a)
-    env->add_axiom(ran_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}, {a, A}},
-                                       Eq(B(a), Bp(Cast(A, Ap, DomInj(A, Ap, B, Bp, H), a)))));
-
-    // CastEq : Pi (A B : Type u) (H : A == B) (x : A), x == (cast A B H x)
-    env->add_axiom(cast_eq_fn_name, Pi({{A, TypeU}, {B, TypeU}, {H, Eq(A, B)}, {x, A}}, Eq(x, Cast(A, B, H, x))));
-
-    // CastApp : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H1 : (Pi x : A, B x) = (Pi x : A', B' x)) (H2 : A = A')
-    //              (f : Pi x : A, B x) (x : A),  Cast(Pi(x : A, B x), Pi(x : A', B' x), H1, f)(Cast(A, A', H2, x)) ==  f(x)
-    env->add_axiom(cast_app_fn_name, Pi({{A, TypeU},
-                    {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H1, Eq(piABx, piApBpx)}, {H2, Eq(A, Ap)}, {f, piABx}, {x, A}},
-            Eq(Cast(piABx, piApBpx, H1, f)(Cast(A, Ap, H2, x)), f(x))));
-}
-}

src/library/cast/cast.h

@@ -1,60 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "kernel/expr.h"
-
-namespace lean {
-/** \brief Type Cast. It has type <tt>Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B</tt> */
-expr mk_cast_fn();
-/** \brief Return the term (cast A B H a) */
-inline expr mk_cast(expr const & A, expr const & B, expr const & H, expr const & a) { return mk_app(mk_cast_fn(), A, B, H, a); }
-inline expr Cast(expr const & A, expr const & B, expr const & H, expr const & a) { return mk_cast(A, B, H, a); }
-
-/** \brief Axiom a == (cast A B H a) */
-expr mk_cast_eq_fn();
-inline expr CastEq(expr const & A, expr const & B, expr const & H, expr const & a) { return mk_app({mk_cast_eq_fn(), A, B, H, a}); }
-
-/** \brief Axiom
-    CastApp :
-    Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H1 : (Pi x : A, B x) = (Pi x : A', B' x)) (H2 : A = A')
-       (f : Pi x : A, B x) (x : A), Cast(Pi(x : A, B x), Pi(x : A', B' x), H1, f)(Cast(A, A', H2, x)) ==  f(x)
-*/
-expr mk_cast_app_fn();
-inline expr CastApp(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H1, expr const & H2,
-                    expr const & f, expr const & x) {
-    return mk_app({mk_cast_app_fn(), A, Ap, B, Bp, H1, H2, f, x});
-}
-
-/** \brief Domain Injectivity.
-    It has type <tt>Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A' </tt>
-*/
-expr mk_dom_inj_fn();
-/** \brief Return the term (DomInj A A' B B' H) */
-inline expr mk_dom_inj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H) {
-    return mk_app({mk_dom_inj_fn(), A, Ap, B, Bp, H});
-}
-inline expr DomInj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H) {
-    return mk_dom_inj(A, Ap, B, Bp, H);
-}
-
-/** \brief Range Injectivity.
-    It has type <tt>Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A),
-                       B a = B' (cast A A' (DomInj A A' B B' H) a)</tt>
-*/
-expr mk_ran_inj_fn();
-/** \brief Return the term (RanInj A A' B B' H) */
-inline expr mk_ran_inj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H, expr const & a) {
-    return mk_app({mk_ran_inj_fn(), A, Ap, B, Bp, H, a});
-}
-inline expr RanInj(expr const & A, expr const & Ap, expr const & B, expr const & Bp, expr const & H, expr const & a) {
-    return mk_ran_inj(A, Ap, B, Bp, H, a);
-}
-
-class environment;
-/** \brief Import type "casting" library */
-void import_cast(environment const & env);
-}

src/shell/CMakeLists.txt

@@ -4,15 +4,23 @@ add_executable(lean lean.cpp)
 add_dependencies(lean githash)
 target_link_libraries(lean ${EXTRA_LIBS})
 
+function(add_extra_dependency indir file)
+  get_filename_component(FNAME ${file} NAME)
+  add_custom_command(OUTPUT ${LEAN_BINARY_DIR}/shell/${indir}/${FNAME}
+    COMMAND ${CMAKE_COMMAND} -E copy ${file} ${LEAN_BINARY_DIR}/shell/${indir}/${FNAME}
+    MAIN_DEPENDENCY ${file})
+  add_custom_target("${FNAME}_extra" DEPENDS ${LEAN_BINARY_DIR}/shell/${indir}/${FNAME})
+  add_dependencies(lean "${FNAME}_extra")
+endfunction()
+
 function(add_extra_module indir)
   file(GLOB EXTRA_LUA_FILES "${LEAN_SOURCE_DIR}/extra/${indir}/*.lua")
   foreach(FILE ${EXTRA_LUA_FILES})
-    get_filename_component(FNAME ${FILE} NAME)
-    add_custom_command(OUTPUT ${LEAN_BINARY_DIR}/shell/${indir}/${FNAME}
-      COMMAND ${CMAKE_COMMAND} -E copy ${FILE} ${LEAN_BINARY_DIR}/shell/${indir}/${FNAME}
-      MAIN_DEPENDENCY ${FILE})
-    add_custom_target("${FNAME}_extra" DEPENDS ${LEAN_BINARY_DIR}/shell/${indir}/${FNAME})
-    add_dependencies(lean "${FNAME}_extra")
+    add_extra_dependency(${indir} ${FILE})
+  endforeach(FILE)
+  file(GLOB EXTRA_LEAN_FILES "${LEAN_SOURCE_DIR}/extra/${indir}/*.lean")
+  foreach(FILE ${EXTRA_LEAN_FILES})
+    add_extra_dependency(${indir} ${FILE})
   endforeach(FILE)
 endfunction()
 

tests/lean/cast1.lean

@@ -1,3 +1,5 @@
+Import "cast.lean"
+
 Variable vector : Type -> Nat -> Type
 Axiom N0 (n : Nat) : n + 0 = n
 Theorem V0 (T : Type) (n : Nat) : (vector T (n + 0)) = (vector T n) :=

tests/lean/cast1.lean.expected.out

@@ -1,12 +1,18 @@
   Set: pp::colors
   Set: pp::unicode
+Importing file '/home/leo/projects/lean/build/debug/shell/cast.lean'
+  Assumed: cast
+  Assumed: CastEq
+  Assumed: CastApp
+  Assumed: DomInj
+  Assumed: RanInj
   Assumed: vector
   Assumed: N0
   Proved: V0
   Assumed: f
   Assumed: m
   Assumed: v1
-Error (line: 12, pos: 6) type mismatch at application
+Error (line: 14, pos: 6) type mismatch at application
     f m v1
 Function type:
     Π (n : ℕ), vector ℤ n → ℤ

tests/lean/cast2.lean

@@ -1,3 +1,4 @@
+Import "cast.lean"
 Variable A : Type
 Variable B : Type
 Variable A' : Type

tests/lean/cast2.lean.expected.out

@@ -1,5 +1,11 @@
   Set: pp::colors
   Set: pp::unicode
+Importing file '/home/leo/projects/lean/build/debug/shell/cast.lean'
+  Assumed: cast
+  Assumed: CastEq
+  Assumed: CastApp
+  Assumed: DomInj
+  Assumed: RanInj
   Assumed: A
   Assumed: B
   Assumed: A'

tests/lean/cast3.lean

@@ -1,3 +1,5 @@
+Import "cast.lean"
+
 Variables A A' B B' : Type
 Variable x : A
 Eval cast (Refl A) x
@@ -20,4 +22,3 @@ Axiom Hb : A2 = A3
 Variable a : A1
 Eval (cast Hb (cast Ha a))
 Check (cast Hb (cast Ha a))
-

tests/lean/cast3.lean.expected.out

@@ -1,5 +1,11 @@
   Set: pp::colors
   Set: pp::unicode
+Importing file '/home/leo/projects/lean/build/debug/shell/cast.lean'
+  Assumed: cast
+  Assumed: CastEq
+  Assumed: CastApp
+  Assumed: DomInj
+  Assumed: RanInj
   Assumed: A
   Assumed: A'
   Assumed: B

tests/lean/cast4.lean

@@ -1,3 +1,4 @@
+Import "cast.lean"
 SetOption pp::colors false
 
 Definition TypeM := (Type M)

tests/lean/cast4.lean.expected.out

@@ -1,5 +1,11 @@
   Set: pp::colors
   Set: pp::unicode
+Importing file '/home/leo/projects/lean/build/debug/shell/cast.lean'
+  Assumed: cast
+  Assumed: CastEq
+  Assumed: CastApp
+  Assumed: DomInj
+  Assumed: RanInj
   Set: pp::colors
   Defined: TypeM
   Defined: TypeU

tests/lean/mod1.lean.expected.out

@@ -1,13 +1,11 @@
   Set: pp::colors
   Set: pp::unicode
-Importing file 'simple.lean'
+Importing file './simple.lean'
   Assumed: x
   Assumed: y
-Module 'simple.lean' has already been imported
-Importing file 'simple.lean'
+Importing file './simple.lean'
   Assumed: x
   Assumed: y
-Module 'simple.lean' has already been imported
 x + y : ℤ
   Assumed: z
 z : ℤ

tests/lean/norm_bug1.lean

@@ -1,3 +1,4 @@
+Import "cast.lean"
 SetOption pp::colors false
 
 Definition TypeM := (Type M)

tests/lean/norm_bug1.lean.expected.out

@@ -1,5 +1,11 @@
   Set: pp::colors
   Set: pp::unicode
+Importing file '/home/leo/projects/lean/build/debug/shell/cast.lean'
+  Assumed: cast
+  Assumed: CastEq
+  Assumed: CastApp
+  Assumed: DomInj
+  Assumed: RanInj
   Set: pp::colors
   Defined: TypeM
   Defined: TypeU

tests/lean/type_inf_bug1.lean

@@ -1,3 +1,4 @@
+Import "cast.lean"
 SetOption pp::colors false
 
 Definition TypeM := (Type M)

tests/lean/type_inf_bug1.lean.expected.out

@@ -1,5 +1,11 @@
   Set: pp::colors
   Set: pp::unicode
+Importing file '/home/leo/projects/lean/build/debug/shell/cast.lean'
+  Assumed: cast
+  Assumed: CastEq
+  Assumed: CastApp
+  Assumed: DomInj
+  Assumed: RanInj
   Set: pp::colors
   Defined: TypeM
   Defined: TypeU