From 94188b0cbaff6340464d90cc13ee246ea7ec3284 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 21 Nov 2011 09:42:37 +0000 Subject: [PATCH] {pattern} => in pattern; --- .../grafite_parser/grafiteParser.ml | 4 +- matita/matita/help/C/sec_terms.xml | 10 +- matita/matita/help/C/tactics_quickref.xml | 224 +++--------------- matita/matita/lib/basics/jmeq.ma | 10 +- matita/matita/lib/basics/logic.ma | 8 +- 5 files changed, 51 insertions(+), 205 deletions(-) diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml index c1b059991..b616a824b 100644 --- a/matita/components/grafite_parser/grafiteParser.ml +++ b/matita/components/grafite_parser/grafiteParser.ml @@ -128,7 +128,7 @@ EXTEND ]; pattern_spec: [ [ res = OPT [ - SYMBOL "{"; + "in" ; wanted_and_sps = [ "match" ; wanted = tactic_term ; sps = OPT [ "in"; sps = sequent_pattern_spec -> sps ] -> @@ -136,7 +136,7 @@ EXTEND | sps = sequent_pattern_spec -> None,Some sps ]; - SYMBOL "}" -> + SYMBOL ";" -> let wanted,hyp_paths,goal_path = match wanted_and_sps with wanted,None -> wanted, [], Some N.UserInput diff --git a/matita/matita/help/C/sec_terms.xml b/matita/matita/help/C/sec_terms.xml index 8cd75e228..dbb6900d9 100644 --- a/matita/matita/help/C/sec_terms.xml +++ b/matita/matita/help/C/sec_terms.xml @@ -636,18 +636,18 @@ &pattern; ::= - { + in [&id;[: &path;]]… - [⊢ &path;]]} + [⊢ &path;]]; simple pattern | - {match &path; + in match &path; [in [&id;[: &path;]]… - [⊢ &path;]]} + [⊢ &path;]]; full pattern @@ -655,7 +655,7 @@ path - + &path; diff --git a/matita/matita/help/C/tactics_quickref.xml b/matita/matita/help/C/tactics_quickref.xml index c7a789c1a..12e450fdf 100644 --- a/matita/matita/help/C/tactics_quickref.xml +++ b/matita/matita/help/C/tactics_quickref.xml @@ -5,175 +5,115 @@ &tactic; ::= - absurd sterm - - - - | - apply sterm - - - - | - applyS sterm auto_params - - - - | - - assumption + + # + + id + - - - | - auto auto_params. autobatch auto_params - - - - | - - cases - term pattern [([id]…)] - - - - - | - change pattern with sterm - | - clear - id [id…] - - - - - | - clearbody id - - - - | - compose [nat] sterm [with sterm] [intros-spec] - - - - | - constructor nat + + ## + + | - - contradiction + + #_ | - cut sterm [as id] + % [nat] [{sterm…}] | - decompose - [as id…] + * + [as id] | - demodulate auto_params - - - - | - destruct sterm + + -id + | - elim sterm pattern [using sterm] intros-spec + /auto_params/. | - elimType sterm [using sterm] intros-spec + [<|>] sterm pattern | - exact sterm + @ sterm | - - - exists - - + applyS sterm auto_params | - - fail + + assumption - - - | - fold reduction-kind sterm pattern - | - - fourier - - + cases + term pattern + | - fwd id [as id [id]…] + change pattern with sterm | - generalize pattern [as id] + cut sterm | - - - id - - + destruct + [(id…)] [skip (id…)] | - intro [id] + elim sterm pattern | - intros intros-spec + generalize pattern @@ -185,25 +125,9 @@ | lapply - [linear] - [depth=nat] sterm - [to - sterm - [,sterm…] - ] - [as id] - - - | - - - left - - - | @@ -212,91 +136,13 @@ | - normalize pattern - - - - | - - - reflexivity - - - - - - | - replace pattern with sterm - - - - | - rewrite [<|>] sterm pattern - - - - | - - - right - - - - - - | - - - ring - - - - - - | - simplify pattern - - - - | - - - split - - - - - - | - - - subst - - - - - - | - - - symmetry - - - - - - | - transitivity sterm - - - - | - unfold [sterm] pattern + normalize pattern + [nodelta] | - whd pattern + whd pattern [nodelta] diff --git a/matita/matita/lib/basics/jmeq.ma b/matita/matita/lib/basics/jmeq.ma index 274ce3d5b..42e52c0a4 100644 --- a/matita/matita/lib/basics/jmeq.ma +++ b/matita/matita/lib/basics/jmeq.ma @@ -57,14 +57,14 @@ qed. lemma gral: ∀A.∀x,y:A. mk_Sigma A x = mk_Sigma A y → x=y. #A #x #y #E lapply (tech1 ?? E) - generalize {⊢ (??(???%?)? → ?)} #E1 - normalize {E1}; >(K ?? E1) normalize + generalize in ⊢ (??(???%?)? → ?); #E1 + normalize in E1; >(K ?? E1) normalize #H @H qed. lemma jm_to_eq_sigma: ∀A,x,y. jmeq A x A y → mk_Sigma A x = mk_Sigma A y. - #A #x #y #E cases E {⊢ (???%)} % + #A #x #y #E cases E in ⊢ (???%); % qed. definition curry: @@ -77,7 +77,7 @@ qed. lemma G : ∀A.∀x:A.∀P:∀y:A.mk_Sigma A x = mk_Sigma A y →Type[0]. P x (refl ? (mk_Sigma A x)) → ∀y.∀h:mk_Sigma A x = mk_Sigma A y. P y h. - #A #x #P #H #y #E lapply (gral ??? E) #G generalize {match E} + #A #x #P #H #y #E lapply (gral ??? E) #G generalize in match E; @(match G return λy.λ_. ∀e:mk_Sigma A x = mk_Sigma A y. P y e with @@ -94,7 +94,7 @@ lemma E : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0]. #A #a #P #H #b #E letin F ≝ (jm_to_eq_sigma ??? E) lapply (G ?? (curry ?? P) ?? F) [ normalize // - | #H whd {H} @(H : PP ? (P b) ?) ] + | #H whd in H; @(H : PP ? (P b) ?) ] qed. lemma jmeq_elim : ∀A.∀x:A.∀P:∀y:A.jmeq A x A y→Type[0]. diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma index 1fdd851e0..c80fa31f5 100644 --- a/matita/matita/lib/basics/logic.ma +++ b/matita/matita/lib/basics/logic.ma @@ -30,22 +30,22 @@ lemma eq_ind_r : lemma eq_rect_Type0_r: ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. - #A #a #P #H #x #p (generalize {match H}) (generalize {match P}) + #A #a #P #H #x #p lapply H lapply P cases p; //; qed. lemma eq_rect_Type1_r: ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. - #A #a #P #H #x #p (generalize {match H}) (generalize {match P}) + #A #a #P #H #x #p lapply H lapply P cases p; //; qed. lemma eq_rect_Type2_r: ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. - #A #a #P #H #x #p (generalize {match H}) (generalize {match P}) + #A #a #P #H #x #p lapply H lapply P cases p; //; qed. lemma eq_rect_Type3_r: ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. - #A #a #P #H #x #p (generalize {match H}) (generalize {match P}) + #A #a #P #H #x #p lapply H lapply P cases p; //; qed. theorem rewrite_l: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. x = y → P y. -- 2.39.2