## Stream: Coq users

### Topic: ✔ Abstraction error in case analysis

#### Patrick Nicodemus (May 11 2022 at 04:32):

I have the following situation:

``````  n', m' : nat
tree' : Arr n' m'.+2
p' : is_list n' m'.+2 tree'
ival : nat
ibd : ival < m'.+3
jval : nat
jbd : jval < m'.+2
l : jval <= ival
============================
is_list n' m'.+2
(match l in (_ <= n0) return (n0 < m'.+3 -> Arr n' m'.+2) with
| @leq_n _ => fun _ : jval < m'.+3 => tree'
| @leq_S _ m0 l0 =>
fun jbd0 : m0.+1 < m'.+3 =>
match l0 in (_ <= n0) return (n0.+1 < m'.+3 -> jval <= n0 -> Arr n' m'.+2) with
| @leq_n _ => fun (_ : jval.+1 < m'.+3) (_ : jval <= jval) => tree'
| @leq_S _ m1 l1 =>
fun (jbd1 : m1.+2 < m'.+3) (_ : jval <= m1.+1) =>
(tree'
· s
(jval;
mixed_trans1 jval m1 m'.+1 l1 (leq_S_n m1.+1 m'.+1 (leq_S_n m1.+2 m'.+2 jbd1))))
· d (m1.+1; leq_S_n m1.+2 m'.+2 jbd1)
end jbd0 l0
end ibd)
``````

I have a function that operates on binary trees and returns trees, I'm trying to prove that when it operates on a list (a tree such that every right child subtree is a leaf) it returns a list.

Here `a < b` is shorthand for `a.+1 <= b` and `<=` is an inductive type generated by `n <= n` and `n <= m -> n <= m.+1`.

I want to proceed by case analysis on the variable `ibd : ival < m'.+3 ` by running `destruct ibd`. This should break it into the cases `ival+1 =m'.+3` and `ival + 1 < m'.+3`; in the first case it will rewrite every occurrence of `m'.+3` with `ival+1.`

But this has the consequence of abstracting/patterning on `m'.+3` as well, and there are things in the body of the function which depend on this being that value. I don't know how to move forward in my proof without doing case analysis on this variable and I don't know my way around it. Can anybody suggest the way forward?

``````             pattern (m'.+3).

Error: Illegal application:
The term "leq_S_n" of type "forall n m : nat, n.+1 <= m.+1 -> n <= m"
cannot be applied to the terms
"m0.+2" : "nat"
"m'.+2" : "nat"
"jbd1" : "m0.+2 < n"
The 3rd term has type "m0.+2 < n" which should be coercible to "m0.+3 <= m'.+3".
``````

#### Patrick Nicodemus (May 11 2022 at 04:58):

I must admit I find this very frustrating, it seems like I should be able to do a simple case analysis without running into these kinds of errors.

#### Guillaume Melquiond (May 11 2022 at 05:04):

Note that, due to your definition of `<=`, this is not a "simple" case analysis. You would not have encountered this issue if you had used a boolean function instead. Anyway, the usual way to solve this kind of issue is to introduce a new variable, e.g., `k`, such that `k = m'.+3`. Then, you replace as many occurrences of `m'.+3` as possible with `k`, in particular the one in `ibd`. Now you can destruct `ibd`, since it will not rewrite the remaining occurrence of `m'.+3`.

#### Patrick Nicodemus (May 11 2022 at 05:28):

Ok, thank you. I'll try booleans instead and see if that makes my life easier.

#### Notification Bot (May 11 2022 at 06:33):

Patrick Nicodemus has marked this topic as resolved.

#### Patrick Nicodemus (May 11 2022 at 06:33):

i'll mark this resolved for now as making that change to the algorithm got me over the hump.

Last updated: Sep 25 2023 at 12:01 UTC