/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: Leonardo de Moura
*/
#include <utility>
#include "util/sstream.h"
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "kernel/inductive/inductive.h"
#include "library/io_state_stream.h"
#include "library/locals.h"
#include "library/util.h"
#include "library/reducible.h"
#include "library/tactic/tactic.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/tactic/class_instance_synth.h"
#include "library/tactic/inversion_tactic.h"

namespace lean {
namespace inversion {
result::result(list<goal> const & gs, list<list<name>> const & args, list<implementation_list> const & imps,
               list<rename_map> const & rs, name_generator const & ngen, substitution const & subst):
    m_goals(gs), m_args(args), m_implementation_lists(imps),
    m_renames(rs), m_ngen(ngen), m_subst(subst) {
    lean_assert_eq(length(m_goals), length(m_args));
    lean_assert_eq(length(m_goals), length(m_implementation_lists));
    lean_assert_eq(length(m_goals), length(m_renames));
}
}

/**
    \brief Given eq_rec of the form <tt>@eq.rec.{l₂ l₁} A a (λ (a' : A) (h : a = a'), B a') b a p</tt>,
    apply the eq_rec_eq definition to produce the equality

       b = @eq.rec.{l₂ l₁} A a (λ (a' : A) (h : a = a'), B a') b a p

    The eq_rec_eq definition is of the form

    definition eq_rec_eq.{l₁ l₂} {A : Type.{l₁}} {B : A → Type.{l₂}} [h : is_hset A] {a : A} (b : B a) (p : a = a) :
       b = @eq.rec.{l₂ l₁} A a (λ (a' : A) (h : a = a'), B a') b a p :=
    ...
*/
optional<expr> apply_eq_rec_eq(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & eq_rec) {
    buffer<expr> args;
    expr const & eq_rec_fn = get_app_args(eq_rec, args);
    if (args.size() != 6)
        return none_expr();
    expr const & p = args[5];
    if (!is_local(p) || !is_eq_a_a(tc, mlocal_type(p)))
        return none_expr();
    expr const & A = args[0];
    auto is_hset_A = mk_hset_instance(tc, ios, ctx, A);
    if (!is_hset_A)
        return none_expr();
    levels ls = const_levels(eq_rec_fn);
    level l2  = head(ls);
    level l1  = head(tail(ls));
    expr C    = tc.whnf(args[2]).first;
    if (!is_lambda(C))
        return none_expr();
    expr a1   = mk_local(tc.mk_fresh_name(), binding_domain(C));
    C         = tc.whnf(instantiate(binding_body(C), a1)).first;
    if (!is_lambda(C))
        return none_expr();
    C         = binding_body(C);
    if (!closed(C))
        return none_expr();
    expr B    = Fun(a1, C);
    expr a    = args[1];
    expr b    = args[3];
    expr r    = mk_constant("eq_rec_eq", {l1, l2});
    return some_expr(mk_app({r, A, B, *is_hset_A, a, b, p}));
}

typedef inversion::implementation_ptr  implementation_ptr;
typedef inversion::implementation_list implementation_list;
static void abstract_locals(implementation_list const & imps, unsigned nlocals, expr const * locals) {
    for (implementation_ptr const & imp : imps) {
        imp->update_exprs([&](expr const & e) { return abstract_locals(e, nlocals, locals); });
    }
}

static void instantiate(implementation_list const & imps, expr const & local) {
    for (implementation_ptr const & imp : imps) {
        imp->update_exprs([&](expr const & e) { return instantiate(e, local); });
    }
}

static void abstract_locals(implementation_list const & imps, buffer<expr> const & locals) {
    abstract_locals(imps, locals.size(), locals.data());
}

static void abstract_local(implementation_list const & imps, expr const & local) {
    abstract_locals(imps, 1, &local);
}

class inversion_tac {
    environment const &           m_env;
    io_state const &              m_ios;
    type_checker &                m_tc;
    list<name>                    m_ids;
    name_generator                m_ngen;
    substitution                  m_subst;

    bool                          m_dep_elim;
    bool                          m_proof_irrel;
    unsigned                      m_nparams;
    unsigned                      m_nindices;
    unsigned                      m_nminors;
    declaration                   m_I_decl;
    declaration                   m_cases_on_decl;

    void init_inductive_info(name const & n) {
        m_dep_elim       = inductive::has_dep_elim(m_env, n);
        m_nindices       = *inductive::get_num_indices(m_env, n);
        m_nparams        = *inductive::get_num_params(m_env, n);
        // This tactic is bases on cases_on construction which only has
        // minor premises for the introduction rules of this datatype.
        // For non-mutually recursive datatypes inductive::get_num_intro_rules == inductive::get_num_minor_premises
        m_nminors        = *inductive::get_num_intro_rules(m_env, n);
        m_I_decl         = m_env.get(n);
        m_cases_on_decl  = m_env.get({n, "cases_on"});
    }

    bool is_inversion_applicable(expr const & t) {
        buffer<expr> args;
        expr const & fn = get_app_args(t, args);
        if (!is_constant(fn))
            return false;
        if (!inductive::is_inductive_decl(m_env, const_name(fn)))
            return false;
        if (!m_env.find(name{const_name(fn), "cases_on"}) || !m_env.find(name("eq")))
            return false;
        if (m_proof_irrel && !m_env.find(name("heq")))
            return false;
        init_inductive_info(const_name(fn));
        if (args.size() != m_nindices + m_nparams)
            return false;
        return true;
    }

