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

refactor(library/cast): replace cast semantic attachment with axioms, add heterogeneous symmetry axiom

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-21 18:23:37 -08:00
parent df58eb132e
commit 9128a437b8
15 changed files with 148 additions and 137 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/frontends/lean/notation.cpp
View file

@ -83,17 +83,21 @@ void init_builtin_notation(environment const & env, io_state & ios) {
add_coercion(env, mk_nat_to_real_fn());
// implicit arguments for builtin axioms
mark_implicit_arguments(env, mk_cast_fn(), 2);
mark_implicit_arguments(env, mk_mp_fn(), 2);
mark_implicit_arguments(env, mk_discharge_fn(), 2);
mark_implicit_arguments(env, mk_refl_fn(), 1);
mark_implicit_arguments(env, mk_subst_fn(), 4);
add_alias(env, "Subst", "SubstP");
mark_implicit_arguments(env, "SubstP", 3);
mark_implicit_arguments(env, mk_trans_ext_fn(), 6);
mark_implicit_arguments(env, mk_eta_fn(), 2);
mark_implicit_arguments(env, mk_abst_fn(), 4);
mark_implicit_arguments(env, mk_imp_antisym_fn(), 2);
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);

13
src/kernel/builtin.cpp
View file

@ -196,12 +196,14 @@ MK_CONSTANT(mp_fn, name("MP"));
MK_CONSTANT(discharge_fn, name("Discharge"));
MK_CONSTANT(case_fn, name("Case"));
MK_CONSTANT(refl_fn, name("Refl"));
MK_CONSTANT(trans_ext_fn, name("TransExt"));
MK_CONSTANT(subst_fn, name("Subst"));
MK_CONSTANT(eta_fn, name("Eta"));
MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
MK_CONSTANT(abst_fn, name("Abst"));
MK_CONSTANT(htrans_fn, name("HTrans"));
MK_CONSTANT(hsymm_fn, name("HSymm"));
void import_basic(environment const & env) {
if (!env->mark_builtin_imported("basic"))
return;
@ -269,9 +271,6 @@ void import_basic(environment const & env) {
// Refl : Pi (A : Type u) (a : A), a = a
env->add_axiom(refl_fn_name, Pi({{A, TypeU}, {a, A}}, Eq(a, a)));
// TransExt : Pi (A B C: Type u) (a : A) (b : B) (c : C) (H1 : a = b) (H2 : b = c), a = c
env->add_axiom(trans_ext_fn_name, Pi({{A, TypeU}, {B, TypeU}, {C, TypeU}, {a, A}, {b, B}, {c, C}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)));
// Subst : Pi (A : Type u) (a b : A) (P : A -> bool) (H1 : P a) (H2 : a = b), P b
env->add_axiom(subst_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {P, A_pred}, {H1, P(a)}, {H2, Eq(a, b)}}, P(b)));
@ -283,5 +282,11 @@ void import_basic(environment const & env) {
// Abst : Pi (A : Type u) (B : A -> Type u), f g : (Pi x : A, B x), H : (Pi x : A, (f x) = (g x)), f = g
env->add_axiom(abst_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {H, Pi(x, A, Eq(f(x), g(x)))}}, Eq(f, g)));
// HSymm : Pi (A B : Type u) (a : A) (b : B) (H1 : a = b), b = a
env->add_axiom(hsymm_fn_name, Pi({{A, TypeU}, {B, TypeU}, {a, A}, {b, B}, {H1, Eq(a, b)}}, Eq(b, a)));
// HTrans : Pi (A B C: Type u) (a : A) (b : B) (c : C) (H1 : a = b) (H2 : b = c), a = c
env->add_axiom(htrans_fn_name, Pi({{A, TypeU}, {B, TypeU}, {C, TypeU}, {a, A}, {b, B}, {c, C}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)));
}
}

21
src/kernel/builtin.h
View file

