ninductive Admit : CProp[0] ≝ .
naxiom admit : Admit.
+(* single = is for the abstract equality of setoids, == is for concrete
+ equalities (that may be lifted to the setoid level when needed *)
+notation < "hvbox(a break mpadded width -50% (=)= b)" non associative with precedence 45 for @{ 'eq_low $a $b }.
+notation > "a == b" non associative with precedence 45 for @{ 'eq_low $a $b }.
+
+
+(* XXX move to lists.ma *)
ninductive list (A:Type[0]) : Type[0] ≝
| nil: list A
| cons: A -> list A -> list A.
[ nil ⇒ match l2 return λ_.CProp[0] with [ nil ⇒ True | _ ⇒ False ]
| cons x xs ⇒ match l2 with [ nil ⇒ False | cons y ys ⇒ x = y ∧ eq_list ? xs ys]].
+interpretation "eq_list" 'eq_low a b = (eq_list ? a b).
+
ndefinition LIST : setoid → setoid.
-#S; @(list S); @(eq_list S); ncases admit; nqed.
+#S; @(list S); @(eq_list S);
+##[ #l; nelim l; //; #; @; //;
+##| #l1; nelim l1; ##[ #y; ncases y; //] #x xs H y; ncases y; ##[*] #y ys; *; #; @; /2/;
+##| #l1; nelim l1; ##[ #l2 l3; ncases l2; ncases l3; /3/; #z zs y ys; *]
+ #x xs H l2 l3; ncases l2; ncases l3; /2/; #z zs y yz; *; #H1 H2; *; #H3 H4; @; /3/;##]
+nqed.
alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
unification hint 0 ≔ S : setoid;
+ T ≟ carr S,
P1 ≟ refl ? (eq0 (LIST S)),
P2 ≟ sym ? (eq0 (LIST S)),
P3 ≟ trans ? (eq0 (LIST S)),
- X ≟ mk_setoid (list S) (mk_equivalence_relation ? (eq_list S) P1 P2 P3),
- T ≟ carr S
+ X ≟ mk_setoid (list S) (mk_equivalence_relation ? (eq_list T) P1 P2 P3)
(*-----------------------------------------------------------------------*) ⊢
carr X ≡ list T.
-unification hint 0 ≔ S,a,b;
- R ≟ LIST S,
+unification hint 0 ≔ S:setoid,a,b:list S;
+ R ≟ eq0 (LIST S),
L ≟ (list S)
(* -------------------------------------------- *) ⊢
- eq_list S a b ≡ eq_rel L (eq0 R) a b.
+ eq_list S a b ≡ eq_rel L R a b.
notation "hvbox(hd break :: tl)"
right associative with precedence 47
ndefinition associative ≝ λA:setoid.λf:A → A → A.∀x,y,z.f x (f y z) = f (f x y) z.
-
ntheorem associative_append: ∀A:setoid.associative (list A) (append A).
-#A;#x;#y;#z;nelim x[ napply # |#a;#x1;#H;nnormalize;/2/]nqed.
+#A;#x;#y;#z;nelim x[ napply (refl ???) |#a;#x1;#H;nnormalize;/2/]nqed.
+
+nlet rec flatten S (l : list (list S)) on l : list S ≝
+match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
+
+(* end move to list *)
interpretation "iff" 'iff a b = (iff a b).
#A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
nqed.
-notation < "a = b" non associative with precedence 45 for @{ 'eqpp $a $b}.
-interpretation "bool eq" 'eqpp a b = (eq bool a b).
+(* XXX move to bool *)
+interpretation "bool eq" 'eq_low a b = (eq bool a b).
ndefinition BOOL : setoid.
@bool; @(eq bool); ncases admit.nqed.
carr X ≡ bool.
unification hint 0 ≔ a,b;
- R ≟ BOOL,
+ R ≟ eq0 BOOL,
L ≟ bool
(* -------------------------------------------- *) ⊢
- eq bool a b ≡ eq_rel L (eq0 R) a b.
+ eq bool a b ≡ eq_rel L R a b.
nrecord Alpha : Type[1] ≝ {
acarr :> setoid;
eqb_true: ∀x,y. (eqb x y = true) = (x = y)
}.
-notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
-interpretation "eqb" 'eqb a b = (eqb ? a b).
+interpretation "eqb" 'eq_low a b = (eqb ? a b).
ninductive re (S: Type[0]) : Type[0] ≝
z: re S
| o: re S → re S → re S
| k: re S → re S.
-naxiom eq_re : ∀S:Alpha.re S → re S → CProp[0].
+nlet rec eq_re (S:Alpha) (a,b : re S) on a : CProp[0] ≝
+ match a with
+ [ z ⇒ match b with [ z ⇒ True | _ ⇒ False]
+ | e ⇒ match b with [ e ⇒ True | _ ⇒ False]
+ | s x ⇒ match b with [ s y ⇒ x = y | _ ⇒ False]
+ | c r1 r2 ⇒ match b with [ c s1 s2 ⇒ eq_re ? r1 s1 ∧ eq_re ? r2 s2 | _ ⇒ False]
+ | o r1 r2 ⇒ match b with [ o s1 s2 ⇒ eq_re ? r1 s1 ∧ eq_re ? r2 s2 | _ ⇒ False]
+ | k r1 ⇒ match b with [ k r2 ⇒ eq_re ? r1 r2 | _ ⇒ False]].
+
ndefinition RE : Alpha → setoid.
-#A; @(re A); @(eq_re A); ncases admit. nqed.
+#A; @(re A); @(eq_re A);
+##[ #p; nelim p; /2/;
+##| #p1; nelim p1; ##[##1,2: #p2; ncases p2; /2/;
+ ##|##2,3: #x p2; ncases p2; /2/;
+ ##|##4,5: #e1 e2 H1 H2 p2; ncases p2; /3/; #e3 e4; *; #; @; /2/;
+ ##|#r H p2; ncases p2; /2/;##]
+##| #p1; nelim p1;
+ ##[ ##1,2: #y z; ncases y; ncases z; //; nnormalize; #; ncases (?:False); //;
+ ##| ##3: #a; #y z; ncases y; ncases z; /2/; nnormalize; #; ncases (?:False); //;
+ ##| ##4,5: #r1 r2 H1 H2 y z; ncases y; ncases z; //; nnormalize;
+ ##[##1,3,4,5,6,8: #; ncases (?:False); //;##]
+ #r1 r2 r3 r4; nnormalize; *; #H1 H2; *; #H3 H4; /3/;
+ ##| #r H y z; ncases y; ncases z; //; nnormalize; ##[##1,2,3: #; ncases (?:False); //]
+ #r2 r3; /3/; ##]##]
+nqed.
alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
alias id "carr" = "cic:/matita/ng/sets/setoids/carr.fix(0,0,1)".
unification hint 0 ≔ A : Alpha;
+ S ≟ acarr A,
+ T ≟ carr S,
P1 ≟ refl ? (eq0 (RE A)),
P2 ≟ sym ? (eq0 (RE A)),
P3 ≟ trans ? (eq0 (RE A)),
- X ≟ mk_setoid (re A) (mk_equivalence_relation ? (eq_re A) P1 P2 P3),
- T ≟ acarr A
+ X ≟ mk_setoid (re T) (mk_equivalence_relation ? (eq_re A) P1 P2 P3)
(*-----------------------------------------------------------------------*) ⊢
- carr X ≡ (re T).
+ carr X ≡ re T.
-unification hint 0 ≔ A,a,b;
- R ≟ RE A,
+unification hint 0 ≔ A:Alpha,a,b:re A;
+ R ≟ eq0 (RE A),
L ≟ re A
(* -------------------------------------------- *) ⊢
- eq_re A a b ≡ eq_rel L (eq0 R) a b.
+ eq_re A a b ≡ eq_rel L R a b.
notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
notation > "a ^ *" non associative with precedence 75 for @{ 'pk $a}.
notation > "'lang' S" non associative with precedence 90 for @{ Ω^(list $S) }.
notation > "'Elang' S" non associative with precedence 90 for @{ 𝛀^(list $S) }.
-nlet rec flatten S (l : list (list S)) on l : list S ≝
-match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
-
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 ].
| po: pitem S → pitem S → pitem S
| pk: pitem S → pitem S.
+nlet rec eq_pitem (S : Alpha) (p1, p2 : pitem S) on p1 : CProp[0] ≝
+ match p1 with
+ [ pz ⇒ match p2 with [ pz ⇒ True | _ ⇒ False]
+ | pe ⇒ match p2 with [ pe ⇒ True | _ ⇒ False]
+ | ps x ⇒ match p2 with [ ps y ⇒ x = y | _ ⇒ False]
+ | pp x ⇒ match p2 with [ pp y ⇒ x = y | _ ⇒ False]
+ | pc a1 a2 ⇒ match p2 with [ pc b1 b2 ⇒ eq_pitem ? a1 b1 ∧ eq_pitem ? a2 b2| _ ⇒ False]
+ | po a1 a2 ⇒ match p2 with [ po b1 b2 ⇒ eq_pitem ? a1 b1 ∧ eq_pitem ? a2 b2| _ ⇒ False]
+ | pk a ⇒ match p2 with [ pk b ⇒ eq_pitem ? a b | _ ⇒ False]].
+
+interpretation "eq_pitem" 'eq_low a b = (eq_pitem ? a b).
+
+nlemma PITEM : ∀S:Alpha.setoid.
+#S; @(pitem S); @(eq_pitem …);
+##[ #p; nelim p; //; nnormalize; #; @; //;
+##| #p; nelim p; ##[##1,2: #y; ncases y; //; ##|##3,4: #x y; ncases y; //; #; napply (?^-1); nassumption;
+ ##|##5,6: #r1 r2 H1 H2 p2; ncases p2; //; #s1 s2; nnormalize; *; #; @; /2/;
+ ##| #r H y; ncases y; //; nnormalize; /2/;##]
+##| #x; nelim x;
+ ##[ ##1,2: #y z; ncases y; ncases z; //; nnormalize; #; ncases (?:False); //;
+ ##| ##3,4: #a; #y z; ncases y; ncases z; /2/; nnormalize; #; ncases (?:False); //;
+ ##| ##5,6: #r1 r2 H1 H2 y z; ncases y; ncases z; //; nnormalize;
+ ##[##1,2,5,6,7,8,4,10: #; ncases (?:False); //;##]
+ #r1 r2 r3 r4; nnormalize; *; #H1 H2; *; #H3 H4; /3/;
+ ##| #r H y z; ncases y; ncases z; //; nnormalize; ##[##1,2,3,4: #; ncases (?:False); //]
+ #r2 r3; /3/; ##]##]
+nqed.
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+unification hint 0 ≔ SS:Alpha;
+ S ≟ acarr SS,
+ A ≟ carr S,
+ P1 ≟ refl ? (eq0 (PITEM SS)),
+ P2 ≟ sym ? (eq0 (PITEM SS)),
+ P3 ≟ trans ? (eq0 (PITEM SS)),
+ R ≟ mk_setoid (pitem S) (mk_equivalence_relation (pitem A) (eq_pitem SS) P1 P2 P3)
+(*---------------------------*)⊢
+ carr R ≡ pitem A.
+
+unification hint 0 ≔ S:Alpha,a,b:pitem S;
+ R ≟ PITEM S,
+ L ≟ (pitem S)
+(* -------------------------------------------- *) ⊢
+ eq_pitem S a b ≡ eq_rel L (eq0 R) a b.
+
+(* XXX move to pair.ma *)
+nlet rec eq_pair (A, B : setoid) (a : A × B) (b : A × B) on a : CProp[0] ≝
+ match a with [ mk_pair a1 a2 ⇒
+ match b with [ mk_pair b1 b2 ⇒ a1 = b1 ∧ a2 = b2 ]].
+
+interpretation "eq_pair" 'eq_low a b = (eq_pair ?? a b).
+
+nlemma PAIR : ∀A,B:setoid. setoid.
+#A B; @(A × B); @(eq_pair …);
+##[ #ab; ncases ab; #a b; @; napply #;
+##| #ab cd; ncases ab; ncases cd; #a1 a2 b1 b2; *; #E1 E2;
+ @; napply (?^-1); //;
+##| #a b c; ncases a; ncases b; ncases c; #c1 c2 b1 b2 a1 a2;
+ *; #E1 E2; *; #E3 E4; @; ##[ napply (.= E1); //] napply (.= E2); //.##]
+nqed.
+
+alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
+unification hint 0 ≔ AA, BB;
+ A ≟ carr AA, B ≟ carr BB,
+ P1 ≟ refl ? (eq0 (PAIR AA BB)),
+ P2 ≟ sym ? (eq0 (PAIR AA BB)),
+ P3 ≟ trans ? (eq0 (PAIR AA BB)),
+ R ≟ mk_setoid (A × B) (mk_equivalence_relation ? (eq_pair …) P1 P2 P3)
+(*---------------------------------------------------------------------------*)⊢
+ carr R ≡ A × B.
+
+unification hint 0 ≔ S1,S2,a,b;
+ R ≟ PAIR S1 S2,
+ L ≟ (pair S1 S2)
+(* -------------------------------------------- *) ⊢
+ eq_pair S1 S2 a b ≡ eq_rel L (eq0 R) a b.
+
+(* end move to pair *)
+
ndefinition pre ≝ λS.pitem S × bool.
notation "\fst term 90 x" non associative with precedence 90 for @{'fst $x}.
(*-----------------------------------------------------------------*) ⊢
list S ≡ carr1 TT.
-(* Ex setoid support *)
+(* XXX 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.
ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S.
#S r; @(𝐋\p r); #w1 w2 E; nelim r;
-##[ /2/;
-##| /2/;
+##[ ##1,2: /2/;
##| #x; @; *;
##| #x; @; #H; nchange in H with ([?] =_0 ?); ##[ napply ((.=_0 H) E); ##]
napply ((.=_0 H) E^-1);
//;
nqed.
-FINQUI
-manca setoide per pair (e pre)
+(* XXX problem: auto does not find # (refl) when it has a concrete == *)
+nlemma odotEt : ∀S:Alpha.∀e1,e2:pitem S.∀b2:bool.
+ 〈e1,true〉 ⊙ 〈e2,b2〉 = 〈e1 · \fst (•e2),b2 || \snd (•e2)〉.
+#S e1 e2 b2; ncases b2; nnormalize; @; //; @; napply refl; nqed.
-nlemma odotEt :
- ∀S:Alpha.∀e1,e2:pitem S.∀b2. 〈e1,true〉 ⊙ 〈e2,b2〉 = ?.〈e1 · \fst (•e2),b2 || \snd (•e2)〉.
-#S e1 e2 b2; nnormalize; ncases (•e2); //; nqed.
+nlemma LcatE : ∀S:Alpha.∀e1,e2:pitem S.
+ 𝐋\p (e1 · e2) = 𝐋\p e1 · 𝐋 |e2| ∪ 𝐋\p e2. //; nqed.
-nlemma LcatE : ∀S.∀e1,e2:pitem S.𝐋\p (e1 · e2) = 𝐋\p e1 · 𝐋 .|e2| ∪ 𝐋\p e2. //; nqed.
-
-nlemma cup_dotD : ∀S.∀p,q,r:lang S.(p ∪ q) · r = (p · r) ∪ (q · r).
-#S p q r; napply extP; #w; nnormalize; @;
+nlemma cup_dotD : ∀S:Alpha.∀p,q,r:lang S.(p ∪ q) · r = (p · r) ∪ (q · r).
+#S p q r; napply ext_set; #w; nnormalize; @;
##[ *; #x; *; #y; *; *; #defw; *; /7/ by or_introl, or_intror, ex_intro, conj;
##| *; *; #x; *; #y; *; *; /7/ by or_introl, or_intror, ex_intro, conj; ##]
nqed.
-nlemma erase_dot : ∀S.∀e1,e2:pitem S.𝐋 .|e1 · e2| = 𝐋 .|e1| · 𝐋 .|e2|.
-#S e1 e2; napply extP; nnormalize; #w; @; *; #w1; *; #w2; *; *; /7/ by ex_intro, conj;
+nlemma erase_dot : ∀S:Alpha.∀e1,e2:pitem S.𝐋 |e1 · e2| = 𝐋 |e1| · 𝐋 |e2|.
+#S e1 e2; napply ext_set; nnormalize; #w; @; *; #w1; *; #w2; *; *; /7/ by ex_intro, conj;
nqed.
-nlemma erase_plus : ∀S.∀e1,e2:pitem S.𝐋 .|e1 + e2| = 𝐋 .|e1| ∪ 𝐋 .|e2|.
-#S e1 e2; napply extP; nnormalize; #w; @; *; /4/ by or_introl, or_intror; nqed.
+nlemma erase_plus : ∀S:Alpha.∀e1,e2:pitem S.𝐋 |e1 + e2| = 𝐋 |e1| ∪ 𝐋 |e2|.
+#S e1 e2; napply ext_set; nnormalize; #w; @; *; /4/ by or_introl, or_intror; nqed.
-nlemma erase_star : ∀S.∀e1:pitem S.𝐋 .|e1|^* = 𝐋 .|e1^*|. //; nqed.
+nlemma erase_star : ∀S:Alpha.∀e1:pitem S.𝐋 |e1|^* = 𝐋 |e1^*|. //; nqed.
-ndefinition substract := λS.λp,q:word S → Prop.λw.p w ∧ ¬ q w.
+ndefinition substract := λS:Alpha.λp,q:lang S.{ w | w ∈ p ∧ ¬ w ∈ q }.
interpretation "substract" 'minus a b = (substract ? a b).
-nlemma cup_sub: ∀S.∀a,b:word S → Prop. ¬ (a []) → a ∪ (b - {[]}) = (a ∪ b) - {[]}.
-#S a b c; napply extP; #w; nnormalize; @; *; /4/; *; /4/; nqed.
+FINQUI: manca ext per substract
+
+nlemma memnil : ∀S:Alpha.∀a:list S. a ∈ {[]} → a = [ ].
+#S a; ncases a; //; nqed.
+
+nlemma cup_sub: ∀S:Alpha.∀a,b:Elang S. ¬ ([]∈ a) → a ∪ (b - {[]}) = (a ∪ b) - {[]}.
+#S a b c; napply ext_set; #w; @;
+##[ *; ##[ #wa; @; ##[@;//] #H; napply c; napply (. ?╪_0?);
+ napply (. (memnil ?? H)^-1‡#);
+/4/; *; /4/; nqed.
nlemma sub0 : ∀S.∀a:word S → Prop. a - {} = a.
#S a; napply extP; #w; nnormalize; @; /3/; *; //; nqed.
projects / helm.git / blobdiff