interpretation "hint_decl_CProp0" 'hint_decl a b = (hint_declaration_CProp0 ? a b).
interpretation "hint_decl_Type0" 'hint_decl a b = (hint_declaration_Type0 ? a b).
-(* little test
-naxiom A : Type[0].
-naxiom C : A → A → Type[0].
-ndefinition D ≝ C.
-alias symbol "hint_decl" = "hint_decl_Type1".
-unification hint 0 ≔
- X, R : A, Y ; Z ≟ X, W ≟ Y ⊢ C X Y ≡ D Z W.
-*)
+(* Non uniform coercions support *)
+nrecord lock2 (S : Type[2]) (s : S) : Type[3] ≝ {
+ force2 : Type[2];
+ lift2 : force2
+}.
+
+nrecord lock1 (S : Type[1]) (s : S) : Type[2] ≝ {
+ force1 : Type[1];
+ lift1 : force1
+}.
+
+ncoercion lift1 : ∀S:Type[1].∀s:S.∀l:lock1 S s. force1 S s l ≝ lift1
+ on s : ? to force1 ???.
+
+ncoercion lift2 : ∀S:Type[2].∀s:S.∀l:lock2 S s. force2 S s l ≝ lift2
+ on s : ? to force2 ???.
+
+(* Example of a non uniform coercion declaration
+
+ Type[0] setoid
+ >--->
+ MR R
+
+ provided MR = carr R
+
+unification hint 0 ≔ R : setoid;
+ MR ≟ carr R,
+ lock ≟ mk_lock1 Type[0] MR setoid R
+(* ---------------------------------------- *) ⊢
+ setoid ≡ force1 ? MR lock.
+
+*)
\ No newline at end of file
(*-----------------------------------------------------------------------*) ⊢
carr X ≡ list T.
+unification hint 0 ≔ S,a,b;
+ R ≟ LIST S,
+ L ≟ (list S)
+(* -------------------------------------------- *) ⊢
+ eq_list S a b ≡ eq_rel L (eq0 R) a b.
+
notation "hvbox(hd break :: tl)"
right associative with precedence 47
for @{'cons $hd $tl}.
ndefinition associative ≝ λA:setoid.λf:A → A → A.∀x,y,z.f x (f y z) = f (f x y) z.
-ninductive one : Type[0] ≝ unit : one.
-
-ndefinition force ≝
- λS:Type[2].λs:S.λT:Type[2].λt:T.λlock:one.
- match lock return λ_.Type[2] with [ unit ⇒ T].
-
-nlet rec lift (S:Type[2]) (s:S) (T:Type[2]) (t:T) (lock:one) on lock : force S s T t lock ≝
- match lock return λlock.force S s T t lock with [ unit ⇒ t ].
-
-ncoercion lift1 : ∀S:Type[1].∀s:S.∀T:Type[1].∀t:T.∀lock:one. force S s T t lock ≝ lift
- on s : ? to force ?????.
-
-ncoercion lift2 : ∀S:Type[2].∀s:S.∀T:Type[2].∀t:T.∀lock:one. force S s T t lock ≝ lift
- on s : ? to force ?????.
-
-unification hint 0 ≔ R : setoid;
- TR ≟ setoid, MR ≟ (carr R), lock ≟ unit
-(* ---------------------------------------- *) ⊢
- setoid ≡ force ?(*Type[0]*) MR TR R lock.
-
-unification hint 0 ≔ R : setoid1;
- TR ≟ setoid1, MR ≟ (carr1 R), lock ≟ unit
-(* ---------------------------------------- *) ⊢
- setoid1 ≡ force ? MR TR R lock.
ntheorem associative_append: ∀A:setoid.associative (list A) (append A).
-#A;#x;#y;#z;nelim x[//|#a;#x1;#H;nnormalize;/2/]nqed.
+#A;#x;#y;#z;nelim x[ napply # |#a;#x1;#H;nnormalize;/2/]nqed.
interpretation "iff" 'iff a b = (iff a b).
(*-----------------------------------------------------------------------*) ⊢
carr X ≡ bool.
+unification hint 0 ≔ a,b;
+ R ≟ BOOL,
+ L ≟ bool
+(* -------------------------------------------- *) ⊢
+ eq bool a b ≡ eq_rel L (eq0 R) a b.
+
nrecord Alpha : Type[1] ≝ {
acarr :> setoid;
eqb: acarr → acarr → bool;
(*-----------------------------------------------------------------------*) ⊢
carr X ≡ (re T).
+unification hint 0 ≔ A,a,b;
+ R ≟ RE A,
+ L ≟ re A
+(* -------------------------------------------- *) ⊢
+ eq_re A a b ≡ eq_rel L (eq0 R) a b.
+
notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
notation > "a ^ *" non associative with precedence 75 for @{ 'pk $a}.
interpretation "star" 'pk a = (k ? a).
notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
interpretation "epsilon" 'epsilon = (e ?).
-notation "0" non associative with precedence 90 for @{ 'empty }.
-interpretation "empty" 'empty = (z ?).
+notation "0" non associative with precedence 90 for @{ 'empty_r }.
+interpretation "empty" 'empty_r = (z ?).
notation > "'lang' S" non associative with precedence 90 for @{ Ω^(list $S) }.
notation > "'Elang' S" non associative with precedence 90 for @{ 𝛀^(list $S) }.
nlet rec conjunct S (l : list (list S)) (L : lang S) on l: CProp[0] ≝
match l with [ nil ⇒ True | cons w tl ⇒ w ∈ L ∧ conjunct ? tl L ].
-
-ndefinition empty_set : ∀A.Ω^A ≝ λA.{ w | False }.
-notation "∅" non associative with precedence 90 for @{'emptyset}.
-interpretation "empty set" 'emptyset = (empty_set ?).
-
-(*
-notation "{}" non associative with precedence 90 for @{'empty_lang}.
-interpretation "empty lang" 'empty_lang = (empty_lang ?).
-*)
-
ndefinition sing_lang : ∀A:setoid.∀x:A.Ω^A ≝ λS.λx.{ w | x = w }.
interpretation "sing lang" 'singl x = (sing_lang ? x).
ncoercion pc : ∀S.∀p:pitem S. pitem S → pitem S ≝ pc on _p : pitem ? to ∀_:?.?.
interpretation "patom" 'ps a = (ps ? a).
interpretation "pepsilon" 'epsilon = (pe ?).
-interpretation "pempty" 'empty = (pz ?).
+interpretation "pempty" 'empty_r = (pz ?).
notation > "|term 19 e|" non associative with precedence 70 for @{forget ? $e}.
nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝
notation "𝐋\sub(\p) term 70 E" non associative with precedence 75 for @{'L_pi $E}.
interpretation "in_pl" 'L_pi E = (L_pi ? E).
-unification hint 0 ≔ S,a,b;
- R ≟ LIST S,
- L ≟ (list S)
-(* -------------------------------------------- *) ⊢
- eq_list S a b ≡ eq_rel L (eq0 R) a b.
-
+(* The caml, as some patches for it *)
ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid on _s: setoid to setoid1.
alias symbol "hint_decl" (instance 1) = "hint_decl_CProp2".
(*-----------------------------------------------------------------*) ⊢
list S ≡ carr1 TT.
-
+(* Ex setoid support *)
nlemma Sig: ∀S,T:setoid.∀P: S → (T → CPROP).
∀y,z:T.y = z → (∀x.y=z → P x y = P x z) → (Ex S (λx.P x y)) =_1 (Ex S (λx.P x z)).
#S T P y z Q E; @; *; #x Px; @x; nlapply (E x Q); *; /2/; nqed.
napply (.=_1 (∑ E (λw,H.(H ╪_1 #) ╪_1 #)) ╪_1 #).
napply #.
nqed.
+(* Ex setoid support end *)
ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
#S r; @(𝐋\p r); #w1 w2 E; nelim r;
ndefinition reclose ≝ λS:Alpha.λp:pre S.let p' ≝ •\fst p in 〈\fst p',\snd p || \snd p'〉.
interpretation "reclose" 'eclose x = (reclose ? x).
-nlemma cup0 :∀S.∀p:lang S.p ∪ ∅ = p.
-#S p; @; #w; ##[*; //| #; @1; //] *; nqed.
-
-nlemma cupC : ∀S. ∀a,b:lang S.a ∪ b = b ∪ a.
-#S a b; @; #w; *; nnormalize; /2/; nqed.
-
-nlemma cupID : ∀S. ∀a:lang S.a ∪ a = a.
-#S a; @; #w; ##[*; //] /2/; nqed.
-
nlemma epsilon_or : ∀S:Alpha.∀b1,b2. ϵ(b1 || b2) = ϵ b1 ∪ ϵ b2. ##[##2: napply S]
#S b1 b2; ncases b1; ncases b2;
nchange in match (true || true) with true;
nchange in match (ϵ true) with {[]};
nchange in match (ϵ false) with ∅;
##[##1,4: napply ((cupID…)^-1);
-##| napply ((cup0 S {[]})^-1);
-##| napply (.= (cup0 S {[]})^-1); napply cupC; ##]
+##| napply ((cup0 ? {[]})^-1);
+##| napply (.= (cup0 ? {[]})^-1); napply cupC; ##]
nqed.
-nlemma cupA : ∀S.∀a,b,c:lang S.a ∪ b ∪ c = a ∪ (b ∪ c).
-#S a b c; @; #w; *; /3/; *; /3/; nqed.
-
+(* XXX move somewere else *)
ndefinition if': ∀A,B:CPROP. A = B → A → B.
#A B; *; /2/. nqed.
id_neutral_right: ∀o1,o2. ∀a: arrows o1 o2. comp ??? a (id o1) = a
}.
-notation "hvbox(A break ⇒ B)" right associative with precedence 50 for @{ 'arrows $A $B }.
-interpretation "arrows1" 'arrows A B = (unary_morphism1 A B).
-interpretation "arrows" 'arrows A B = (unary_morphism A B).
-
notation > "𝐈𝐝 term 90 A" non associative with precedence 90 for @{ 'id $A }.
notation < "mpadded width -90% (𝐈) 𝐝 \sub term 90 A" non associative with precedence 90 for @{ 'id $A }.
@ setoid; @;
##[ #T1; #T2;
alias symbol "eq" = "setoid eq".
- napply (∃f:T1 ⇒ T2.∃g:T2 ⇒ T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y));
+ napply (∃f:T1 ⇒_0 T2.∃g:T2 ⇒_0 T1. (∀x.f (g x) = x) ∧ (∀y.g (f y) = y));
##| #A; @ (𝐈𝐝 A); @ (𝐈𝐝 A); @; #x; napply #;
##| #A; #B; *; #f; *; #g; *; #Hfg; #Hgf; @g; @f; @; nassumption;
##| #A; #B; #C; *; #f; *; #f'; *; #Hf; #Hf'; *; #g; *; #g'; *; #Hg; #Hg';
nrecord unary_morphism01 (A : setoid) (B: setoid1) : Type[1] ≝
{ fun01:1> A → B;
- prop01: ∀a,a'. eq ? a a' → eq1 ? (fun01 a) (fun01 a')
+ prop01: ∀a,a'. eq0 ? a a' → eq1 ? (fun01 a) (fun01 a')
}.
interpretation "prop01" 'prop1 c = (prop01 ????? c).
eq0: equivalence_relation carr
}.
+(* activate non uniform coercions on: Type → setoid *)
+unification hint 0 ≔ R : setoid;
+ MR ≟ carr R,
+ lock ≟ mk_lock1 Type[0] MR setoid R
+(* ---------------------------------------- *) ⊢
+ setoid ≡ force1 ? MR lock.
+
interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y).
notation > "hvbox(a break =_0 b)" non associative with precedence 45
(* -------------------------------------------------------------------- *) ⊢
fun1 ?? R ≡ (composition … f g).
-ndefinition comp_binary_morphisms:
- ∀o1,o2,o3.
- (unary_morph_setoid o2 o3) ⇒_0
- (unary_morph_setoid (unary_morph_setoid o1 o2) (unary_morph_setoid o1 o3)).
+ndefinition comp_binary_morphisms:
+ ∀o1,o2,o3.(o2 ⇒_0 o3) ⇒_0 ((o1 ⇒_0 o2) ⇒_0 (o1 ⇒_0 o3)).
#o1; #o2; #o3; napply mk_binary_morphism
- [ #f; #g; napply (comp_unary_morphisms … f g) (*CSC: why not ∘?*)
+ [ #f; #g; napply (comp_unary_morphisms ??? f g)
+ (* CSC: why not ∘?
+ GARES: because the coercion to FunClass is not triggered if there
+ are no "extra" arguments. We could fix that in the refiner
+ *)
| #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ]
nqed.
eq1: equivalence_relation1 carr1
}.
+unification hint 0 ≔ R : setoid1;
+ MR ≟ (carr1 R),
+ lock ≟ mk_lock2 Type[1] MR setoid1 R
+(* ---------------------------------------- *) ⊢
+ setoid1 ≡ force2 ? MR lock.
+
ndefinition setoid1_of_setoid: setoid → setoid1.
#s; @ (carr s); @ (eq0…) (refl…) (sym…) (trans…);
nqed.
fun11 ?? R ≡ (composition1 … f g).
ndefinition comp1_binary_morphisms:
- ∀o1,o2,o3.
- (unary_morphism1_setoid1 o2 o3) ⇒_1
- (unary_morphism1_setoid1 (unary_morphism1_setoid1 o1 o2) (unary_morphism1_setoid1 o1 o3)).
+ ∀o1,o2,o3. (o2 ⇒_1 o3) ⇒_1 ((o1 ⇒_1 o2) ⇒_1 (o1 ⇒_1 o3)).
#o1; #o2; #o3; napply mk_binary_morphism1
- [ #f; #g; napply (comp1_unary_morphisms … f g) (*CSC: why not ∘?*)
+ [ #f; #g; napply (comp1_unary_morphisms … f g)
| #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ]
nqed.
#A; @(Ω^A);//.
nqed.
-include "hints_declaration.ma".
-
alias symbol "hint_decl" = "hint_decl_Type2".
unification hint 0 ≔ A;
R ≟ (mk_setoid1 (Ω^A) (eq1 (powerclass_setoid A)))
carr1 R ≡ ext_powerclass A.
nlemma mem_ext_powerclass_setoid_is_morph:
- ∀A. (setoid1_of_setoid A) ⇒_1 (unary_morphism1_setoid1 (ext_powerclass_setoid A) CPROP).
- #A; napply (mk_binary_morphism1 … (λx:setoid1_of_setoid A.λS: 𝛀^A. x ∈ S));
- #a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; @; #H
- [ napply (. (ext_prop … Ha^-1)) | napply (. (ext_prop … Ha)) ] /2/.
+ ∀A. (setoid1_of_setoid A) ⇒_1 ((𝛀^A) ⇒_1 CPROP).
+#A; napply (mk_binary_morphism1 … (λx:setoid1_of_setoid A.λS: 𝛀^A. x ∈ S));
+#a; #a'; #b; #b'; #Ha; *; #Hb1; #Hb2; @; #H
+[ napply (. (ext_prop … Ha^-1)) | napply (. (ext_prop … Ha)) ] /2/.
nqed.
unification hint 0 ≔ AA, x, S;
nlemma ext_set : ∀S.∀A,B:Ω^S.(∀x:S. (x ∈ A) = (x ∈ B)) → A = B.
#S A B H; @; #x; ncases (H x); #H1 H2; ##[ napply H1 | napply H2] nqed.
-nlemma subseteq_is_morph: ∀A.
- (ext_powerclass_setoid A) ⇒_1
- (unary_morphism1_setoid1 (ext_powerclass_setoid A) CPROP).
+nlemma subseteq_is_morph: ∀A. 𝛀^A ⇒_1 𝛀^A ⇒_1 CPROP.
#A; napply (mk_binary_morphism1 … (λS,S':𝛀^A. S ⊆ S'));
#a; #a'; #b; #b'; *; #H1; #H2; *; /5/ by mk_iff, sym1, subseteq_trans;
nqed.
R ≟ (mk_ext_powerclass ? (B ∩ C) (ext_prop ? (intersect_is_ext ? B C)))
(* ------------------------------------------*) ⊢
ext_carr A R ≡ intersect ? (ext_carr ? B) (ext_carr ? C).
-
-nlemma intersect_is_morph:
- ∀A. (powerclass_setoid A) ⇒_1 (unary_morphism1_setoid1 (powerclass_setoid A) (powerclass_setoid A)).
- #A; napply (mk_binary_morphism1 … (λS,S'. S ∩ S'));
- #a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #x; nnormalize; *;/3/.
+
+nlemma intersect_is_morph: ∀A. Ω^A ⇒_1 Ω^A ⇒_1 Ω^A.
+#A; napply (mk_binary_morphism1 … (λS,S'. S ∩ S'));
+#a; #a'; #b; #b'; *; #Ha1; #Ha2; *; #Hb1; #Hb2; @; #x; nnormalize; *;/3/.
nqed.
alias symbol "hint_decl" = "hint_decl_Type1".
(prop11 (ext_powerclass_setoid ?)
(unary_morphism1_setoid1 (ext_powerclass_setoid ?) ?) ? ?? l ?? r).
-nlemma intersect_is_ext_morph:
- ∀A.
- (ext_powerclass_setoid A) ⇒_1
- (unary_morphism1_setoid1 (ext_powerclass_setoid A) (ext_powerclass_setoid A)).
+nlemma intersect_is_ext_morph: ∀A. 𝛀^A ⇒_1 𝛀^A ⇒_1 𝛀^A.
#A; napply (mk_binary_morphism1 … (intersect_is_ext …));
#a; #a'; #b; #b'; #Ha; #Hb; napply (prop11 … (intersect_is_morph A)); nassumption.
nqed.
(* ------------------------------------------------------*) ⊢
ext_carr AA (R B C) ≡ intersect A BB CC.
-nlemma union_is_morph :
- ∀A. (powerclass_setoid A) ⇒_1 (unary_morphism1_setoid1 (powerclass_setoid A) (powerclass_setoid A)).
-(*XXX ∀A.Ω^A ⇒_1 (Ω^A ⇒_1 Ω^A). avec non-unif-coerc*)
+nlemma union_is_morph : ∀A. Ω^A ⇒_1 (Ω^A ⇒_1 Ω^A).
#X; napply (mk_binary_morphism1 … (λA,B.A ∪ B));
#A1 A2 B1 B2 EA EB; napply ext_set; #x;
nchange in match (x ∈ (A1 ∪ B1)) with (?∨?);
(*--------------------------------------------------------------------------*) ⊢
fun11 ?? (fun11 ?? MM A) B ≡ A ∪ B.
-nlemma union_is_ext_morph:∀A.
- (ext_powerclass_setoid A) ⇒_1
- (unary_morphism1_setoid1 (ext_powerclass_setoid A) (ext_powerclass_setoid A)).
-(*XXX ∀A:setoid.𝛀^A ⇒_1 (𝛀^A ⇒_1 𝛀^A). with coercion non uniformi *)
+nlemma union_is_ext_morph:∀A.𝛀^A ⇒_1 𝛀^A ⇒_1 𝛀^A.
#A; napply (mk_binary_morphism1 … (union_is_ext …));
#x1 x2 y1 y2 Ex Ey; napply (prop11 … (union_is_morph A)); nassumption.
nqed.
f_inj: injective … S iso_f
}.
-nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W.
-#A; #U; #V; #W; *; #H; #x; *; /2/.
-nqed.
-
-nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W.
-#A; #U; #V; #W; #H; #H1; #x; *; /2/.
-nqed.
-
-nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V.
-/3/. nqed.
(*
nrecord isomorphism (A, B : setoid) (S: qpowerclass A) (T: qpowerclass B) : CProp[0] ≝
;
}.
-*)
\ No newline at end of file
+*)
+
+(* Set theory *)
+
+nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W.
+#A; #U; #V; #W; *; #H; #x; *; /2/.
+nqed.
+
+nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W.
+#A; #U; #V; #W; #H; #H1; #x; *; /2/.
+nqed.
+
+nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V.
+/3/. nqed.
+
+nlemma cupC : ∀S. ∀a,b:Ω^S.a ∪ b = b ∪ a.
+#S a b; @; #w; *; nnormalize; /2/; nqed.
+
+nlemma cupID : ∀S. ∀a:Ω^S.a ∪ a = a.
+#S a; @; #w; ##[*; //] /2/; nqed.
+
+(* XXX Bug notazione \cup, niente parentesi *)
+nlemma cupA : ∀S.∀a,b,c:Ω^S.a ∪ b ∪ c = a ∪ (b ∪ c).
+#S a b c; @; #w; *; /3/; *; /3/; nqed.
+
+ndefinition Empty_set : ∀A.Ω^A ≝ λA.{ x | False }.
+
+notation "∅" non associative with precedence 90 for @{ 'empty }.
+interpretation "empty set" 'empty = (Empty_set ?).
+
+nlemma cup0 :∀S.∀A:Ω^S.A ∪ ∅ = A.
+#S p; @; #w; ##[*; //| #; @1; //] *; nqed.
+
projects / helm.git / commitdiff