From 32af98424d4320a4a38fff23ac0398e026fe0ffc Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 28 Sep 2009 19:27:14 +0000 Subject: [PATCH 1/1] non ho resistito! --- .../matita/nlibrary/sets/partitions.ma | 31 +++---- helm/software/matita/nlibrary/sets/sets.ma | 80 ++++++++++++++++--- .../software/matita/nlibrary/topology/igft.ma | 20 +++-- 3 files changed, 92 insertions(+), 39 deletions(-) diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index 93f9cd6b5..c1092c497 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -25,6 +25,7 @@ alias symbol "eq" = "setoid 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; @@ -165,28 +166,28 @@ napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##] nlapply (iso_nat_nat_union_uniq n s nindex (fst … (iso_nat_nat_union s xxx n)) nindex2 (snd … (iso_nat_nat_union s xxx n)) ?????) - [##2: *; #E1; #E2; nrewrite > E1; nrewrite > E2; napply refl - | napply le_S_S_to_le; nassumption + [##6: *; #E1; #E2; nrewrite > E1; nrewrite > E2; napply refl + |##5: napply le_S_S_to_le; nassumption |##*: nassumption]##] ##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx'; #E; - ngeneralize in match (? : ∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ pc ? (Nat_ (s i1)) → i2' ∈ pc ? (Nat_ (s i1')) → eq_rel (carr A) (eq A) (iso_f ???? (fi i1) i2) (iso_f ???? (fi i1') i2') → i1=i1' ∧ i2=i2') in ⊢ ? - [##2: #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E; - ngeneralize in match (disjoint ? P (iso_f ???? f i1) (iso_f ???? f i1') ???) in ⊢ ? + ncut(∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ pc ? (Nat_ (s i1)) → i2' ∈ pc ? (Nat_ (s i1')) → eq_rel (carr A) (eq A) (iso_f ???? (fi i1) i2) (iso_f ???? (fi i1') i2') → i1=i1' ∧ i2=i2'); + ##[ #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E; + nlapply(disjoint … P (f i1) (f i1') ???) [##2,3: napply f_closed; nassumption - |##4: napply ex_intro [ napply (iso_f ???? (fi i1) i2) ] napply conj - [ napply f_closed; nassumption ##| napply (. ?‡#) [ nassumption | ##2: ##skip] - nwhd; napply f_closed; nassumption]##] - #E'; ngeneralize in match (? : i1=i1') in ⊢ ? - [##2: napply (f_inj … E'); nassumption - | #E''; nrewrite < E''; napply conj - [ napply refl | nrewrite < E'' in E; #E'''; napply (f_inj … E''') + |##1: @ (fi i1 i2); @; + ##[ napply f_closed; nassumption ##| napply (. E‡#); + nwhd; napply f_closed; nassumption]##] + #E'; ncut(i1 = i1'); ##[ napply (f_inj … E'); nassumption; ##] + #E''; nrewrite < E''; @; + ##[ @; + ##| nrewrite < E'' in E; #E'''; napply (f_inj … E''') [ nassumption | nrewrite > E''; nassumption ]##]##] ##] #K; nelim (iso_nat_nat_union_char n s x Hx); *; #i1x; #i2x; #i3x; nelim (iso_nat_nat_union_char n s x' Hx'); *; #i1x'; #i2x'; #i3x'; - ngeneralize in match (K … E) in ⊢ ? - [##2,3: napply le_to_le_S_S; nassumption - |##4,5: nassumption] + nlapply (K … E) + [##1,2: nassumption; + ##|##3,4:napply le_to_le_S_S; nassumption; ##] *; #K1; #K2; napply (eq_rect_CProp0_r ?? (λX.λ_.? = X) ?? i1x'); napply (eq_rect_CProp0_r ?? (λX.λ_.X = ?) ?? i1x); diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index c4fc89f21..965217737 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -102,13 +102,13 @@ ndefinition qpowerclass_setoid: setoid → setoid1. [ napply (qpowerclass A) | napply (qseteq A) ] nqed. - + unification hint 0 ≔ A ⊢ - carr1 (qpowerclass_setoid A) ≡ qpowerclass A. + carr1 (mk_setoid1 (qpowerclass A) (eq1 (qpowerclass_setoid A))) +≡ qpowerclass A. -(*CSC: non va! -unification hint 0 ≔ A ⊢ - carr1 (mk_setoid1 (qpowerclass A) (eq1 (qpowerclass_setoid A))) ≡ qpowerclass A.*) +ncoercion pc' : ∀A.∀x:qpowerclass_setoid A. Ω^A ≝ pc +on _x : (carr1 (qpowerclass_setoid ?)) to (Ω^?). nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) CPROP. #A; @ @@ -120,15 +120,15 @@ nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid ##] nqed. -(*CSC: bug qui se metto x o S al posto di ? -nlemma foo: True. -nletin xxx ≝ (λA:setoid.λx,S. let SS ≝ pc ? S in - fun21 ??? (mk_binary_morphism1 ??? (λx.λS. ? ∈ ?) (prop21 ??? (mem_ok A))) x S); -*) unification hint 0 ≔ A:setoid, x, S; - SS ≟ (pc ? S) + SS ≟ (pc ? S), + TT ≟ (mk_binary_morphism1 ??? + (λx:setoid1_of_setoid ?.λS:qpowerclass_setoid ?. x ∈ S) + (prop21 ??? (mem_ok A))) + (*-------------------------------------*) ⊢ - fun21 ??? (mk_binary_morphism1 ??? (λx,S. x ∈ S) (prop21 ??? (mem_ok A))) x S ≡ mem A SS x. + fun21 ? ? ? TT x S + ≡ mem A SS x. nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP. #A; @ @@ -144,6 +144,53 @@ unification hint 0 ≔ A,a,a' (*-----------------------------------------------------------------*) ⊢ eq_rel ? (eq A) a a' ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) a a'. +nlemma intersect_ok: ∀A. qpowerclass A → qpowerclass A → qpowerclass A. + #A; #S; #S'; @ (S ∩ S'); + #a; #a'; #Ha; @; *; #H1; #H2; @ + [##1,2: napply (. Ha^-1‡#); nassumption; +##|##3,4: napply (. Ha‡#); nassumption] +nqed. + +alias symbol "hint_decl" = "hint_decl_Type1". +unification hint 1 ≔ + A : setoid, B,C : qpowerclass A ⊢ + pc A (mk_qpowerclass ? (B ∩ C) (mem_ok' ? (intersect_ok ? B C))) + ≡ intersect ? (pc ? B) (pc ? C). + +nlemma intersect_ok': ∀A. binary_morphism1 (powerclass_setoid A) (powerclass_setoid A) (powerclass_setoid A). + #A; @ (λS,S'. S ∩ S'); + #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #x; nnormalize; *; #Ka; #Kb; @ + [ napply Ha1; nassumption + | napply Hb1; nassumption + | napply Ha2; nassumption + | napply Hb2; nassumption] +nqed. + +alias symbol "hint_decl" = "hint_decl_Type1". +unification hint 0 ≔ + A : Type[0], B,C : powerclass A ⊢ + fun21 … + (mk_binary_morphism1 … + (λS,S'.S ∩ S') + (prop21 … (intersect_ok' A))) B C + ≡ intersect ? B C. + +ndefinition prop21_mem : + ∀A,C.∀f:binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) C. + ∀a,a':setoid1_of_setoid A. + ∀b,b':qpowerclass_setoid A.a = a' → b = b' → f a b = f a' b'. +#A; #C; #f; #a; #a'; #b; #b'; #H1; #H2; napply prop21; nassumption; +nqed. + +interpretation "prop21 mem" 'prop2 l r = (prop21_mem ??????? l r). + + +nlemma test: ∀U.∀A,B:qpowerclass U. A ∩ B = A → + ∀x,y. x=y → x ∈ A → y ∈ A ∩ B. + #U; #A; #B; #H; #x; #y; #K; #K2; napply (. K^-1‡H); nassumption; +nqed. + +(* nlemma intersect_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) (qpowerclass_setoid A). #A; @ [ #S; #S'; @ @@ -162,11 +209,18 @@ nqed. alias symbol "hint_decl" = "hint_decl_Type1". unification hint 0 ≔ A : setoid, B,C : qpowerclass A ⊢ - pc A (intersect_ok A B C) ≡ intersect ? (pc ? B) (pc ? C). + pc A (fun21 … + (mk_binary_morphism1 … + (λS,S':qpowerclass_setoid A.mk_qpowerclass ? (S ∩ S') (mem_ok' ? (intersect_ok ? S S'))) + (prop21 … (intersect_ok A))) + B + C) + ≡ intersect ? (pc ? B) (pc ? C). 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; napply (. (H^-1‡#)); nassumption. nqed. +*) ndefinition image: ∀A,B. (carr A → carr B) → Ω^A → Ω^B ≝ λA,B:setoid.λf:carr A → carr B.λSa:Ω^A. diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma index ce02f95df..d35030b35 100644 --- a/helm/software/matita/nlibrary/topology/igft.ma +++ b/helm/software/matita/nlibrary/topology/igft.ma @@ -823,27 +823,25 @@ Appendix: natural deduction like tactics explanation ----------------------------------------------------- In this appendix we try to give a description of tactics -in terms of natural deduction rules annotated with proofs. +in terms of sequent calculus rules annotated with proofs. The `:` separator has to be read as _is a proof of_, in the spirit of the Curry-Howard isomorphism. - f : A1 → … → An → B ?1 : A1 … ?n : An - napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ - (f ?1 … ?n ) : B + Γ ⊢ f : A1 → … → An → B Γ ⊢ ?1 : A1 … ?n : An + napply f; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ + Γ ⊢ (f ?1 … ?n ) : B foo - [x : T] - ⋮ - ? : P(x) + Γ; x : T ⊢ ? : P(x) #x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ - λx:T.? : ∀x:T.P(x) + Γ ⊢ λx:T.? : ∀x:T.P(x) baz - (?1 args1) : P(k1 args1) … (?n argsn) : P(kn argsn) - ncases x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ - match x with k1 args1 ⇒ ?1 | … | kn argsn ⇒ ?n : P(x) + Γ; args… : Args… ⊢ ?i : P(k1 args1) … (?n argsn) : P(kn argsn) + ncases x; ⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼⎼ + Γ ⊢ match x with k1 args1 ⇒ ?1 | … | kn argsn ⇒ ?n : P(x) bar -- 2.39.2