max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/lean/guessLexFailures.lean.expected.out
Joachim Breitner 1311e36a98
feat: structural mutual recursion (#4575) 
This adds support for mutual structural recursive functions.

For now this is opt-in: The functions must have a `termination_by
structural …` annotation (new since #4542) for this to work:

```lean
mutual
inductive A
  | self : A → A
  | other : B → A
  | empty
inductive B
  | self : B → B
  | other : A → B
  | empty
end

mutual
def A.size : A → Nat
  | .self a => a.size + 1
  | .other b => b.size + 1
  | .empty => 0
termination_by structural x => x
def B.size : B → Nat
  | .self b => b.size + 1
  | .other a => a.size + 1
  | .empty => 0
termination_by structural x => x
end
```

The recursive functions don’t have to be in a one-to-one relation to a
set of mutually recursive inductive data types. It is possible to ignore
some of the types:

```lean
def A.self_size : A → Nat
  | .self a => a.self_size + 1
  | .other _ => 0
  | .empty => 0
termination_by structural x => x
```

or have more than one function per argument type:

```lean
  def isEven : Nat → Prop
    | 0 => True
    | n+1 => ¬ isOdd n
  termination_by structural x => x

  def isOdd : Nat → Prop
    | 0 => False
    | n+1 => ¬ isEven n
  termination_by structural x => x
```


This does not include

 * Support for nested inductive data types or nested recursion
* Inferring mutual structural recursion in the absence of
`termination_by`.
 * Functional induction principles for these.
* Mutually recursive functions that live in different universes. This
may be possible,
maybe after beefing up the `.below` and `.brecOn` functions; we can look
into this some
   other time, maybe when there are concrete use cases.

---------

Co-authored-by: Richard Kiss <him@richardkiss.com>
Co-authored-by: Tobias Grosser <tobias@grosser.es>
2024-07-08 14:39:50 +00:00

151 lines
5.3 KiB
Text
Raw Blame History

guessLexFailures.lean:9:4-9:18: error: fail to show termination for
nonTerminating
with errors
structural recursion cannot be used:
argument #1 cannot be used for structural recursion
failed to eliminate recursive application
nonTerminating n.succ m.succ
argument #2 cannot be used for structural recursion
failed to eliminate recursive application
nonTerminating n.succ m.succ
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) 11:12-46 ? ?
Please use `termination_by` to specify a decreasing measure.
guessLexFailures.lean:15:0-18:31: error: 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) 17:12-47 ? ?
Please use `termination_by` to specify a decreasing measure.
guessLexFailures.lean:20:4-20:15: error: fail to show termination for
noArguments
with errors
structural recursion cannot be used:
well-founded recursion cannot be used, 'noArguments' does not take any (non-fixed) arguments
guessLexFailures.lean:22:4-22:23: error: fail to show termination for
noNonFixedArguments
with errors
structural recursion cannot be used:
argument #1 cannot be used for structural recursion
it is unchanged in the recursive calls
well-founded recursion cannot be used, 'noNonFixedArguments' does not take any (non-fixed) arguments
guessLexFailures.lean:27:0-33:31: error: 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) 29:6-25 = = =
2) 30:6-23 = < _
3) 31:6-23 < _ _
Please use `termination_by` to specify a decreasing measure.
guessLexFailures.lean:37:0-43:31: error: 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 x4
1) 39:6-27 = = =
2) 40:6-25 = < _
3) 41:6-25 < _ _
Please use `termination_by` to specify a decreasing measure.
guessLexFailures.lean:48:0-54:31: error: 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) 50:6-25 = = =
2) 51:6-23 = < _
3) 52:6-23 < _ _
Please use `termination_by` to specify a decreasing measure.
guessLexFailures.lean:59:6-59:7: error: fail to show termination for
Mutual.f
Mutual.g
Mutual.h
with errors
mutual structural recursion requires explicit `termination_by` clauses
Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
Call from Mutual.f to Mutual.f at 61:8-33:
n m l
= = =
Call from Mutual.f to Mutual.f at 62:8-31:
n m l
= < <
Call from Mutual.f to Mutual.g at 63:8-39:
n m l
n < ? ?
m ? = ?
l ? ? <
Call from Mutual.g to Mutual.g at 68:8-35:
n m l
? ? =
Call from Mutual.g to Mutual.g at 69:8-33:
n m l
_ _ <
Call from Mutual.g to Mutual.h at 70:8-27:
n m l
n _ _ ?
m _ _ ?
Call from Mutual.h to Mutual.f at 75:8-33:
n m
n _ _
m _ _
l _ _
Call from Mutual.h to Mutual.h at 76:8-27:
n m
_ _
Call from Mutual.h to Mutual.h at 77:8-27:
n m
_ _
Please use `termination_by` to specify a decreasing measure.
guessLexFailures.lean:87:4-87:5: error: fail to show termination for
DuplicatedCall.f
with errors
structural recursion cannot be used:
argument #1 cannot be used for structural recursion
failed to eliminate recursive application
DuplicatedCall.f (n + 2) (m + 1)
argument #2 cannot be used for structural recursion
failed to eliminate recursive application
DuplicatedCall.f (n + 2) (m + 1)
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
1) 89:19-32 ? ?
Please use `termination_by` to specify a decreasing measure.
guessLexFailures.lean:100:0-103:31: error: 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
1) 101:83-105 ? ?
Please use `termination_by` to specify a decreasing measure.
guessLexFailures.lean:113:14-113:31: error: 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
n✝ m n : Nat
⊢ n < n✝
guessLexFailures.lean:119:0-123:31: error: 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
1) 121:31-54 ? ?
Please use `termination_by` to specify a decreasing measure.
guessLexFailures.lean:131:14-131:31: error: 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
m n✝ n : Nat
⊢ n < n✝ + 1
Reference in a new issue View git blame Copy permalink