From 8cb2490b5b202549a596cfd1d0f166a5ee43fc4e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 28 Sep 2009 11:12:13 +0000 Subject: [PATCH] Experiment... --- helm/software/matita/nlibrary/logic/cprop.ma | 15 ++---------- .../matita/nlibrary/sets/partitions.ma | 23 ++++++++++--------- helm/software/matita/nlibrary/sets/sets.ma | 13 +++++++++-- 3 files changed, 25 insertions(+), 26 deletions(-) diff --git a/helm/software/matita/nlibrary/logic/cprop.ma b/helm/software/matita/nlibrary/logic/cprop.ma index d857ba6a7..0302264c6 100644 --- a/helm/software/matita/nlibrary/logic/cprop.ma +++ b/helm/software/matita/nlibrary/logic/cprop.ma @@ -52,7 +52,6 @@ ndefinition and_morphism: binary_morphism1 CPROP CPROP CPROP. | napply (H4 K2)]##] nqed. -(*unification hint 0 ≔ A,B ⊢ fun21 … and_morphism A B ≡ And A B.*) unification hint 0 ≔ A,B ⊢ fun21 … (mk_binary_morphism1 … And (prop21 … and_morphism)) A B ≡ And A B. (*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B. @@ -60,14 +59,6 @@ unification hint 0 ≔ A,B ⊢ fun21 … (mk_binary_morphism1 … And (prop21 napply (. ((#‡H1)‡H2^-1)); nnormalize; nqed.*) - -(*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B. - #A; #A'; #B; #H1; #H2; - napply (. ((#‡H1)‡H2^-1)); nnormalize; -nqed.*) - -(*interpretation "and_morphism" 'and a b = (fun21 ??? and_morphism a b).*) - ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP. napply mk_binary_morphism1 [ napply Or @@ -79,9 +70,7 @@ ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP. | napply (H4 H)]##] nqed. -unification hint 0 ≔ A,B ⊢ fun21 … or_morphism A B ≡ Or A B. - -(*interpretation "or_morphism" 'or a b = (fun21 ??? or_morphism a b).*) +unification hint 0 ≔ A,B ⊢ fun21 … (mk_binary_morphism1 … Or (prop21 … or_morphism)) A B ≡ Or A B. ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP. napply mk_binary_morphism1 @@ -89,4 +78,4 @@ ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP. | #a; #a'; #b; #b'; #H1; #H2; napply mk_iff; #H; #w [ napply (if … H2); napply H; napply (fi … H1); nassumption | napply (fi … H2); napply H; napply (if … H1); nassumption]##] -nqed. \ No newline at end of file +nqed. diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index 61173c78e..93f9cd6b5 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -24,6 +24,7 @@ alias symbol "eq" = "setoid1 eq". alias symbol "eq" = "setoid eq". alias symbol "eq" = "setoid eq". alias symbol "eq" = "setoid1 eq". +alias symbol "eq" = "setoid eq". nrecord partition (A: setoid) : Type[1] ≝ { support: setoid; indexes: qpowerclass support; @@ -146,25 +147,25 @@ nlemma partition_splits_card: | #a; #a'; #H; nrewrite < H; napply refl ] ##| #x; #Hx; nwhd; napply I ##| #y; #_; - ngeneralize in match (covers ? P) in ⊢ ?; *; #_; #Hc; - ngeneralize in match (Hc y I) in ⊢ ?; *; #index; *; #Hi1; #Hi2; - ngeneralize in match (f_sur ???? f ? Hi1) in ⊢ ?; *; #nindex; *; #Hni1; #Hni2; - ngeneralize in match (f_sur ???? (fi nindex) y ?) in ⊢ ? - [##2: alias symbol "refl" = "refl". + nlapply (covers ? P); *; #_; #Hc; + nlapply (Hc y I); *; #index; *; #Hi1; #Hi2; + nlapply (f_sur ???? f ? Hi1); *; #nindex; *; #Hni1; #Hni2; + nlapply (f_sur ???? (fi nindex) y ?) + [ alias symbol "refl" = "refl". alias symbol "prop1" = "prop11". napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##] *; #nindex2; *; #Hni21; #Hni22; nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2); - napply (ex_intro … xxx); napply conj + @ xxx; @ [ napply iso_nat_nat_union_pre [ napply le_S_S_to_le; nassumption | nassumption ] ##| nwhd in ⊢ (???%%); napply (.= ?) [##3: nassumption|##skip] - ngeneralize in match (iso_nat_nat_union_char n s xxx ?) in ⊢ ? - [##2: napply iso_nat_nat_union_pre [ napply le_S_S_to_le; nassumption | nassumption]##] + nlapply (iso_nat_nat_union_char n s xxx ?) + [napply iso_nat_nat_union_pre [ napply le_S_S_to_le; nassumption | nassumption]##] *; *; #K1; #K2; #K3; - ngeneralize in match + 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)) ?????) in ⊢ ? - [ *; #E1; #E2; nrewrite > E1; nrewrite > E2; napply refl + 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 |##*: nassumption]##] ##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx'; #E; diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index 4e7418fd9..c4fc89f21 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -71,7 +71,7 @@ nqed. include "hints_declaration.ma". alias symbol "hint_decl" = "hint_decl_Type2". -unification hint 0 ≔ A ⊢ carr1 (powerclass_setoid A) ≡ Ω^A. +unification hint 0 ≔ A ⊢ carr1 (mk_setoid1 (Ω^A) (eq1 (powerclass_setoid A))) ≡ Ω^A. (************ SETS OVER SETOIDS ********************) @@ -106,6 +106,10 @@ nqed. unification hint 0 ≔ A ⊢ carr1 (qpowerclass_setoid A) ≡ qpowerclass A. +(*CSC: non va! +unification hint 0 ≔ A ⊢ + carr1 (mk_setoid1 (qpowerclass A) (eq1 (qpowerclass_setoid A))) ≡ qpowerclass A.*) + nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid A) CPROP. #A; @ [ napply (λx,S. x ∈ S) @@ -116,10 +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) (*-------------------------------------*) ⊢ - fun21 ??? (mem_ok A) x S ≡ mem A SS x. + fun21 ??? (mk_binary_morphism1 ??? (λx,S. x ∈ S) (prop21 ??? (mem_ok A))) x S ≡ mem A SS x. nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP. #A; @ -- 2.39.2