Блог

Я совсем новичок в мире 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 .

Я следил за курсом Основы программного обеспечения, и в настоящее время я больше изучаю «Сертифицированное программирование с зависимыми типами», что тоже действительно хорошо. Заранее спасибо, Мигель

Когда вы 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.