max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/tactic): we should preserve names when using the revert/do_something/intro idiom

Browse source
This commit is contained in:
Leonardo de Moura 2017-03-11 12:16:15 -08:00
parent ab1a92ac3b
commit 740d42ea45
10 changed files with 106 additions and 78 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/equations_compiler/elim_match.cpp
View file

@ -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<name> var_names;
bool use_unused_names = false;
optional<expr> 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<name> new_H_names;
optional<expr> M_3 = intron(m_env, m_opts, m_mctx, M_2, to_revert.size(), new_H_names);
bool use_unused_names = false;
optional<expr> 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' "

5
src/library/tactic/cases_tactic.cpp
View file

@ -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<expr> mvar1 = intron(m_env, m_opts, m_mctx, mvar, 1);
optional<expr> 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();

14
src/library/tactic/induction_tactic.cpp
View file

@ -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<name> & ns, buffer<name> & new_names) {
static void set_intron(expr & R, type_context & ctx, expr const & M, unsigned n, list<name> & ns, buffer<name> & 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<name> & new_names) {
static void set_intron(expr & R, type_context & ctx, expr const & M, unsigned n, buffer<name> & new_names, bool use_unused_names) {
list<name> 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<expr> induction(environment const & env, options const & opts, transparency
lean_assert(to_revert.size() >= indices.size() + 1);
/* Re-introduce indices and major. */
buffer<name> indices_H;
optional<expr> mvar2 = intron(env, opts, mctx, mvar1, indices.size() + 1, indices_H);
optional<expr> 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<expr> induction(environment const & env, options const & opts, transparency
expr aux_M;
buffer<name> param_names; buffer<name> 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. */

43
src/library/tactic/intro_tactic.cpp
View file

@ -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<name> & given_names, name const & default_name) {
static name mk_aux_name(local_context const & lctx, list<name> & 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<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
expr const & mvar, unsigned n, list<name> & given_names, buffer<name> & new_Hns) {
expr const & mvar, unsigned n, list<name> & given_names, buffer<name> & new_Hns,
bool use_unused_names) {
lean_assert(is_metavar(mvar));
optional<metavar_decl> g = mctx.find_metavar_decl(mvar);
if (!g) return none_expr();
@ -41,16 +43,18 @@ optional<expr> 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<expr> intron(environment const & env, options const & opts, metavar_con
}
optional<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
expr const & mvar, unsigned n, list<name> & given_names) {
expr const & mvar, unsigned n, list<name> & given_names, bool use_unused_names) {
buffer<name> 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<expr> 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<name> empty;
return intron(env, opts, mctx, mvar, n, empty);
return intron(env, opts, mctx, mvar, n, empty, use_unused_names);
}
optional<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
expr const & mvar, unsigned n, buffer<name> & new_Hns) {
expr const & mvar, unsigned n, buffer<name> & new_Hns, bool use_unused_names) {
list<name> 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<tactic_state> intron(unsigned n, tactic_state const & s, buffer<name> & new_Hns) {
optional<tactic_state> intron(unsigned n, tactic_state const & s, buffer<name> & new_Hns, bool use_unused_names) {
if (n == 0) return some_tactic_state(s);
optional<expr> mvar = s.get_main_goal();
if (!mvar) return none_tactic_state();
list<name> new_names;
metavar_context mctx = s.mctx();
if (optional<expr> new_M = intron(s.env(), s.get_options(), mctx, *mvar, n, new_names, new_Hns)) {
if (optional<expr> new_M = intron(s.env(), s.get_options(), mctx, *mvar, n, new_names, new_Hns, use_unused_names)) {
list<expr> new_gs(*new_M, tail(s.goals()));
return some_tactic_state(set_mctx_goals(s, mctx, new_gs));
} else {
@ -108,16 +112,17 @@ optional<tactic_state> intron(unsigned n, tactic_state const & s, buffer<name> &
}
}
optional<tactic_state> intron(unsigned n, tactic_state const & s) {
optional<tactic_state> intron(unsigned n, tactic_state const & s, bool use_unused_names) {
buffer<name> 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<metavar_decl> g = tactic::to_state(s).get_main_goal_decl();
if (!g) return mk_no_goals_exception(tactic::to_state(s));
buffer<name> 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));

11
src/library/tactic/intro_tactic.h
View file

@ -18,13 +18,16 @@ optional<tactic_state> 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<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
expr const & mvar, unsigned n, list<name> & new_hs_names, buffer<name> & new_Hns);
expr const & mvar, unsigned n, list<name> & new_hs_names, buffer<name> & new_Hns,
bool use_unused_names);
optional<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
expr const & mvar, unsigned n, list<name> & new_hs_names);
expr const & mvar, unsigned n, list<name> & new_hs_names,
bool use_unused_names);
optional<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
expr const & mvar, unsigned n, buffer<name> & new_Hns);
expr const & mvar, unsigned n, buffer<name> & new_Hns,
bool use_unused_names);
optional<expr> 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);

6
src/library/tactic/subst_tactic.cpp
View file

@ -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<name> lhsH2;
optional<expr> mvar2 = intron(env, opts, mctx, mvar1, 2, lhsH2);
bool use_unused_names = false;
optional<expr> 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<name> new_Hnames;
optional<expr> mvar6 = intron(env, opts, mctx, mvar5, to_revert.size() - 2, new_Hnames);
use_unused_names = false;
optional<expr> 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) {

15
tests/lean/run/cases_renaming_issue.lean Normal file
View file

@ -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

24
tests/lean/whnf.lean.expected.out
View file

@ -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⟩,

12
tests/lean/whnf_cache_bug.lean.expected.out
View file

@ -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⟩,

48
tests/lean/whnf_core1.lean.expected.out
View file

@ -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⟩,