From: Enrico Tassi Date: Wed, 16 Sep 2009 16:27:04 +0000 (+0000) Subject: some more work... X-Git-Tag: make_still_working~3461 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=021fd04f3bf776eeb4b8da45b3c7103ebabd789d;p=helm.git some more work... --- diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index 8ee6ea1ae..c8a19354c 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -116,9 +116,11 @@ nlemma mem_ok: ∀A. binary_morphism1 (setoid1_of_setoid A) (qpowerclass_setoid ##] nqed. -unification hint 0 ≔ - A : setoid, x, S ⊢ (mem_ok A) x S ≡ mem A S x. - +unification hint 0 ≔ A:setoid, x, S; + SS ≟ (pc ? S) + (*-------------------------------------*) ⊢ + fun21 ??? (mem_ok A) x S ≡ mem A SS x. + nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) CPROP. #A; @ [ napply (λS,S'. S ⊆ S') @@ -129,14 +131,8 @@ nlemma subseteq_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_s [ nassumption | napply (subseteq_trans … b'); nassumption ] ##] nqed. -(* hints can pass under mem *) (* ??? XXX why is it needed? *) -unification hint 0 ≔ A,B,x ; - C ≟ B - (*---------------------*) ⊢ - mem A B x ≡ mem A C x. - 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. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_setoid A) (qpowerclass_setoid A). @@ -144,7 +140,6 @@ nlemma intersect_ok: ∀A. binary_morphism1 (qpowerclass_setoid A) (qpowerclass_ [ #S; #S'; @ [ napply (S ∩ S') | #a; #a'; #Ha; - (*napply (.= #‡#);*) nwhd in ⊢ (? ? ? % %); @; *; #H1; #H2; @ [##1,2: napply (. Ha^-1‡#); nassumption; ##|##3,4: napply (. Ha‡#); nassumption]##] @@ -176,10 +171,6 @@ ndefinition counter_image: ∀A,B. (carr A → carr B) → Ω^B → Ω^A ≝ nrecord compatible_equivalence_relation (A: setoid) : Type[1] ≝ { rel:> equivalence_relation A; compatibility: ∀x,x':A. x=x' → rel x x' - (* coercion qui non andava per via di un Failure invece di Uncertain - ritornato dall'unificazione per il problema: - ?[] A =?= ?[Γ]->?[Γ+1] - *) }. ndefinition quotient: ∀A. compatible_equivalence_relation A → setoid. @@ -227,7 +218,7 @@ ndefinition injective ≝ nlemma first_omomorphism_theorem_functions2: ∀A,B.∀f: unary_morphism A B. surjective … (Full_set ?) (Full_set ?) (canonical_proj ? (eqrel_of_morphism … f)). - #A; #B; #f; nwhd; #y; #Hy; @ y; @ [ napply I | napply refl] + #A; #B; #f; nwhd; #y; #Hy; @ y; @ I ; napply refl; (* bug, prova @ I refl *) nqed.