#coq #convoy-pattern
#coq #convoy-шаблон
Вопрос:
Я совсем новичок в мире ATP, но определенно очень мотивирован. Я начинаю разбираться с зависимыми типами. Я участвую в проекте, где я определил тип для (конечных и бесконечных) последовательностей.
Inductive sequence {X : Type} : Type :=
| FinSeq (x : list X)
| InfSeq (f : nat -> X).
Теперь я хочу определить head непустой последовательности.
Lemma aux_hd : forall {A : Type} (l : list A),
0 < Datatypes.length l -> @hd_error A l = None -> False.
Proof. destruct l.
simpl. lia.
simpl. intros S. discriminate.
Qed.
Definition Hd {A : Type} (l : list A) : 0 < Datatypes.length l -> A :=
match (hd_error l) with
| Some a => (fun _ => a)
| None => fun pf => match (aux_hd l pf ??) with end
end.
Definition Head {A : Type} (s :sequence) (H : 0 << length s),
match s with
| FinSeq x => Hd x H
| InfSeq f => f 0 end.
Моя проблема в определении Hd: я не знаю, как доказать @hd_error A l = None
, поскольку мы уже находимся в такой ветке соответствия. Я считаю, что это должно быть действительно легко.
У меня аналогичная проблема в последнем определении, потому что я не знаю, как преобразовать H для конкретного случая первой ветви соответствия, где я знаю, что length s = Datatypes.length x
и, таким образом, 0 << length s -> 0 < Datatypes.length x
.
Наконец, я опустил подробности о << и последовательности длины, потому что я не думаю, что это имеет отношение к вопросу, но в основном я поднял nat с помощью Inf для представления длины бесконечных последовательностей, а << — это < для nat и num .
Я следил за курсом Основы программного обеспечения, и в настоящее время я больше изучаю «Сертифицированное программирование с зависимыми типами», что тоже действительно хорошо. Заранее спасибо, Мигель
Ответ №1:
Когда вы match
что-то делаете, все дополнительные доказательства должны быть переданы в качестве аргументов для сопоставления (это «шаблон convoy», описанный в CPDT).
Если Hd
вы хотите запомнить это hd_error l = None
, передайте это как аргумент. Это немного сложно, потому что вам нужно явно аннотировать match
return
предложение with a (которое в более простых случаях было выведено для вас):
Definition Hd {A : Type} (l : list A) : 0 < Datatypes.length l -> A :=
match (hd_error l) as X return hd_error l = X -> 0 < Datatypes.length l -> A with
| Some a => (fun _ _ => a)
| None => fun pf1 pf2 => match (aux_hd l pf2 pf1) with end
end eq_refl.
Аналогично Head
, после сопоставления с образцом s
вы хотите упростить 0 << length s
; передайте его в качестве аргумента:
Definition Head {A : Type} (s :sequence) (H : 0 << length s) :=
match s return (0 << length s) -> _ with
| FinSeq x => fun H => Hd x H
| InfSeq f => fun _ => f 0
end H.