@ -164,13 +164,6 @@ expr mk_subst_fn();
/** \brief (Axiom) {A : Type u}, {a b : A}, P : A -> Bool, H1 : P a, H2 : a = b |- Subst(A, a, b, P, H1, H2) : P b */
inline expr Subst(expr const & A, expr const & a, expr const & b, expr const & P, expr const & H1, expr const & H2) { return mk_app({mk_subst_fn(), A, a, b, P, H1, H2}); }
/** \brief Heterogeneous Transitivity axiom */
expr mk_trans_ext_fn();
/** \brief (Axiom) {A : Type u}, {B : Type u}, {B : Type u}, {a : A}, {b : B} {c : C}, H1 : a = b, H2 : b = c |- TransExt(A, B, a, b, c, H1, H2) : a = c */
inline expr TransExt(expr const & A, expr const & B, expr const & C, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) {
return mk_app({mk_trans_ext_fn(), A, B, C, a, b, c, H1, H2});
}
/** \brief Eta conversion axiom */
expr mk_eta_fn();
/** \brief (Axiom) {A : Type u}, {B : A -> Type u}, f : (Pi x : A, B x) |- Eta(A, B, f) : ((Fun x : A => f x) = f) */
@ -186,6 +179,20 @@ expr mk_abst_fn();
/** \brief (Axiom) {A : Type u} {B : A -> Type u}, f g : {Pi x : A, B x}, H : (Pi x : A, (f x) = (g x)) |- Abst(A, B, f, g, H) : f = g */
inline expr Abst(expr const & A, expr const & B, expr const & f, expr const & g, expr const & H) { return mk_app({mk_abst_fn(), A, B, f, g, H}); }
/** \brief Heterogeneous symmetry axiom */
expr mk_hsymm_fn();
/** \brief (Axiom) {A : Type u}, {B : Type u}, {a : A}, {b : B}, H1 : a = b |- HSymm(A, B, a, b, H1) : b = a */
inline expr HSymm(expr const & A, expr const & B, expr const & a, expr const & b, expr const & H1) {
return mk_app({mk_hsymm_fn(), A, B, a, b, H1});
}
/** \brief Heterogeneous Transitivity axiom */
expr mk_htrans_fn();
/** \brief (Axiom) {A : Type u}, {B : Type u}, {C : Type u}, {a : A}, {b : B} {c : C}, H1 : a = b, H2 : b = c |- TransExt(A, B, a, b, c, H1, H2) : a = c */
inline expr HTrans(expr const & A, expr const & B, expr const & C, expr const & a, expr const & b, expr const & c, expr const & H1, expr const & H2) {
return mk_app({mk_htrans_fn(), A, B, C, a, b, c, H1, H2});
}
class environment;
/** \brief Initialize the environment with basic builtin declarations and axioms */
void import_basic(environment const & env);

4
src/library/basic_thms.cpp
View file

@ -253,8 +253,8 @@ void import_basic_thms(environment const & env) {
// Congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (a b : A) (H1 : f = g) (H2 : a = b), f a = g b
env->add_theorem(congr_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, Eq(f(a), g(b))),
Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}},
TransExt(B(a), B(b), B(b), f(a), f(b), g(b),
Congr2(A, B, a, b, f, H2), Congr1(A, B, f, g, b, H1))));
HTrans(B(a), B(b), B(b), f(a), f(b), g(b),
Congr2(A, B, a, b, f, H2), Congr1(A, B, f, g, b, H1))));
// ForallElim : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a

109
src/library/cast/cast.cpp
View file

