coq
Recherche d'un fait existant avec Recherche et variantes
Recherche…
Syntaxe
-
Search qualid.(* pour Coq 8.4 et versions plus récentes *) -
SearchAbout qualid.(* synonyme obsolète. *)
Paramètres
| Paramètre | La description |
|---|---|
qualid | Identifiant ou modèle à rechercher. Il peut s'agir de notations |
Remarques
Avant Coq 8.4, Search avait le sens de SearchHead actuel: rechercher uniquement les faits où le motif correspond dans la conclusion de l'instruction.
Faits sur un identifiant particulier
Pour voir tous les faits concernant le le rapport du prélude:
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
...
Pour rechercher tous les faits impliquant la notation < :
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
...
Recherche d'un motif
Rechercher tous les faits impliquant un motif dans une hypothèse ou une conclusion:
Coq < Search (_ + O).
plus_n_O: forall n : nat, n = n + 0
Le caractère _ sert de caractère générique, il peut être utilisé plusieurs fois:
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
Vous pouvez également rechercher des motifs non linéaires:
Coq < Search (?x <= ?x).
le_n: forall n : nat, n <= n
Recherche d'un motif dans la conclusion d'un lemme
Recherchez un lemme quand vous savez quelle devrait être sa conclusion:
Coq < SearchPattern (S _ <= _).
le_n_S: forall n m : nat, n <= m -> S n <= S m
Vous pouvez également rechercher une conclusion partielle (la conclusion et une ou plusieurs dernières hypothèses).
Coq < Require Import Arith.
Coq < SearchPattern (?x <= ?y -> ?y <= _ -> ?x <= _).
Nat.le_trans: forall n m p : nat, n <= m -> m <= p -> n <= p
Attention: si vous mélangez l'ordre des hypothèses, vous ne trouverez rien:
Coq < SearchPattern (?y <= _ -> ?x <= ?y -> ?x <= _).