У меня есть вопрос, касающийся определений проверки типов в Coq.Я столкнулся с ситуацией, когда у меня есть два термина типа t1 и t2, где я знаю, что t1 и t2 равны (t1 = t2) из определения.Тем не менее, я не могу использовать эти два термина вместе, так как типы не считаются равными при проверке типов.Я попытался выделить минимальный пример, моделирующий ситуацию (да, я знаю, что это глупое свойство, но я просто хочу, чтобы оно проверялось на типе;)):
Require Import Coq.Lists.List.
Lemma myLemma :
forall t1 t2 : Type,
forall (l1 : list t1) (l2 : list t2),
t1 = t2 ->
l1 = l2.
Просто предположим, что я не могу написать (l2 : list t1)вместо этого, поскольку я получаю его из другого определения.
Я пытался использовать Program, потому что надеялся, что смогу как-то отложить задачу, чтобы доказать, что типы совпадают, но это не помогло (получил тот же типпроверка ошибок).
Если приведенного выше примера недостаточно для прояснения проблемы, вот выдержка из моей реальной проблемы:
Definition taclet_sound_new (t : taclet) :=
forall K st seSt, let S := (sig K) in
[(K, st)] |= (pathC seSt) ->
(forall K', let S' := (sig K') in
S' = (newSig t S) ->
exists (seSt' : (@sestatesc (newSig t S))),
List.In seSt' (apply t S seSt) ->
[(K', st)] |= (conv S' (pathC seSt'))).
Система жалуется, что The term "pathC seSt'" has type "@pathCond (newSig t S)" while it is expected to have type "@pathCond S'".;однако из предпосылки S' = (newSig t S) я бы ожидал, что каким-то образом можно будет проверить этот тип определения.
(Примечание: conv - это тривиальное определение, которое я добавил только для улучшения Coq'sвывод - Definition conv (S : signature) (pc : (@pathCond S)) : list (@formulas S) := pc. - без этого он говорит The term "pathC seSt'" has type "pathCond" while it is expected to have type "list formulas"., что скрывало реальную проблему.)
Для полноты: запись taclet определяется как
Record taclet : Type := {
defined (prog : P) : Prop;
newSig (S1 : signature) : signature ;
apply : forall (S1 : signature),
(@sestatesc S1) -> list (@sestatesc (newSig S1)) ;
}.
Итак, там есть термин newSig.Следовательно, альтернативное определение
Definition taclet_sound_new (t : taclet) :=
forall K st seSt, let S := (sig K) in
[(K, st)] |= (pathC seSt) ->
(forall K', let S' := (sig K') in
exists (seSt' : (@sestatesc S')),
S' = (newSig t S) ->
List.In seSt' (apply t S seSt) ->
[(K', st)] |= (pathC seSt')).
также не проверяет тип с аналогичной ошибкой The term "apply t S seSt" has type "list (sestatesc P (newSig t S))" while it is expected to have type "list (sestatesc P S')"., которая, опять же, должна быть ясна из предпосылки.
Я был бы очень рад, если быкто-нибудь может мне помочь.Этот механизм проверки типов Coq иногда немного неудобен ...;)
Заранее спасибо!
/ edit (2018-09-27): Хотя я дал себе ответ ниже, который успокаивает проверку типов, я все еще сталкиваюсь с множеством проблем, пытаясь решить свои проблемы вокруг некоторых теорем и определений в области логики предикатов.Например, Я полностью не могу определить удовлетворительную версию теоремы консервативности (если формула действительна в структуре, она также действительна во всех расширениях) из-за проверки типа, и , даже еслидобавьте сумасшедшее ограничение (расширение имеет ту же сигнатуру, так что на самом деле это не расширение) и добавьте (рабочее) приведение, Я не могу доказать это !
На этот раз,Я думал, что приведу полный пример .Я выделил проблему и поместил ее в один файл "firstorder.v" в виде GitHub Gist (https://gist.github.com/rindPHI/9c55346965418bd5db26bfa8404aa7fe).. В документе есть комментарии, объясняющие проблемы, которые я обнаружил для себя. Если кто-нибудь найдетответ на один или два из "главных вызовов", я был бы действительно рад узнать о них (и принял бы это как ответ на вопрос здесь). Еще раз спасибо! Я надеюсьчто решение этих проблем не только помогает мне, но и другим людям, которые отчаялись из-за зависимых проблем;)