Proof-Modus-Definitionen in Coq?

Question

Kann mir jemand eine gute Quelle geben, wie man Proof-Modus-Definitionen liest (ein Beispiel wird gegeben :)

Definition A (ss: FSS) (n:nat)
             (s: {s:S | state_is_wf s
                            /\ RESS.get_element n (proj1_sig ss) = Some s})
    : FS.
    destruct s. destruct a.
    refine (exist _ x _).
    apply H.
  Defined.

Dabei sind 'FSS', 'FS' und 'S' zuvor definierte Sig-Typen. Ich weiß, was die einzelnen Taktiken "Zerstören", "Verfeinern" und "Anwenden" bewirken, aber in einem Beweisbegriff für eine Definition kann ich diesen Beweis nicht lesen, ohne ihn wahrscheinlich zu kompilieren (ich kann diese Dateien nicht kompilieren, kann nur ihre Quelle lesen Code.) Kann mir jemand beim Lesen solcher Definitionen helfen oder mich auf eine Quelle verweisen?

Answer 1

Ohne die Definition zu kompilieren (und ohne die Definitionen von FSund zu sehen FSS) ist es unmöglich, aber wir können immer noch ein bisschen raten. Die destructTaktik erstellt ein match withKonstrukt svom Typ sig, das einen eindeutigen Konstruktor hat exist. Es gibt kein aArgument der Funktion, also aentweder ein globales Symbol oder eine Variable, die vom ersten erstellt wurde destruct. Nehmen wir an, es ist das letztere. Gleiches für x.

Taktik refineschafft einen Begriff, möglicherweise mit Löchern. Begriff exist _ x _enthält zwei Löcher. Der erste _wird von Coq gefüllt, aber der letzte muss vermutlich vom Benutzer ausgefüllt werden, also ist das der apply HZweck. Was H, lassen Sie uns annehmen , dass es aus einem der vorherigen kommt destruct.

Beachten Sie, dass applyinduktive Werte möglicherweise zuerst mit nur einem Konstruktor zerlegt werden. Also, wenn Hzufällig vom Typ ist A /\ B(was es wäre, wenn es vom ersten kommt destruct), apply Hkönnte es tatsächlich sein apply (proj1 H)oder apply (proj2 H). Wie auch immer, da der Beweis jetzt fertig ist, ist dies applyvermutlich exact.

Es gibt also zahlreiche Möglichkeiten. Hier ist ein Beispiel:

Definition A ss n s :=
  match s with
  | exist _ a H =>
    match a with
    | ... x ... =>         (* H could come from there too *)
      exist _ x (proj1 H)  (* or (proj2 H), or plain H *)
    end
  end.