    pair<expr, expr> mk_eq(expr const & lhs, expr const & rhs) {
        expr lhs_type = m_tc.infer(lhs).first;
        expr rhs_type = m_tc.infer(rhs).first;
        level l       = sort_level(m_tc.ensure_type(lhs_type).first);
        constraint_seq cs;
        if (m_tc.is_def_eq(lhs_type, rhs_type, justification(), cs) && !cs) {
            return mk_pair(mk_app(mk_constant("eq", to_list(l)), lhs_type, lhs, rhs),
                           mk_app(mk_constant({"eq", "refl"}, to_list(l)), rhs_type, rhs));
        } else {
            return mk_pair(mk_app(mk_constant("heq", to_list(l)), lhs_type, lhs, rhs_type, rhs),
                           mk_app(mk_constant({"heq", "refl"}, to_list(l)), rhs_type, rhs));
        }
    }

    void assign(name const & n, expr const & val) {
        m_subst.assign(n, val);
    }

    /** \brief Split hyps into two "telescopes".
        - non_deps : hypotheses that do not depend on H
        - deps     : hypotheses that depend on H (directly or indirectly)
    */
    void split_deps(buffer<expr> const & hyps, expr const & H, buffer<expr> & non_deps, buffer<expr> & deps) {
        for (expr const & hyp : hyps) {
            expr const & hyp_type = mlocal_type(hyp);
            if (depends_on(hyp_type, H) || std::any_of(deps.begin(), deps.end(), [&](expr const & dep) { return depends_on(hyp_type, dep); })) {
                deps.push_back(hyp);
            } else {
                non_deps.push_back(hyp);
            }
        }
    }

