Как применить разрешимые, когда они известны?

Я пытаюсь доказать, что вставка дерева бинарной сортировки. Я нахожусь в середине доказательства, и среда выглядит так:

  -- new rx : ℕ

  Goal: SortedTree (node leaf x (node (insertTree new rl) rx rr))
  Have: SortedTree (insertTree new (node rl rx rr) | new ≤? rx) 
  ————————————————————————————————————————————————————————————
  new≤rx : new ≤ rx

Обратите внимание на | new ≤? rx, который на AFAIK означает «Мне нужно знать значение, чтобы уменьшить его еще больше».

Как применить new≤rx?

insertTree определяется следующим образом:

  insertTree : (a : ℕ) →  (t : Tree ℕ) → Tree ℕ
  insertTree a (node l x r) with a ≤? x
  insertTree a (node l x r) | yes p = node (insertTree a l) x r
  insertTree a (node l x r) | no ¬p = node l x (insertTree a r)

Я знаю значение нового ≤? rx (это yes new≤rx), на самом деле я withed by new ≤? x прямо сейчас:

  ... | no  ¬n≤x with new ≤? rx
  ...        | yes new≤rx = {!proof⟦insertTree⟧ (node rl rx rr)  (sorted-rhs st) new !}
  ...        | no  p = {!!}

Итак, как я могу сообщить agda, что значение new ≤? rx известно и оно должно идти вместе с insertTree a (node l x r) | yes p = node (insertTree a l) x r?

Я пытался использовать перезапись

             where prf : (new ≤? rx ≡ yes new≤rx) → SortedTree (node (insertTree new rl) rx rr)
                   prf p1 rewrite p1 = {!proof⟦insertTree⟧ (node rl rx rr)  (sorted-rhs st) new !}

Но хоть у меня p1 : new ≤? rx ≡ yes new≤rx, агда игнорирует и говорит, что у меня SortedTree (insertTree new (node rl rx rr) | new ≤? rx)


agda
person user2998754    schedule 31.05.2014    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Мне удалось получить его с помощью проверки + перезаписи.

       proof⟦insertTree⟧ (node leaf x (node rl rx rr)) st new with new ≤? x 
       ... | yes p = st-node (empty new) (sorted-rhs st) p (st-cmp-rhs st)
       ... | no  ¬n≤x with new ≤? rx |  inspect (_≤?_ new) rx
       ...               | yes p | PropEq.[ eq ] = {!!}
              where prf : (new ≤? rx ≡ yes p) →  SortedTree (insertTree new (node rl rx rr)) → SortedTree (node (insertTree new rl) rx rr)
                    prf p0 p rewrite p0 = p

Обратите внимание, что prf subproof принимает p типа SortedTree (insertTree new (node rl rx rr)) и возвращает сам p, но благодаря перезаписи возвращаемый тип изменяется.

person user2998754    schedule 31.05.2014