From b91d9e60b0a5f450d2725d4b9bb3ed7f81ef6d3a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 14 Sep 2009 08:45:55 +0000 Subject: [PATCH] New tactics ncut and nlapply. --- .../software/components/grafite/grafiteAst.ml | 2 ++ .../components/grafite/grafiteAstPp.ml | 12 ++++--- .../grafite_engine/grafiteEngine.ml | 2 ++ .../grafite_parser/grafiteParser.ml | 2 ++ .../components/ng_refiner/nCicCoercion.ml | 2 -- .../components/ng_tactics/nTactics.ml | 13 ++++++++ .../components/ng_tactics/nTactics.mli | 2 ++ .../matita/nlibrary/sets/partitions.ma | 31 +++++++------------ helm/software/matita/nlibrary/sets/sets.ma | 17 +++++----- 9 files changed, 48 insertions(+), 35 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 8d0679230..5c8f461c1 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -56,10 +56,12 @@ type ntactic = | NCase1 of loc * string | NChange of loc * npattern * CicNotationPt.term | NConstructor of loc * int option * CicNotationPt.term list + | NCut of loc * CicNotationPt.term | NElim of loc * CicNotationPt.term * npattern | NGeneralize of loc * npattern | NId of loc | NIntro of loc * string + | NLApply of loc * CicNotationPt.term | NLetIn of loc * npattern * CicNotationPt.term * string | NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern | NRewrite of loc * direction * CicNotationPt.term * npattern diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index e21f98c27..3d6b86492 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -96,6 +96,11 @@ let rec pp_ntactic ~map_unicode_to_tex = pp_tactic_pattern ~map_unicode_to_tex ~lazy_term_pp ~term_pp in function | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t + | NAuto (_,(l,flgs)) -> + "nauto" ^ + (if l <> [] then (" by " ^ + (String.concat "," (List.map CicNotationPp.pp_term l))) else "") ^ + String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs) | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^ assert false ^ " " ^ assert false | NConstructor (_,None,l) -> "@ " ^ @@ -105,18 +110,15 @@ let rec pp_ntactic ~map_unicode_to_tex = | NCase1 (_,n) -> "*" ^ n ^ ":" | NChange (_,what,wwhat) -> "nchange " ^ assert false ^ " with " ^ CicNotationPp.pp_term wwhat + | NCut (_,t) -> "ncut " ^ CicNotationPp.pp_term t | NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^ assert false ^ " " ^ assert false | NId _ -> "nid" | NIntro (_,n) -> "#" ^ n + | NLApply (_,t) -> "lapply " ^ CicNotationPp.pp_term t | NRewrite (_,dir,n,where) -> "nrewrite " ^ (match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^ " " ^ CicNotationPp.pp_term n ^ " " ^ pp_tactic_pattern where - | NAuto (_,(l,flgs)) -> - "nauto" ^ - (if l <> [] then (" by " ^ - (String.concat "," (List.map CicNotationPp.pp_term l))) else "") ^ - String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs) | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> "TO BE IMPLEMENTED" | NDot _ -> "##." | NSemicolon _ -> "##;" diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 7e314670b..f7df56315 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -656,6 +656,7 @@ let eval_ng_tac tac = | GrafiteAst.NConstructor (_loc,num,args) -> NTactics.constructor_tac ?num ~args:(List.map (fun x -> text,prefix_len,x) args) + | GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t) | GrafiteAst.NDot _ -> NTactics.dot_tac | GrafiteAst.NElim (_loc, what, where) -> NTactics.elim_tac @@ -666,6 +667,7 @@ let eval_ng_tac tac = NTactics.generalize_tac ~where:(text,prefix_len,where) | GrafiteAst.NId _ -> (fun x -> x) | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n + | GrafiteAst.NLApply (_loc, t) -> NTactics.lapply_tac (text,prefix_len,t) | GrafiteAst.NLetIn (_loc,where,what,name) -> NTactics.letin_tac ~where:(text,prefix_len,where) ~what:(text,prefix_len,what) name diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 6b80c32cf..c9ece6dba 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -256,10 +256,12 @@ EXTEND | SYMBOL "@"; num = OPT NUMBER; l = LIST0 tactic_term -> G.NConstructor (loc, (match num with None -> None | Some x -> Some (int_of_string x)),l) + | IDENT "ncut"; t = tactic_term -> G.NCut (loc, t) | IDENT "nelim"; what = tactic_term ; where = pattern_spec -> G.NElim (loc, what, where) | IDENT "ngeneralize"; p=pattern_spec -> G.NGeneralize (loc, p) + | IDENT "nlapply"; t = tactic_term -> G.NLApply (loc, t) | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode> ; t = tactic_term; where = pattern_spec -> G.NLetIn (loc,where,t,name) diff --git a/helm/software/components/ng_refiner/nCicCoercion.ml b/helm/software/components/ng_refiner/nCicCoercion.ml index 037c5c6e2..7d5d0101a 100644 --- a/helm/software/components/ng_refiner/nCicCoercion.ml +++ b/helm/software/components/ng_refiner/nCicCoercion.ml @@ -46,13 +46,11 @@ class status = let index_coercion status name c src tgt arity arg = let db_src,db_tgt = status#coerc_db in let data = (name,c,arity,arg,src,tgt) in - debug (lazy ("INDEX:" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] src ^ " ===> " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] tgt ^ " := " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] c ^ " " ^ string_of_int arg ^ " " ^ string_of_int arity)); - let db_src = DB.index db_src src data in let db_tgt = DB.index db_tgt tgt data in status#set_coerc_db (db_src, db_tgt) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index b3f05293f..0ba8e4b44 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -402,6 +402,19 @@ let generalize_tac ~where = ) s) ] ;; +let cut_tac t = + block_tac [ + exact_tac ("",0, Ast.Appl [Ast.Implicit `JustOne; Ast.Implicit `JustOne]); + branch_tac; + pos_tac [2]; exact_tac t; + shift_tac; pos_tac [1]; skip_tac; + merge_tac ] +;; + +let lapply_tac (s,n,t) = + exact_tac (s,n, Ast.Appl [Ast.Implicit `JustOne; t]) +;; + let reduce_tac ~reduction ~where = let change status t = match reduction with diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index 4e21cbb45..9afd918ea 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -32,6 +32,7 @@ val assumption_tac: 's NTacStatus.tactic val change_tac: where:NTacStatus.tactic_pattern -> with_what:NTacStatus.tactic_term -> 's NTacStatus.tactic +val cut_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic val elim_tac: what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic @@ -40,6 +41,7 @@ val cases_tac: what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> 's NTacStatus.tactic val case1_tac: string -> 's NTacStatus.tactic +val lapply_tac: NTacStatus.tactic_term -> 's NTacStatus.tactic val rewrite_tac: dir:[ `LeftToRight | `RightToLeft ] -> what:NTacStatus.tactic_term -> where:NTacStatus.tactic_pattern -> diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index e83175f18..e33ddfa1d 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -22,11 +22,6 @@ include "datatypes/pairs.ma". alias symbol "eq" = "setoid eq". alias symbol "eq" = "setoid1 eq". alias symbol "eq" = "setoid eq". -alias symbol "eq" = "setoid1 eq". -alias symbol "eq" = "setoid eq". -alias symbol "eq" = "setoid1 eq". -alias symbol "eq" = "setoid eq". -alias symbol "eq" = "setoid1 eq". nrecord partition (A: setoid) : Type[1] ≝ { support: setoid; indexes: qpowerclass support; @@ -63,7 +58,6 @@ naxiom ad_hoc15: ∀a,a',b,c. a=a' → b < c → a + b < c + a'. naxiom ad_hoc16: ∀a,b,c. a < c → a < b + c. naxiom not_lt_to_le: ∀a,b. ¬ (a < b) → b ≤ a. naxiom le_to_le_S_S: ∀a,b. a ≤ b → S a ≤ S b. -naxiom minus_S_S: ∀a,b. S a - S b = a - b. naxiom minus_S: ∀n. S n - n = S O. naxiom ad_hoc17: ∀a,b,c,d,d'. a+c+d=b+c+d' → a+d=b+d'. naxiom split_big_plus: @@ -81,8 +75,8 @@ ntheorem iso_nat_nat_union_char: fst … p ≤ n ∧ snd … p < s (fst … p). #n; #s; nelim n [ #m; nwhd in ⊢ (??% → let p ≝ % in ?); nwhd in ⊢ (??(??%) → ?); - nrewrite > (plus_n_O (s O)); #H; nrewrite > (ltb_t … H); nnormalize; - napply conj [ napply conj [ napply refl | napply le_n ] ##| nassumption ] + nrewrite > (plus_n_O (s O)); #H; nrewrite > (ltb_t … H); nnormalize; @ + [ @ [ napply refl | napply le_n ] ##| nassumption ] ##| #n'; #Hrec; #m; nwhd in ⊢ (??% → let p ≝ % in ?); #H; ncases (ltb_cases m (s (S n'))); *; #H1; #H2; nrewrite > H2; nwhd in ⊢ (let p ≝ % in ?); nwhd @@ -91,10 +85,10 @@ ntheorem iso_nat_nat_union_char: | nnormalize; napply le_n] ##| nnormalize; nassumption ] ##| nchange in H with (m < s (S n') + big_plus (S n') (λi.λ_.s i)); - ngeneralize in match (Hrec (m - s (S n')) ?) in ⊢ ? - [##2: napply ad_hoc9; nassumption] *; *; #Hrec1; #Hrec2; #Hrec3; napply conj + nlapply (Hrec (m - s (S n')) ?) + [ napply ad_hoc9; nassumption] *; *; #Hrec1; #Hrec2; #Hrec3; @ [##2: nassumption - |napply conj + |@ [nrewrite > (split_big_plus …); ##[##2:napply ad_hoc11;##|##3:##skip] nrewrite > (ad_hoc12 …); ##[##2: nassumption] nwhd in ⊢ (????(?(??%)?)); @@ -135,17 +129,16 @@ nlemma partition_splits_card: ∀A. ∀P:partition A. ∀n,s. ∀f:isomorphism ?? (Nat_ n) (indexes ? P). (∀i. isomorphism ?? (Nat_ (s i)) (class ? P (iso_f ???? f i))) → - (isomorphism ?? (Nat_ (big_plus n (λi.λ_.s i))) (Full_set A)). - STOP #A; #P; #Sn; ncases Sn - [ #s; #f; #fi; - ngeneralize in match (covers ? P) in ⊢ ?; *; #_; #H; + (isomorphism ?? (Nat_ (big_plus n (λi.λ_.s i))) A). + #A; #P; #Sn; ncases Sn + [ #s; #f; #fi; nlapply (covers ? P); *; #_; #H; (* - ngeneralize in match - (big_union_preserves_iso ??? (indexes A P) (Nat_ O) (λx.class ? P x) f) in ⊢ ?; + nlapply + (big_union_preserves_iso ??? (indexes A P) (Nat_ O) (λx.class ? P x) f); *; #K; #_; nwhd in K: (? → ? → %);*) nelim daemon (* impossibile *) - | #n; #s; #f; #fi; napply mk_isomorphism - [ napply mk_unary_morphism + | #n; #s; #f; #fi; @ + [ @ [ napply (λm.let p ≝ iso_nat_nat_union s m n in iso_f ???? (fi (fst … p)) (snd … p)) | #a; #a'; #H; nrewrite < H; napply refl ] ##| #x; #Hx; nwhd; napply I diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index 89650db96..f3bd3b889 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -52,13 +52,13 @@ nqed. include "properties/relations1.ma". ndefinition seteq: ∀A. equivalence_relation1 (Ω^A). - #A; napply mk_equivalence_relation1 + #A; @ [ napply (λS,S'. S ⊆ S' ∧ S' ⊆ S) | #S; @; napply subseteq_refl | #S; #S'; *; #H1; #H2; @; nassumption | #S; #T; #U; *; #H1; #H2; *; #H3; #H4; @; napply subseteq_trans; ##[##2,5: nassumption |##1,4: ##skip |##*: nassumption]##] -nqed. +nqed. include "sets/setoids1.ma". @@ -83,10 +83,9 @@ nrecord qpowerclass (A: setoid) : Type[1] ≝ }. ndefinition Full_set: ∀A. qpowerclass A. - #A; @ - [ napply (full_set A) - | #x; #x'; #H; napply refl1; ##] + #A; @[ napply A | #x; #x'; #H; napply refl1] nqed. +ncoercion Full_set: ∀A. qpowerclass A ≝ Full_set on A: setoid to qpowerclass ?. ndefinition qseteq: ∀A. equivalence_relation1 (qpowerclass A). #A; @ @@ -108,7 +107,7 @@ unification hint 0 ≔ A ⊢ nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) CPROP. #A; @ [ napply (λx,S. x ∈ S) - | #a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; napply mk_iff; #H; + | #a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; @; #H; ##[ napply Hb1; napply (. (mem_ok' …)); ##[##3: napply H| napply Ha^-1;##] ##| napply Hb2; napply (. (mem_ok' …)); ##[##3: napply H| napply Ha;##] ##] @@ -121,7 +120,7 @@ unification hint 0 ≔ nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP. #A; @ [ napply (λS,S'. S ⊆ S') - | #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; napply mk_iff; #H + | #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #H [ napply (subseteq_trans … a) [ nassumption | napply (subseteq_trans … b); nassumption ] ##| napply (subseteq_trans … a') @@ -132,7 +131,7 @@ nlemma intersect_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_ #A; @ [ #S; #S'; @ [ napply (S ∩ S') - | #a; #a'; #Ha; nwhd in ⊢ (? ? ? % %); napply mk_iff; *; #H1; #H2; @ + | #a; #a'; #Ha; nwhd in ⊢ (? ? ? % %); @; *; #H1; #H2; @ [##1,2: napply (. (mem_ok' …)^-1) [##3,6: nassumption |##2,5: nassumption |##*: ##skip] ##|##3,4: napply (. (mem_ok' …)) [##1,3,4,6: nassumption |##*: ##skip]##]##] ##| #a; #a'; #b; #b'; #Ha; #Hb; nwhd; @; #x; nwhd in ⊢ (% → %); #H @@ -182,7 +181,7 @@ nqed. ndefinition eqrel_of_morphism: ∀A,B. unary_morphism A B → compatible_equivalence_relation A. - #A; #B; #f; napply mk_compatible_equivalence_relation + #A; #B; #f; @ [ @ [ napply (λx,y. f x = f y) | #x; napply refl | #x; #y; napply sym | #x; #y; #z; napply trans] -- 2.39.2