    /** \brief Given a goal of the form

              Ctx, h : I A j, D |- T

        where the type of h is the inductive datatype (I A j) where A are parameters,
        and j the indices. Generate the goal

              Ctx, h : I A j, D, j' : J, h' : I A j' |- j == j' -> h == h' -> T

        Remark: (j == j' -> h == h') is a "telescopic" equality. If the environment
        is proof irrelevant, it is built using homogenous and heterogeneous equalities.
        If the environment is proof relevant, it is built using homogeneous equality
        and the eq.rec (this construction is much more complex than the proof irrelevant
        one).

        Remark: j is sequence of terms, and j' a sequence of local constants.

        The original goal is solved if we can solve the produced goal.

        \remark h_type is mlocal_type(h) after normalization
    */
    goal generalize_indices(goal const & g, expr const & h, expr const & h_type) {
        buffer<expr> hyps;
        g.get_hyps(hyps);
        expr m            = g.get_meta();
        expr m_type       = g.get_type();
        name h_new_name   = get_unused_name(local_pp_name(h), hyps);
        buffer<expr> I_args;
        expr const & I    = get_app_args(h_type, I_args);
        expr h_new_type  = mk_app(I, I_args.size() - m_nindices, I_args.data());
        expr d           = m_tc.whnf(m_tc.infer(h_new_type).first).first;
        name t_prefix("t");
        unsigned nidx = 1;
        if (m_proof_irrel) {
            unsigned eq_idx  = 1;
            name eq_prefix("H");
            buffer<expr> ts;
            buffer<expr> eqs;
            buffer<expr> refls;
            auto add_eq = [&](expr const & lhs, expr const & rhs) {
                pair<expr, expr> p = mk_eq(lhs, rhs);
                expr new_eq   = p.first;
                expr new_refl = p.second;
                eqs.push_back(mk_local(m_ngen.next(), g.get_unused_name(eq_prefix, eq_idx), new_eq, binder_info()));
                refls.push_back(new_refl);
            };
            for (unsigned i = I_args.size() - m_nindices; i < I_args.size(); i++) {
                expr t_type = binding_domain(d);
                expr t      = mk_local(m_ngen.next(), g.get_unused_name(t_prefix, nidx), t_type, binder_info());
                expr const & index = I_args[i];
                add_eq(t, index);
                h_new_type  = mk_app(h_new_type, t);
                hyps.push_back(t);
                ts.push_back(t);
                d           = instantiate(binding_body(d), t);
            }
            expr h_new    = mk_local(m_ngen.next(), h_new_name, h_new_type, local_info(h));
            if (m_dep_elim)
                add_eq(h_new, h);
            hyps.push_back(h_new);
            expr new_type = Pi(eqs, g.get_type());
            expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps);
            goal new_g(new_meta, new_type);
            expr val      = g.abstract(mk_app(mk_app(mk_app(Fun(ts, Fun(h_new, new_meta)), m_nindices, I_args.end() - m_nindices), h),
                                              refls));
            assign(g.get_name(), val);
            return new_g;
        } else {
            // proof relevant version
            buffer<expr> ss;
            buffer<expr> ts;
            buffer<expr> refls;
            for (unsigned i = I_args.size() - m_nindices; i < I_args.size(); i++) {
                expr t_type = binding_domain(d);
                expr t      = mk_local(m_ngen.next(), g.get_unused_name(t_prefix, nidx), t_type, binder_info());
                h_new_type  = mk_app(h_new_type, t);
                ss.push_back(I_args[i]);
                refls.push_back(mk_refl(m_tc, I_args[i]));
                hyps.push_back(t);
                ts.push_back(t);
                d           = instantiate(binding_body(d), t);
            }
            expr h_new    = mk_local(m_ngen.next(), h_new_name, h_new_type, local_info(h));
            ts.push_back(h_new);
            ss.push_back(h);
            refls.push_back(mk_refl(m_tc, h));
            hyps.push_back(h_new);
            buffer<expr> eqs;
            mk_telescopic_eq(m_tc, ss, ts, eqs);
            ts.pop_back();
            expr new_type = Pi(eqs, g.get_type());
            expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps);
            goal new_g(new_meta, new_type);
            expr val      = g.abstract(mk_app(mk_app(mk_app(Fun(ts, Fun(h_new, new_meta)), m_nindices, I_args.end() - m_nindices), h),
                                              refls));
            assign(g.get_name(), val);
            return new_g;
        }
    }

    /** \brief Generalize h dependencies.

        This tactic uses this method only for non-indexed inductive families.

        The hypotheses that depend on h are stored in deps.
    */
    goal generalize_dependecies(goal const & g, expr const & h, buffer<expr> & deps) {
        buffer<expr> hyps;
        g.get_hyps(hyps);
        hyps.erase_elem(h);
        buffer<expr> non_deps;
        split_deps(hyps, h, non_deps, deps);
        buffer<expr> & new_hyps = non_deps;
        new_hyps.push_back(h);
        expr new_type = Pi(deps, g.get_type());
        expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)), new_hyps);
        goal new_g(new_meta, new_type);
        expr val      = g.abstract(mk_app(new_meta, deps));
        assign(g.get_name(), val);
        return new_g;
    }

    /**
       \brief Given a goal of the form

                 Ctx, h : I A j |- T[h]

        produce the subgoals

                 Ctx, h : I A j |- b_1 : B_1 -> T [C_1 A b_1]
                 ...
                 Ctx, h : I A j |- b_n : B_n -> T [C_n A b_n]

        where the C_i's are the constructors (aka introduction rules) of the inductive datatype h.

        The hypothesis h must be the last hypothesis in the input goal. Consequently, no other
        hypothesis depends on it.

        The implementation list is external auxiliary data associated with constructors.
        For example, we use it to compile recursive equations. Each implementation corresponds to one
        equation. Each equation is tagged with a constructor C_i. The constructor is retrieved using
        the virtual method get_constructor_name. We split the list imps in n lists. One for each
        subgoal. An implementation associated with the constructor i is in the i-th resulting list.

        \remark This method assumes the indices j are local constants, and only h and j may depend on j.
    */
    std::pair<list<goal>, list<implementation_list>> apply_cases_on(goal const & g, implementation_list const & imps) {
        buffer<expr> hyps;
        g.get_hyps(hyps);
        expr const & h      = hyps.back();
        expr const & h_type = mlocal_type(h);
        buffer<expr> I_args;
        expr const & I      = get_app_args(h_type, I_args);
        name const & I_name = const_name(I);
        expr g_type         = g.get_type();
        expr cases_on;
        if (length(m_cases_on_decl.get_univ_params()) != length(m_I_decl.get_univ_params())) {
            level g_lvl  = sort_level(m_tc.ensure_type(g_type).first);
            cases_on     = mk_constant({I_name, "cases_on"}, cons(g_lvl, const_levels(I)));
        } else {
            cases_on     = mk_constant({I_name, "cases_on"}, const_levels(I));
        }
        // add params
        cases_on          = mk_app(cases_on, m_nparams, I_args.data());
        // add type former
        expr type_former  = g_type;
        if (m_dep_elim)
            type_former   = Fun(h, type_former);
        type_former       = Fun(m_nindices, I_args.end() - m_nindices, type_former);
        cases_on          = mk_app(cases_on, type_former);
        // add indices
        cases_on          = mk_app(cases_on, m_nindices, I_args.end() - m_nindices);
        // add h
        cases_on          = mk_app(cases_on, h);
        buffer<name> intro_names;
        get_intro_rule_names(m_env, I_name, intro_names);
        lean_assert(m_nminors == intro_names.size());
        buffer<expr> new_hyps;
        new_hyps.append(hyps.size() - m_nindices - 1, hyps.data());
        // add a subgoal for each minor premise of cases_on
        expr cases_on_type = m_tc.whnf(m_tc.infer(cases_on).first).first;
        buffer<goal> new_goals;
        buffer<implementation_list> new_imps;
        for (unsigned i = 0; i < m_nminors; i++) {
            expr new_type = binding_domain(cases_on_type);
            expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, new_type)), new_hyps);
            goal new_g(new_meta, new_type);
            new_goals.push_back(new_g);
            cases_on      = mk_app(cases_on, new_meta);
            cases_on_type = m_tc.whnf(binding_body(cases_on_type)).first; // the minor premises do not depend on each other
            name const & intro_name = intro_names[i];
            new_imps.push_back(filter(imps, [&](implementation_ptr const & imp) { return imp->get_constructor_name() == intro_name; }));
        }
        expr val        = g.abstract(cases_on);
        assign(g.get_name(), val);
        return mk_pair(to_list(new_goals), to_list(new_imps));
    }

    // Store in \c r the number of arguments for each cases_on minor.
    void get_minors_nargs(buffer<unsigned> & r) {
        expr cases_on_type = m_cases_on_decl.get_type();
        for (unsigned i = 0; i < m_nparams + 1 + m_nindices + 1; i++)
            cases_on_type = binding_body(cases_on_type);
        for (unsigned i = 0; i < m_nminors; i++) {
            expr minor_type = binding_domain(cases_on_type);
            unsigned nargs  = 0;
            while (is_pi(minor_type)) {
                nargs++;
                minor_type = binding_body(minor_type);
            }
            r.push_back(nargs);
            cases_on_type   = binding_body(cases_on_type);
        }
    }

    /**
       The method apply_cases_on produces subgoals of the form

                 Ctx, h : I A j |- b_i : B_i -> T [C_i A b_i]

       The b_i are the arguments of the constructor C_i.
       This method moves the b_i's to the hypotheses list.
    */
    std::pair<list<goal>, list<list<name>>> intros_minors_args(list<goal> gs) {
        buffer<unsigned> minors_nargs;
        get_minors_nargs(minors_nargs);
        lean_assert(length(gs) == minors_nargs.size());
        buffer<goal> new_gs;
        buffer<list<name>> new_args;
        for (unsigned i = 0; i < minors_nargs.size(); i++) {
            goal const & g = head(gs);
            unsigned nargs = minors_nargs[i];
            buffer<expr> hyps;
            g.get_hyps(hyps);
            buffer<expr> new_hyps;
            new_hyps.append(hyps);
            expr g_type    = g.get_type();
            buffer<name> curr_new_args;
            for (unsigned i = 0; i < nargs; i++) {
                expr type  = binding_domain(g_type);
                name new_h_name;
                if (m_ids) {
                    new_h_name = head(m_ids);
                    m_ids      = tail(m_ids);
                } else {
                    new_h_name = binding_name(g_type);
                }
                expr new_h = mk_local(m_ngen.next(), get_unused_name(new_h_name, new_hyps), type, binder_info());
                curr_new_args.push_back(mlocal_name(new_h));
                new_hyps.push_back(new_h);
                g_type     = instantiate(binding_body(g_type), new_h);
            }
            new_args.push_back(to_list(curr_new_args));
            g_type = head_beta_reduce(g_type);
            expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, g_type)), new_hyps);
            goal new_g(new_meta, g_type);
            new_gs.push_back(new_g);
            expr val      = g.abstract(Fun(nargs, new_hyps.end() - nargs, new_meta));
            assign(g.get_name(), val);
            gs = tail(gs);
        }
        return mk_pair(to_list(new_gs), to_list(new_args));
    }

    struct inversion_exception : public exception {
        inversion_exception(char const * msg):exception(msg) {}
        inversion_exception(sstream const & strm):exception(strm) {}
    };

    [[ noreturn ]] void throw_ill_formed_goal() {
        throw inversion_exception("ill-formed goal");
    }

    [[ noreturn ]] void throw_ill_typed_goal() {
        throw inversion_exception("ill-typed goal");
    }

    void throw_unification_eq_rec_failure() {
        throw inversion_exception("unification failed to eliminate eq.rec in homogeneous equality");
    }

    /** \brief Process goal of the form:  Pi (H : eq.rec A s C a s p = b), R
        The idea is to reduce it to
            Pi (H : a = b), R
        when A is a hset
        and then invoke intro_next_eq recursively.

        \remark \c type is the type of \c g after some normalization
    */
    goal intro_next_eq_rec(goal const & g, expr const & type) {
        lean_assert(is_pi(type));
        buffer<expr> hyps;
        g.get_hyps(hyps);
        expr const & eq  = binding_domain(type);
        expr const & lhs = app_arg(app_fn(eq));
        expr const & rhs = app_arg(eq);
        lean_assert(is_eq_rec(lhs));
        // lhs is of the form  (eq.rec A s C a s p)
        // aux_eq is a term of type ((eq.rec A s C a s p) = a)
        auto aux_eq = apply_eq_rec_eq(m_tc, m_ios, to_list(hyps), lhs);
        if (!aux_eq)
            throw_unification_eq_rec_failure();
        buffer<expr> lhs_args;
        get_app_args(lhs, lhs_args);
        expr const & reduced_lhs = lhs_args[3];
        expr new_eq      = ::lean::mk_eq(m_tc, reduced_lhs, rhs);
        expr new_type    = update_binding(type, new_eq, binding_body(type));
        expr new_meta    = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps);
        goal new_g(new_meta, new_type);
        // create assignment for g
        expr A           = m_tc.infer(lhs).first;
        level lvl        = sort_level(m_tc.ensure_type(A).first);
        // old_eq : eq.rec A s C a s p = b
        expr old_eq      = mk_local(m_ngen.next(), binding_name(type), eq, binder_info());
        // aux_eq : a = eq.rec A s C a s p
        expr trans_eq    = mk_app({mk_constant(name{"eq", "trans"}, {lvl}), A, reduced_lhs, lhs, rhs, *aux_eq, old_eq});
        // trans_eq : a = b
        expr val         = g.abstract(Fun(old_eq, mk_app(new_meta, trans_eq)));
        assign(g.get_name(), val);
        return intro_next_eq(new_g);
    }

    /**
       \brief Process goal of the form:  Ctx |- Pi (H : a == b), R   when a and b have the same type
       The idea is to reduce it to
           Ctx, H : a = b |- R
       This method is only used if the environment has a proof irrelevant Prop.
    */
    goal intro_next_heq(goal const & g) {
        lean_assert(m_proof_irrel);
        expr const & type   = g.get_type();
        expr eq             = binding_domain(type);
        lean_assert(const_name(get_app_fn(eq)) == "heq");
        buffer<expr> args;
        expr const & heq_fn = get_app_args(eq, args);
        constraint_seq cs;
        if (m_tc.is_def_eq(args[0], args[2], justification(), cs) && !cs) {
            buffer<expr> hyps;
            g.get_hyps(hyps);
            expr new_eq   = mk_app(mk_constant("eq", const_levels(heq_fn)), args[0], args[1], args[3]);
            expr new_hyp  = mk_local(m_ngen.next(), g.get_unused_name(binding_name(type)), new_eq, binder_info());
            expr new_type = instantiate(binding_body(type), new_hyp);
            hyps.push_back(new_hyp);
            expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type));
            expr new_meta = mk_app(new_mvar, hyps);
            goal new_g(new_meta, new_type);
            hyps.pop_back();
            expr H        = mk_local(m_ngen.next(), g.get_unused_name(binding_name(type)), binding_domain(type), binder_info());
            expr to_eq    = mk_app(mk_constant({"heq", "to_eq"}, const_levels(heq_fn)), args[0], args[1], args[3], H);
            expr val      = g.abstract(Fun(H, mk_app(mk_app(new_mvar, hyps), to_eq)));
            assign(g.get_name(), val);
            return new_g;
        } else {
            throw inversion_exception("unification failed to reduce heterogeneous equality into homogeneous one");
        }
    }

    /** \brief Process goal of the form:  Ctx |- Pi (H : a = b), R
        The idea is to reduce it to
            Ctx, H : a = b |- R

         \remark \c type is the type of \c g after some normalization
    */
    goal intro_next_eq_simple(goal const & g, expr const & type) {
        expr eq            = binding_domain(type);
        lean_assert(const_name(get_app_fn(eq)) == "eq");
        buffer<expr> hyps;
        g.get_hyps(hyps);
        expr new_hyp  = mk_local(m_ngen.next(), g.get_unused_name(binding_name(type)), binding_domain(type), binder_info());
        expr new_type = instantiate(binding_body(type), new_hyp);
        hyps.push_back(new_hyp);
        expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps);
        goal new_g(new_meta, new_type);
        expr val      = g.abstract(Fun(new_hyp, new_meta));
        assign(g.get_name(), val);
        return new_g;
    }

    goal intro_next_eq(goal const & g) {
        expr type          = g.get_type();
        if (!is_pi(type))
            throw_ill_formed_goal();
        expr eq            = binding_domain(type);
        expr const & eq_fn = get_app_fn(eq);
        if (!is_constant(eq_fn))
            throw_ill_formed_goal();
        if (const_name(eq_fn) == "eq") {
            expr const & lhs = app_arg(app_fn(eq));
            expr const & rhs = app_arg(eq);
            expr new_lhs     = m_tc.whnf(lhs).first;
            expr new_rhs     = m_tc.whnf(rhs).first;
            if (lhs != new_lhs || rhs != new_rhs) {
                eq   = mk_app(app_fn(app_fn(eq)), new_lhs, new_rhs);
                type = update_binding(type, eq, binding_body(type));
            }
            if (!m_proof_irrel && is_eq_rec(new_lhs)) {
                return intro_next_eq_rec(g, type);
            } else {
                return intro_next_eq_simple(g, type);
            }
        } else if (m_proof_irrel && const_name(eq_fn) == "heq") {
            return intro_next_heq(g);
        } else {
            throw_ill_formed_goal();
        }
    }

    /**
       \brief The no_confusion constructions uses lifts in the proof relevant version.
       We must apply lift.down to eliminate the auxiliary lift.
    */
    expr lift_down(expr const & v) {
        if (!m_proof_irrel) {
            expr v_type       = m_tc.whnf(m_tc.infer(v).first).first;
            if (!is_app(v_type))
                throw_unification_eq_rec_failure();
            expr const & lift = app_fn(v_type);
            if (!is_constant(lift) || const_name(lift) != "lift")
                throw_unification_eq_rec_failure();
            return mk_app(mk_constant(name{"lift", "down"}, const_levels(lift)), app_arg(v_type), v);
        } else {
            return v;
        }
    }

    rename_map          m_renames;
    implementation_list m_imps;

    /** \brief Update m_renames with old_hyps --> new_hyps. */
    void store_renames(buffer<expr> const & old_hyps, buffer<expr> const & new_hyps) {
        lean_assert(old_hyps.size() == new_hyps.size());
        for (unsigned i = 0; i < old_hyps.size(); i++) {
            m_renames.insert(mlocal_name(old_hyps[i]), mlocal_name(new_hyps[i]));
        }
    }

    // Remark: it also updates m_renames and m_imps
    optional<goal> unify_eqs(goal g, unsigned neqs) {
        if (neqs == 0)
            return optional<goal>(g); // done
        g = intro_next_eq(g);
        buffer<expr> hyps;
        g.get_hyps(hyps);
        lean_assert(!hyps.empty());
        expr eq = hyps.back();
        buffer<expr> eq_args;
        get_app_args(mlocal_type(eq), eq_args);
        expr const & A   = m_tc.whnf(eq_args[0]).first;
        expr lhs         = m_tc.whnf(eq_args[1]).first;
        expr rhs         = m_tc.whnf(eq_args[2]).first;
        constraint_seq cs;
        if (m_proof_irrel && m_tc.is_def_eq(lhs, rhs, justification(), cs) && !cs) {
            // deletion transition: t == t
            hyps.pop_back(); // remove t == t equality
            expr new_type = g.get_type();
            expr new_meta = mk_app(mk_metavar(m_ngen.next(), Pi(hyps, new_type)), hyps);
            goal new_g(new_meta, new_type);
            expr val      = g.abstract(new_meta);
            assign(g.get_name(), val);
            return unify_eqs(new_g, neqs-1);
        }
        buffer<expr> lhs_args, rhs_args;
        expr const & lhs_fn = get_app_args(lhs, lhs_args);
        expr const & rhs_fn = get_app_args(rhs, rhs_args);
        expr const & g_type = g.get_type();
        level const & g_lvl = sort_level(m_tc.ensure_type(g_type).first);
        if (is_constant(lhs_fn) &&
            is_constant(rhs_fn) &&
            inductive::is_intro_rule(m_env, const_name(lhs_fn)) &&
            inductive::is_intro_rule(m_env, const_name(rhs_fn))) {
            buffer<expr> A_args;
            expr const & A_fn   = get_app_args(A, A_args);
            if (!is_constant(A_fn) || !inductive::is_inductive_decl(m_env, const_name(A_fn)))
                throw_ill_typed_goal();
            name no_confusion_name(const_name(A_fn), "no_confusion");
            if (!m_env.find(no_confusion_name))
                throw inversion_exception(sstream() << "construction '" << no_confusion_name << "' is not available in the environment");
            expr no_confusion = mk_app(mk_app(mk_constant(no_confusion_name, cons(g_lvl, const_levels(A_fn))), A_args), g_type, lhs, rhs, eq);
            if (const_name(lhs_fn) == const_name(rhs_fn)) {
                // injectivity transition
                expr new_type = binding_domain(m_tc.whnf(m_tc.infer(no_confusion).first).first);
                if (m_proof_irrel)
                    hyps.pop_back(); // remove processed equality
                expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type));
                expr new_meta = mk_app(new_mvar, hyps);
                goal new_g(new_meta, new_type);
                expr val      = g.abstract(lift_down(mk_app(no_confusion, new_meta)));
                assign(g.get_name(), val);
                unsigned A_nparams = *inductive::get_num_params(m_env, const_name(A_fn));
                lean_assert(lhs_args.size() >= A_nparams);
                return unify_eqs(new_g, neqs - 1 + lhs_args.size() - A_nparams);
            } else {
                // conflict transition, eq is of the form c_1 ... = c_2 ..., where c_1 and c_2 are different constructors/intro rules.
                expr val      = g.abstract(lift_down(no_confusion));
                assign(g.get_name(), val);
                return optional<goal>(); // goal has been solved
            }
        }
        if (is_local(rhs)) {
            // solution transition, eq is of the form t = y, where y is a local constant

            // assume the current goal is of the form
            //
            //  non_deps, deps[rhs], H : lhs = rhs |- C[rhs]
            //
            //  We use non_deps to denote hypotheses that do not depend on rhs,
            //  and deps[rhs] to denote hypotheses that depend on it.
            //
            //  The resultant goal is of the form
            //
            //  non_deps, deps[lhs] |- C[lhs]
            //
            // Now, assume ?m1 is a solution for the resultant goal.
            // Then,
            //
            //     @eq.rec A lhs (fun rhs, Pi(deps[rhs], C[rhs])) (?m1 non_deps) rhs H deps[rhs]
            //
            // is a solution for the original goal.
            // Remark: A is the type of lhs and rhs
            hyps.pop_back(); // remove processed equality
            buffer<expr> non_deps, deps;
            split_deps(hyps, rhs, non_deps, deps);
            if (deps.empty() && !depends_on(g_type, rhs)) {
                // eq.rec is not necessary
                buffer<expr> & new_hyps = non_deps;
                expr new_type           = g_type;
                expr new_mvar           = mk_metavar(m_ngen.next(), Pi(new_hyps, new_type));
                expr new_meta           = mk_app(new_mvar, new_hyps);
                goal new_g(new_meta, new_type);
                expr val                = g.abstract(new_meta);
                assign(g.get_name(), val);
                return unify_eqs(new_g, neqs-1);
            } else {
                expr deps_g_type    = Pi(deps, g_type);
                abstract_locals(m_imps, deps);
                level eq_rec_lvl1   = sort_level(m_tc.ensure_type(deps_g_type).first);
                level eq_rec_lvl2   = sort_level(m_tc.ensure_type(A).first);
                expr tformer;
                if (m_proof_irrel)
                    tformer = Fun(rhs, deps_g_type);
                else
                    tformer = Fun(rhs, Fun(eq, deps_g_type));
                expr eq_rec         = mk_constant(name{"eq", "rec"}, {eq_rec_lvl1, eq_rec_lvl2});
                eq_rec              = mk_app(eq_rec, A, lhs, tformer);
                buffer<expr> new_hyps;
                new_hyps.append(non_deps);
                expr new_type       = instantiate(abstract_local(deps_g_type, rhs), lhs);
                abstract_local(m_imps, rhs);
                instantiate(m_imps, lhs);
                if (!m_proof_irrel) {
                    new_type = abstract_local(new_type, eq);
                    new_type = instantiate(new_type, mk_refl(m_tc, lhs));
                }
                buffer<expr> new_deps;
                for (unsigned i = 0; i < deps.size(); i++) {
                    expr new_hyp = mk_local(m_ngen.next(), binding_name(new_type), binding_domain(new_type),
                                            binding_info(new_type));
                    new_hyps.push_back(new_hyp);
                    new_deps.push_back(new_hyp);
                    new_type     = instantiate(binding_body(new_type), new_hyp);
                    instantiate(m_imps, new_hyp);
                }
                lean_assert(deps.size() == new_deps.size());
                store_renames(deps, new_deps);
                expr new_mvar       = mk_metavar(m_ngen.next(), Pi(new_hyps, new_type));
                expr new_meta       = mk_app(new_mvar, new_hyps);
                goal new_g(new_meta, new_type);
                expr eq_rec_minor   = mk_app(new_mvar, non_deps);
                eq_rec              = mk_app(eq_rec, eq_rec_minor, rhs, eq);
                expr val            = g.abstract(mk_app(eq_rec, deps));
                assign(g.get_name(), val);
                return unify_eqs(new_g, neqs-1);
            }
        } else if (is_local(lhs)) {
            // flip equation and reduce to previous case
            if (m_proof_irrel)
                hyps.pop_back(); // remove processed equality
            expr symm_eq   = mk_eq(rhs, lhs).first;
            expr new_type  = mk_arrow(symm_eq, g_type);
            expr new_mvar = mk_metavar(m_ngen.next(), Pi(hyps, new_type));
            expr new_meta = mk_app(new_mvar, hyps);
            goal new_g(new_meta, new_type);
            level eq_symm_lvl = sort_level(m_tc.ensure_type(A).first);
            expr symm_pr  = mk_constant(name{"eq", "symm"}, {eq_symm_lvl});
            symm_pr       = mk_app(symm_pr, A, lhs, rhs, eq);
            expr val      = g.abstract(mk_app(new_meta, symm_pr));
            assign(g.get_name(), val);
            return unify_eqs(new_g, neqs);
        }
        throw inversion_exception("unification failed");
    }

    auto unify_eqs(list<goal> const & gs, list<list<name>> args, list<implementation_list> imps) ->
        std::tuple<list<goal>, list<list<name>>, list<implementation_list>, list<rename_map>> {
        lean_assert(length(gs) == length(imps));
        unsigned neqs = m_nindices + (m_dep_elim ? 1 : 0);
        buffer<goal>                new_goals;
        buffer<list<name>>          new_args;
        buffer<implementation_list> new_imps;
        buffer<rename_map>          new_renames;
        for (goal const & g : gs) {
            flet<rename_map>          set1(m_renames, rename_map());
            flet<implementation_list> set2(m_imps,    head(imps));
            if (optional<goal> new_g = unify_eqs(g, neqs)) {
                new_goals.push_back(*new_g);
                list<name> new_as = map(head(args), [&](name const & n) { return m_renames.find(n); });
                new_args.push_back(new_as);
                new_imps.push_back(m_imps);
                new_renames.push_back(m_renames);
            }
            imps  = tail(imps);
            args = tail(args);
        }
        return std::make_tuple(to_list(new_goals), to_list(new_args), to_list(new_imps), to_list(new_renames));
    }

    std::pair<goal, rename_map> intro_deps(goal const & g, buffer<expr> const & deps) {
        buffer<expr> hyps;
        g.get_hyps(hyps);
        buffer<expr> new_hyps;
        new_hyps.append(hyps);
        rename_map rs;
        expr g_type    = g.get_type();
        for (expr const & d : deps) {
            expr type  = binding_domain(g_type);
            expr new_d = mk_local(m_ngen.next(), get_unused_name(local_pp_name(d), new_hyps), type, local_info(d));
            rs.insert(mlocal_name(d), mlocal_name(new_d));
            new_hyps.push_back(new_d);
            g_type     = instantiate(binding_body(g_type), new_d);
        }
        expr new_meta  = mk_app(mk_metavar(m_ngen.next(), Pi(new_hyps, g_type)), new_hyps);
        goal new_g(new_meta, g_type);
        unsigned ndeps = deps.size();
        expr val       = g.abstract(Fun(ndeps, new_hyps.end() - ndeps, new_meta));
        assign(g.get_name(), val);
        return mk_pair(new_g, rs);
    }

    std::pair<list<goal>, list<rename_map>> intro_deps(list<goal> const & gs, buffer<expr> const & deps) {
        buffer<goal> new_goals;
        buffer<rename_map> new_rs;
        for (goal const & g : gs) {
            auto p = intro_deps(g, deps);
            new_goals.push_back(p.first);
            new_rs.push_back(p.second);
        }
        return mk_pair(to_list(new_goals), to_list(new_rs));
    }

