From: Enrico Tassi Date: Tue, 8 Sep 2009 18:48:55 +0000 (+0000) Subject: snapshot for CSC X-Git-Tag: make_still_working~3493 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f5f35ef830b1335dad2fcc3c1aae2b57815f73b1;p=helm.git snapshot for CSC --- diff --git a/helm/software/matita/matitaGtkMisc.ml b/helm/software/matita/matitaGtkMisc.ml index 872780540..772f17a41 100644 --- a/helm/software/matita/matitaGtkMisc.ml +++ b/helm/software/matita/matitaGtkMisc.ml @@ -398,14 +398,14 @@ let utf8_parsed_text s floc = let start, stop = HExtlib.loc_of_floc floc in let start_bytes = Glib.Utf8.offset_to_pos s ~pos:0 ~off:start in let stop_bytes = Glib.Utf8.offset_to_pos s ~pos:0 ~off:stop in - assert(stop_bytes >= start_bytes); + if (stop_bytes < start_bytes) then + Printf.sprintf "ERROR (%d > %d)" start_bytes stop_bytes, 0 + else let bytes = stop_bytes - start_bytes in try String.sub s start_bytes bytes, bytes with Invalid_argument _ -> - Printf.eprintf "%s/%d/%d\n" s start_bytes bytes; - assert false - + Printf.sprintf "ERROR (%s/%d/%d)" s start_bytes bytes, 0 let utf8_string_length s = if BuildTimeConf.debug then diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma index 24203f209..775cbd390 100644 --- a/helm/software/matita/nlibrary/algebra/magmas.ma +++ b/helm/software/matita/nlibrary/algebra/magmas.ma @@ -24,9 +24,14 @@ nrecord magma (A: magma_type) : Type[1] ≝ op_closed: ∀x,y. x ∈ mcarr → y ∈ mcarr → op A x y ∈ mcarr }. +unification hint 0 ≔ + A : ? ⊢ carr1 (qpowerclass_setoid A) ≡ qpowerclass A. + +(* ncoercion mcarr' : ∀A. ∀M: magma A. carr1 (qpowerclass_setoid (mtcarr A)) ≝ λA.λM: magma A.mcarr ? M on _M: magma ? to carr1 (qpowerclass_setoid (mtcarr ?)). +*) nrecord magma_morphism_type (A,B: magma_type) : Type[0] ≝ { mmcarr:> unary_morphism A B; diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends index 301939368..105946ce0 100644 --- a/helm/software/matita/nlibrary/depends +++ b/helm/software/matita/nlibrary/depends @@ -1,4 +1,4 @@ -logic/cprop.ma sets/setoids1.ma +logic/cprop.ma hints_declaration.ma sets/setoids1.ma sets/sets.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma topology/igft.ma logic/connectives.ma datatypes/bool.ma logic/pts.ma @@ -17,6 +17,7 @@ nat/big_ops.ma algebra/magmas.ma nat/order.ma nat/nat.ma logic/equality.ma sets/setoids.ma properties/relations.ma logic/pts.ma nat/compare.ma datatypes/bool.ma nat/order.ma +hints_declaration.ma logic/pts.ma logic/pts.ma nat/order.ma nat/nat.ma sets/sets.ma algebra/unital_magmas.ma algebra/magmas.ma diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot index ec3b85946..521bb637d 100644 --- a/helm/software/matita/nlibrary/depends.dot +++ b/helm/software/matita/nlibrary/depends.dot @@ -1,5 +1,6 @@ digraph g { "logic/cprop.ma" []; + "logic/cprop.ma" -> "hints_declaration.ma" []; "logic/cprop.ma" -> "sets/setoids1.ma" []; "sets/sets.ma" []; "sets/sets.ma" -> "logic/connectives.ma" []; @@ -48,6 +49,8 @@ digraph g { "nat/compare.ma" []; "nat/compare.ma" -> "datatypes/bool.ma" []; "nat/compare.ma" -> "nat/order.ma" []; + "hints_declaration.ma" []; + "hints_declaration.ma" -> "logic/pts.ma" []; "logic/pts.ma" []; "nat/order.ma" []; "nat/order.ma" -> "nat/nat.ma" []; diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png index fe86e43b3..04d00a692 100644 Binary files a/helm/software/matita/nlibrary/depends.png and b/helm/software/matita/nlibrary/depends.png differ diff --git a/helm/software/matita/nlibrary/hints_declaration.ma b/helm/software/matita/nlibrary/hints_declaration.ma new file mode 100644 index 000000000..29d17382b --- /dev/null +++ b/helm/software/matita/nlibrary/hints_declaration.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "logic/pts.ma". +ndefinition hint_declaration_Type0 ≝ λA:Type[0] .λa,b:A.a. +ndefinition hint_declaration_Type1 ≝ λA:Type[1].λa,b:A.a. +ndefinition hint_declaration_Type2 ≝ λa,b:Type[1].a. +ndefinition hint_declaration_CProp0 ≝ λA:CProp[0].λa,b:A.a. +ndefinition hint_declaration_CProp1 ≝ λA:CProp[1].λa,b:A.a. +ndefinition hint_declaration_CProp2 ≝ λa,b:CProp[1].a. + +notation > "≔ (list0 (ident x : T )sep ,) ⊢ term 19 Px ≡ term 19 Py" + with precedence 90 + for @{ ${ fold right @{'hint_decl $Px $Py} rec acc @{ ∀${ident x}:$T.$acc } } }. + +interpretation "hint_decl_Type2" 'hint_decl a b = (hint_declaration_Type2 a b). +interpretation "hint_decl_CProp2" 'hint_decl a b = (hint_declaration_CProp2 a b). +interpretation "hint_decl_Type1" 'hint_decl a b = (hint_declaration_Type1 ? a b). +interpretation "hint_decl_CProp1" 'hint_decl a b = (hint_declaration_CProp1 ? a b). +interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a b). +interpretation "hint_decl_Type0" 'hint_decl a b = (hint_declaration_Type0 ? a b). diff --git a/helm/software/matita/nlibrary/logic/cprop.ma b/helm/software/matita/nlibrary/logic/cprop.ma index d006599ed..339f73356 100644 --- a/helm/software/matita/nlibrary/logic/cprop.ma +++ b/helm/software/matita/nlibrary/logic/cprop.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "hints_declaration.ma". include "sets/setoids1.ma". ndefinition CPROP: setoid1. @@ -25,7 +26,8 @@ ndefinition CPROP: setoid1. [ napply (H3 (H1 w)) | napply (H2 (H4 w))]##]##] nqed. -unification hint 0 ((λx,y.True) (carr1 CPROP) CProp[0]). +alias symbol "hint_decl" = "hint_decl_CProp2". +unification hint 0 ≔ ⊢ CProp[0] ≡ carr1 CPROP. (*ndefinition CProp0_of_CPROP: carr1 CPROP → CProp[0] ≝ λx.x. ncoercion CProp0_of_CPROP : ∀x: carr1 CPROP. CProp[0] ≝ CProp0_of_CPROP diff --git a/helm/software/matita/nlibrary/nat/nat.ma b/helm/software/matita/nlibrary/nat/nat.ma index 362a5ad36..e9d32973b 100644 --- a/helm/software/matita/nlibrary/nat/nat.ma +++ b/helm/software/matita/nlibrary/nat/nat.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "hints_declaration.ma". include "logic/equality.ma". include "sets/setoids.ma". @@ -23,4 +24,5 @@ ndefinition NAT: setoid. napply mk_setoid [ napply nat | napply EQ] nqed. -unification hint 0 ((λx,y.True) (carr NAT) nat). +alias symbol "hint_decl" = "hint_decl_Type1". +unification hint 0 ≔ ⊢ carr NAT ≡ nat. diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index c5771028d..3b17099a3 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -18,14 +18,7 @@ include "nat/compare.ma". include "nat/minus.ma". 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". + alias symbol "eq" = "setoid eq". alias symbol "eq" = "setoid1 eq". alias symbol "eq" = "setoid eq". @@ -101,25 +94,15 @@ ntheorem iso_nat_nat_union_char: [##2: napply ad_hoc9; nassumption] *; *; #Hrec1; #Hrec2; #Hrec3; napply conj [##2: nassumption |napply conj - [napply (eq_rect_CProp0_r ?? (λx.λ_. m = x + snd … (iso_nat_nat_union s (m - s (S n')) n')) ?? - (split_big_plus - (S n' - fst … (iso_nat_nat_union s (m - s (S n')) n')) - (n' - fst … (iso_nat_nat_union s (m - s (S n')) n')) - (λi.λ_.s (S (i + fst … (iso_nat_nat_union s (m - s (S n')) n'))))?)) - [##2: napply ad_hoc11] - napply (eq_rect_CProp0_r ?? (λx.λ_. ? = ? + big_plus x (λ_.λ_:? < x.?) + ?) - ?? (ad_hoc12 n' (fst … (iso_nat_nat_union s (m - s (S n')) n')) ?)) - [##2: nassumption] - nwhd in ⊢ (???(?(??%)?)); - nrewrite > (ad_hoc13 n' (fst … (iso_nat_nat_union s (m - s (S n')) n')) ?) - [##2: nassumption] + [nrewrite > (split_big_plus …); ##[##2:napply ad_hoc11;##|##3:##skip] + nrewrite > (ad_hoc12 …); ##[##2: nassumption] + nwhd in ⊢ (????(?(??%)?)); + nrewrite > (ad_hoc13 …);##[##2: nassumption] napply ad_hoc14 [ napply not_lt_to_le; nassumption ] nwhd in ⊢ (???(?(??%)?)); - napply (eq_rect_CProp0_r ?? (λx.λ_. ? = x + ?) ?? - (plus_n_O (big_plus (n' - fst … (iso_nat_nat_union s (m - s (S n')) n')) - (λi.λ_.s (S (i + fst … (iso_nat_nat_union s (m - s (S n')) n'))))))); - nassumption - | napply le_S; nassumption ]##]##]##] + nrewrite > (plus_n_O …); + nassumption; + ##| napply le_S; nassumption ]##]##]##] nqed. ntheorem iso_nat_nat_union_pre: @@ -130,7 +113,11 @@ ntheorem iso_nat_nat_union_pre: nrewrite > (split_big_plus (S n) (S i1) (λi.λ_.s i) ?) [##2: napply le_to_le_S_S; nassumption] napply ad_hoc15 - [ nrewrite > (minus_S_S n i1 …); napply big_plus_preserves_ext; #i; #_; + [ nwhd in ⊢ (???(?%?)); + + napply (eq_rect_CProp0_r nat (n - i1) (λx.λy.?) ?? (minus_S_S …)); STOP + + nrewrite > (minus_S_S n i1); napply big_plus_preserves_ext; #i; #_; nrewrite > (plus_n_S i i1); napply refl | nrewrite > (split_big_plus (S i1) i1 (λi.λ_.s i) ?) [##2: napply le_S; napply le_n] napply ad_hoc16; nrewrite > (minus_S i1); nnormalize; nrewrite > (plus_n_O (s i1) …); @@ -151,7 +138,7 @@ nlemma partition_splits_card: ∀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)). - #A; #P; #Sn; ncases Sn + STOP #A; #P; #Sn; ncases Sn [ #s; #f; #fi; ngeneralize in match (covers ? P) in ⊢ ?; *; #_; #H; (* diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index 4579054c5..2f0725d85 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -1,3 +1,4 @@ + (**************************************************************************) (* ___ *) (* ||M|| *) @@ -39,8 +40,7 @@ ndefinition big_union ≝ λA,B.λT:Ω \sup A.λf:A → Ω \sup B.{ x | ∃i. i ndefinition big_intersection ≝ λA,B.λT:Ω \sup A.λf:A → Ω \sup B.{ x | ∀i. i ∈ T → x ∈ f i }. ndefinition full_set: ∀A. Ω \sup A ≝ λA.{ x | True }. -(* bug dichiarazione coercion qui *) -(* ncoercion full_set : ∀A:Type[0]. Ω \sup A ≝ full_set on _A: Type[0] to (Ω \sup ?). *) +ncoercion full_set : ∀A:Type[0]. Ω \sup A ≝ full_set on A: Type[0] to (Ω \sup ?). nlemma subseteq_refl: ∀A.∀S: Ω \sup A. S ⊆ S. #A; #S; #x; #H; nassumption. @@ -69,27 +69,29 @@ ndefinition powerclass_setoid: Type[0] → setoid1. | napply seteq ] nqed. -unification hint 0 (∀A. (λx,y.True) (carr1 (powerclass_setoid A)) (Ω \sup A)). +include "hints_declaration.ma". + +alias symbol "hint_decl" = "hint_decl_Type2". +unification hint 0 ≔ A : ? ⊢ carr1 (powerclass_setoid A) ≡ Ω^A. (************ SETS OVER SETOIDS ********************) include "logic/cprop.ma". nrecord qpowerclass (A: setoid) : Type[1] ≝ - { pc:> Ω \sup A; + { pc:> Ω^A; mem_ok': ∀x,x':A. x=x' → (x ∈ pc) = (x' ∈ pc) }. ndefinition Full_set: ∀A. qpowerclass A. #A; napply mk_qpowerclass [ napply (full_set A) - | #x; #x'; #H; nnormalize in ⊢ (?%?%%); (* bug universi qui napply refl1;*) - napply mk_iff; #K; nassumption ] + | #x; #x'; #H; napply refl1; ##] nqed. ndefinition qseteq: ∀A. equivalence_relation1 (qpowerclass A). #A; napply mk_equivalence_relation1 - [ napply (λS,S':qpowerclass A. eq_rel1 ? (eq1 (powerclass_setoid A)) S S') + [ napply (λS,S':qpowerclass A. S = S') | #S; napply (refl1 ? (seteq A)) | #S; #S'; napply (sym1 ? (seteq A)) | #S; #T; #U; napply (trans1 ? (seteq A))] @@ -101,31 +103,29 @@ ndefinition qpowerclass_setoid: setoid → setoid1. | napply (qseteq A) ] nqed. -unification hint 0 (∀A. (λx,y.True) (carr1 (qpowerclass_setoid A)) (qpowerclass A)). -ncoercion qpowerclass_hint: ∀A: setoid. ∀S: qpowerclass_setoid A. Ω \sup A ≝ λA.λS.S - on _S: (carr1 (qpowerclass_setoid ?)) to (Ω \sup ?). +unification hint 0 ≔ A : ? ⊢ carr1 (qpowerclass_setoid A) ≡ qpowerclass A. nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) CPROP. #A; napply mk_binary_morphism1 - [ napply (λx.λS: qpowerclass_setoid A. x ∈ S) (* CSC: ??? *) - | #a; #a'; #b; #b'; #Ha; #Hb; (* CSC: qui *; non funziona *) - nwhd; nwhd in ⊢ (? (? % ??) (? % ??)); napply mk_iff; #H - [ ncases Hb; #Hb1; #_; napply Hb1; napply (. (mem_ok' …)) - [ nassumption | napply Ha^-1 | ##skip ] - ##| ncases Hb; #_; #Hb2; napply Hb2; napply (. (mem_ok' …)) - [ nassumption | napply Ha | ##skip ]##] + [ #x; napply (λS: qpowerclass_setoid ?. x ∈ S) (* ERROR CSC: ??? *) + | #a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; napply mk_iff; #H; + ##[ napply Hb1; napply (. (mem_ok' …)); ##[##3: napply H| napply Ha^-1;##] + ##| napply Hb2; napply (. (mem_ok' …)); ##[##3: napply H| napply Ha;##] + ##] + ##] nqed. -unification hint 0 (∀A,x,S. (λx,y.True) (fun21 ??? (mem_ok A) x S) (mem A S x)). +unification hint 0 ≔ + A : setoid, x : ?, S : ? ⊢ (mem_ok A) x S ≡ mem A S x. nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP. #A; napply mk_binary_morphism1 [ napply (λS,S': qpowerclass_setoid ?. S ⊆ S') | #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; napply mk_iff; #H - [ napply (subseteq_trans … a' a) (* anche qui, perche' serve a'? *) - [ nassumption | napply (subseteq_trans … a b); nassumption ] - ##| napply (subseteq_trans … a a') (* anche qui, perche' serve a'? *) - [ nassumption | napply (subseteq_trans … a' b'); nassumption ] ##] + [ napply (subseteq_trans … a) + [ nassumption | napply (subseteq_trans … b); nassumption ] + ##| napply (subseteq_trans … a') + [ nassumption | napply (subseteq_trans … b'); nassumption ] ##] nqed. nlemma intersect_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) (qpowerclass_setoid A). @@ -133,14 +133,17 @@ nlemma intersect_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_ [ #S; #S'; napply mk_qpowerclass [ napply (S ∩ S') | #a; #a'; #Ha; nwhd in ⊢ (? ? ? % %); napply mk_iff; *; #H1; #H2; napply conj - [##1,2: napply (. (mem_ok' …)^-1) [##3,6: nassumption |##1,4: nassumption |##*: ##skip] - ##|##3,4: napply (. (mem_ok' …)) [##2,5: nassumption |##1,4: nassumption |##*: ##skip]##]##] + [##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; napply conj; #x; nwhd in ⊢ (% → %); #H [ napply (. ((#‡Ha^-1)‡(#‡Hb^-1))); nassumption | napply (. ((#‡Ha)‡(#‡Hb))); nassumption ]##] nqed. -unification hint 0 (∀A.∀U,V.(λx,y.True) (fun21 ??? (intersect_ok A) U V) (intersect A U V)). +(* +unification hint 0 ≔ + A : setoid, U : qpowerclass_setoid A, V : ? ⊢ (intersect_ok A) U V ≡ U ∩ V. + *) nlemma test: ∀A:setoid. ∀U,V:qpowerclass A. ∀x,x':setoid1_of_setoid A. x=x' → x ∈ U ∩ V → x' ∈ U ∩ V. #A; #U; #V; #x; #x'; #H; #p; diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index 1fb59f067..6628e36ef 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -74,6 +74,9 @@ nlet corec fish_rec (A:axiom_set) (U: Ω^A) nqed. (* +alias symbol "covers" (instance 0) = "covers". +alias symbol "covers" (instance 2) = "covers". +alias symbol "covers" (instance 1) = "covers set". ntheorem covers_elim2: ∀A: axiom_set. ∀U:Ω^A.∀P: A → CProp[0]. (∀a:A. a ∈ U → P a) → @@ -101,6 +104,8 @@ nelim aU; ##] nqed. +STOP + definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {y|b=y}. interpretation "covered by one" 'leq a b = (leq ? a b).