From 740d42ea451cc2ee4c3676acbffd8e6fba44cf7d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 11 Mar 2017 12:16:15 -0800 Subject: [PATCH] fix(library/tactic): we should preserve names when using the revert/do_something/intro idiom --- src/library/equations_compiler/elim_match.cpp | 6 ++- src/library/tactic/cases_tactic.cpp | 5 +- src/library/tactic/induction_tactic.cpp | 14 +++--- src/library/tactic/intro_tactic.cpp | 43 +++++++++-------- src/library/tactic/intro_tactic.h | 11 +++-- src/library/tactic/subst_tactic.cpp | 6 ++- tests/lean/run/cases_renaming_issue.lean | 15 ++++++ tests/lean/whnf.lean.expected.out | 24 +++++----- tests/lean/whnf_cache_bug.lean.expected.out | 12 ++--- tests/lean/whnf_core1.lean.expected.out | 48 +++++++++---------- 10 files changed, 106 insertions(+), 78 deletions(-) create mode 100644 tests/lean/run/cases_renaming_issue.lean diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index a8a98817cd..50b5ddc59f 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -416,8 +416,9 @@ struct elim_match_fn { expr mvar = m_mctx.mk_metavar_decl(lctx, fn_type); unsigned arity = get_eqns_arity(lctx, e); buffer var_names; + bool use_unused_names = false; optional goal = intron(m_env, m_opts, m_mctx, mvar, - arity, var_names); + arity, var_names, use_unused_names); if (!goal) throw_ill_formed_eqns(); P.m_goal = *goal; local_context goal_lctx = get_local_context(*goal); @@ -1067,7 +1068,8 @@ struct elim_match_fn { /* Step 3 */ buffer new_H_names; - optional M_3 = intron(m_env, m_opts, m_mctx, M_2, to_revert.size(), new_H_names); + bool use_unused_names = false; + optional M_3 = intron(m_env, m_opts, m_mctx, M_2, to_revert.size(), new_H_names, use_unused_names); if (!M_3) { throw_error("equation compiler failed, when reintroducing reverted variables " "(use 'set_option trace.eqn_compiler.elim_match true' " diff --git a/src/library/tactic/cases_tactic.cpp b/src/library/tactic/cases_tactic.cpp index 716aebac3e..5a5055d5c4 100644 --- a/src/library/tactic/cases_tactic.cpp +++ b/src/library/tactic/cases_tactic.cpp @@ -229,7 +229,8 @@ struct cases_tactic_fn { /* assign mvar := aux_mvar indices h refls */ m_mctx.assign(mvar, mk_app(mk_app(mk_app(aux_mvar, m_nindices, I_args.end() - m_nindices), h), refls)); /* introduce indices j' and h' */ - auto r = intron(m_env, m_opts, m_mctx, aux_mvar, m_nindices + 1, new_indices_H); + bool use_unused_names = false; + auto r = intron(m_env, m_opts, m_mctx, aux_mvar, m_nindices + 1, new_indices_H, use_unused_names); lean_assert(r); num_eqs = eqs.size(); return *r; @@ -307,7 +308,7 @@ struct cases_tactic_fn { } } /* Introduce next equality */ - optional mvar1 = intron(m_env, m_opts, m_mctx, mvar, 1); + optional mvar1 = intron(m_env, m_opts, m_mctx, mvar, 1, false); if (!mvar1) throw_exception(mvar, "cases tactic failed, unexpected failure when introducing auxiliary equatilies"); metavar_decl g1 = m_mctx.get_metavar_decl(*mvar1); local_decl H_decl = g1.get_context().get_last_local_decl(); diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp index 3107790a15..230e28c47c 100644 --- a/src/library/tactic/induction_tactic.cpp +++ b/src/library/tactic/induction_tactic.cpp @@ -27,12 +27,12 @@ namespace lean { throw exception(sstream() << "induction tactic failed, recursor '" << rec_info.get_name() << "' is ill-formed"); } -static void set_intron(expr & R, type_context & ctx, expr const & M, unsigned n, list & ns, buffer & new_names) { +static void set_intron(expr & R, type_context & ctx, expr const & M, unsigned n, list & ns, buffer & new_names, bool use_unused_names) { if (n == 0) { R = M; } else { metavar_context mctx = ctx.mctx(); - if (auto M1 = intron(ctx.env(), ctx.get_options(), mctx, M, n, ns, new_names)) { + if (auto M1 = intron(ctx.env(), ctx.get_options(), mctx, M, n, ns, new_names, use_unused_names)) { R = *M1; ctx.set_mctx(mctx); } else { @@ -41,9 +41,9 @@ static void set_intron(expr & R, type_context & ctx, expr const & M, unsigned n, } } -static void set_intron(expr & R, type_context & ctx, expr const & M, unsigned n, buffer & new_names) { +static void set_intron(expr & R, type_context & ctx, expr const & M, unsigned n, buffer & new_names, bool use_unused_names) { list tmp; - set_intron(R, ctx, M, n, tmp, new_names); + set_intron(R, ctx, M, n, tmp, new_names, use_unused_names); } static void set_clear(expr & R, type_context & ctx, expr const & M, expr const & H) { @@ -153,7 +153,7 @@ list induction(environment const & env, options const & opts, transparency lean_assert(to_revert.size() >= indices.size() + 1); /* Re-introduce indices and major. */ buffer indices_H; - optional mvar2 = intron(env, opts, mctx, mvar1, indices.size() + 1, indices_H); + optional mvar2 = intron(env, opts, mctx, mvar1, indices.size() + 1, indices_H, false); if (!mvar2) throw exception("induction tactic failed, failed to reintroduce major premise"); hsubstitution base_subst; /* substitutions for all branches */ @@ -272,9 +272,9 @@ list induction(environment const & env, options const & opts, transparency expr aux_M; buffer param_names; buffer extra_names; /* Introduce constructor parameter for new goal associated with minor premise. */ - set_intron(aux_M, ctx2, new_M, nparams, ns, param_names); + set_intron(aux_M, ctx2, new_M, nparams, ns, param_names, true); /* Introduce hypothesis that had to be reverted because they depended on indices and/or major premise. */ - set_intron(aux_M, ctx2, aux_M, nextra, extra_names); + set_intron(aux_M, ctx2, aux_M, nextra, extra_names, false); local_context aux_M_lctx = ctx2.mctx().get_metavar_decl(aux_M).get_context(); if (ilist) { /* Save name of constructor parameters that have been introduced for new goal. */ diff --git a/src/library/tactic/intro_tactic.cpp b/src/library/tactic/intro_tactic.cpp index 99fc3eece1..88af41af65 100644 --- a/src/library/tactic/intro_tactic.cpp +++ b/src/library/tactic/intro_tactic.cpp @@ -14,18 +14,20 @@ Author: Leonardo de Moura #include "library/tactic/tactic_state.h" namespace lean { -static name mk_aux_name(local_context const & lctx, list & given_names, name const & default_name) { +static name mk_aux_name(local_context const & lctx, list & given_names, name const & default_name, + bool use_unused_names) { if (given_names) { name r = head(given_names); given_names = tail(given_names); return r == "_" ? lctx.get_unused_name(default_name) : r; } else { - return lctx.get_unused_name(default_name); + return use_unused_names ? lctx.get_unused_name(default_name) : default_name; } } optional intron(environment const & env, options const & opts, metavar_context & mctx, - expr const & mvar, unsigned n, list & given_names, buffer & new_Hns) { + expr const & mvar, unsigned n, list & given_names, buffer & new_Hns, + bool use_unused_names) { lean_assert(is_metavar(mvar)); optional g = mctx.find_metavar_decl(mvar); if (!g) return none_expr(); @@ -41,16 +43,18 @@ optional intron(environment const & env, options const & opts, metavar_con } lean_assert(is_pi(type) || is_let(type)); if (is_pi(type)) { - expr H = new_locals.push_local(mk_aux_name(ctx.lctx(), given_names, binding_name(type)), annotated_head_beta_reduce(binding_domain(type)), - binding_info(type)); - type = instantiate(binding_body(type), H); + name H_name = mk_aux_name(ctx.lctx(), given_names, binding_name(type), use_unused_names); + expr H = new_locals.push_local(H_name, annotated_head_beta_reduce(binding_domain(type)), + binding_info(type)); + type = instantiate(binding_body(type), H); new_Hs.push_back(H); new_Hns.push_back(mlocal_name(H)); } else { lean_assert(is_let(type)); - expr H = new_locals.push_let(mk_aux_name(ctx.lctx(), given_names, let_name(type)), annotated_head_beta_reduce(let_type(type)), let_value(type)); - type = instantiate(let_body(type), H); + name H_name = mk_aux_name(ctx.lctx(), given_names, let_name(type), use_unused_names); + expr H = new_locals.push_let(H_name, annotated_head_beta_reduce(let_type(type)), let_value(type)); + type = instantiate(let_body(type), H); new_Hs.push_back(H); new_Hns.push_back(mlocal_name(H)); } @@ -77,30 +81,30 @@ optional intron(environment const & env, options const & opts, metavar_con } optional intron(environment const & env, options const & opts, metavar_context & mctx, - expr const & mvar, unsigned n, list & given_names) { + expr const & mvar, unsigned n, list & given_names, bool use_unused_names) { buffer tmp; - return intron(env, opts, mctx, mvar, n, given_names, tmp); + return intron(env, opts, mctx, mvar, n, given_names, tmp, use_unused_names); } optional intron(environment const & env, options const & opts, metavar_context & mctx, - expr const & mvar, unsigned n) { + expr const & mvar, unsigned n, bool use_unused_names) { list empty; - return intron(env, opts, mctx, mvar, n, empty); + return intron(env, opts, mctx, mvar, n, empty, use_unused_names); } optional intron(environment const & env, options const & opts, metavar_context & mctx, - expr const & mvar, unsigned n, buffer & new_Hns) { + expr const & mvar, unsigned n, buffer & new_Hns, bool use_unused_names) { list empty; - return intron(env, opts, mctx, mvar, n, empty, new_Hns); + return intron(env, opts, mctx, mvar, n, empty, new_Hns, use_unused_names); } -optional intron(unsigned n, tactic_state const & s, buffer & new_Hns) { +optional intron(unsigned n, tactic_state const & s, buffer & new_Hns, bool use_unused_names) { if (n == 0) return some_tactic_state(s); optional mvar = s.get_main_goal(); if (!mvar) return none_tactic_state(); list new_names; metavar_context mctx = s.mctx(); - if (optional new_M = intron(s.env(), s.get_options(), mctx, *mvar, n, new_names, new_Hns)) { + if (optional new_M = intron(s.env(), s.get_options(), mctx, *mvar, n, new_names, new_Hns, use_unused_names)) { list new_gs(*new_M, tail(s.goals())); return some_tactic_state(set_mctx_goals(s, mctx, new_gs)); } else { @@ -108,16 +112,17 @@ optional intron(unsigned n, tactic_state const & s, buffer & } } -optional intron(unsigned n, tactic_state const & s) { +optional intron(unsigned n, tactic_state const & s, bool use_unused_names) { buffer tmp; - return intron(n, s, tmp); + return intron(n, s, tmp, use_unused_names); } vm_obj tactic_intron(vm_obj const & num, vm_obj const & s) { optional g = tactic::to_state(s).get_main_goal_decl(); if (!g) return mk_no_goals_exception(tactic::to_state(s)); buffer new_Hs; - if (auto new_s = intron(force_to_unsigned(num, 0), tactic::to_state(s), new_Hs)) + bool use_unused_names = true; + if (auto new_s = intron(force_to_unsigned(num, 0), tactic::to_state(s), new_Hs, use_unused_names)) return tactic::mk_success(*new_s); else return tactic::mk_exception("intron tactic failed, insufficient binders", tactic::to_state(s)); diff --git a/src/library/tactic/intro_tactic.h b/src/library/tactic/intro_tactic.h index b3f090c408..50a17ddd4f 100644 --- a/src/library/tactic/intro_tactic.h +++ b/src/library/tactic/intro_tactic.h @@ -18,13 +18,16 @@ optional intron(unsigned n, tactic_state const & s); \remark if new_hs_names doesn't have sufficient names, then the procedure will create unused local context names using the binder names. */ optional intron(environment const & env, options const & opts, metavar_context & mctx, - expr const & mvar, unsigned n, list & new_hs_names, buffer & new_Hns); + expr const & mvar, unsigned n, list & new_hs_names, buffer & new_Hns, + bool use_unused_names); optional intron(environment const & env, options const & opts, metavar_context & mctx, - expr const & mvar, unsigned n, list & new_hs_names); + expr const & mvar, unsigned n, list & new_hs_names, + bool use_unused_names); optional intron(environment const & env, options const & opts, metavar_context & mctx, - expr const & mvar, unsigned n, buffer & new_Hns); + expr const & mvar, unsigned n, buffer & new_Hns, + bool use_unused_names); optional intron(environment const & env, options const & opts, metavar_context & mctx, - expr const & mvar, unsigned n); + expr const & mvar, unsigned n, bool use_unused_names); vm_obj intro(name const & n, tactic_state const & s); diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/tactic/subst_tactic.cpp index d6560f8dd9..6623864d7b 100644 --- a/src/library/tactic/subst_tactic.cpp +++ b/src/library/tactic/subst_tactic.cpp @@ -53,7 +53,8 @@ expr subst(environment const & env, options const & opts, transparency_mode cons lean_subst_trace_state(mvar1, "after revert:\n"); lean_assert(to_revert.size() >= 2); buffer lhsH2; - optional mvar2 = intron(env, opts, mctx, mvar1, 2, lhsH2); + bool use_unused_names = false; + optional mvar2 = intron(env, opts, mctx, mvar1, 2, lhsH2, use_unused_names); if (!mvar2) throw exception("subst tactic failed, unexpected failure during intro"); lean_subst_trace_state(*mvar2, "after intro2:\n"); metavar_decl g2 = mctx.get_metavar_decl(*mvar2); @@ -85,7 +86,8 @@ expr subst(environment const & env, options const & opts, transparency_mode cons expr mvar4 = clear(mctx, mvar3, H2); expr mvar5 = clear(mctx, mvar4, lhs); buffer new_Hnames; - optional mvar6 = intron(env, opts, mctx, mvar5, to_revert.size() - 2, new_Hnames); + use_unused_names = false; + optional mvar6 = intron(env, opts, mctx, mvar5, to_revert.size() - 2, new_Hnames, use_unused_names); if (!mvar6) throw exception("subst tactic failed, unexpected failure when re-introducing dependencies"); lean_assert(new_Hnames.size() == to_revert.size() - 2); if (subst) { diff --git a/tests/lean/run/cases_renaming_issue.lean b/tests/lean/run/cases_renaming_issue.lean new file mode 100644 index 0000000000..f7fab241f4 --- /dev/null +++ b/tests/lean/run/cases_renaming_issue.lean @@ -0,0 +1,15 @@ +inductive fi : ℕ → Type +| zero : Π {n}, fi (n + 1) +| suc : Π {n}, fi n → fi (n + 1) +open fi + +namespace fi + +def lift {n k} : Π m, (fi n → fi k) → fi (n + m) → fi (k + m) := +begin + intros m f i, induction m with m ih_m, exact f i, + cases i with n n i, exact fi.zero, + exact fi.suc (ih_m i) +end + +end fi diff --git a/tests/lean/whnf.lean.expected.out b/tests/lean/whnf.lean.expected.out index fbe027a2f7..2250065628 100644 --- a/tests/lean/whnf.lean.expected.out +++ b/tests/lean/whnf.lean.expected.out @@ -1,24 +1,24 @@ succ ((⟨nat.rec - ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), + ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_2 : ℕ) (_F : nat.below (succ a_2)), succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F^.fst)^.fst a)) _F) - a a_1 + a _F) 0 punit.star, punit.star⟩ (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), + ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_2 : ℕ) (_F : nat.below (succ a_2)), succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F^.fst)^.fst a)) _F) - a a_1 + a _F) (succ a) ⟨ih_1, punit.star⟩, @@ -29,25 +29,25 @@ succ 3 succ ((⟨nat.rec - ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), + ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_2 : ℕ) (_F : nat.below (succ a_2)), succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F^.fst)^.fst a)) _F) - a a_1 + a _F) 0 punit.star, punit.star⟩ (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), + ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_2 : ℕ) (_F : nat.below (succ a_2)), succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (succ a_1)), succ ((_F^.fst)^.fst a)) _F) - a a_1 + a _F) (succ a) ⟨ih_1, punit.star⟩, diff --git a/tests/lean/whnf_cache_bug.lean.expected.out b/tests/lean/whnf_cache_bug.lean.expected.out index 98c16b6e4c..3476f290bf 100644 --- a/tests/lean/whnf_cache_bug.lean.expected.out +++ b/tests/lean/whnf_cache_bug.lean.expected.out @@ -1,25 +1,25 @@ ?m_1 nat.succ ((⟨nat.rec - ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), + ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) _F) - a a_1 + a _F) 0 punit.star, punit.star⟩ (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), + ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) _F) - a a_1 + a _F) (nat.succ a) ⟨ih_1, punit.star⟩, diff --git a/tests/lean/whnf_core1.lean.expected.out b/tests/lean/whnf_core1.lean.expected.out index 2ccf7fece4..0b1e48c7bb 100644 --- a/tests/lean/whnf_core1.lean.expected.out +++ b/tests/lean/whnf_core1.lean.expected.out @@ -1,48 +1,48 @@ nat.succ ((⟨nat.rec - ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), + ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) _F) - a a_1 + a _F) 0 punit.star, punit.star⟩ (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), + ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) _F) - a a_1 + a _F) (nat.succ a) ⟨ih_1, punit.star⟩, ⟨ih_1, punit.star⟩⟩) ((⟨nat.rec - ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), + ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) _F) - a a_1 + a _F) 0 punit.star, punit.star⟩ (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), + ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) _F) - a a_1 + a _F) (nat.succ a) ⟨ih_1, punit.star⟩, @@ -54,49 +54,49 @@ nat.succ a) nat.succ ((⟨nat.rec - ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), + ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) _F) - a a_1 + a _F) 0 punit.star, punit.star⟩ (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), + ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) _F) - a a_1 + a _F) (nat.succ a) ⟨ih_1, punit.star⟩, ⟨ih_1, punit.star⟩⟩) ((⟨nat.rec - ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), + ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) _F) - a a_1 + a _F) 0 punit.star, punit.star⟩ (λ (a : ℕ) (ih_1 : pprod ((λ (a : ℕ), ℕ → ℕ) a) (nat.below a)), - ⟨(λ (a_1 : ℕ) (_F : nat.below a_1) (a : ℕ), + ⟨(λ (a : ℕ) (_F : nat.below a) (a_1 : ℕ), (λ (a a_1 : ℕ) (_F : nat.below a_1), nat.cases_on a_1 (λ (_F : nat.below 0), a) - (λ (a_2 : ℕ) (_F : nat.below (nat.succ a_2)), nat.succ ((_F^.fst)^.fst a)) + (λ (a_1 : ℕ) (_F : nat.below (nat.succ a_1)), nat.succ ((_F^.fst)^.fst a)) _F) - a a_1 + a _F) (nat.succ a) ⟨ih_1, punit.star⟩,