Stream: Coq users

Topic: ✔ Abstraction error in case analysis

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (May 11 2022 at 05:28):

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

view this post on Zulip Notification Bot (May 11 2022 at 06:33):

Patrick Nicodemus has marked this topic as resolved.

view this post on Zulip 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