Сопоставление с образцом, не специализирующиеся на типах - PullRequest
Новая
       51

Сопоставление с образцом, не специализирующиеся на типах

6 голосов
/ 23 мая 2011

Я играю в 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.

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

Ответы [ 2 ]

7 голосов
/ 23 мая 2011

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

     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.

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

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

6 голосов
/ 23 мая 2011

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

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

...