Add Cast, DomInj and RanInj. Improve operator << for lean_frontend objects.

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

src/frontends/lean/lean_notation.cpp

@@ -75,12 +75,15 @@ void init_builtin_notation(frontend & f) {
     f.add_coercion(mk_nat_to_real_fn());
 
     // implicit arguments for builtin axioms
+    f.mark_implicit_arguments(mk_cast_fn(), {true, true, false, false});
     f.mark_implicit_arguments(mk_mp_fn(), {true, true, false, false});
     f.mark_implicit_arguments(mk_discharge_fn(), {true, true, false});
     f.mark_implicit_arguments(mk_refl_fn(), {true, false});
     f.mark_implicit_arguments(mk_subst_fn(), {true, true, true, false, false, false});
     f.mark_implicit_arguments(mk_eta_fn(), {true, true, false});
     f.mark_implicit_arguments(mk_imp_antisym_fn(), {true, true, false, false});
+    f.mark_implicit_arguments(mk_dom_inj_fn(), {true, true, true, true, false});
+    f.mark_implicit_arguments(mk_ran_inj_fn(), {true, true, true, true, false, false});
 
     // implicit arguments for basic theorems
     f.mark_implicit_arguments(mk_absurd_fn(), {true, false, false});

src/frontends/lean/lean_pp.cpp

@@ -1291,7 +1291,13 @@ formatter mk_pp_formatter(frontend const & fe) {
 std::ostream & operator<<(std::ostream & out, frontend const & fe) {
     options const & opts = fe.get_state().get_options();
     formatter fmt = mk_pp_formatter(fe);
-    out << mk_pair(fmt(fe, opts), opts);
+    bool first = true;
+    std::for_each(fe.begin_objects(),
+                  fe.end_objects(),
+                  [&](object const & obj) {
+                      if (first) first = false; else out << "\n";
+                      out << mk_pair(fmt(obj, opts), opts);
+                  });
     return out;
 }
 }

src/kernel/builtin.cpp

@@ -149,6 +149,7 @@ MK_CONSTANT(not_fn,     name("not"));
 MK_CONSTANT(forall_fn,  name("forall"));
 MK_CONSTANT(exists_fn,  name("exists"));
 MK_CONSTANT(homo_eq_fn, name("heq"));
+MK_CONSTANT(cast_fn,    name("cast"));
 
 // Axioms
 MK_CONSTANT(mp_fn,          name("MP"));
@@ -158,6 +159,8 @@ MK_CONSTANT(case_fn,        name("Case"));
 MK_CONSTANT(subst_fn,       name("Subst"));
 MK_CONSTANT(eta_fn,         name("Eta"));
 MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
+MK_CONSTANT(dom_inj_fn,     name("DomInj"));
+MK_CONSTANT(ran_inj_fn,     name("RanInj"));
 
 void add_basic_theory(environment & env) {
     env.add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
@@ -171,10 +174,13 @@ void add_basic_theory(environment & env) {
     expr x         = Const("x");
     expr y         = Const("y");
     expr A         = Const("A");
+    expr Ap        = Const("A'");
     expr A_pred    = A >> Bool;
     expr B         = Const("B");
+    expr Bp        = Const("B'");
     expr q_type    = Pi({A, TypeU}, A_pred >> Bool);
     expr piABx     = Pi({x, A}, B(x));
+    expr piApBpx   = Pi({x, Ap}, Bp(x));
     expr A_arrow_u = A >> TypeU;
     expr P         = Const("P");
     expr H         = Const("H");
@@ -209,6 +215,9 @@ void add_basic_theory(environment & env) {
     // homogeneous equality
     env.add_definition(homo_eq_fn_name, Pi({{A,TypeU},{x,A},{y,A}}, Bool), Fun({{A,TypeU}, {x,A}, {y,A}}, Eq(x, y)));
 
+    // Cast: Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B
+    env.add_var(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}, {H, Eq(A,B)}, {a, A}}, B));
+
     // MP : Pi (a b : Bool) (H1 : a => b) (H2 : a), b
     env.add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b));
 
@@ -229,5 +238,13 @@ void add_basic_theory(environment & env) {
 
     // ImpliesAntisym : Pi (a b : Bool) (H1 : a => b) (H2 : b => a), a = b
     env.add_axiom(imp_antisym_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Implies(b, a)}}, Eq(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)))));
 }
 }

src/kernel/builtin.h

@@ -113,6 +113,12 @@ expr mk_homo_eq_fn();
 inline expr mk_homo_eq(expr const & A, expr const & l, expr const & r) { return mk_app(mk_homo_eq_fn(), A, l, r); }
 inline expr hEq(expr const & A, expr const & l, expr const & r) { return mk_homo_eq(A, l, r); }
 
+/** \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 Modus Ponens axiom */
 expr mk_mp_fn();
 /** \brief (Axiom) {a : Bool}, {b : Bool}, H1 : a => b, H2 : a |- MP(a, b, H1, H2) : b */
@@ -148,6 +154,20 @@ expr mk_imp_antisym_fn();
 /** \brief (Axiom) {a : Bool}, {b : Bool}, H1 : a => b, H2 : b => a |- ImpAntisym(a, b, H1, H2) : a = b */
 inline expr ImpAntisym(expr const & a, expr const & b, expr const & H1, expr const & H2) { return mk_app(mk_imp_antisym_fn(), a, b, H1, H2); }
 
+/** \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 Initialize the environment with basic builtin declarations and axioms */
 void add_basic_theory(environment & env);

tests/lean/cast1.lean

@@ -0,0 +1,20 @@
+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) :=
+   Congr (Refl (vector T)) (N0 n)
+Variable f (n : Nat) (v : vector Int n) : Int
+Variable m : Nat
+Variable v1 : vector Int (m + 0)
+(*
+   The following application will fail because (vector Int (m + 0)) and (vector Int m)
+   are not definitionally equal.
+*)
+Check f m v1
+(*
+   The next one succeeds using the "casting" operator.
+   We can do it, because (V0 Int m) is a proof that
+   (vector Int (m + 0)) and (vector Int m) are propositionally equal.
+   That is, they have the same interpretation in the lean set theoretic
+   semantics.
+*)
+Check f m (cast (V0 Int m) v1)

tests/lean/cast1.lean.expected.out

@@ -0,0 +1,16 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: vector
+  Assumed: N0
+  Proved: V0
+  Assumed: f
+  Assumed: m
+  Assumed: v1
+Error (line: 12, pos: 6) type mismatch at application
+    f m v1
+Function type:
+    Π (n : ℕ) (v : vector ℤ n), ℤ
+Arguments types:
+    m : ℕ
+    v1 : vector ℤ (m + 0)
+ℤ

tests/lean/cast2.lean

@@ -0,0 +1,11 @@
+Variable A : Type
+Variable B : Type
+Variable A' : Type
+Variable B' : Type
+Axiom H : A -> B = A' -> B'
+Variable a : A
+Check DomInj H
+Theorem BeqB' : B = B' := RanInj H a
+Set pp::implicit true
+Show DomInj H
+Show RanInj H a

tests/lean/cast2.lean.expected.out

@@ -0,0 +1,13 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: A
+  Assumed: B
+  Assumed: A'
+  Assumed: B'
+  Assumed: H
+  Assumed: a
+A = A'
+  Proved: BeqB'
+  Set: lean::pp::implicit
+DomInj::explicit A A' (λ x : A, B) (λ x : A', B') H
+RanInj::explicit A A' (λ x : A, B) (λ x : A', B') H a