+
(**************************************************************************)
(* ___ *)
(* ||M|| *)
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.
| 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))]
| 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).
[ #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;