Eliminando cofix en prueba Coq

15

Mientras trato de probar algunas propiedades básicas usando tipos coinductores en Coq, sigo encontrando el siguiente problema y no puedo solucionarlo. He destilado el problema en un simple script Coq de la siguiente manera.

El tipo de árbol define árboles posiblemente infinitos con ramas marcadas con elementos de tipo A . Una rama no tiene que estar definida para todos los elementos de A . El valor Univ es el árbol infinito con todas las ramas A siempre definidas. isUniv prueba si un árbol dado es igual a Univ . El lema dice que Univ realmente satisface a 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.

En este punto renuncio a la prueba. El objetivo actual es:

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

No sé qué táctica aplicar para eliminar el cofix en el objetivo de producir (Nodo algo) para poder aplicar isuniv .

¿Alguien puede ayudar a probar este lema?
¿Cuáles son las formas estándar de eliminar el cofix en tal situación?

Dave Clarke
fuente
1
La etiqueta "pruebas interactivas" no es adecuada, ya que generalmente se refiere a los sistemas de pruebas interactivas en su sentido teórico de la complejidad. Supongo que el término correcto es "prueba de teorema interactiva" o "prueba de teorema".
Iddo Tzameret
Solucionado, el uso de "asistentes de prueba"
Dave Clarke

Respuestas:

6

Puede eliminar el cofix usando una función auxiliar que coincida con el patrón Tree.

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.

Obtendrás este objetivo, que es un paso sin cuerda.

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

Adapté esta técnica de http://adam.chlipala.net/cpdt/html/Coinductive.html

yhirai
fuente
Gracias por esto. Estaba mirando esa página casi al mismo tiempo que recibiste tu respuesta. Loco, pero parece funcionar ... y luego me quedo atascado un poco más, pero golpearé mi cabeza contra eso por un poco más.
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
fuente
Gracias por esta respuesta algo embarazosa. Me encontré con el problema de que A estaba habitada, pero me las arreglé para evitarlo. Sorprendentemente, el universo no se desarrolló.
Dave Clarke
Bueno, no estoy avergonzado por mi respuesta :-) Pensé que podría dar una respuesta integral si doy una.
Andrej Bauer
Tu respuesta fue vergonzosa para mí. Pero ciertamente muy apreciado.
Dave Clarke
Estaba bromeando ... De todos modos, no hay nada de qué avergonzarse. He cometido peores errores. Además, la web invita a las personas a publicar antes de pensar. Yo mismo publiqué una solución errónea de su definición aquí, pero afortunadamente lo noté antes que usted.
Andrej Bauer, el