@ -13,92 +13,11 @@ Author: Leonardo de Moura
namespace lean {
// Cast builtin operator
static name g_cast_name("Cast");
static format g_cast_fmt(g_cast_name);
expr mk_Cast_fn();
class cast_fn_value : public value {
expr m_type;
public:
cast_fn_value() {
expr A = Const("A");
expr B = Const("B");
// Cast: Pi (A : Type u) (B : Type u) (H : A = B) (a : A), B
m_type = Pi({{A, TypeU}, {B, TypeU}}, Eq(A, B) >> (A >> B));
}
virtual ~cast_fn_value() {}
virtual expr get_type() const { return m_type; }
virtual name get_name() const { return g_cast_name; }
virtual optional<expr> normalize(unsigned num_as, expr const * as) const {
if (num_as > 4 && as[1] == as[2]) {
// Cast T T H a == a
if (num_as == 5)
return some_expr(as[4]);
else
return some_expr(mk_app(num_as - 4, as + 4));
} else if (is_app(as[4]) &&
arg(as[4], 0) == mk_Cast_fn() &&
num_args(as[4]) == 5 &&
as[1] == arg(as[4], 2)) {
// Cast T1 T2 H1 (Cast T3 T1 H2 a) == Cast T3 T2 (Trans H1 H2) a
expr const & nested = as[4];
expr const & T1 = as[1];
expr const & T2 = as[2];
expr const & T3 = arg(nested, 1);
expr const & H1 = as[3];
expr const & H2 = arg(nested, 3);
expr const & a = arg(nested, 4);
expr c = Cast(T3, T2, Trans(TypeU, T3, T1, T2, H1, H2), a);
if (num_as == 5) {
return some_expr(c);
} else {
buffer<expr> new_as;
new_as.push_back(c);
new_as.append(num_as - 5, as + 5);
return some_expr(mk_app(new_as));
}
} else if (num_as > 5 && is_pi(as[1]) && is_pi(as[2])) {
// cast T1 T2 H f a_1 ... a_k
// Propagate application over cast.
// Remark: we check if T1 is a Pi to prevent non-termination
// For example, H can be a bogus hypothesis that shows
// that A == A -> A
// Since T1 and T2 are Pi's, we decompose them
expr const & T1 = as[1]; // Pi x : A1, B1
expr const & T2 = as[2]; // Pi x : A2, B2
expr const & H = as[3];
expr const & f = as[4];
expr const & a_1 = as[5]; // a_1 : A2
expr const & A1 = abst_domain(T1);
expr const & B1 = abst_body(T1);
expr const & A2 = abst_domain(T2);
expr const & B2 = abst_body(T2);
expr B1f = mk_lambda(abst_name(T1), A1, B1);
expr B2f = mk_lambda(abst_name(T2), A2, B2);
expr A2_eq_A1 = DomInj(A1, A2, B1f, B2f, Symm(TypeU, T1, T2, H));
expr a_1p = Cast(A2, A1, A2_eq_A1, a_1); // a_1p : A1
expr fa_1 = f(a_1p); // fa_1 : (A1 a_1p)
// Cast fa_1 back to B2 since the type of cast T1 T2 H f a_1
// is in B2 a_1p
expr B1_eq_B2_at_a_1p = RanInj(A1, A2, B1f, B2f, H, a_1p);
expr fa_1_B2 = Cast(instantiate(B1, 0, a_1p), instantiate(B2, 0, a_1), B1_eq_B2_at_a_1p, fa_1);
if (num_as == 6) {
return some_expr(fa_1_B2);
} else {
buffer<expr> new_as;
new_as.push_back(fa_1_B2);
new_as.append(num_as - 6, as + 6);
return some_expr(mk_app(new_as));
}
} else {
return none_expr();
}
}
};
MK_BUILTIN(Cast_fn, cast_fn_value);
MK_CONSTANT(cast_fn, name("cast"));
MK_CONSTANT(dom_inj_fn, name("DomInj"));
MK_CONSTANT(ran_inj_fn, name("RanInj"));
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"))
@ -111,14 +30,13 @@ void import_cast(environment const & env) {
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_builtin(mk_Cast_fn());
// Alias for Cast operator. We create the alias to be able to mark
// implicit arguments.
env->add_definition(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}}, Eq(A, B) >> (A >> B)), mk_Cast_fn());
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)));
@ -127,5 +45,14 @@ void import_cast(environment const & env) {
// 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))));
}
}

15
src/library/cast/cast.h
View file

@ -14,6 +14,21 @@ expr mk_cast_fn();
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>
*/

10
tests/lean/cast3.lean.expected.out
View file

