Пытаясь доказать некоторые базовые свойства с помощью коиндуктивных типов в Coq, я продолжаю сталкиваться со следующей проблемой и не могу ее обойти. Я перевел проблему в простой сценарий Coq следующим образом.
Типа дерево определяет , возможно , бесконечные дерева с ветвями , меченных с элементами типа A . Ветвь не обязательно быть определена для всех элементов A . Значение ун - та есть бесконечное дерево со всеми A ветвей всегда определены. isUniv проверяет, равно ли данное дерево Univ . Лемма утверждает, что Univ действительно удовлетворяет isUniv .
Parameter A : Set.
CoInductive Tree: Set := Node : (A -> option Tree) -> Tree.
Definition derv (a : A) (t: Tree): option Tree :=
match t with Node f => f a end.
CoFixpoint Univ : Tree := Node (fun _ => Some Univ).
CoInductive isUniv : Tree -> Prop :=
isuniv : forall (nf : A -> option Tree) (a : A) (t : Tree),
nf a = Some t ->
isUniv t ->
isUniv (Node nf).
Lemma UnivIsUniv : isUniv Univ.
Proof.
cofix CH. (* this application of cofix is fine *)
unfold Univ.
Admitted.
На данный момент я отказываюсь от доказательства. Текущая цель:
CH : isUniv Univ
============================
isUniv (cofix Univ : Tree := Node (fun _ : A => Some Univ))
Я не знаю, какую тактику применить, чтобы устранить кофикс в цели, чтобы произвести (Узел-то), чтобы я мог применить isuniv .
Кто-нибудь может помочь доказать эту лемму?
Каковы стандартные способы устранения cofix в такой ситуации?
источник
Ответы:
Вы можете устранить cofix, используя вспомогательную функцию, которая соответствует шаблону Tree.
Вы получите эту цель, которая является шагом без вознаграждения.
Я адаптировал эту технику с http://adam.chlipala.net/cpdt/html/Coinductive.html
источник
источник