coq
Suche nach einem vorhandenen Sachverhalt mit Suche und Varianten
Suche…
Syntax
-
Search qualid.(* für Coq 8.4 und neuere Versionen *) -
SearchAbout qualid.(* veraltetes Synonym. *)
Parameter
| Parameter | Beschreibung |
|---|---|
qualid | Der Bezeichner oder das Muster, nach dem gesucht werden soll. Es kann Notationen enthalten |
Bemerkungen
Vor Coq 8.4 hatte Search die Bedeutung des aktuellen SearchHead : Suche nur nach Fakten, bei denen das Muster in der Schlussfolgerung der Anweisung übereinstimmt.
Fakten zu einer bestimmten Kennung
Um zu sehen , alle Fakten , die Einbeziehung le Beziehung vom Auftakt:
Coq < Search le.
le_n: forall n : nat, n <= n
le_S: forall n m : nat, n <= m -> n <= S m
...
max_l: forall n m : nat, m <= n -> Nat.max n m = n
max_r: forall n m : nat, n <= m -> Nat.max n m = m
...
Um nach allen Fakten zu suchen, die die Notation betreffen < :
Coq < Search "<".
exists_lt: forall (Q : nat -> Prop) (k l : nat), exists_between Q k l -> k < l
in_int_intro: forall p q r : nat, p <= r -> r < q -> in_int p q r
in_int_lt: forall p q r : nat, in_int p q r -> p < q
...
Nach einem Muster suchen
Suchen Sie nach allen Fakten, die ein Muster in einer Hypothese oder Schlussfolgerung betreffen:
Coq < Search (_ + O).
plus_n_O: forall n : nat, n = n + 0
Das Zeichen _ dient als Platzhalter, es kann mehrmals verwendet werden:
Coq < Search (S _ <= _).
le_S_n: forall n m : nat, S n <= S m -> n <= m
le_n_S: forall n m : nat, n <= m -> S n <= S m
Sie können auch nach nichtlinearen Mustern suchen:
Coq < Search (?x <= ?x).
le_n: forall n : nat, n <= n
Suche nach einem Muster zum Abschluss eines Lemmas
Suchen Sie nach einem Lemma, wenn Sie wissen, was seine Schlussfolgerung sein sollte:
Coq < SearchPattern (S _ <= _).
le_n_S: forall n m : nat, n <= m -> S n <= S m
Sie können auch nach einer partiellen Schlussfolgerung (der Schlussfolgerung und einer oder mehreren letzten Hypothesen) suchen.
Coq < Require Import Arith.
Coq < SearchPattern (?x <= ?y -> ?y <= _ -> ?x <= _).
Nat.le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p
Achtung: Wenn Sie die Reihenfolge der Hypothesen verwechseln, werden Sie nichts finden:
Coq < SearchPattern (?y <= _ -> ?x <= ?y -> ?x <= _).