@ -5,23 +5,23 @@
Assumed: B
Assumed: B'
Assumed: x
x
x == x
cast (Refl A) x
x == cast (Refl A) x
Assumed: b
Defined: f
Assumed: H
Assumed: a'
b
cast H (λ x : A, b) a'
Assumed: H2
Defined: g
0
g (cast H2 f a') : ℕ
Cast B B' (RanInj H2 (Cast A' A (DomInj (Symm H2)) a')) b
cast H2 (λ x : A, b) a'
Assumed: A1
Assumed: A2
Assumed: A3
Assumed: Ha
Assumed: Hb
Assumed: a
Cast A1 A3 (Trans Hb Ha) a
cast Hb (cast Ha a)
cast Hb (cast Ha a) : A3

29
tests/lean/cast4.lean Normal file
View file

@ -0,0 +1,29 @@
SetOption pp::colors false
Definition TypeM := (Type M)
Definition TypeU := (Type U)
Check fun (A A': TypeM)
(B : A -> TypeM)
(B' : A' -> TypeM)
(f : Pi x : A, B x)
(g : Pi x : A', B' x)
(a : A)
(b : A')
(H1 : (Pi x : A, B x) == (Pi x : A', B' x))
(H2 : f == g)
(H3 : a == b),
let
S1 : (Pi x : A', B' x) == (Pi x : A, B x) := Symm H1,
L2 : A' == A := DomInj S1,
b' : A := cast L2 b,
L3 : b == b' := CastEq L2 b,
L4 : a == b' := HTrans H3 L3,
L5 : f a == f b' := Congr2 f L4,
g' : (Pi x : A, B x) := cast S1 g,
L6 : g == g' := CastEq S1 g,
L7 : f == g' := HTrans H2 L6,
L8 : f b' == g' b' := Congr1 b' L7,
L9 : f a == g' b' := HTrans L5 L8,
L10 : g' b' == g b := CastApp S1 L2 g b
in HTrans L9 L10

30
tests/lean/cast4.lean.expected.out Normal file
View file

@ -0,0 +1,30 @@
Set: pp::colors
Set: pp::unicode
Set: pp::colors
Defined: TypeM
Defined: TypeU
λ (A A' : TypeM)
(B : A → TypeM)
(B' : A' → TypeM)
(f : Π x : A, B x)
(g : Π x : A', B' x)
(a : A)
(b : A')
(H1 : (Π x : A, B x) == (Π x : A', B' x))
(H2 : f == g)
(H3 : a == b),
let S1 : (Π x : A', B' x) == (Π x : A, B x) := Symm H1,
L2 : A' == A := DomInj S1,
b' : A := cast L2 b,
L3 : b == b' := CastEq L2 b,
L4 : a == b' := HTrans H3 L3,
L5 : f a == f b' := Congr2 f L4,
g' : Π x : A, B x := cast S1 g,
L6 : g == g' := CastEq S1 g,
L7 : f == g' := HTrans H2 L6,
L8 : f b' == g' b' := Congr1 b' L7,
L9 : f a == g' b' := HTrans L5 L8,
L10 : g' b' == g b := CastApp S1 L2 g b
in HTrans L9 L10 :
Π (A A' : TypeM) (B : A → TypeM) (B' : A' → TypeM) (f : Π x : A, B x) (g : Π x : A', B' x) (a : A) (b : A'),
(Π x : A, B x) == (Π x : A', B' x) → f == g → a == b → f a == g b

6
tests/lean/eq3.lean
View file

@ -1,5 +1,3 @@
Variable Vector : Nat -> Type
Variable n : Nat
Variable v1 : Vector n
@ -7,6 +5,6 @@ Variable v2 : Vector (n + 0)
Variable v3 : Vector (0 + n)
Axiom H1 : v1 == v2
Axiom H2 : v2 == v3
Check TransExt H1 H2
Check HTrans H1 H2
SetOption pp::implicit true
Check TransExt H1 H2
Check HTrans H1 H2

4
tests/lean/eq3.lean.expected.out
View file

@ -7,6 +7,6 @@
Assumed: v3
Assumed: H1
Assumed: H2
TransExt H1 H2 : v1 == v3
HTrans H1 H2 : v1 == v3
Set: lean::pp::implicit
@TransExt (Vector n) (Vector (n + 0)) (Vector (0 + n)) v1 v2 v3 H1 H2 : v1 == v3
@HTrans (Vector n) (Vector (n + 0)) (Vector (0 + n)) v1 v2 v3 H1 H2 : v1 == v3

3
tests/lean/norm_bug1.lean
View file

@ -2,7 +2,6 @@ SetOption pp::colors false
Definition TypeM := (Type M)
Definition TypeU := (Type U)
Variable CastEq {A : TypeU} {A' : TypeU} (H : A == A') (x : A) : x == cast H x
Check fun (A A': TypeM)
(a : A)
@ -26,6 +25,6 @@ Check fun (A A': TypeM)
L2 : A' == A := Symm L1,
b' : A := cast L2 b,
L3 : b == b' := CastEq L2 b,
L4 : a == b' := TransExt H3 L3,
L4 : a == b' := HTrans H3 L3,
L5 : f a == f b' := Congr2 f L4
in L5

5
tests/lean/norm_bug1.lean.expected.out
View file

@ -3,7 +3,6 @@
Set: pp::colors
Defined: TypeM
Defined: TypeU
Assumed: CastEq
λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := CastEq L2 b in L3 :
Π (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
λ (A A' : TypeM)
@ -20,7 +19,7 @@
L2 : A' == A := Symm L1,
b' : A := cast L2 b,
L3 : b == b' := CastEq L2 b,
L4 : a == b' := TransExt H3 L3,
L4 : a == b' := HTrans H3 L3,
L5 : f a == f b' := Congr2 f L4
in L5 :
Π (A A' : TypeM)
@ -31,4 +30,4 @@
(a : A)
(b : A')
(H1 : (Π x : A, B x) == (Π x : A', B' x)),
f == g → a == b → f a == f (Cast A' A (Symm (DomInj H1)) b)
f == g → a == b → f a == f (cast (Symm (DomInj H1)) b)

13
tests/lean/type_inf_bug1.lean
View file

@ -2,14 +2,13 @@ SetOption pp::colors false
Definition TypeM := (Type M)
Definition TypeU := (Type U)
Variable MyCastEq {A : TypeU} {A' : TypeU} (H : A == A') (x : A) : x == cast H x
Check fun (A A': TypeM)
(a : A)
(b : A')
(L2 : A' == A),
let b' : A := cast L2 b,
L3 : b == b' := MyCastEq L2 b
L3 : b == b' := CastEq L2 b
in L3
Check fun (A A': TypeM)
@ -25,13 +24,13 @@ Check fun (A A': TypeM)
let L1 : A == A' := DomInj H1,
L2 : A' == A := Symm L1,
b' : A := cast L2 b,
L3 : b == b' := MyCastEq L2 b,
L4 : a == b' := TransExt H3 L3,
L3 : b == b' := CastEq L2 b,
L4 : a == b' := HTrans H3 L3,
L5 : f a == f b' := Congr2 f L4,
S1 : (Pi x : A', B' x) == (Pi x : A, B x) := Symm H1,
g' : (Pi x : A, B x) := cast S1 g,
L6 : g == g' := MyCastEq S1 g,
L7 : f == g' := TransExt H2 L6,
L6 : g == g' := CastEq S1 g,
L7 : f == g' := HTrans H2 L6,
L8 : f b' == g' b' := Congr1 b' L7,
L9 : f a == g' b' := TransExt L5 L8
L9 : f a == g' b' := HTrans L5 L8
in L9

15
tests/lean/type_inf_bug1.lean.expected.out
View file

@ -3,8 +3,7 @@
Set: pp::colors
Defined: TypeM
Defined: TypeU
Assumed: MyCastEq
λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := MyCastEq L2 b in L3 :
λ (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), let b' : A := cast L2 b, L3 : b == b' := CastEq L2 b in L3 :
Π (A A' : TypeM) (a : A) (b : A') (L2 : A' == A), b == cast L2 b
λ (A A' : TypeM)
(B : A → TypeM)
@ -19,15 +18,15 @@
let L1 : A == A' := DomInj H1,
L2 : A' == A := Symm L1,
b' : A := cast L2 b,
L3 : b == b' := MyCastEq L2 b,
L4 : a == b' := TransExt H3 L3,
L3 : b == b' := CastEq L2 b,
L4 : a == b' := HTrans H3 L3,
L5 : f a == f b' := Congr2 f L4,
S1 : (Π x : A', B' x) == (Π x : A, B x) := Symm H1,
g' : Π x : A, B x := cast S1 g,
L6 : g == g' := MyCastEq S1 g,
L7 : f == g' := TransExt H2 L6,
L6 : g == g' := CastEq S1 g,
L7 : f == g' := HTrans H2 L6,
L8 : f b' == g' b' := Congr1 b' L7,
L9 : f a == g' b' := TransExt L5 L8
L9 : f a == g' b' := HTrans L5 L8
in L9 :
Π (A A' : TypeM)
(B : A → TypeM)
@ -37,4 +36,4 @@
(a : A)
(b : A')
(H1 : (Π x : A, B x) == (Π x : A', B' x)),
f == g → a == b → f a == Cast (Π x : A', B' x) (Π x : A, B x) (Symm H1) g (Cast A' A (Symm (DomInj H1)) b)
f == g → a == b → f a == cast (Symm H1) g (cast (Symm (DomInj H1)) b)