public:
    inversion_tac(environment const & env, io_state const & ios, name_generator const & ngen,
                  type_checker & tc, substitution const & subst, list<name> const & ids):
        m_env(env), m_ios(ios), m_tc(tc), m_ids(ids),
        m_ngen(ngen), m_subst(subst) {
        m_proof_irrel = m_env.prop_proof_irrel();
    }

    inversion_tac(environment const & env, io_state const & ios, type_checker & tc):
        inversion_tac(env, ios, tc.mk_ngen(), tc, substitution(), list<name>()) {}

    typedef inversion::result result;

    optional<result> execute(goal const & g, expr const & h, implementation_list const & imps) {
        try {
            expr h_type                         = m_tc.whnf(mlocal_type(h)).first;
            if (!is_inversion_applicable(h_type))
                return optional<result>();
            if (m_nindices == 0) {
                buffer<expr> deps;
                goal g1                             = generalize_dependecies(g, h, deps);
                auto gs_imps_pair                   = apply_cases_on(g1, imps);
                list<goal> gs2                      = gs_imps_pair.first;
                list<implementation_list> new_imps  = gs_imps_pair.second;
                auto gs_args_pair                   = intros_minors_args(gs2);
                list<goal> gs3                      = gs_args_pair.first;
                list<list<name>> args               = gs_args_pair.second;
                auto gs_rs_pair                     = intro_deps(gs3, deps);
                list<goal> gs4                      = gs_rs_pair.first;
                list<rename_map> rs                 = gs_rs_pair.second;
                return optional<result>(result(gs4, args, new_imps, rs, m_ngen, m_subst));
            } else {
                goal g1                             = generalize_indices(g, h, h_type);
                auto gs_imps_pair                   = apply_cases_on(g1, imps);
                list<goal> gs2                      = gs_imps_pair.first;
                list<implementation_list> new_imps  = gs_imps_pair.second;
                auto gs_args_pair                   = intros_minors_args(gs2);
                list<goal> gs3                      = gs_args_pair.first;
                list<list<name>> args               = gs_args_pair.second;
                list<goal> gs4;
                list<rename_map> rs;
                std::tie(gs4, args, new_imps, rs)   = unify_eqs(gs3, args, new_imps);
                return optional<result>(result(gs4, args, new_imps, rs, m_ngen, m_subst));
            }
        } catch (inversion_exception & ex) {
            return optional<result>();
        }
    }

    optional<result> execute(goal const & g, name const & n, implementation_list const & imps) {
        auto p         = g.find_hyp(n);
        if (!p)
            return optional<result>();
        expr const & h = p->first;
        return execute(g, h, imps);
    }
};

