inductive C : Nat → Type where
| C0 : C 0
| C1 : C n → C (1 + n)
| C2 : C n → C n → C n
open C
def id_C (c : C n) : C n :=
match c with
| C0 => C0
| C1 c => C1 (id_C c)
| C2 c₁ c₂ => C2 (id_C c₁) (id_C c₂)
We can prove the following theorem with match or induction:
theorem id_c_is_identity (c : C n) : id_C c = c := by
match c with
| C0 => simp [id_C]
| C1 inner => simp [id_C, id_c_is_identity inner]
| C2 lhs rhs => simp [id_C, id_c_is_identity lhs, id_c_is_identity rhs]
this will use the structural termination metric on c as expected.
However the following:
theorem id_c_is_identity (c : C n) : id_C c = c := by
cases c with
| C0 => simp [id_C]
| C1 inner => simp [id_C, id_c_is_identity inner]
| C2 lhs rhs => simp [id_C, id_c_is_identity lhs, id_c_is_identity rhs]
Fails to prove termination, if we force a use of the structural metric:
theorem id_c_is_identity (c : C n) : id_C c = c := by
cases c with
| C0 => simp [id_C]
| C1 inner => simp [id_C, id_c_is_identity inner]
| C2 lhs rhs => simp [id_C, id_c_is_identity lhs, id_c_is_identity rhs]
termination_by structural c
We get
failed to infer structural recursion:
Cannot use parameter c:
failed to eliminate recursive application
id_c_is_identity lhs
Steps to Reproduce
Expected behavior: Given that it works with match it should either also work with cases or there should be a better error message explaining why that is not the case (haha).
Prerequisites
Please put an X between the brackets as you perform the following steps:
Description
Consider:
We can prove the following theorem with
match
orinduction
:this will use the structural termination metric on
c
as expected. However the following:Fails to prove termination, if we force a use of the structural metric:
We get
Steps to Reproduce
Expected behavior: Given that it works with
match
it should either also work withcases
or there should be a better error message explaining why that is not the case (haha).Actual behavior:
match
works,cases
doesn't.Versions
"4.12.0-nightly-2024-10-13"
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.