(* USARE L'ESISTENZIALE DEBOLE *)
nrecord OAlgebra : Type[2] := {
oa_P :> setoid1;
- oa_leq : binary_morphism1 oa_P oa_P CPROP; (*CSC: dovrebbe essere CProp bug refiner*)
- oa_overlap: binary_morphism1 oa_P oa_P CPROP;
- binary_meet: binary_morphism1 oa_P oa_P oa_P;
+ oa_leq : unary_morphism1 oa_P (unary_morphism1_setoid1 oa_P CPROP); (*CSC: dovrebbe essere CProp bug refiner*)
+ oa_overlap: unary_morphism1 oa_P (unary_morphism1_setoid1 oa_P CPROP);
+ binary_meet: unary_morphism1 oa_P (unary_morphism1_setoid1 oa_P oa_P);
(*CSC: oa_join: ∀I:setoid.unary_morphism1 (setoid1_of_setoid … I ⇒ oa_P) oa_P;*)
oa_one: oa_P;
oa_zero: oa_P;
∀p,q.(∀r.oa_overlap p r → oa_overlap q r) → oa_leq p q
}.
-interpretation "o-algebra leq" 'leq a b = (fun21 ??? (oa_leq ?) a b).
+interpretation "o-algebra leq" 'leq a b = (fun11 ?? (fun11 ?? (oa_leq ?) a) b).
notation "hovbox(a mpadded width -150% (>)< b)" non associative with precedence 45
for @{ 'overlap $a $b}.
-interpretation "o-algebra overlap" 'overlap a b = (fun21 ??? (oa_overlap ?) a b).
+interpretation "o-algebra overlap" 'overlap a b = (fun11 ?? (fun11 ?? (oa_overlap ?) a) b).
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)"
non associative with precedence 50 for @{ 'oa_meet $p }.
qed.*)
interpretation "o-algebra binary meet" 'and a b =
- (fun21 ??? (binary_meet ?) a b).
+ (fun11 ?? (fun11 ?? (binary_meet ?) a) b).
(*
prefer coercion Type1_OF_OAlgebra.
napply (. (or_prop3 … a' …)^-1); (*CSC: why a'? *)
napply (. ?‡#)
[##2: napply (a r)
- | ngeneralize in match r in ⊢ %;
- nchange with (or_f … a' = or_f … a);
- napply (.= †e^-1);
- napply #]
+ | napply (e^-1); //]
napply (. (or_prop3 …));
napply oa_overlap_sym;
nassumption.
nlemma ORelation_eq2:
∀P,Q:OAlgebra.∀r,r':ORelation P Q.
r=r' → r⎻ = r'⎻.
- #P; #Q; #a; #a'; #e; #x;
+ #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_
- [ napply e | napply e^-1]
+ [ napply e | napply (e^-1)]
nqed.
ndefinition or_f_minus_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
R ≟ (mk_unary_morphism1 … (or_f_minus …) (prop11 … (or_f_minus_morphism1 …)))
(* ------------------------ *) ⊢
fun11 … R r ≡ or_f_minus P Q r.
+
+naxiom daemon : False.
nlemma ORelation_eq_respects_leq_or_f_star_:
∀P,Q:OAlgebra.∀r,r':ORelation P Q.
r=r' → ∀x. r* x ≤ r'* x.
#P; #Q; #a; #a'; #e; #x; (*CSC: una schifezza *)
+ ncases daemon.
+ (*
ngeneralize in match (. (or_prop1 P Q a' (a* x) x)^-1) in ⊢ %; #H; napply H;
nchange with (or_f P Q a' (a* x) ≤ x);
napply (. ?‡#)
nchange with (or_f P Q a' = or_f P Q a);
napply (.= †e^-1); napply #]
napply (. (or_prop1 …));
- napply oa_leq_refl.
+ napply oa_leq_refl.*)
nqed.
nlemma ORelation_eq3:
∀P,Q:OAlgebra.∀r,r':ORelation P Q.
r=r' → r* = r'*.
- #P; #Q; #a; #a'; #e; #x;
+ #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_star_
- [ napply e | napply e^-1]
+ [ napply e | napply (e^-1)]
nqed.
ndefinition or_f_star_morphism1: ∀P,Q:OAlgebra.unary_morphism1 (ORelation_setoid P Q)
∀P,Q:OAlgebra.∀r,r':ORelation P Q.
r=r' → ∀x. r⎻* x ≤ r'⎻* x.
#P; #Q; #a; #a'; #e; #x; (*CSC: una schifezza *)
+ ncases daemon. (*
ngeneralize in match (. (or_prop2 P Q a' (a⎻* x) x)^-1) in ⊢ %; #H; napply H;
nchange with (or_f_minus P Q a' (a⎻* x) ≤ x);
napply (. ?‡#)
nchange with (a'⎻ = a⎻);
napply (.= †e^-1); napply #]
napply (. (or_prop2 …));
- napply oa_leq_refl.
+ napply oa_leq_refl.*)
nqed.
nlemma ORelation_eq4:
∀P,Q:OAlgebra.∀r,r':ORelation P Q.
r=r' → r⎻* = r'⎻*.
- #P; #Q; #a; #a'; #e; #x;
+ #P; #Q; #a; #a'; #e; #x; #x'; #Hx; napply (.= †Hx);
napply oa_leq_antisym; napply ORelation_eq_respects_leq_or_f_minus_star_
- [ napply e | napply e^-1]
+ [ napply e | napply (e^-1)]
nqed.
ndefinition or_f_minus_star_morphism1:
| napply ORelation_eq4]
nqed.
+
unification hint 0 ≔ P, Q, r;
R ≟ (mk_unary_morphism1 … (or_f_minus_star …) (prop11 … (or_f_minus_star_morphism1 …)))
(* ------------------------ *) ⊢
fun11 … R r ≡ or_f_minus_star P Q r.
-
-(*CSC:
-ndefinition ORelation_composition : ∀P,Q,R.
- binary_morphism1 (ORelation_setoid P Q) (ORelation_setoid Q R) (ORelation_setoid P R).
-#P; #Q; #R; @
-[ #F; #G; @
- [ napply (G ∘ F);
- | apply rule (G⎻* ∘ F⎻* );
- | apply (F* ∘ G* );
- | apply (F⎻ ∘ G⎻);
- | intros;
- change with ((G (F p) ≤ q) = (p ≤ (F* (G* q))));
- apply (.= (or_prop1 :?));
- apply (or_prop1 :?);
- | intros;
- change with ((F⎻ (G⎻ p) ≤ q) = (p ≤ (G⎻* (F⎻* q))));
- apply (.= (or_prop2 :?));
- apply or_prop2 ;
- | intros; change with ((G (F (p)) >< q) = (p >< (F⎻ (G⎻ q))));
- apply (.= (or_prop3 :?));
- apply or_prop3;
- ]
-| intros; split; simplify;
- [3: unfold arrows1_of_ORelation_setoid; apply ((†e)‡(†e1));
- |1: apply ((†e)‡(†e1));
- |2,4: apply ((†e1)‡(†e));]]
-qed.
-
-definition OA : category2.
-split;
-[ apply (OAlgebra);
-| intros; apply (ORelation_setoid o o1);
-| intro O; split;
- [1,2,3,4: apply id2;
- |5,6,7:intros; apply refl1;]
-| apply ORelation_composition;
-| intros (P Q R S F G H); split;
- [ change with (H⎻* ∘ G⎻* ∘ F⎻* = H⎻* ∘ (G⎻* ∘ F⎻* ));
- apply (comp_assoc2 ????? (F⎻* ) (G⎻* ) (H⎻* ));
- | apply ((comp_assoc2 ????? (H⎻) (G⎻) (F⎻))^-1);
- | apply ((comp_assoc2 ????? F G H)^-1);
- | apply ((comp_assoc2 ????? H* G* F* ));]
-| intros; split; unfold ORelation_composition; simplify; apply id_neutral_left2;
-| intros; split; unfold ORelation_composition; simplify; apply id_neutral_right2;]
-qed.
-
-definition OAlgebra_of_objs2_OA: objs2 OA → OAlgebra ≝ λx.x.
-coercion OAlgebra_of_objs2_OA.
-
-definition ORelation_setoid_of_arrows2_OA:
- ∀P,Q. arrows2 OA P Q → ORelation_setoid P Q ≝ λP,Q,c.c.
-coercion ORelation_setoid_of_arrows2_OA.
-
-prefer coercion Type_OF_objs2.
-*)
-(* alias symbol "eq" = "setoid1 eq". *)
-
+
(* qui la notazione non va *)
(*CSC
nlemma leq_to_eq_join: ∀S:OAlgebra.∀p,q:S. p ≤ q → q = (binary_join ? p q).
napply oa_leq_refl.
nqed.
-lemma lemma_10_2_b: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻ (R⎻* p) ≤ p.
- intros;
- apply (. (or_prop2 : ?));
- apply oa_leq_refl.
-qed.
+nlemma lemma_10_2_b: ∀S,T.∀R:ORelation S T.∀p. R⎻ (R⎻* p) ≤ p.
+ #S; #T; #R; #p;
+ napply (. (or_prop2 …));
+ napply oa_leq_refl.
+nqed.
-lemma lemma_10_2_c: ∀S,T.∀R:arrows2 OA S T.∀p. p ≤ R* (R p).
- intros;
- apply (. (or_prop1 : ?)^-1);
- apply oa_leq_refl.
-qed.
+nlemma lemma_10_2_c: ∀S,T.∀R:ORelation S T.∀p. p ≤ R* (R p).
+ #S; #T; #R; #p;
+ napply (. (or_prop1 … p …)^-1);
+ napply oa_leq_refl.
+nqed.
-lemma lemma_10_2_d: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* p) ≤ p.
- intros;
- apply (. (or_prop1 : ?));
- apply oa_leq_refl.
-qed.
+nlemma lemma_10_2_d: ∀S,T.∀R:ORelation S T.∀p. R (R* p) ≤ p.
+ #S; #T; #R; #p;
+ napply (. (or_prop1 …));
+ napply oa_leq_refl.
+nqed.
-lemma lemma_10_3_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻ (R⎻* (R⎻ p)) = R⎻ p.
- intros; apply oa_leq_antisym;
- [ apply lemma_10_2_b;
- | apply f_minus_image_monotone;
- apply lemma_10_2_a; ]
-qed.
+nlemma lemma_10_3_a: ∀S,T.∀R:ORelation S T.∀p. R⎻ (R⎻* (R⎻ p)) = R⎻ p.
+ #S; #T; #R; #p; napply oa_leq_antisym
+ [ napply lemma_10_2_b
+ | napply f_minus_image_monotone;
+ napply lemma_10_2_a ]
+nqed.
-lemma lemma_10_3_b: ∀S,T.∀R:arrows2 OA S T.∀p. R* (R (R* p)) = R* p.
- intros; apply oa_leq_antisym;
- [ apply f_star_image_monotone;
- apply (lemma_10_2_d ?? R p);
- | apply lemma_10_2_c; ]
-qed.
+nlemma lemma_10_3_b: ∀S,T.∀R:ORelation S T.∀p. R* (R (R* p)) = R* p.
+ #S; #T; #R; #p; napply oa_leq_antisym
+ [ napply f_star_image_monotone;
+ napply (lemma_10_2_d ?? R p)
+ | napply lemma_10_2_c ]
+nqed.
-lemma lemma_10_3_c: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R p)) = R p.
- intros; apply oa_leq_antisym;
- [ apply lemma_10_2_d;
- | apply f_image_monotone;
- apply (lemma_10_2_c ?? R p); ]
-qed.
+nlemma lemma_10_3_c: ∀S,T.∀R:ORelation S T.∀p. R (R* (R p)) = R p.
+ #S; #T; #R; #p; napply oa_leq_antisym
+ [ napply lemma_10_2_d
+ | napply f_image_monotone;
+ napply (lemma_10_2_c ?? R p) ]
+nqed.
-lemma lemma_10_3_d: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* p)) = R⎻* p.
- intros; apply oa_leq_antisym;
- [ apply f_minus_star_image_monotone;
- apply (lemma_10_2_b ?? R p);
- | apply lemma_10_2_a; ]
-qed.
+nlemma lemma_10_3_d: ∀S,T.∀R:ORelation S T.∀p. R⎻* (R⎻ (R⎻* p)) = R⎻* p.
+ #S; #T; #R; #p; napply oa_leq_antisym
+ [ napply f_minus_star_image_monotone;
+ napply (lemma_10_2_b ?? R p)
+ | napply lemma_10_2_a ]
+nqed.
-lemma lemma_10_4_a: ∀S,T.∀R:arrows2 OA S T.∀p. R⎻* (R⎻ (R⎻* (R⎻ p))) = R⎻* (R⎻ p).
- intros; apply (†(lemma_10_3_a ?? R p));
-qed.
+nlemma lemma_10_4_a: ∀S,T.∀R:ORelation S T.∀p. R⎻* (R⎻ (R⎻* (R⎻ p))) = R⎻* (R⎻ p).
+ #S; #T; #R; #p; napply (†(lemma_10_3_a …)).
+nqed.
+
+nlemma lemma_10_4_b: ∀S,T.∀R:ORelation S T.∀p. R (R* (R (R* p))) = R (R* p).
+ #S; #T; #R; #p; napply (†(lemma_10_3_b …));
+nqed.
-lemma lemma_10_4_b: ∀S,T.∀R:arrows2 OA S T.∀p. R (R* (R (R* p))) = R (R* p).
-intros; unfold in ⊢ (? ? ? % %); apply (†(lemma_10_3_b ?? R p));
+nlemma oa_overlap_sym': ∀o:OAlgebra.∀U,V:o. (U >< V) = (V >< U).
+ #o; #U; #V; @; #H; napply oa_overlap_sym; nassumption.
+nqed.
+
+(******************* CATEGORIES **********************)
+
+ninductive one : Type[0] ≝ unit : one.
+
+ndefinition force : ∀S:Type[2]. S → ∀T:Type[2]. T → one → Type[2] ≝
+ λS,s,T,t,lock. match lock with [ unit => S ].
+
+ndefinition enrich_as :
+ ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one.force S s T t lock ≝
+ λS,s,T,t,lock. match lock return λlock.match lock with [ unit ⇒ S ]
+ with [ unit ⇒ s ].
+
+ncoercion enrich_as : ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one. force S s T t lock
+ ≝ enrich_as on t: ? to force ? ? ? ? ?.
+
+(* does not work here
+nlemma foo : ∀A,B,C:setoid1.∀f:B ⇒ C.∀g:A ⇒ B. unary_morphism1 A C.
+#A; #B; #C; #f; #g; napply(f \circ g).
+nqed.*)
+
+(* This precise hint does not leave spurious metavariables *)
+unification hint 0 ≔ A,B,C : setoid1, f:B ⇒ C, g: A ⇒ B;
+ lock ≟ unit
+(* --------------------------------------------------------------- *) ⊢
+ (unary_morphism1 A C)
+ ≡
+ (force (unary_morphism1 A C) (comp1_unary_morphisms A B C f g)
+ (carr1 A → carr1 C) (composition1 A B C f g) lock)
+ .
+
+(* This uniform hint opens spurious metavariables
+unification hint 0 ≔ A,B,C : setoid1, f:B ⇒ C, g: A ⇒ B, X;
+ lock ≟ unit
+(* --------------------------------------------------------------- *) ⊢
+ (unary_morphism1 A C)
+ ≡
+ (force (unary_morphism1 A C) X (carr1 A → carr1 C) (fun11 … X) lock)
+ .
+*)
+
+nlemma foo : ∀A,B,C:setoid1.∀f:B ⇒ C.∀g:A ⇒ B. unary_morphism1 A C.
+#A; #B; #C; #f; #g; napply(f ∘ g).
+nqed.
+
+(*
+
+ndefinition uffa: ∀A,B. ∀U: unary_morphism1 A B. (A → B) → CProp[0].
+ #A;#B;#_;#_; napply True.
+nqed.
+ndefinition mk_uffa: ∀A,B.∀U: unary_morphism1 A B. ∀f: (A → B). uffa A B U f.
+ #A; #B; #U; #f; napply I.
+nqed.
+
+ndefinition coerc_to_unary_morphism1:
+ ∀A,B. ∀U: unary_morphism1 A B. uffa A B U (fun11 … U) → unary_morphism1 A B.
+ #A; #B; #U; #_; nassumption.
+nqed.
+
+ncheck (λA,B,C,f,g.coerc_to_unary_morphism1 ??? (mk_uffa ??? (composition1 A B C f g))).
+*)
+ndefinition ORelation_composition : ∀P,Q,R.
+ unary_morphism1 (ORelation_setoid P Q)
+ (unary_morphism1_setoid1 (ORelation_setoid Q R) (ORelation_setoid P R)).
+#P; #Q; #R; napply mk_binary_morphism1
+[ #F; #G; @
+ [ napply (G ∘ F) (* napply (comp1_unary_morphisms … G F) (*CSC: was (G ∘ F);*) *)
+ | napply (G⎻* ∘ F⎻* ) (* napply (comp1_unary_morphisms … G⎻* F⎻* ) (*CSC: was (G⎻* ∘ F⎻* );*)*)
+ | napply (comp1_unary_morphisms … F* G* ) (*CSC: was (F* ∘ G* );*)
+ | napply (comp1_unary_morphisms … F⎻ G⎻) (*CSC: was (F⎻ ∘ G⎻);*)
+ | #p; #q; nnormalize;
+ napply (.= (or_prop1 … G …)); (*CSC: it used to understand without G *)
+ napply (or_prop1 …)
+ | #p; #q; nnormalize;
+ napply (.= (or_prop2 … F …));
+ napply or_prop2
+ | #p; #q; nnormalize;
+ napply (.= (or_prop3 … G …));
+ napply or_prop3
+ ]
+##| nnormalize; /3/]
+nqed.
+
+(*
+ndefinition OA : category2.
+split;
+[ apply (OAlgebra);
+| intros; apply (ORelation_setoid o o1);
+| intro O; split;
+ [1,2,3,4: apply id2;
+ |5,6,7:intros; apply refl1;]
+| apply ORelation_composition;
+| intros (P Q R S F G H); split;
+ [ change with (H⎻* ∘ G⎻* ∘ F⎻* = H⎻* ∘ (G⎻* ∘ F⎻* ));
+ apply (comp_assoc2 ????? (F⎻* ) (G⎻* ) (H⎻* ));
+ | apply ((comp_assoc2 ????? (H⎻) (G⎻) (F⎻))^-1);
+ | apply ((comp_assoc2 ????? F G H)^-1);
+ | apply ((comp_assoc2 ????? H* G* F* ));]
+| intros; split; unfold ORelation_composition; simplify; apply id_neutral_left2;
+| intros; split; unfold ORelation_composition; simplify; apply id_neutral_right2;]
qed.
-lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U).
- intros; split; intro; apply oa_overlap_sym; assumption.
-qed.
\ No newline at end of file
+definition OAlgebra_of_objs2_OA: objs2 OA → OAlgebra ≝ λx.x.
+coercion OAlgebra_of_objs2_OA.
+
+definition ORelation_setoid_of_arrows2_OA:
+ ∀P,Q. arrows2 OA P Q → ORelation_setoid P Q ≝ λP,Q,c.c.
+coercion ORelation_setoid_of_arrows2_OA.
+
+prefer coercion Type_OF_objs2.
+*)
+(* alias symbol "eq" = "setoid1 eq". *)
projects / helm.git / blobdiff