Сопоставление с образцом без специализации типов

Я играю в Coq, пытаясь создать отсортированный список. Мне просто нужна функция, которая берет список [1,2,3,2,4] и возвращает что-то вроде Sorted [1,2,3,4], т.е. удаляет плохие части, но не сортирует весь список.

Я подумал, что начну с определения функции lesseq типа (m n : nat) -> option (m <= n), а затем смогу довольно легко сопоставлять ее с образцом. Может быть, это плохая идея.

Суть проблемы, с которой я сейчас сталкиваюсь, заключается в том, что (фрагмент, вся функция внизу)

Fixpoint lesseq (m n : nat) : option (m <= n) :=
    match m with
        | 0 => match n with
            | 0 => Some (le_n 0)
            ...

не проверяет тип; он говорит, что ожидает option (m <= n), но Some (le_n 0) имеет тип option (0 <= 0). Я не понимаю, потому что очевидно, что и m, и n равны нулю в этом контексте, но я понятия не имею, как сказать об этом Coq.

Вся функция такова:

Fixpoint lesseq (m n : nat) : option (m <= n) :=
    match m with
    | 0 => match n with
        | 0 => Some (le_n 0)
        | S n_  => None
        end
    | S m_  => match n with
        | 0 => None
        | S _   => match lesseq m_ n with
                | Some x=> le_S m n x
                | None  => None
                end
            end
    end.

Возможно, я забегаю вперед, и мне просто нужно продолжать читать, прежде чем я займусь этим.


dependent-type theorem-proving coq
person Amos Robinson    schedule 23.05.2011    source источник

Ответы (2)


arrow_upward
7
arrow_downward

Вы, вероятно, захотите определить следующую функцию (даже если вы правильно ее аннотируете, у вас [le_S m n x] нет нужного вам типа):

     Fixpoint lesseq (m n : nat) : option (m <= n) :=
     match n with
     | 0 =>
         match m with
         | 0 => Some (le_n 0)
         | S m0 => None
         end
     | S p =>
         match lesseq m p with
         | Some l => Some (le_S m p l)
         | None => None
         end
     end.

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

     Fixpoint lesseq (m n : nat) : option (m <= n) :=
     match n return (option (m <= n)) with
     | 0 =>
         match m return (option (m <= 0)) with
         | 0 => Some (le_n 0)
         | S m0 => None
         end
     | S p =>
         match lesseq m p with
         | Some l => Some (le_S m p l)
         | None => None
         end
     end.

См. справочное руководство, если вы действительно хотите понять, как сопоставление с образцом работает с зависимыми типами. Если вы не чувствуете себя достаточно храбрым для этого, вы предпочтете использовать механизмы тактики для построения своего доказательства (тактика «уточнить» — отличный инструмент для этого).

     Definition lesseq m n : option (m <= n).
     refine (fix lesseq (m : nat) (n : nat) {struct n} := _).

     destruct n.
     destruct m.
     apply Some; apply le_n.
     apply None.

     destruct (lesseq m n).
     apply Some.
     apply le_S.
     assumption.
     apply None.
     Defined.

Кстати, я не думаю, что ваша функция будет действительно полезной (даже если это хорошая идея), потому что вам нужно будет доказать следующую лемму: Lemma lesseq_complete: forall mn, lesseq mn ‹> None -> m > н.

Вот почему люди используют Coq.Arith.Compare_dec. Повеселись.

person Marc    schedule 23.05.2011
comment
Кстати, если вы будете следовать этому подходу, я настоятельно рекомендую использовать функцию «Программа». Это позволяет вам написать вашу программу в стиле 1-го листинга, но оставить любое количество дыр (_), которые вы потом сможете заполнить с помощью тактики (стиль второго листинга). Следовательно, это позволяет вам красиво разделить программирование и доказательство. - person akoprowski; 23.05.2011
comment
Спасибо вам обоим за помощь. Мне нужно многому научиться, я не знал, что вы можете использовать тактику для определения функций (хотя это имеет смысл). Теперь я согласен с тем, что тип суммы (a ‹= b \/ a › b) был бы замечательным, потому что мне удалось реализовать неправильный lesseq, возвращая None, когда я хочу Some; это было бы невозможно с более конкретным типом. Я обязательно еще раз просмотрю стандартную библиотеку. - person Amos Robinson; 24.05.2011

arrow_upward
6
arrow_downward

Вы хотите написать эту функцию в качестве упражнения или только для достижения большей цели? В последнем случае вам следует взглянуть на стандартную библиотеку, которая полна функций принятия решений, которые выполнят эту работу здесь, Coq.Arith.Compare_dec; см., например, le_gt_dec.

Также обратите внимание, что предлагаемая вами функция даст вам только информацию о том, m <= n. Для сопоставления с образцом тип суммы { ... } + { ... } гораздо полезнее, поскольку дает вам два возможных случая.

person akoprowski    schedule 23.05.2011