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

feat(frontends/lean): add 'show' expression syntax sugar

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-06 07:50:22 -08:00
parent 90f5a4f813
commit ba9a8f9d98
24 changed files with 70 additions and 68 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
doc/lean/tutorial.md
View file

@ -675,10 +675,10 @@ as syntax sugar for `fun x : A, H`. This may been silly, but it allows us to sim
theorem subset_trans {A : Type} {s1 s2 s3 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3) : s1 ⊆ s3
:= take x : A,
assume Hin : x ∈ s1,
have x ∈ s3 :
show x ∈ s3, from
let L1 : x ∈ s2 := H1 x Hin
in H2 x L1
```
Finally, the construct `have A : H` means "have" a proof for `A` using `H`. It is just syntax sugar for
`let L : A := H in L`. It is useful to document intermediate steps in manually constructed proofs.
Finally, the construct `show A, from H` means "have" a proof for `A` using `H`. It is just syntax sugar for
`let H_show : A := H in H_show`. It is useful to document intermediate steps in manually constructed proofs.

10
examples/lean/set.lean
View file

@ -11,7 +11,7 @@ infix 50 ⊆ : subset
theorem subset_trans {A : Type} {s1 s2 s3 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3) : s1 ⊆ s3
:= take x : A,
assume Hin : x ∈ s1,
have x ∈ s3 :
show x ∈ s3, from
let L1 : x ∈ s2 := H1 x Hin
in H2 x L1
@ -19,7 +19,7 @@ theorem subset_ext {A : Type} {s1 s2 : Set A} (H : ∀ x, x ∈ s1 = x ∈ s2) :
:= funext H
theorem subset_antisym {A : Type} {s1 s2 : Set A} (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s1) : s1 = s2
:= subset_ext (have (∀ x, x ∈ s1 = x ∈ s2) :
take x, have x ∈ s1 = x ∈ s2 :
boolext (have x ∈ s1 → x ∈ s2 : H1 x)
(have x ∈ s2 → x ∈ s1 : H2 x))
:= subset_ext (show (∀ x, x ∈ s1 = x ∈ s2), from
take x, show x ∈ s1 = x ∈ s2, from
boolext (show x ∈ s1 → x ∈ s2, from H1 x)
(show x ∈ s2 → x ∈ s1, from H2 x))

6
examples/lean/tactic1.lean
View file

@ -14,13 +14,13 @@ conj = conj_tac()
-- The "hint" is a tactic that should be used to fill the "hole".
-- In the following example, we use the tactic "auto" defined by the Lua code above.
--
-- The (have [expr] by [tactic]) expression is also creating a "hole" and associating a "hint" to it.
-- The (show [expr], by [tactic]) expression is also creating a "hole" and associating a "hint" to it.
-- The expression [expr] after the shows is fixing the type of the "hole"
theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := (by auto),
lemma2 : B := (by auto)
in (have B /\ A by auto)
in (show B /\ A, by auto)
print environment 1. -- print proof for the previous theorem
@ -52,6 +52,6 @@ theorem T4 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := _, -- first hole
lemma2 : B := _ -- second hole
in (have B /\ A by auto).
in (show B /\ A, by auto).
auto. done. -- tactic command sequence for the first hole
auto. done. -- tactic command sequence for the second hole

4
examples/lean/tc.lean
View file

@ -24,7 +24,7 @@ theorem tcls_refl {A : TypeU} (R : A → A → Bool) : ∀ a, R⁺ a a
theorem tcls_sub {A : TypeU} (R : A → A → Bool) : R ⊆ R⁺
:= take a b,
assume Hab : R a b,
have R⁺ a b :
show R⁺ a b, from
take P, assume Hrefl Htrans Hsub,
Hsub a b Hab
@ -35,4 +35,4 @@ theorem tcls_step {A : TypeU} {R : A → A → Bool} {a b c : A} (H1 : R a b) (H
theorem tcls_smallest {A : TypeU} (R : A → A → Bool) : ∀ P, (reflexive P) → (transitive P) → (R ⊆ P) → (R⁺ ⊆ P)
:= take P, assume Hrefl Htrans Hsub,
take a b, assume H : R⁺ a b,
have P a b : H P Hrefl Htrans Hsub
show P a b, from H P Hrefl Htrans Hsub

21
src/builtin/Nat.lean
View file

@ -60,7 +60,7 @@ theorem discriminate {B : Bool} {a : Nat} (H1: a = 0 → B) (H2 : ∀ n, a = n +
theorem add_zerol (a : Nat) : 0 + a = a
:= induction_on a
(have 0 + 0 = 0 : add_zeror 0)
(show 0 + 0 = 0, from add_zeror 0)
(λ (n : Nat) (iH : 0 + n = n),
calc 0 + (n + 1) = (0 + n) + 1 : add_succr 0 n
... = n + 1 : { iH })
@ -72,7 +72,7 @@ theorem add_succl (a b : Nat) : (a + 1) + b = (a + b) + 1
(λ (n : Nat) (iH : (a + 1) + n = (a + n) + 1),
calc (a + 1) + (n + 1) = ((a + 1) + n) + 1 : add_succr (a + 1) n
... = ((a + n) + 1) + 1 : { iH }
... = (a + (n + 1)) + 1 : { have (a + n) + 1 = a + (n + 1) : symm (add_succr a n) })
... = (a + (n + 1)) + 1 : { show (a + n) + 1 = a + (n + 1), from symm (add_succr a n) })
theorem add_comm (a b : Nat) : a + b = b + a
:= induction_on b
@ -91,11 +91,11 @@ theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c)
calc (n + 1) + (b + c) = (n + (b + c)) + 1 : add_succl n (b + c)
... = ((n + b) + c) + 1 : { iH }
... = ((n + b) + 1) + c : symm (add_succl (n + b) c)
... = ((n + 1) + b) + c : { have (n + b) + 1 = (n + 1) + b : symm (add_succl n b) }))
... = ((n + 1) + b) + c : { show (n + b) + 1 = (n + 1) + b, from symm (add_succl n b) }))
theorem mul_zerol (a : Nat) : 0 * a = 0
:= induction_on a
(have 0 * 0 = 0 : mul_zeror 0)
(show 0 * 0 = 0, from mul_zeror 0)
(λ (n : Nat) (iH : 0 * n = 0),
calc 0 * (n + 1) = (0 * n) + 0 : mul_succr 0 n
... = 0 + 0 : { iH }
@ -110,7 +110,8 @@ theorem mul_succl (a b : Nat) : (a + 1) * b = a * b + b
calc (a + 1) * (n + 1) = (a + 1) * n + (a + 1) : mul_succr (a + 1) n
... = a * n + n + (a + 1) : { iH }
... = a * n + n + a + 1 : symm (add_assoc (a * n + n) a 1)
... = a * n + (n + a) + 1 : { have a * n + n + a = a * n + (n + a) : add_assoc (a * n) n a }
... = a * n + (n + a) + 1 : { show a * n + n + a = a * n + (n + a),
from add_assoc (a * n) n a }
... = a * n + (a + n) + 1 : { add_comm n a }
... = a * n + a + n + 1 : { symm (add_assoc (a * n) a n) }
... = a * (n + 1) + n + 1 : { symm (mul_succr a n) }
@ -118,14 +119,14 @@ theorem mul_succl (a b : Nat) : (a + 1) * b = a * b + b
theorem mul_onel (a : Nat) : 1 * a = a
:= induction_on a
(have 1 * 0 = 0 : mul_zeror 1)
(show 1 * 0 = 0, from mul_zeror 1)
(λ (n : Nat) (iH : 1 * n = n),
calc 1 * (n + 1) = 1 * n + 1 : mul_succr 1 n
... = n + 1 : { iH })
theorem mul_oner (a : Nat) : a * 1 = a
:= induction_on a
(have 0 * 1 = 0 : mul_zeror 1)
(show 0 * 1 = 0, from mul_zeror 1)
(λ (n : Nat) (iH : n * 1 = n),
calc (n + 1) * 1 = n * 1 + 1 : mul_succl n 1
... = n + 1 : { iH })
@ -214,7 +215,7 @@ theorem add_eqz {a b : Nat} (H : a + b = 0) : a = 0
... ≠ 0 : succ_nz (n + b)))
theorem le_intro {a b c : Nat} (H : a + c = b) : a ≤ b
:= (symm (le_def a b)) ◂ (have (∃ x, a + x = b) : exists_intro c H)
:= (symm (le_def a b)) ◂ (show (∃ x, a + x = b), from exists_intro c H)
theorem le_elim {a b : Nat} (H : a ≤ b) : ∃ x, a + x = b
:= (le_def a b) ◂ H
@ -332,12 +333,12 @@ theorem strong_induction {P : Nat → Bool} (H : ∀ n, (∀ m, m < n → P m)
let stronger : P a ∧ ∀ m, m < a → P m :=
-- we prove a stronger result by regular induction on a
induction_on a
(have P 0 ∧ ∀ m, m < 0 → P m :
(show P 0 ∧ ∀ m, m < 0 → P m, from
let c2 : ∀ m, m < 0 → P m := λ (m : Nat) (Hlt : m < 0), absurd_elim (P m) Hlt (not_lt_0 m),
c1 : P 0 := H 0 c2
in and_intro c1 c2)
(λ (n : Nat) (iH : P n ∧ ∀ m, m < n → P m),
have P (n + 1) ∧ ∀ m, m < n + 1 → P m :
show P (n + 1) ∧ ∀ m, m < n + 1 → P m, from
let iH1 : P n := and_eliml iH,
iH2 : ∀ m, m < n → P m := and_elimr iH,
c2 : ∀ m, m < n + 1 → P m := λ (m : Nat) (Hlt : m < n + 1),

9
src/builtin/kernel.lean
View file

@ -244,9 +244,9 @@ theorem not_not_elim {a : Bool} (H : ¬ ¬ a) : a
theorem not_imp_eliml {a b : Bool} (Hnab : ¬ (a → b)) : a
:= not_not_elim
(have ¬ ¬ a :
assume Hna : ¬ a, absurd (assume Ha : a, absurd_elim b Ha Hna)
Hnab)
(show ¬ ¬ a,
from assume Hna : ¬ a, absurd (assume Ha : a, absurd_elim b Ha Hna)
Hnab)
theorem not_imp_elimr {a b : Bool} (H : ¬ (a → b)) : ¬ b
:= assume Hb : b, absurd (assume Ha : a, Hb)
@ -265,7 +265,7 @@ theorem and_elimr {a b : Bool} (H : a ∧ b) : b
theorem or_elim {a b c : Bool} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
:= not_not_elim
(assume H : ¬ c,
absurd (have c : H3 (have b : resolve1 H1 (have ¬ a : (mt (assume Ha : a, H2 Ha) H))))
absurd (H3 (resolve1 H1 (mt (assume Ha : a, H2 Ha) H)))
H)
theorem refute {a : Bool} (H : ¬ a → false) : a
@ -966,4 +966,3 @@ theorem hproof_irrel {a b : Bool} (H1 : a) (H2 : b) : H1 == H2
H1_eq_H1b : H1 == H1b := hsymm (cast_heq (by simp) H1),
H1b_eq_H2 : H1b == H2 := to_heq (proof_irrel H1b H2)
in htrans H1_eq_H1b H1b_eq_H2

4
src/builtin/macros.lua
View file

@ -76,13 +76,13 @@ end
-- Axiom Ax2: forall x y, not P x y
-- Now, the following macro expression
-- obtain (a b : Nat) (H : P a b) from Ax1,
-- have false : absurd H (instantiate Ax2 a b)
-- show false, from absurd H (instantiate Ax2 a b)
-- expands to
-- exists::elim Ax1
-- (fun (a : Nat) (Haux : ...),
-- exists::elim Haux
-- (fun (b : Na) (H : P a b),
-- have false : absurd H (instantiate Ax2 a b)
-- show false, from absurd H (instantiate Ax2 a b)
macro("obtain", { macro_arg.Parameters, macro_arg.Comma, macro_arg.Id, macro_arg.Expr, macro_arg.Comma, macro_arg.Expr },
function (env, bindings, fromid, exPr, body)
local n = #bindings

BIN
src/builtin/obj/Nat.olean
View file

Binary file not shown.

BIN
src/builtin/obj/kernel.olean
View file

Binary file not shown.

2
src/emacs/lean-mode.el
View file

@ -26,7 +26,7 @@
'("--") ;; comments start with
'("import" "definition" "variable" "variables" "print" "theorem" "axiom" "universe" "alias" "help" "environment" "options" "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end" "using" "namespace" "builtin" "scope" "pop_scope" "set_opaque" "set_option" "rewrite_set" "add_rewrite" "enable_rewrite" "disable_rewrite") ;; some keywords
'(("\\_<\\(Bool\\|Int\\|Nat\\|Real\\|Type\\|TypeU\\|ℕ\\|ℤ\\)\\_>" . 'font-lock-type-face)
("\\_<\\(calc\\|have\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face)
("\\_<\\(calc\\|have\\|show\\|by\\|in\\|let\\|forall\\|fun\\|exists\\|if\\|then\\|else\\|assume\\|take\\|obtain\\|from\\)\\_>" . font-lock-keyword-face)
("\"[^\"]*\"" . 'font-lock-string-face)
("\\(->\\|↔\\|/\\\\\\|==\\|\\\\/\\|[*+/<=>¬∧∨≠≤≥-]\\)" . 'font-lock-constant-face)
("\\(λ\\|→\\|∃\\|∀\\|:\\|:=\\)" . font-lock-constant-face)

22
src/frontends/lean/parser_expr.cpp
View file

@ -978,23 +978,27 @@ tactic parser_imp::parse_tactic_expr() {
}
}
static name g_have_expr("have_expr");
static name g_H_show("H_show");
static name g_from("from");
/** \brief Parse <tt>'have' expr 'by' tactic</tt> and <tt>'have' expr ':' expr</tt> */
expr parser_imp::parse_have_expr() {
/** \brief Parse <tt>'show' expr, 'from' expr</tt> and <tt>'show' expr, 'by' expr</tt>*/
expr parser_imp::parse_show_expr() {
auto p = pos();
next();
expr t = parse_expr();
if (curr_is_colon()) {
check_comma_next("invalid 'show' expression, ',' expected");
if (curr() == scanner::token::By) {
next();
expr b = parse_expr();
return mk_let(g_have_expr, t, b, Var(0));
} else {
check_next(scanner::token::By, "invalid 'have' expression, 'by' or ':' expected");
tactic tac = parse_tactic_expr();
expr r = mk_placeholder(some_expr(t));
m_tactic_hints.insert(mk_pair(r, tac));
return save(r, p);
} else if (curr_is_identifier() && curr_name() == g_from) {
next();
expr b = parse_expr();
return mk_let(g_H_show, t, b, Var(0));
} else {
throw parser_error("invalid 'show' expected, 'from' or 'by' expected", p);
}
}
@ -1025,7 +1029,7 @@ expr parser_imp::parse_nud() {
case scanner::token::StringVal: return parse_string();
case scanner::token::Placeholder: return parse_placeholder();
case scanner::token::Type: return parse_type(false);
case scanner::token::Have: return parse_have_expr();
case scanner::token::Show: return parse_show_expr();
case scanner::token::Tuple: return parse_tuple();
case scanner::token::Proj1: return parse_proj(true);
case scanner::token::Proj2: return parse_proj(false);

2
src/frontends/lean/parser_imp.h
View file

@ -319,7 +319,7 @@ private:
expr parse_tuple();
expr parse_proj(bool first);
tactic parse_tactic_macro(name tac_id, pos_info const & p);
expr parse_have_expr();
expr parse_show_expr();
expr parse_calc();
expr parse_nud_id();
expr parse_nud();

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

@ -26,8 +26,9 @@ static name g_exists_name("exists");
static name g_Exists_name("Exists");
static name g_exists_unicode("\u2203");
static name g_placeholder_name("_");
static name g_have_name("have");
static name g_using_name("using");
static name g_have_name("have");
static name g_show_name("show");
static name g_by_name("by");
static name g_sig_name("sig");
static name g_tuple_name("tuple");
@ -223,6 +224,8 @@ scanner::token scanner::read_a_symbol() {
return token::Placeholder;
} else if (m_name_val == g_have_name) {
return token::Have;
} else if (m_name_val == g_show_name) {
return token::Show;
} else if (m_name_val == g_by_name) {
return token::By;
} else if (m_name_val == g_Exists_name) {
@ -468,8 +471,9 @@ std::ostream & operator<<(std::ostream & out, scanner::token const & t) {
case scanner::token::Tuple: out << "tuple"; break;
case scanner::token::Placeholder: out << "_"; break;
case scanner::token::ScriptBlock: out << "Script"; break;
case scanner::token::Have: out << "have"; break;
case scanner::token::CartesianProduct: out << "#"; break;
case scanner::token::Have: out << "have"; break;
case scanner::token::Show: out << "show"; break;
case scanner::token::By: out << "by"; break;
case scanner::token::Ellipsis: out << "..."; break;
case scanner::token::Eof: out << "EOF"; break;

2
src/frontends/lean/scanner.h
View file

@ -21,7 +21,7 @@ public:
enum class token {
LeftParen, RightParen, LeftCurlyBracket, RightCurlyBracket, Colon, Comma, Period, Lambda, Pi, Arrow,
Sig, Tuple, Proj1, Proj2, Let, In, Exists, Id, CommandId, IntVal, DecimalVal, StringVal, Assign, Type, Placeholder,
Have, By, ScriptBlock, Ellipsis, CartesianProduct, Eof
Have, Show, By, ScriptBlock, Ellipsis, CartesianProduct, Eof
};
protected:
int m_spos; // position in the current line of the stream

4
tests/lean/add_assoc.lean
View file

@ -6,9 +6,9 @@ add_rewrite add_zerol add_succl eq_id : basic
theorem add_assoc (a b c : Nat) : a + (b + c) = (a + b) + c
:= induction_on a
(have 0 + (b + c) = (0 + b) + c : by simp basic)
(show 0 + (b + c) = (0 + b) + c, by simp basic)
(λ (n : Nat) (iH : n + (b + c) = (n + b) + c),
have (n + 1) + (b + c) = ((n + 1) + b) + c : by simp basic)
show (n + 1) + (b + c) = ((n + 1) + b) + c, by simp basic)
check add_zerol
check add_succl

16
tests/lean/add_assoc.lean.expected.out
View file

@ -9,15 +9,9 @@ Nat::add_succl : ∀ a b : ℕ, a + 1 + b = a + b + 1
theorem add_assoc (a b c : ℕ) : a + (b + c) = a + b + c :=
Nat::induction_on
a
(let have_expr : 0 + (b + c) = 0 + b + c :=
eqt_elim (trans (congr (congr2 eq (Nat::add_zerol (b + c)))
(congr1 c (congr2 Nat::add (Nat::add_zerol b))))
(eq_id (b + c)))
in have_expr)
(eqt_elim (trans (congr (congr2 eq (Nat::add_zerol (b + c))) (congr1 c (congr2 Nat::add (Nat::add_zerol b))))
(eq_id (b + c))))
(λ (n : ℕ) (iH : n + (b + c) = n + b + c),
let have_expr : n + 1 + (b + c) = n + 1 + b + c :=
eqt_elim (trans (congr (congr2 eq (trans (Nat::add_succl n (b + c)) (congr1 1 (congr2 Nat::add iH))))
(trans (congr1 c (congr2 Nat::add (Nat::add_succl n b)))
(Nat::add_succl (n + b) c)))
(eq_id (n + b + c + 1)))
in have_expr)
eqt_elim (trans (congr (congr2 eq (trans (Nat::add_succl n (b + c)) (congr1 1 (congr2 Nat::add iH))))
(trans (congr1 c (congr2 Nat::add (Nat::add_succl n b))) (Nat::add_succl (n + b) c)))
(eq_id (n + b + c + 1))))

4
tests/lean/interactive/t12.lean
View file

@ -8,7 +8,7 @@ theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := (by auto),
lemma2 : B := (by auto)
in (have B /\ A by auto)
in (show B /\ A, by auto)
print environment 1. -- print proof for the previous theorem
@ -34,6 +34,6 @@ theorem T4 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 : A := _,
lemma2 : B := _
in (have B /\ A by auto).
in (show B /\ A, by auto).
conj_hyp. exact. done.
conj_hyp. exact. done.

6
tests/lean/interactive/t13.lean
View file

@ -5,8 +5,8 @@ auto = Repeat(OrElse(assumption_tac(), conj_tac(), conj_hyp_tac()))
theorem T1 (A B : Bool) : A /\ B -> B /\ A :=
fun assumption : A /\ B,
let lemma1 := (have A by auto),
lemma2 := (have B by auto)
in (have B /\ A by auto)
let lemma1 := (show A, by auto),
lemma2 := (show B, by auto)
in (show B /\ A, by auto)
print environment 1.

2
tests/lean/j1.lean
View file

@ -10,7 +10,7 @@ add_rewrite imp_truel imp_truer imp_id eq_id : basic
theorem bracket_eq (x : Bool) : bracket x = x
:= boolext
(assume H : ∀ p : Bool, (x → p) → p,
(have ((x → x) → x) = x : by simp basic) ◂ H x)
(show ((x → x) → x) = x, by simp basic) ◂ H x)
(assume H : x,
take p,
assume Hxp : x → p,

2
tests/lean/scope_bug1.lean
View file

@ -10,7 +10,7 @@ scope
theorem mul_zerol2 (a : Nat) : 0 * a = 0
:= induction_on a
(have 0 * 0 = 0 : mul_zeror 0)
(show 0 * 0 = 0, from mul_zeror 0)
(λ (n : Nat) (iH : 0 * n = 0),
calc 0 * (n + 1) = (0 * n) + 0 : mul_succr 0 n
... = 0 + 0 : { iH }

2
tests/lean/sig5.lean
View file

@ -3,7 +3,7 @@ definition vec_with_len := sig len, vec len
variable n : Nat
variable v : vec n
check tuple n, v
check (have vec_with_len : tuple n, v)
check (show vec_with_len, from tuple n, v)
check (let v2 : vec_with_len := tuple n, v
in v2)
check (tuple vec_with_len : n, v)

2
tests/lean/sig5.lean.expected.out
View file

@ -5,6 +5,6 @@
Assumed: n
Assumed: v
tuple n, v : ℕ ⨯ vec n
let have_expr : vec_with_len := tuple (sig x : ℕ, vec x) : n, v in have_expr : vec_with_len
let H_show : vec_with_len := tuple (sig x : ℕ, vec x) : n, v in H_show : vec_with_len
let v2 : vec_with_len := tuple (sig x : ℕ, vec x) : n, v in v2 : vec_with_len
tuple vec_with_len : n, v : sig len : ℕ, vec len

2
tests/lean/tactic14.lean
View file

@ -10,6 +10,6 @@ exit -- temporarily disable the following test
theorem T1 (a b : Int) (f : Int -> Int) : a = b -> (f (f a)) = (f (f b)) :=
fun assumption : a = b,
have (f (f a)) = (f (f b)) by congr_tac
show (f (f a)) = (f (f b)), by congr_tac
print environment 1.

2
tests/lean/using_bug1.lean
View file

@ -8,7 +8,7 @@ check add_succr a
theorem mul_zerol2 (a : Nat) : 0 * a = 0
:= induction_on a
(have 0 * 0 = 0 : mul_zeror 0)
(show 0 * 0 = 0, from mul_zeror 0)
(λ (n : Nat) (iH : 0 * n = 0),
calc 0 * (n + 1) = (0 * n) + 0 : mul_succr 0 n
... = 0 + 0 : { iH }