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".
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.
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
.
Ok, thank you. I'll try booleans instead and see if that makes my life easier.
Patrick Nicodemus has marked this topic as resolved.
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