namespace inversion {
optional<result> apply(environment const & env, io_state const & ios, type_checker & tc,
                       goal const & g, expr const & h, implementation_list const & imps) {
    return inversion_tac(env, ios, tc).execute(g, h, imps);
}
}

tactic inversion_tactic(name const & n, list<name> const & ids) {
    auto fn = [=](environment const & env, io_state const & ios, proof_state const & ps) -> optional<proof_state> {
        goals const & gs  = ps.get_goals();
        if (empty(gs))
            return none_proof_state();
        goal  g           = head(gs);
        goals tail_gs     = tail(gs);
        name_generator ngen              = ps.get_ngen();
        std::unique_ptr<type_checker> tc = mk_type_checker(env, ngen.mk_child(), ps.relax_main_opaque());
        inversion_tac tac(env, ios, ngen, *tc, ps.get_subst(), ids);
        if (auto res = tac.execute(g, n, implementation_list())) {
            proof_state new_s(ps, append(res->m_goals, tail_gs), res->m_subst, res->m_ngen);
            return some_proof_state(new_s);
        } else {
            return none_proof_state();
        }
    };
    return tactic01(fn);
}

void initialize_inversion_tactic() {
    register_tac(name({"tactic", "inversion"}),
                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
                     name n = tactic_expr_to_id(app_arg(e), "invalid 'inversion/cases' tactic, argument must be an identifier");
                     return inversion_tactic(n, list<name>());
                 });
    register_tac(name({"tactic", "inversion_with"}),
                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
                     name n = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'cases-with' tactic, argument must be an identifier");
                     buffer<name> ids;
                     get_tactic_id_list_elements(app_arg(e), ids, "invalid 'cases-with' tactic, list of identifiers expected");
                     return inversion_tactic(n, to_list(ids.begin(), ids.end()));
                 });
}
void finalize_inversion_tactic() {}
}