From f511e0dbbbc4c9a5d425076307c935062d78809d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 19 Jun 2006 17:21:47 +0000 Subject: [PATCH 1/1] Patterns are now documented. But: how do we do multiple selections in matita? --- helm/software/matita/help/C/matita.xml | 1 + helm/software/matita/help/C/sec_terms.xml | 96 ++++++++++++++++++++++- 2 files changed, 95 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/help/C/matita.xml b/helm/software/matita/help/C/matita.xml index dba730919..a20663fec 100644 --- a/helm/software/matita/help/C/matita.xml +++ b/helm/software/matita/help/C/matita.xml @@ -41,6 +41,7 @@ intros-spec"> pattern"> reduction-kind"> + path"> ]> diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml index 11b06b21c..30692211e 100644 --- a/helm/software/matita/help/C/sec_terms.xml +++ b/helm/software/matita/help/C/sec_terms.xml @@ -242,6 +242,12 @@ Set the impredicate sort of datatypes + + + | + CProp + one fixed predicative sort of constructive propositions + | @@ -531,12 +537,98 @@ &pattern; ::= - &TODO; + in + [&id;[: &path;]]… + [⊢ &path;]] + simple pattern + + + + | + in match &term; + [in + [&id;[: &path;]]… + [⊢ &path;]] + full pattern + + + + + + path + + + + &path; + ::= + 〈〈any &sterm; whithout occurrences of Set, Prop, CProp, Type, &id;, &uri; and user provided notation; however, % is now an additional production for &sterm;〉〉
- &TODO; + A path locates zero or more subterms of a given term by mimicking the term structure up to: + + Occurrences of the subterms to locate that are + represented by %. + Subterms without any occurrence of subterms to locate + that can be represented by ?. + + + For instance, the path + ∀_,_:?.(? ? % ?)→(? ? ? %) + locates at once the subterms + x+y and x*y in the + term ∀x,y:nat.x+y=1→0=x*y + (where the notation A=B hides the term + (eq T A B) for some type T). + + A simple pattern extends paths to locate + subterms in a whole sequent. In particular, the pattern + in H: p K: q ⊢ r locates at once all the subterms + located by the pattern r in the conclusion of the + sequent and by the patterns p and + q in the hypotheses H + and K of the sequent. + + If no list of hypotheses is provided in a simple pattern, no subterm + is selected in the hypothesis. If the ⊢ p + part of the pattern is not provided, no subterm will be matched in the + conclusion if at least one hypothesis is provided; otherwise the whole + conclusion is selected. + + Finally, a full pattern is interpreted in three + steps. In the first step the match T in + part is ignored and a set S of subterms is + located as for the case of + simple patterns. In the second step the term T + is parsed and interpreted in the context of each subterm + s ∈ S. In the last term for each + s ∈ S the interpreted term T + computed in the previous step is looked for. The final set of subterms + located by the full pattern is the set of occurrences of + the interpreted T in the subterms s. + + A full pattern can always be replaced by a simple pattern, + often at the cost of increased verbosity or decreased readability. + Example: the pattern + ⊢ in match x+y in ∀_,_:?.(? ? % ?) + locates only the first occurrence of x+y + in the sequent x,y: nat ⊢ ∀z,w:nat. (x+y) * (z+w) = + z * (x+y) + w * (x+y). The corresponding simple pattern + is ⊢ ∀_,_:?.(? ? (? % ?) ?). + + Every tactic that acts on subterms of the selected sequents have + a pattern argument for uniformity. To automatically generate a simple + pattern: + + Select in the current goal the subterms to pass to the + tactic by using the mouse. In order to perform a multiple selection of + subterms, hold the Ctrl key while selecting every subterm after the + first one. + From the contextual menu select "Copy". + From the "Edit" or the contextual menu select + "Paste as pattern" + -- 2.39.2