Eliminierung von Cofix in Coq Proof

15

Während ich versuche, einige grundlegende Eigenschaften mithilfe von coinduktiven Typen in Coq zu beweisen, stoße ich weiterhin auf das folgende Problem und kann es nicht umgehen. Ich habe das Problem folgendermaßen in ein einfaches Coq-Skript unterteilt.

Der Typ Tree definiert möglicherweise unendliche Bäume mit Zweigen, die mit Elementen des Typs A gekennzeichnet sind . Eine Verzweigung muss nicht für alle Elemente von A definiert werden . Der Wert Univ ist der unendliche Baum, in dem immer alle A- Zweige definiert sind. isUniv testet, ob ein gegebener Baum dem Univ entspricht . Das Lemma besagt, dass Univ tatsächlich isUniv erfüllt .

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.

An dieser Stelle gebe ich den Beweis auf. Das aktuelle Ziel ist:

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

Ich weiß nicht, welche Taktik ich anwenden soll, um das Cofix im Ziel zu eliminieren (Node etwas), damit ich isuniv anwenden kann .

Kann jemand helfen, dieses Lemma zu beweisen?
Was sind die Standardmethoden, um cofix in einer solchen Situation zu eliminieren ?

Dave Clarke
quelle
1
Der Begriff "interaktive Proofs" ist nicht ausreichend, da er sich im Allgemeinen auf interaktive Proofsysteme in ihrem komplexitätstheoretischen Sinne bezieht. Ich nehme an, der richtige Begriff ist "interaktiver Theorembeweis" oder "Theorembeweis".
Iddo Tzameret
Behoben, mit "Proof-Assistenten"
Dave Clarke

Antworten:

6

Sie können cofix mit einer Hilfsfunktion entfernen, deren Muster mit Tree übereinstimmt.

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.

Sie erhalten dieses Ziel, das ein Schritt abgewickelt ist.

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

Ich habe diese Technik von http://adam.chlipala.net/cpdt/html/Coinductive.html angepasst

yhirai
quelle
Danke dafür. Ich habe diese Seite ungefähr zur selben Zeit durchgesehen, als Ihre Antwort eingegangen ist. Verrückt, aber es scheint zu funktionieren ... und dann stecke ich ein wenig weiter fest, aber ich werde meinen Kopf ein wenig länger dagegen drücken.
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
quelle
Vielen Dank für diese etwas peinliche Antwort. Ich bin zwar auf das Problem mit A gestoßen, habe es aber geschafft, mich darin zurechtzufinden. Überraschenderweise hat sich das Universum nicht entfaltet.
Dave Clarke
Nun, ich schäme mich nicht für meine Antwort :-) Ich dachte, ich könnte genauso gut eine umfassende Antwort geben, wenn ich eine gebe.
Andrej Bauer
Ihre Antwort war mir peinlich. Aber sicherlich sehr geschätzt.
Dave Clarke
Ich habe nur Spaß gemacht ... Jedenfalls gibt es nichts, wofür man sich schämen müsste. Ich habe schlimmere Fehler gemacht. Außerdem lädt das Web die Leute dazu ein, zu posten, bevor sie denken. Ich selbst habe hier eine fehlerhafte Korrektur Ihrer Definition vorgenommen, aber zum Glück habe ich sie vor Ihnen bemerkt.
Andrej Bauer