Eliminando cofix na prova de Coq

15

Ao tentar provar algumas propriedades básicas usando tipos coindutores no Coq, continuo com o seguinte problema e não consigo contorná-lo. Eu destilei o problema em um script Coq simples da seguinte maneira.

O tipo de árvore define árvores possivelmente infinitas com ramos rotulados com elementos do tipo A . Um ramo não precisa ser definido para todos os elementos A . O valor Univ é a árvore infinita com todos os ramos A sempre definidos. O isUniv testa se uma determinada árvore é igual à Univ . O lema afirma que o Univ realmente satisfaz o 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.

Neste ponto, desisto da prova. O objetivo atual é:

CH : isUniv Univ
============================
isUniv (cofix Univ  : Tree := Node (fun _ : A => Some Univ))

Não sei qual tática aplicar para eliminar o cofix no objetivo de produzir (Nó alguma coisa) para que eu possa aplicar isiv .

Alguém pode ajudar a provar esse lema?
Quais são as formas padrão de eliminar o cofix em tal situação?

Dave Clarke
fonte
11
O tag "provas interativas" não é adequado, pois geralmente se refere a sistemas de provas interativas no sentido teórico da complexidade. O termo correto, suponho, é "prova do teorema interativo" ou "prova do teorema".
Iddo Tzameret 01/09/10
Corrigido, usando "revisores"
Dave Clarke

Respostas:

6

Você pode eliminar o cofix usando uma função auxiliar que corresponda ao padrão em Árvore.

Definition TT (t:Tree) :=
  match t with
    | Node o => Node o
  end.

Lemma TTid : forall t: Tree, t = TT t.
  intro t.
  destruct t.
  reflexivity.
  Qed.

Lemma UnivIsUniv : isUniv Univ.
Proof.
  cofix.
  rewrite TTid.
  unfold TT.
  unfold Univ.

Você obterá esse objetivo, que é um passo livre.

  UnivIsUniv : isUniv Univ
  ============================
   isUniv
     (Node
        (fun _ : A =>
         Some (cofix Univ  : Tree := Node (fun _ : A => Some Univ))))

Eu adaptei essa técnica em http://adam.chlipala.net/cpdt/html/Coinductive.html

yhirai
fonte
Obrigado por isso. Eu estava olhando para essa página mais ou menos na mesma hora em que sua resposta chegou. Louca, mas parece funcionar ... e então fico um pouco mais longe, mas vou bater minha cabeça contra isso por mais um pouco.
Dave Clarke
9
(* I post my answer as a Coq file. In it I show that supercoooldave's
   definition of a universal tree is not what he intended. His isUniv
   means "the tree has an infinite branch". I provide the correct
   definition, show that the universal tree is universal according to
   the new definition, and I provide counter-examples to
   supercooldave's definition. I also point out that the universal
   tree of branching type A has an infinite path iff A is inhabited.
   *)

Set Implicit Arguments.

CoInductive Tree (A : Set): Set := Node : (A -> option (Tree A)) -> Tree A.

Definition child (A : Set) (t : Tree A) (a : A) :=
  match t with
    Node f => f a
  end.

(* We consider two trees, one is the universal tree on A (always
   branches out fully), and the other is a binary tree which always
   branches to one side and not to the other, so it is like an
   infinite path with branches of length 1 shooting off at each node.  *)

CoFixpoint Univ (A : Set) : Tree A := Node (fun _ => Some (Univ A)).

CoFixpoint Thread : Tree (bool) :=
  Node (fun (b : bool) => if b then Some Thread else None).

(* The original definition of supercooldave should be called "has an
   infinite path", so we rename it to "hasInfinitePath". *)
CoInductive hasInfinitePath (A : Set) : Tree A -> Prop :=
  haspath : forall (f : A -> option (Tree A)) (a : A) (t : Tree A),
    f a = Some t ->
    hasInfinitePath t -> 
    hasInfinitePath (Node f).

(* The correct definition of universal tree. *)
CoInductive isUniv (A : Set) : Tree A -> Prop :=
  isuniv : forall (f : A -> option (Tree A)),
    (forall  a, exists t, f a = Some t /\ isUniv t) -> 
    isUniv (Node f).

(* Technicalities that allow us to get coinductive proofs done. *)
Definition TT (A : Set) (t : Tree A) :=
  match t with
    | Node o => Node o
  end.

Lemma TTid (A : Set) : forall t: Tree A, t = TT t.
  intros A t.
  destruct t.
  reflexivity.
  Qed.

(* Thread has an infinite path. *)
Lemma ThreadHasInfinitePath : hasInfinitePath Thread.
Proof.
  cofix H.
  rewrite TTid.
  unfold TT.
  unfold Thread.
  (* there is a path down the "true" branch leading to Thread. *)
  apply haspath with (a := true) (t := Thread).
  auto.
  auto.
Qed.

(* Auxiliary lemma *)
Lemma univChildNotNone (A : Set) (t : Tree A) (a : A):
  isUniv t -> (child t a <> None).
Proof.
  intros A t a [f H].
  destruct (H a) as [u [G _]].
  unfold child.
  rewrite G.
  discriminate.
Qed.

(* Thread is not universal. *)
Lemma ThreadNotUniversal: ~ (isUniv Thread).
Proof.
  unfold not.
  intro H.
  eapply univChildNotNone with (t := Thread) (a := false).
  auto.
  unfold Thread, child.
  auto.
Qed.

(* Now let us show that Univ is universal. *)
Lemma univIsuniv (A : Set): isUniv (Univ A).
Proof.
  intro A.
  cofix H.
  rewrite TTid.
  unfold TT.
  unfold Univ.
  apply isuniv.
  intro a.
  exists (Univ A).
  auto.
Qed.

(* By the way, it need not be the case that a universal tree has
   an infinite path! In fact, the universal tree of branching type
   A has an infinite path iff A is inhabited. *)

Lemma whenUnivHasInfiniteBranch (A : Set):
  hasInfinitePath (Univ A) <-> exists a : A, True.
Proof.
  intro A.
  split.
  intro H.
  destruct H as [f a t _].
  exists a.
  trivial.
  intros [a _].
  cofix H.
  rewrite TTid.
  unfold TT.
  unfold Univ.
  apply haspath with (t := Univ A); auto.
Qed.
Andrej Bauer
fonte
Obrigado por esta resposta um tanto embaraçosa. Eu me deparei com o problema de A estar sendo habitado, mas consegui me contornar. Surpreendentemente, o universo não se desenrolou.
Dave Clarke
Bem, não estou envergonhado com a minha resposta :-) Pensei que poderia dar uma resposta abrangente se desse uma.
Andrej Bauer
Sua resposta foi embaraçosa para mim. Mas certamente muito apreciado.
Dave Clarke
Eu estava brincando ... De qualquer forma, não há nada para se envergonhar. Eu cometi erros piores. Além disso, a web convida as pessoas a postar antes que pensem. Eu próprio publiquei uma correção incorreta da sua definição aqui, mas felizmente notei isso antes de você.
Andrej Bauer