Specify a termination argument for recursive functions.
```
termination_by a - b
```
indicates that termination of the currently defined recursive function follows
because the difference between the arguments `a` and `b` decreases.
If the function takes further argument after the colon, you can name them as follows:
```
def example (a : Nat) : Nat → Nat → Nat :=
termination_by b c => a - b
```
By default, a `termination_by` clause will cause the function to be constructed using well-founded
recursion. The syntax `termination_by structural a` (or `termination_by structural _ c => c`)
indicates the function is expected to be structural recursive on the argument. In this case
the body of the `termination_by` clause must be one of the function's parameters.
If omitted, a termination argument will be inferred. If written as `termination_by?`,
the inferrred termination argument will be suggested.
terminationBy::= ...
|Specify a termination argument for recursive functions.
```
termination_by a - b
```
indicates that termination of the currently defined recursive function follows
because the difference between the arguments `a` and `b` decreases.
If the function takes further argument after the colon, you can name them as follows:
```
def example (a : Nat) : Nat → Nat → Nat :=
termination_by b c => a - b
```
By default, a `termination_by` clause will cause the function to be constructed using well-founded
recursion. The syntax `termination_by structural a` (or `termination_by structural _ c => c`)
indicates the function is expected to be structural recursive on the argument. In this case
the body of the `termination_by` clause must be one of the function's parameters.
If omitted, a termination argument will be inferred. If written as `termination_by?`,
the inferrred termination argument will be suggested.
termination_by(ident*=>)?term
この証明義務のコンテキストは、再帰呼び出しのローカルコンテキストです。具体的には、ローカルの仮定（if h : _・match h : _ with ・have などで導入されるものなど）が利用できます。関数のパラメータが（例えば Lean.Parser.Term.match : termPattern matching. `match e, ... with | p, ... => f | ...` matches each given
term `e` against each pattern `p` of a match alternative. When all patterns
of an alternative match, the `match` term evaluates to the value of the
corresponding right-hand side `f` with the pattern variables bound to the
respective matched values.
If used as `match h : e, ... with | p, ... => f | ...`, `h : e = p` is available
within `f`.
When not constructing a proof, `match` does not automatically substitute variables
matched on in dependent variables' types. Use `match (generalizing := true) ...` to
enforce this.
Syntax quotations can also be used in a pattern match.
This matches a `Syntax` value against quotations, pattern variables, or `_`.
Quoted identifiers only match identical identifiers - custom matching such as by the preresolved
names only should be done explicitly.
`Syntax.atom`s are ignored during matching by default except when part of a built-in literal.
For users introducing new atoms, we recommend wrapping them in dedicated syntax kinds if they
should participate in matching.
For example, in
```lean
syntax "c" ("foo" <|> "bar") ...
```
`foo` and `bar` are indistinguishable during matching, but in
```lean
syntax foo := "foo"
syntax "c" (foo <|> "bar") ...
```
they are not.
match 式による）パターンマッチの 判別子 である場合、このパラメータは証明義務の中でマッチしたパターンに絞り込まれます。
deffib(n:Nat):=ifh:n≤1then1elsefib(n-1)+fib(n-2)termination_bynunsolved goals
n : Nat
h : ¬n ≤ 1
⊢ n - 1 < n
n : Nat
h : ¬n ≤ 1
⊢ n - 2 < ndecreasing_byn:Nath:¬n ≤ 1⊢ n - 1 < nn:Nath:¬n ≤ 1⊢ n - 2 < n
deffib:Nat→Nat|0|1=>1|.succ(.succn)=>fib(n+1)+fibntermination_byn=>nunsolved goals
n : Nat
⊢ n + 1 < n.succ.succ
n : Nat
⊢ n < n.succ.succdecreasing_byn:Nat⊢ n + 1 < n.succ.succn:Nat⊢ n < n.succ.succ
ここで、 termIfThenElse : term`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
if は条件についてのローカルの仮定をスコープに入れません。とはいえ、停止証明のコンテキストでは利用可能です。
deffib(n:Nat):=ifn≤1then1elsefib(n-1)+fib(n-2)termination_bynunsolved goals
n : Nat
h✝ : ¬n ≤ 1
⊢ n - 1 < n
n : Nat
h✝ : ¬n ≤ 1
⊢ n - 2 < ndecreasing_byn:Nath✝:¬n ≤ 1⊢ n - 1 < nn:Nath✝:¬n ≤ 1⊢ n - 2 < n
defTree.depth(t:Tree):Nat:=letdepths:=t.children.map(func=>failed to prove termination, possible solutions:
- Use `have`-expressions to prove the remaining goals
- Use `termination_by` to specify a different well-founded relation
- Use `decreasing_by` to specify your own tactic for discharging this kind of goal
t c : Tree
⊢ sizeOf c < sizeOf tTree.depthc)matchdepths.max?with|somed=>d+1|none=>0termination_byt
failed to prove termination, possible solutions:
- Use `have`-expressions to prove the remaining goals
- Use `termination_by` to specify a different well-founded relation
- Use `decreasing_by` to specify your own tactic for discharging this kind of goal
t c : Tree
⊢ sizeOf c < sizeOf t
ローカル変数 c とパラメータ t の間に関連がないため、この停止の証明義務は証明できません。ただし、 List.map は与えられたリストの要素にのみ関数の引数を適用します；そのため c は常に t.children の要素です。
Extensible helper tactic for decreasing_tactic. This handles the "base case"
reasoning after applying lexicographic order lemmas.
It can be extended by adding more macro definitions, e.g.
String.Iterator.sizeOf_next_lt_of_hasNext と String.Iterator.sizeOf_next_lt_of_atEnd 、これは Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `ToStream` typeclass.
for を用いた文字列に対する繰り返しを扱います
defsynack:Nat→Nat→Nat|0,n=>n+1|m+1,0=>synackm1|m+1,n+1=>synackm(failed to prove termination, possible solutions:
- Use `have`-expressions to prove the remaining goals
- Use `termination_by` to specify a different well-founded relation
- Use `decreasing_by` to specify your own tactic for discharging this kind of goal
case h
m n : Nat
⊢ m / 2 + 1 < m + 1synack(m/2+1)n)termination_bymn=>(m,n)
failed to prove termination, possible solutions:
- Use `have`-expressions to prove the remaining goals
- Use `termination_by` to specify a different well-founded relation
- Use `decreasing_by` to specify your own tactic for discharging this kind of goal
case h
m n : Nat
⊢ m / 2 + 1 < m + 1
測度についてすべてのタプルを試行することによる組み合わせ爆発を避けるために、Lean はまず 基本停止測度 を集計し、基本測度が減少的・狭義に減少的・非減少的のどれであるかを決定します。減少的な測度とは少なくとも1つの再帰呼び出しに対して小さくなり、任意の再帰呼び出しにおいて決して増加しないものを指します。一方、狭義に減少的な測度はすべての再帰呼び出しに対して小さくなります。非減少的な測度は停止タクティクが減少または狭義に減少することを示せないような測度です。こうして得られたテーブルに基づいて適切なタプルが選択されます。 このアプローチは Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow, 2007. “Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL”. In Proceedings of the International Conference on Theorem Proving in Higher Order Logics (TPHOLS 2007). (LNTCS 4732) に基づいています。 このテーブルは、測度が自動的に見つからなかった時のエラーメッセージに表示されます。
Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
n m l
1) 38:6-25 = = =
2) 39:6-23 = < _
3) 40:6-23 < _ _
Please use `termination_by` to specify a decreasing measure.deff:(nml:Nat)→Nat|n+1,m+1,l+1=>[f(n+1)(m+1)(l+1),f(n+1)(m-1)(l),f(n)(m+1)(l)].sum|_,_,_=>0decreasing_byall_goalsdecreasing_tactic
Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
n m l
1) 38:6-25 = = =
2) 39:6-23 = < _
3) 40:6-23 < _ _
Please use `termination_by` to specify a decreasing measure.
Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
x1 x2
1) 911:16-23 ? ?
2) 912:27-40 _ _
3) 912:20-41 _ _
Please use `termination_by` to specify a decreasing measure.defack:Nat→Nat→Nat|0,n=>n+1|m+1,0=>ackm1|m+1,n+1=>ackm(ack(m+1)n)decreasing_by·applyProd.Lex.leftomega·applyProd.Lex.rightomega·applyProd.Lex.leftomega
failed to prove termination, possible solutions:
- Use `have`-expressions to prove the remaining goals
- Use `termination_by` to specify a different well-founded relation
- Use `decreasing_by` to specify your own tactic for discharging this kind of goal
case h
m n : Nat
⊢ m / 2 + 1 < m + 1
A relation r is WellFounded if all elements of α are accessible within r.
If a relation is WellFounded, it does not allow for an infinite descent along the relation.
If the arguments of the recursive calls in a function definition decrease according to
a well founded relation, then the function terminates.
Well-founded relations are sometimes called Artinian or said to satisfy the “descending chain condition”.
A value is accessible if for all y such that ryx, y is also accessible.
Note that if there exists no y such that ryx, then x is accessible. Such an x is called a
base case.