From: Enrico Tassi Date: Sat, 25 Sep 2010 14:55:09 +0000 (+0000) Subject: some reorganization + some more re-setoids.ma proofs X-Git-Tag: make_still_working~2824 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4b940bfbeab1181dd18c56e46761f5e6690d9f9d;p=helm.git some reorganization + some more re-setoids.ma proofs --- diff --git a/helm/software/matita/nlibrary/datatypes/bool-setoids.ma b/helm/software/matita/nlibrary/datatypes/bool-setoids.ma new file mode 100644 index 000000000..366bd9efa --- /dev/null +++ b/helm/software/matita/nlibrary/datatypes/bool-setoids.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "datatypes/bool.ma". +include "sets/setoids.ma". + +ndefinition eq_bool ≝ + λa,b.match a with + [ true ⇒ match b with [ true ⇒ True | _ ⇒ False ] + | false ⇒ match b with [ false ⇒ True | _ ⇒ False ]]. + + (* XXX move to bool *) +interpretation "bool eq" 'eq_low a b = (eq_bool a b). + +ndefinition BOOL : setoid. +@bool; @(eq_bool); #x; ncases x; //; #y; ncases y; //; #z; ncases z; //; nqed. + +alias symbol "hint_decl" (instance 1) = "hint_decl_Type1". +alias id "refl" = "cic:/matita/ng/properties/relations/refl.fix(0,1,3)". +unification hint 0 ≔ ; + P1 ≟ refl ? (eq0 BOOL), + P2 ≟ sym ? (eq0 BOOL), + P3 ≟ trans ? (eq0 BOOL), + X ≟ mk_setoid bool (mk_equivalence_relation ? (eq_bool) P1 P2 P3) +(*-----------------------------------------------------------------------*) ⊢ + carr X ≡ bool. + +unification hint 0 ≔ a,b; + R ≟ eq0 BOOL, + L ≟ bool +(* -------------------------------------------- *) ⊢ + eq_bool a b ≡ eq_rel L R a b. diff --git a/helm/software/matita/nlibrary/datatypes/bool.ma b/helm/software/matita/nlibrary/datatypes/bool.ma index be42b597a..eda979d69 100644 --- a/helm/software/matita/nlibrary/datatypes/bool.ma +++ b/helm/software/matita/nlibrary/datatypes/bool.ma @@ -14,6 +14,9 @@ include "logic/pts.ma". -ninductive bool: Type[0] ≝ - true: bool - | false: bool. \ No newline at end of file +ninductive bool: Type[0] ≝ true: bool | false: bool. + +ndefinition orb ≝ λa,b:bool. match a with [ true ⇒ true | _ ⇒ b ]. + +notation "a || b" left associative with precedence 30 for @{'orb $a $b}. +interpretation "orb" 'orb a b = (orb a b). \ No newline at end of file diff --git a/helm/software/matita/nlibrary/datatypes/list-setoids.ma b/helm/software/matita/nlibrary/datatypes/list-setoids.ma new file mode 100644 index 000000000..c836f4bf3 --- /dev/null +++ b/helm/software/matita/nlibrary/datatypes/list-setoids.ma @@ -0,0 +1,80 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "datatypes/list.ma". +include "sets/setoids.ma". + +nlet rec eq_list (A : setoid) (l1, l2 : list A) on l1 : CProp[0] ≝ +match l1 with +[ 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); +##[ #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 T) P1 P2 P3) +(*-----------------------------------------------------------------------*) ⊢ + carr X ≡ list T. + +unification hint 0 ≔ S:setoid,a,b:list S; + R ≟ eq0 (LIST S), + L ≟ (list S) +(* -------------------------------------------- *) ⊢ + eq_list S a b ≡ eq_rel L R a b. + +nlemma append_is_morph : ∀A:setoid.(list A) ⇒_0 (list A) ⇒_0 (list A). +#A; napply (mk_binary_morphism … (λs1,s2:list A. s1 @ s2)); #a; nelim a; +##[ #l1 l2 l3 defl1 El2l3; ncases l1 in defl1; ##[#;nassumption] #x xs; *; +##| #x xs IH l1 l2 l3 defl1 El2l3; ncases l1 in defl1; ##[ *] #y ys; *; #; /3/] +nqed. + +alias symbol "hint_decl" (instance 1) = "hint_decl_Type0". +unification hint 0 ≔ S:setoid, A,B:list S; + MM ≟ mk_unary_morphism ?? + (λA:list S.mk_unary_morphism ?? (λB:list S.A @ B) (prop1 ?? (append_is_morph S A))) + (prop1 ?? (append_is_morph S)), + T ≟ LIST S +(*--------------------------------------------------------------------------*) ⊢ + fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ A @ B. + + +(* XXX to understand if are always needed or only if the coercion is active *) +include "sets/setoids1.ma". + +unification hint 0 ≔ SS : setoid; + S ≟ carr SS, + TT ≟ setoid1_of_setoid (LIST SS) +(*-----------------------------------------------------------------*) ⊢ + list S ≡ carr1 TT. + +alias symbol "hint_decl" (instance 1) = "hint_decl_CProp2". +unification hint 0 ≔ S : setoid, x,y; + SS ≟ LIST S, + TT ≟ setoid1_of_setoid SS +(*-----------------------------------------*) ⊢ + eq_list S x y ≡ eq_rel1 ? (eq1 TT) x y. + \ No newline at end of file diff --git a/helm/software/matita/nlibrary/datatypes/list-theory.ma b/helm/software/matita/nlibrary/datatypes/list-theory.ma new file mode 100644 index 000000000..14bab26e3 --- /dev/null +++ b/helm/software/matita/nlibrary/datatypes/list-theory.ma @@ -0,0 +1,298 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "arithmetics/nat.ma". +include "datatypes/list.ma". + +ntheorem nil_cons: + ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ []. +#A;#l;#a; @; #H; ndestruct; +nqed. + +ntheorem append_nil: ∀A:Type.∀l:list A.l @ □ = l. +#A;#l;nelim l;//; +#a;#l1;#IH;nnormalize;//; +nqed. + +ntheorem associative_append: ∀A:Type[0].associative (list A) (append A). +#A;#x;#y;#z;nelim x +##[// +##|#a;#x1;#H;nnormalize;//] +nqed. + +ntheorem cons_append_commute: + ∀A:Type[0].∀l1,l2:list A.∀a:A. + a :: (l1 @ l2) = (a :: l1) @ l2. +//; +nqed. + +nlemma append_cons: ∀A.∀a:A.∀l,l1. l@(a::l1)=(l@[a])@l1. +#A;#a;#l;#l1;nrewrite > (associative_append ????);//; +nqed. + +(*ninductive permutation (A:Type) : list A -> list A -> Prop \def + | refl : \forall l:list A. permutation ? l l + | swap : \forall l:list A. \forall x,y:A. + permutation ? (x :: y :: l) (y :: x :: l) + | trans : \forall l1,l2,l3:list A. + permutation ? l1 l2 -> permut1 ? l2 l3 -> permutation ? l1 l3 +with permut1 : list A -> list A -> Prop \def + | step : \forall l1,l2:list A. \forall x,y:A. + permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).*) + +(* + +definition x1 \def S O. +definition x2 \def S x1. +definition x3 \def S x2. + +theorem tmp : permutation nat (x1 :: x2 :: x3 :: []) (x1 :: x3 :: x2 :: []). + apply (trans ? (x1 :: x2 :: x3 :: []) (x1 :: x2 :: x3 :: []) ?). + apply refl. + apply (step ? (x1::[]) [] x2 x3). + qed. + +theorem nil_append_nil_both: + \forall A:Type.\forall l1,l2:list A. + l1 @ l2 = [] \to l1 = [] \land l2 = []. + +theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. +reflexivity. +qed. + +theorem test_append: [O;O;O;O;O;O] = [O;O;O] @ [O;O] @ [O]. +simplify. +reflexivity. +qed. + +*) + +nlet rec nth A l d n on n ≝ + match n with + [ O ⇒ match l with + [ nil ⇒ d + | cons (x : A) _ ⇒ x ] + | S n' ⇒ nth A (tail ? l) d n']. + +nlet rec map A B f l on l ≝ + match l with [ nil ⇒ nil B | cons (x:A) tl ⇒ f x :: map A B f tl ]. + +nlet rec foldr (A,B:Type[0]) (f : A → B → B) (b:B) l on l ≝ + match l with [ nil ⇒ b | cons (a:A) tl ⇒ f a (foldr A B f b tl) ]. + +ndefinition length ≝ λT:Type[0].λl:list T.foldr T nat (λx,c.S c) O l. + +ndefinition filter ≝ + λT:Type[0].λl:list T.λp:T → bool. + foldr T (list T) + (λx,l0.match (p x) with [ true => x::l0 | false => l0]) [] l. + +ndefinition iota : nat → nat → list nat ≝ + λn,m. nat_rect_Type0 (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m. + +(* ### induction principle for functions visiting 2 lists in parallel *) +nlemma list_ind2 : + ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop. + length ? l1 = length ? l2 → + (P (nil ?) (nil ?)) → + (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) → + P l1 l2. +#T1;#T2;#l1;#l2;#P;#Hl;#Pnil;#Pcons; +ngeneralize in match Hl; ngeneralize in match l2; +nelim l1 +##[#l2;ncases l2;//; + nnormalize;#t2;#tl2;#H;ndestruct; +##|#t1;#tl1;#IH;#l2;ncases l2 + ##[nnormalize;#H;ndestruct + ##|#t2;#tl2;#H;napply Pcons;napply IH;nnormalize in H;ndestruct;//] +##] +nqed. + +nlemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l. +#A;#B;#f;#g;#l;#Efg; +nelim l; nnormalize;//; +nqed. + +nlemma le_length_filter : ∀A,l,p.length A (filter A l p) ≤ length A l. +#A;#l;#p;nelim l;nnormalize +##[// +##|#a;#tl;#IH;ncases (p a);nnormalize; + ##[napply le_S_S;//; + ##|@2;//] +##] +nqed. + +nlemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m. +#A;#l;#m;nelim l; +##[// +##|#H;#tl;#IH;nnormalize;nrewrite < IH;//] +nqed. + +ninductive in_list (A:Type): A → (list A) → Prop ≝ +| in_list_head : ∀ x,l.(in_list A x (x::l)) +| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)). + +ndefinition incl : \forall A.(list A) \to (list A) →Prop \def + \lambda A,l,m.\forall x.in_list A x l \to in_list A x m. + +notation "hvbox(a break ∉ b)" non associative with precedence 45 +for @{ 'notmem $a $b }. + +interpretation "list member" 'mem x l = (in_list ? x l). +interpretation "list not member" 'notmem x l = (Not (in_list ? x l)). +interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2). + +naxiom not_in_list_nil : \forall A,x.\lnot in_list A x []. +(*intros.unfold.intro.inversion H + [intros;lapply (sym_eq ? ? ? H2);destruct Hletin + |intros;destruct H4] +qed.*) + +naxiom in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to + x = a \lor in_list A x l. +(*intros;inversion H;intros + [destruct H2;left;reflexivity + |destruct H4;right;assumption] +qed.*) + +naxiom in_list_tail : \forall l,x,y. + in_list nat x (y::l) \to x \neq y \to in_list nat x l. +(*intros 4;elim (in_list_cons_case ? ? ? ? H) + [elim (H2 H1) + |assumption] +qed.*) + +naxiom in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y. +(*intros;elim (in_list_cons_case ? ? ? ? H) + [assumption + |elim (not_in_list_nil ? ? H1)] +qed.*) + +naxiom in_list_to_in_list_append_l: \forall A.\forall x:A. +\forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2). +(*intros. +elim H;simplify + [apply in_list_head + |apply in_list_cons;assumption + ] +qed.*) + +naxiom in_list_to_in_list_append_r: \forall A.\forall x:A. +\forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2). +(*intros 3. +elim l1;simplify + [assumption + |apply in_list_cons;apply H;assumption + ] +qed.*) + +naxiom in_list_append_to_or_in_list: \forall A:Type.\forall x:A. +\forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1. +(*intros 3. +elim l + [right.apply H + |simplify in H1.inversion H1;intros; destruct; + [left.apply in_list_head + | elim (H l2) + [left.apply in_list_cons. assumption + |right.assumption + |assumption + ] + ] + ] +qed.*) + +nlet rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝ + match l with + [ nil ⇒ false + | (cons a l') ⇒ + match eq x a with + [ true ⇒ true + | false ⇒ mem A eq x l' + ] + ]. + +naxiom mem_true_to_in_list : + \forall A,equ. + (\forall x,y.equ x y = true \to x = y) \to + \forall x,l.mem A equ x l = true \to in_list A x l. +(* intros 5.elim l + [simplify in H1;destruct H1 + |simplify in H2;apply (bool_elim ? (equ x a)) + [intro;rewrite > (H ? ? H3);apply in_list_head + |intro;rewrite > H3 in H2;simplify in H2; + apply in_list_cons;apply H1;assumption]] +qed.*) + +naxiom in_list_to_mem_true : + \forall A,equ. + (\forall x.equ x x = true) \to + \forall x,l.in_list A x l \to mem A equ x l = true. +(*intros 5.elim l + [elim (not_in_list_nil ? ? H1) + |elim H2 + [simplify;rewrite > H;reflexivity + |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]]. +qed.*) + +naxiom in_list_filter_to_p_true : \forall A,l,x,p. +in_list A x (filter A l p) \to p x = true. +(* intros 4;elim l + [simplify in H;elim (not_in_list_nil ? ? H) + |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1; + simplify in H1 + [elim (in_list_cons_case ? ? ? ? H1) + [rewrite > H3;assumption + |apply (H H3)] + |apply (H H1)]] +qed.*) + +naxiom in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l. +(*intros 4;elim l + [simplify in H;elim (not_in_list_nil ? ? H) + |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1; + simplify in H1 + [elim (in_list_cons_case ? ? ? ? H1) + [rewrite > H3;apply in_list_head + |apply in_list_cons;apply H;assumption] + |apply in_list_cons;apply H;assumption]] +qed.*) + +naxiom in_list_filter_r : \forall A,l,p,x. + in_list A x l \to p x = true \to in_list A x (filter A l p). +(* intros 4;elim l + [elim (not_in_list_nil ? ? H) + |elim (in_list_cons_case ? ? ? ? H1) + [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head + |simplify;apply (bool_elim ? (p a));intro;simplify; + [apply in_list_cons;apply H;assumption + |apply H;assumption]]] +qed.*) + +naxiom incl_A_A: ∀T,A.incl T A A. +(*intros.unfold incl.intros.assumption. +qed.*) + +naxiom incl_append_l : ∀T,A,B.incl T A (A @ B). +(*unfold incl; intros;autobatch. +qed.*) + +naxiom incl_append_r : ∀T,A,B.incl T B (A @ B). +(*unfold incl; intros;autobatch. +qed.*) + +naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B). +(*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch. +qed.*) + diff --git a/helm/software/matita/nlibrary/datatypes/list.ma b/helm/software/matita/nlibrary/datatypes/list.ma index 4188bb288..5d5ed0e34 100644 --- a/helm/software/matita/nlibrary/datatypes/list.ma +++ b/helm/software/matita/nlibrary/datatypes/list.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "arithmetics/nat.ma". +include "logic/pts.ma". ninductive list (A:Type[0]) : Type[0] ≝ | nil: list A @@ -33,301 +33,24 @@ notation "hvbox(l1 break @ l2)" interpretation "nil" 'nil = (nil ?). interpretation "cons" 'cons hd tl = (cons ? hd tl). -ntheorem nil_cons: - ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ []. -#A;#l;#a; @; #H; ndestruct; -nqed. +nlet rec append A (l1: list A) l2 on l1 ≝ + match l1 with + [ nil ⇒ l2 + | cons hd tl ⇒ hd :: append A tl l2 ]. + +interpretation "append" 'append l1 l2 = (append ? l1 l2). nlet rec id_list A (l: list A) on l ≝ match l with [ nil ⇒ [] | cons hd tl ⇒ hd :: id_list A tl ]. -nlet rec append A (l1: list A) l2 on l1 ≝ - match l1 with - [ nil ⇒ l2 - | cons hd tl ⇒ hd :: append A tl l2 ]. ndefinition tail ≝ λA:Type[0].λl:list A. match l with [ nil ⇒ [] | cons hd tl ⇒ tl]. -interpretation "append" 'append l1 l2 = (append ? l1 l2). - -ntheorem append_nil: ∀A:Type.∀l:list A.l @ [] = l. -#A;#l;nelim l;//; -#a;#l1;#IH;nnormalize;//; -nqed. - -ntheorem associative_append: ∀A:Type[0].associative (list A) (append A). -#A;#x;#y;#z;nelim x -##[// -##|#a;#x1;#H;nnormalize;//] -nqed. - -ntheorem cons_append_commute: - ∀A:Type[0].∀l1,l2:list A.∀a:A. - a :: (l1 @ l2) = (a :: l1) @ l2. -//; -nqed. - -nlemma append_cons: ∀A.∀a:A.∀l,l1. l@(a::l1)=(l@[a])@l1. -#A;#a;#l;#l1;nrewrite > (associative_append ????);//; -nqed. - -(*ninductive permutation (A:Type) : list A -> list A -> Prop \def - | refl : \forall l:list A. permutation ? l l - | swap : \forall l:list A. \forall x,y:A. - permutation ? (x :: y :: l) (y :: x :: l) - | trans : \forall l1,l2,l3:list A. - permutation ? l1 l2 -> permut1 ? l2 l3 -> permutation ? l1 l3 -with permut1 : list A -> list A -> Prop \def - | step : \forall l1,l2:list A. \forall x,y:A. - permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).*) - -(* - -definition x1 \def S O. -definition x2 \def S x1. -definition x3 \def S x2. - -theorem tmp : permutation nat (x1 :: x2 :: x3 :: []) (x1 :: x3 :: x2 :: []). - apply (trans ? (x1 :: x2 :: x3 :: []) (x1 :: x2 :: x3 :: []) ?). - apply refl. - apply (step ? (x1::[]) [] x2 x3). - qed. - -theorem nil_append_nil_both: - \forall A:Type.\forall l1,l2:list A. - l1 @ l2 = [] \to l1 = [] \land l2 = []. - -theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. -reflexivity. -qed. - -theorem test_append: [O;O;O;O;O;O] = [O;O;O] @ [O;O] @ [O]. -simplify. -reflexivity. -qed. - -*) - -nlet rec nth A l d n on n ≝ - match n with - [ O ⇒ match l with - [ nil ⇒ d - | cons (x : A) _ ⇒ x ] - | S n' ⇒ nth A (tail ? l) d n']. - -nlet rec map A B f l on l ≝ - match l with [ nil ⇒ nil B | cons (x:A) tl ⇒ f x :: map A B f tl ]. - -nlet rec foldr (A,B:Type[0]) (f : A → B → B) (b:B) l on l ≝ - match l with [ nil ⇒ b | cons (a:A) tl ⇒ f a (foldr A B f b tl) ]. - -ndefinition length ≝ λT:Type[0].λl:list T.foldr T nat (λx,c.S c) O l. - -ndefinition filter ≝ - λT:Type[0].λl:list T.λp:T → bool. - foldr T (list T) - (λx,l0.match (p x) with [ true => x::l0 | false => l0]) [] l. - -ndefinition iota : nat → nat → list nat ≝ - λn,m. nat_rect_Type0 (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m. - -(* ### induction principle for functions visiting 2 lists in parallel *) -nlemma list_ind2 : - ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop. - length ? l1 = length ? l2 → - (P (nil ?) (nil ?)) → - (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) → - P l1 l2. -#T1;#T2;#l1;#l2;#P;#Hl;#Pnil;#Pcons; -ngeneralize in match Hl; ngeneralize in match l2; -nelim l1 -##[#l2;ncases l2;//; - nnormalize;#t2;#tl2;#H;ndestruct; -##|#t1;#tl1;#IH;#l2;ncases l2 - ##[nnormalize;#H;ndestruct - ##|#t2;#tl2;#H;napply Pcons;napply IH;nnormalize in H;ndestruct;//] -##] -nqed. - -nlemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l. -#A;#B;#f;#g;#l;#Efg; -nelim l; nnormalize;//; -nqed. - -nlemma le_length_filter : ∀A,l,p.length A (filter A l p) ≤ length A l. -#A;#l;#p;nelim l;nnormalize -##[// -##|#a;#tl;#IH;ncases (p a);nnormalize; - ##[napply le_S_S;//; - ##|@2;//] -##] -nqed. - -nlemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m. -#A;#l;#m;nelim l; -##[// -##|#H;#tl;#IH;nnormalize;nrewrite < IH;//] -nqed. - -ninductive in_list (A:Type): A → (list A) → Prop ≝ -| in_list_head : ∀ x,l.(in_list A x (x::l)) -| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)). - -ndefinition incl : \forall A.(list A) \to (list A) \to Prop \def - \lambda A,l,m.\forall x.in_list A x l \to in_list A x m. - -notation "hvbox(a break ∉ b)" non associative with precedence 45 -for @{ 'notmem $a $b }. - -interpretation "list member" 'mem x l = (in_list ? x l). -interpretation "list not member" 'notmem x l = (Not (in_list ? x l)). -interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2). - -naxiom not_in_list_nil : \forall A,x.\lnot in_list A x []. -(*intros.unfold.intro.inversion H - [intros;lapply (sym_eq ? ? ? H2);destruct Hletin - |intros;destruct H4] -qed.*) - -naxiom in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to - x = a \lor in_list A x l. -(*intros;inversion H;intros - [destruct H2;left;reflexivity - |destruct H4;right;assumption] -qed.*) - -naxiom in_list_tail : \forall l,x,y. - in_list nat x (y::l) \to x \neq y \to in_list nat x l. -(*intros 4;elim (in_list_cons_case ? ? ? ? H) - [elim (H2 H1) - |assumption] -qed.*) - -naxiom in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y. -(*intros;elim (in_list_cons_case ? ? ? ? H) - [assumption - |elim (not_in_list_nil ? ? H1)] -qed.*) - -naxiom in_list_to_in_list_append_l: \forall A.\forall x:A. -\forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2). -(*intros. -elim H;simplify - [apply in_list_head - |apply in_list_cons;assumption - ] -qed.*) - -naxiom in_list_to_in_list_append_r: \forall A.\forall x:A. -\forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2). -(*intros 3. -elim l1;simplify - [assumption - |apply in_list_cons;apply H;assumption - ] -qed.*) - -naxiom in_list_append_to_or_in_list: \forall A:Type.\forall x:A. -\forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1. -(*intros 3. -elim l - [right.apply H - |simplify in H1.inversion H1;intros; destruct; - [left.apply in_list_head - | elim (H l2) - [left.apply in_list_cons. assumption - |right.assumption - |assumption - ] - ] - ] -qed.*) - -nlet rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝ - match l with - [ nil ⇒ false - | (cons a l') ⇒ - match eq x a with - [ true ⇒ true - | false ⇒ mem A eq x l' - ] - ]. - -naxiom mem_true_to_in_list : - \forall A,equ. - (\forall x,y.equ x y = true \to x = y) \to - \forall x,l.mem A equ x l = true \to in_list A x l. -(* intros 5.elim l - [simplify in H1;destruct H1 - |simplify in H2;apply (bool_elim ? (equ x a)) - [intro;rewrite > (H ? ? H3);apply in_list_head - |intro;rewrite > H3 in H2;simplify in H2; - apply in_list_cons;apply H1;assumption]] -qed.*) - -naxiom in_list_to_mem_true : - \forall A,equ. - (\forall x.equ x x = true) \to - \forall x,l.in_list A x l \to mem A equ x l = true. -(*intros 5.elim l - [elim (not_in_list_nil ? ? H1) - |elim H2 - [simplify;rewrite > H;reflexivity - |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]]. -qed.*) - -naxiom in_list_filter_to_p_true : \forall A,l,x,p. -in_list A x (filter A l p) \to p x = true. -(* intros 4;elim l - [simplify in H;elim (not_in_list_nil ? ? H) - |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1; - simplify in H1 - [elim (in_list_cons_case ? ? ? ? H1) - [rewrite > H3;assumption - |apply (H H3)] - |apply (H H1)]] -qed.*) - -naxiom in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l. -(*intros 4;elim l - [simplify in H;elim (not_in_list_nil ? ? H) - |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1; - simplify in H1 - [elim (in_list_cons_case ? ? ? ? H1) - [rewrite > H3;apply in_list_head - |apply in_list_cons;apply H;assumption] - |apply in_list_cons;apply H;assumption]] -qed.*) - -naxiom in_list_filter_r : \forall A,l,p,x. - in_list A x l \to p x = true \to in_list A x (filter A l p). -(* intros 4;elim l - [elim (not_in_list_nil ? ? H) - |elim (in_list_cons_case ? ? ? ? H1) - [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head - |simplify;apply (bool_elim ? (p a));intro;simplify; - [apply in_list_cons;apply H;assumption - |apply H;assumption]]] -qed.*) - -naxiom incl_A_A: ∀T,A.incl T A A. -(*intros.unfold incl.intros.assumption. -qed.*) - -naxiom incl_append_l : ∀T,A,B.incl T A (A @ B). -(*unfold incl; intros;autobatch. -qed.*) - -naxiom incl_append_r : ∀T,A,B.incl T B (A @ B). -(*unfold incl; intros;autobatch. -qed.*) - -naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B). -(*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch. -qed.*) +nlet rec flatten S (l : list (list S)) on l : list S ≝ +match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ]. diff --git a/helm/software/matita/nlibrary/datatypes/pairs-setoids.ma b/helm/software/matita/nlibrary/datatypes/pairs-setoids.ma new file mode 100644 index 000000000..43c12f768 --- /dev/null +++ b/helm/software/matita/nlibrary/datatypes/pairs-setoids.ma @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "datatypes/pairs.ma". +include "sets/setoids.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. + + \ No newline at end of file diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends index 22a5cb835..0f936d55e 100644 --- a/helm/software/matita/nlibrary/depends +++ b/helm/software/matita/nlibrary/depends @@ -1,52 +1,64 @@ -arithmetics/R.ma arithmetics/nat.ma datatypes/pairs.ma datatypes/sums.ma topology/igft.ma -overlap/o-algebra.ma sets/categories2.ma -algebra/bool.ma logic/connectives.ma -algebra/abelian_magmas.ma algebra/magmas.ma +.unnamed.ma datatypes/list.ma sets/setoids.ma +PTS/subst.ma basics/list2.ma +topology/igft3.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma basics/functions.ma Plogic/connectives.ma Plogic/equality.ma -Plogic/connectives.ma Plogic/equality.ma -arithmetics/nat.ma basics/bool.ma basics/eq.ma basics/functions.ma hints_declaration.ma -datatypes/bool.ma logic/pts.ma -datatypes/sums.ma datatypes/pairs.ma -logic/destruct_bb.ma logic/equality.ma -logic/equality.ma logic/connectives.ma properties/relations.ma -sets/partitions.ma datatypes/pairs.ma nat/compare.ma nat/minus.ma nat/plus.ma sets/sets.ma -logic/cprop.ma hints_declaration.ma sets/setoids1.ma -basics/bool.ma basics/eq.ma basics/functions.ma -topology/igft.ma logic/equality.ma sets/sets.ma -nat/minus.ma nat/order.ma -algebra/magmas.ma sets/sets.ma -hints_declaration.ma logic/pts.ma -arithmetics/Z.ma arithmetics/nat.ma +nat/compare.ma datatypes/bool.ma nat/order.ma arithmetics/compare.ma arithmetics/nat.ma +datatypes/list-setoids.ma datatypes/list.ma sets/setoids.ma +datatypes/list-theory.ma arithmetics/nat.ma datatypes/list.ma +logic/pts.ma +basics/relations.ma Plogic/connectives.ma Plogic/equality.ma logic/pts.ma -properties/relations1.ma logic/pts.ma -TPTP.ma basics/eq.ma -PTS/gpts.ma PTS/subst.ma -datatypes/list.ma arithmetics/nat.ma -nat/compare.ma datatypes/bool.ma nat/order.ma -algebra/unital_magmas.ma algebra/magmas.ma +Plogic/connectives.ma Plogic/equality.ma sets/categories.ma sets/sets.ma -properties/relations2.ma logic/pts.ma -nat/nat.ma hints_declaration.ma logic/equality.ma sets/setoids.ma -logic/connectives.ma logic/pts.ma -basics/list.ma basics/bool.ma basics/eq.ma -basics/relations.ma Plogic/connectives.ma -basics/list2.ma arithmetics/nat.ma basics/list.ma -topology/igft-setoid.ma sets/sets.ma -sets/categories2.ma sets/categories.ma sets/setoids2.ma sets/sets.ma -sets/sets.ma hints_declaration.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma datatypes/pairs.ma logic/pts.ma -nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma -nat/order.ma nat/nat.ma sets/sets.ma -logic/pts.ma +algebra/magmas.ma sets/sets.ma +Plogic/russell_support.ma Plogic/connectives.ma Plogic/jmeq.ma datatypes/sums.ma logic/connectives.ma topology/cantor.ma nat/nat.ma topology/igft.ma -sets/setoids1.ma hints_declaration.ma properties/relations1.ma sets/setoids.ma +logic/cprop.ma hints_declaration.ma sets/setoids1.ma +TPTP.ma basics/eq.ma sets/setoids2.ma properties/relations2.ma sets/setoids1.ma -nat/big_ops.ma algebra/magmas.ma nat/order.ma +nat/plus.ma algebra/abelian_magmas.ma algebra/unital_magmas.ma nat/big_ops.ma +sets/sets.ma logic/connectives.ma logic/cprop.ma properties/relations1.ma sets/setoids1.ma +PTS/gpts.ma PTS/subst.ma +re/re-setoids.ma datatypes/bool-setoids.ma datatypes/list-setoids.ma datatypes/pairs-setoids.ma hints_declaration.ma sets/sets.ma topology/igft2.ma arithmetics/nat.ma topology/igft.ma -PTS/subst.ma basics/list2.ma -topology/igft3.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma +arithmetics/Z.ma arithmetics/nat.ma +datatypes/bool.ma logic/pts.ma +logic/connectives.ma logic/pts.ma +properties/relations2.ma logic/pts.ma +algebra/bool.ma logic/connectives.ma +sets/categories2.ma sets/categories.ma sets/setoids2.ma sets/sets.ma +basics/list2.ma arithmetics/nat.ma basics/list.ma +arithmetics/nat.ma basics/bool.ma basics/eq.ma basics/functions.ma hints_declaration.ma +sets/setoids1.ma hints_declaration.ma properties/relations1.ma sets/setoids.ma +nat/minus.ma nat/order.ma +logic/cologic.ma Plogic/connectives.ma Plogic/equality.ma datatypes/bool.ma logic/equality.ma logic/pts.ma +SET171^3.ma TPTP.ma +datatypes/list.ma logic/pts.ma +Plogic/jmeq.ma Plogic/equality.ma +sets/partitions.ma datatypes/pairs.ma nat/compare.ma nat/minus.ma nat/plus.ma sets/sets.ma +topology/igft-setoid.ma sets/sets.ma +sets/setoids.ma hints_declaration.ma logic/connectives.ma properties/relations.ma properties/relations.ma logic/pts.ma -basics/eq.ma basics/relations.ma +nat/big_ops.ma algebra/magmas.ma nat/order.ma +arithmetics/R.ma arithmetics/nat.ma datatypes/pairs.ma datatypes/sums.ma topology/igft.ma +arithmetics/minimization.ma arithmetics/nat.ma +algebra/unital_magmas.ma algebra/magmas.ma +properties/relations1.ma logic/pts.ma +basics/bool.ma basics/eq.ma basics/functions.ma +datatypes/bool-setoids.ma datatypes/bool.ma sets/setoids.ma +logic/equality.ma logic/connectives.ma properties/relations.ma +datatypes/pairs-setoids.ma datatypes/pairs.ma sets/setoids.ma topology/igft4.ma arithmetics/nat.ma datatypes/bool.ma topology/igft.ma -sets/setoids.ma hints_declaration.ma logic/connectives.ma properties/relations.ma +basics/eq.ma basics/relations.ma +datatypes/sums.ma datatypes/pairs.ma +hints_declaration.ma logic/pts.ma +logic/destruct_bb.ma logic/equality.ma +topology/igft.ma logic/equality.ma sets/sets.ma +algebra/abelian_magmas.ma algebra/magmas.ma +overlap/o-algebra.ma sets/categories2.ma +re/re.ma arithmetics/nat.ma datatypes/list.ma datatypes/pairs.ma hints_declaration.ma +basics/list.ma basics/bool.ma basics/eq.ma +nat/nat.ma hints_declaration.ma logic/equality.ma sets/setoids.ma +nat/order.ma nat/nat.ma sets/sets.ma diff --git a/helm/software/matita/nlibrary/depends.dot b/helm/software/matita/nlibrary/depends.dot index f5f30de8d..f3f71b61d 100644 --- a/helm/software/matita/nlibrary/depends.dot +++ b/helm/software/matita/nlibrary/depends.dot @@ -1,147 +1,189 @@ digraph g { - "arithmetics/R.ma" []; - "arithmetics/R.ma" -> "arithmetics/nat.ma" []; - "arithmetics/R.ma" -> "datatypes/pairs.ma" []; - "arithmetics/R.ma" -> "datatypes/sums.ma" []; - "arithmetics/R.ma" -> "topology/igft.ma" []; - "overlap/o-algebra.ma" []; - "overlap/o-algebra.ma" -> "sets/categories2.ma" []; - "algebra/bool.ma" []; - "algebra/bool.ma" -> "logic/connectives.ma" []; - "algebra/abelian_magmas.ma" []; - "algebra/abelian_magmas.ma" -> "algebra/magmas.ma" []; + ".unnamed.ma" []; + ".unnamed.ma" -> "datatypes/list.ma" []; + ".unnamed.ma" -> "sets/setoids.ma" []; + "PTS/subst.ma" []; + "PTS/subst.ma" -> "basics/list2.ma" []; + "topology/igft3.ma" []; + "topology/igft3.ma" -> "arithmetics/nat.ma" []; + "topology/igft3.ma" -> "datatypes/bool.ma" []; + "topology/igft3.ma" -> "topology/igft.ma" []; "basics/functions.ma" []; "basics/functions.ma" -> "Plogic/connectives.ma" []; "basics/functions.ma" -> "Plogic/equality.ma" []; + "nat/compare.ma" []; + "nat/compare.ma" -> "datatypes/bool.ma" []; + "nat/compare.ma" -> "nat/order.ma" []; + "arithmetics/compare.ma" []; + "arithmetics/compare.ma" -> "arithmetics/nat.ma" []; + "datatypes/list-setoids.ma" []; + "datatypes/list-setoids.ma" -> "datatypes/list.ma" []; + "datatypes/list-setoids.ma" -> "sets/setoids.ma" []; + "datatypes/list-theory.ma" []; + "datatypes/list-theory.ma" -> "arithmetics/nat.ma" []; + "datatypes/list-theory.ma" -> "datatypes/list.ma" []; + "logic/pts.ma" []; + "basics/relations.ma" []; + "basics/relations.ma" -> "Plogic/connectives.ma" []; + "Plogic/equality.ma" []; + "Plogic/equality.ma" -> "logic/pts.ma" []; "Plogic/connectives.ma" []; "Plogic/connectives.ma" -> "Plogic/equality.ma" []; - "arithmetics/nat.ma" []; - "arithmetics/nat.ma" -> "basics/bool.ma" []; - "arithmetics/nat.ma" -> "basics/eq.ma" []; - "arithmetics/nat.ma" -> "basics/functions.ma" []; - "arithmetics/nat.ma" -> "hints_declaration.ma" []; - "datatypes/bool.ma" []; - "datatypes/bool.ma" -> "logic/pts.ma" []; - "datatypes/sums.ma" []; - "datatypes/sums.ma" -> "datatypes/pairs.ma" []; - "logic/destruct_bb.ma" []; - "logic/destruct_bb.ma" -> "logic/equality.ma" []; - "logic/equality.ma" []; - "logic/equality.ma" -> "logic/connectives.ma" []; - "logic/equality.ma" -> "properties/relations.ma" []; - "sets/partitions.ma" []; - "sets/partitions.ma" -> "datatypes/pairs.ma" []; - "sets/partitions.ma" -> "nat/compare.ma" []; - "sets/partitions.ma" -> "nat/minus.ma" []; - "sets/partitions.ma" -> "nat/plus.ma" []; - "sets/partitions.ma" -> "sets/sets.ma" []; + "sets/categories.ma" []; + "sets/categories.ma" -> "sets/sets.ma" []; + "datatypes/pairs.ma" []; + "datatypes/pairs.ma" -> "logic/pts.ma" []; + "algebra/magmas.ma" []; + "algebra/magmas.ma" -> "sets/sets.ma" []; + "Plogic/russell_support.ma" []; + "Plogic/russell_support.ma" -> "Plogic/connectives.ma" []; + "Plogic/russell_support.ma" -> "Plogic/jmeq.ma" []; + "Plogic/russell_support.ma" -> "datatypes/sums.ma" []; + "Plogic/russell_support.ma" -> "logic/connectives.ma" []; + "topology/cantor.ma" []; + "topology/cantor.ma" -> "nat/nat.ma" []; + "topology/cantor.ma" -> "topology/igft.ma" []; "logic/cprop.ma" []; "logic/cprop.ma" -> "hints_declaration.ma" []; "logic/cprop.ma" -> "sets/setoids1.ma" []; - "basics/bool.ma" []; - "basics/bool.ma" -> "basics/eq.ma" []; - "basics/bool.ma" -> "basics/functions.ma" []; - "topology/igft.ma" []; - "topology/igft.ma" -> "logic/equality.ma" []; - "topology/igft.ma" -> "sets/sets.ma" []; - "nat/minus.ma" []; - "nat/minus.ma" -> "nat/order.ma" []; - "algebra/magmas.ma" []; - "algebra/magmas.ma" -> "sets/sets.ma" []; - "hints_declaration.ma" []; - "hints_declaration.ma" -> "logic/pts.ma" []; - "arithmetics/Z.ma" []; - "arithmetics/Z.ma" -> "arithmetics/nat.ma" []; - "arithmetics/compare.ma" []; - "arithmetics/compare.ma" -> "arithmetics/nat.ma" []; - "Plogic/equality.ma" []; - "Plogic/equality.ma" -> "logic/pts.ma" []; - "properties/relations1.ma" []; - "properties/relations1.ma" -> "logic/pts.ma" []; "TPTP.ma" []; "TPTP.ma" -> "basics/eq.ma" []; + "sets/setoids2.ma" []; + "sets/setoids2.ma" -> "properties/relations2.ma" []; + "sets/setoids2.ma" -> "sets/setoids1.ma" []; + "nat/plus.ma" []; + "nat/plus.ma" -> "algebra/abelian_magmas.ma" []; + "nat/plus.ma" -> "algebra/unital_magmas.ma" []; + "nat/plus.ma" -> "nat/big_ops.ma" []; + "sets/sets.ma" []; + "sets/sets.ma" -> "logic/connectives.ma" []; + "sets/sets.ma" -> "logic/cprop.ma" []; + "sets/sets.ma" -> "properties/relations1.ma" []; + "sets/sets.ma" -> "sets/setoids1.ma" []; "PTS/gpts.ma" []; "PTS/gpts.ma" -> "PTS/subst.ma" []; - "datatypes/list.ma" []; - "datatypes/list.ma" -> "arithmetics/nat.ma" []; - "nat/compare.ma" []; - "nat/compare.ma" -> "datatypes/bool.ma" []; - "nat/compare.ma" -> "nat/order.ma" []; - "algebra/unital_magmas.ma" []; - "algebra/unital_magmas.ma" -> "algebra/magmas.ma" []; - "sets/categories.ma" []; - "sets/categories.ma" -> "sets/sets.ma" []; - "properties/relations2.ma" []; - "properties/relations2.ma" -> "logic/pts.ma" []; - "nat/nat.ma" []; - "nat/nat.ma" -> "hints_declaration.ma" []; - "nat/nat.ma" -> "logic/equality.ma" []; - "nat/nat.ma" -> "sets/setoids.ma" []; + "re/re-setoids.ma" []; + "re/re-setoids.ma" -> "datatypes/bool-setoids.ma" []; + "re/re-setoids.ma" -> "datatypes/list-setoids.ma" []; + "re/re-setoids.ma" -> "datatypes/pairs-setoids.ma" []; + "re/re-setoids.ma" -> "hints_declaration.ma" []; + "re/re-setoids.ma" -> "sets/sets.ma" []; + "topology/igft2.ma" []; + "topology/igft2.ma" -> "arithmetics/nat.ma" []; + "topology/igft2.ma" -> "topology/igft.ma" []; + "arithmetics/Z.ma" []; + "arithmetics/Z.ma" -> "arithmetics/nat.ma" []; + "datatypes/bool.ma" []; + "datatypes/bool.ma" -> "logic/pts.ma" []; "logic/connectives.ma" []; "logic/connectives.ma" -> "logic/pts.ma" []; - "basics/list.ma" []; - "basics/list.ma" -> "basics/bool.ma" []; - "basics/list.ma" -> "basics/eq.ma" []; - "basics/relations.ma" []; - "basics/relations.ma" -> "Plogic/connectives.ma" []; - "basics/list2.ma" []; - "basics/list2.ma" -> "arithmetics/nat.ma" []; - "basics/list2.ma" -> "basics/list.ma" []; - "topology/igft-setoid.ma" []; - "topology/igft-setoid.ma" -> "sets/sets.ma" []; + "properties/relations2.ma" []; + "properties/relations2.ma" -> "logic/pts.ma" []; + "algebra/bool.ma" []; + "algebra/bool.ma" -> "logic/connectives.ma" []; "sets/categories2.ma" []; "sets/categories2.ma" -> "sets/categories.ma" []; "sets/categories2.ma" -> "sets/setoids2.ma" []; "sets/categories2.ma" -> "sets/sets.ma" []; - "sets/sets.ma" []; - "sets/sets.ma" -> "hints_declaration.ma" []; - "sets/sets.ma" -> "logic/connectives.ma" []; - "sets/sets.ma" -> "logic/cprop.ma" []; - "sets/sets.ma" -> "properties/relations1.ma" []; - "sets/sets.ma" -> "sets/setoids1.ma" []; - "datatypes/pairs.ma" []; - "datatypes/pairs.ma" -> "logic/pts.ma" []; - "nat/plus.ma" []; - "nat/plus.ma" -> "algebra/abelian_magmas.ma" []; - "nat/plus.ma" -> "algebra/unital_magmas.ma" []; - "nat/plus.ma" -> "nat/big_ops.ma" []; - "nat/order.ma" []; - "nat/order.ma" -> "nat/nat.ma" []; - "nat/order.ma" -> "sets/sets.ma" []; - "logic/pts.ma" []; - "topology/cantor.ma" []; - "topology/cantor.ma" -> "nat/nat.ma" []; - "topology/cantor.ma" -> "topology/igft.ma" []; + "basics/list2.ma" []; + "basics/list2.ma" -> "arithmetics/nat.ma" []; + "basics/list2.ma" -> "basics/list.ma" []; + "arithmetics/nat.ma" []; + "arithmetics/nat.ma" -> "basics/bool.ma" []; + "arithmetics/nat.ma" -> "basics/eq.ma" []; + "arithmetics/nat.ma" -> "basics/functions.ma" []; + "arithmetics/nat.ma" -> "hints_declaration.ma" []; "sets/setoids1.ma" []; "sets/setoids1.ma" -> "hints_declaration.ma" []; "sets/setoids1.ma" -> "properties/relations1.ma" []; "sets/setoids1.ma" -> "sets/setoids.ma" []; - "sets/setoids2.ma" []; - "sets/setoids2.ma" -> "properties/relations2.ma" []; - "sets/setoids2.ma" -> "sets/setoids1.ma" []; + "nat/minus.ma" []; + "nat/minus.ma" -> "nat/order.ma" []; + "logic/cologic.ma" []; + "logic/cologic.ma" -> "Plogic/connectives.ma" []; + "logic/cologic.ma" -> "Plogic/equality.ma" []; + "logic/cologic.ma" -> "datatypes/bool.ma" []; + "logic/cologic.ma" -> "logic/equality.ma" []; + "logic/cologic.ma" -> "logic/pts.ma" []; + "SET171^3.ma" []; + "SET171^3.ma" -> "TPTP.ma" []; + "datatypes/list.ma" []; + "datatypes/list.ma" -> "logic/pts.ma" []; + "Plogic/jmeq.ma" []; + "Plogic/jmeq.ma" -> "Plogic/equality.ma" []; + "sets/partitions.ma" []; + "sets/partitions.ma" -> "datatypes/pairs.ma" []; + "sets/partitions.ma" -> "nat/compare.ma" []; + "sets/partitions.ma" -> "nat/minus.ma" []; + "sets/partitions.ma" -> "nat/plus.ma" []; + "sets/partitions.ma" -> "sets/sets.ma" []; + "topology/igft-setoid.ma" []; + "topology/igft-setoid.ma" -> "sets/sets.ma" []; + "sets/setoids.ma" []; + "sets/setoids.ma" -> "hints_declaration.ma" []; + "sets/setoids.ma" -> "logic/connectives.ma" []; + "sets/setoids.ma" -> "properties/relations.ma" []; + "properties/relations.ma" []; + "properties/relations.ma" -> "logic/pts.ma" []; "nat/big_ops.ma" []; "nat/big_ops.ma" -> "algebra/magmas.ma" []; "nat/big_ops.ma" -> "nat/order.ma" []; - "topology/igft2.ma" []; - "topology/igft2.ma" -> "arithmetics/nat.ma" []; - "topology/igft2.ma" -> "topology/igft.ma" []; - "PTS/subst.ma" []; - "PTS/subst.ma" -> "basics/list2.ma" []; - "topology/igft3.ma" []; - "topology/igft3.ma" -> "arithmetics/nat.ma" []; - "topology/igft3.ma" -> "datatypes/bool.ma" []; - "topology/igft3.ma" -> "topology/igft.ma" []; - "properties/relations.ma" []; - "properties/relations.ma" -> "logic/pts.ma" []; - "basics/eq.ma" []; - "basics/eq.ma" -> "basics/relations.ma" []; + "arithmetics/R.ma" []; + "arithmetics/R.ma" -> "arithmetics/nat.ma" []; + "arithmetics/R.ma" -> "datatypes/pairs.ma" []; + "arithmetics/R.ma" -> "datatypes/sums.ma" []; + "arithmetics/R.ma" -> "topology/igft.ma" []; + "arithmetics/minimization.ma" []; + "arithmetics/minimization.ma" -> "arithmetics/nat.ma" []; + "algebra/unital_magmas.ma" []; + "algebra/unital_magmas.ma" -> "algebra/magmas.ma" []; + "properties/relations1.ma" []; + "properties/relations1.ma" -> "logic/pts.ma" []; + "basics/bool.ma" []; + "basics/bool.ma" -> "basics/eq.ma" []; + "basics/bool.ma" -> "basics/functions.ma" []; + "datatypes/bool-setoids.ma" []; + "datatypes/bool-setoids.ma" -> "datatypes/bool.ma" []; + "datatypes/bool-setoids.ma" -> "sets/setoids.ma" []; + "logic/equality.ma" []; + "logic/equality.ma" -> "logic/connectives.ma" []; + "logic/equality.ma" -> "properties/relations.ma" []; + "datatypes/pairs-setoids.ma" []; + "datatypes/pairs-setoids.ma" -> "datatypes/pairs.ma" []; + "datatypes/pairs-setoids.ma" -> "sets/setoids.ma" []; "topology/igft4.ma" []; "topology/igft4.ma" -> "arithmetics/nat.ma" []; "topology/igft4.ma" -> "datatypes/bool.ma" []; "topology/igft4.ma" -> "topology/igft.ma" []; - "sets/setoids.ma" []; - "sets/setoids.ma" -> "hints_declaration.ma" []; - "sets/setoids.ma" -> "logic/connectives.ma" []; - "sets/setoids.ma" -> "properties/relations.ma" []; + "basics/eq.ma" []; + "basics/eq.ma" -> "basics/relations.ma" []; + "datatypes/sums.ma" []; + "datatypes/sums.ma" -> "datatypes/pairs.ma" []; + "hints_declaration.ma" []; + "hints_declaration.ma" -> "logic/pts.ma" []; + "logic/destruct_bb.ma" []; + "logic/destruct_bb.ma" -> "logic/equality.ma" []; + "topology/igft.ma" []; + "topology/igft.ma" -> "logic/equality.ma" []; + "topology/igft.ma" -> "sets/sets.ma" []; + "algebra/abelian_magmas.ma" []; + "algebra/abelian_magmas.ma" -> "algebra/magmas.ma" []; + "overlap/o-algebra.ma" []; + "overlap/o-algebra.ma" -> "sets/categories2.ma" []; + "re/re.ma" []; + "re/re.ma" -> "arithmetics/nat.ma" []; + "re/re.ma" -> "datatypes/list.ma" []; + "re/re.ma" -> "datatypes/pairs.ma" []; + "re/re.ma" -> "hints_declaration.ma" []; + "basics/list.ma" []; + "basics/list.ma" -> "basics/bool.ma" []; + "basics/list.ma" -> "basics/eq.ma" []; + "nat/nat.ma" []; + "nat/nat.ma" -> "hints_declaration.ma" []; + "nat/nat.ma" -> "logic/equality.ma" []; + "nat/nat.ma" -> "sets/setoids.ma" []; + "nat/order.ma" []; + "nat/order.ma" -> "nat/nat.ma" []; + "nat/order.ma" -> "sets/sets.ma" []; } \ No newline at end of file diff --git a/helm/software/matita/nlibrary/depends.png b/helm/software/matita/nlibrary/depends.png index f030d04c1..63ad7eab1 100644 Binary files a/helm/software/matita/nlibrary/depends.png and b/helm/software/matita/nlibrary/depends.png differ diff --git a/helm/software/matita/nlibrary/re/re-setoids.ma b/helm/software/matita/nlibrary/re/re-setoids.ma index 29e7c5ed2..dcf1d85fe 100644 --- a/helm/software/matita/nlibrary/re/re-setoids.ma +++ b/helm/software/matita/nlibrary/re/re-setoids.ma @@ -12,8 +12,9 @@ (* *) (**************************************************************************) -include "datatypes/pairs.ma". -include "datatypes/bool.ma". +include "datatypes/pairs-setoids.ma". +include "datatypes/bool-setoids.ma". +include "datatypes/list-setoids.ma". include "sets/sets.ma". (* @@ -21,82 +22,13 @@ 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. - -nlet rec eq_list (A : setoid) (l1, l2 : list A) on l1 : CProp[0] ≝ -match l1 with -[ 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); -##[ #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 T) P1 P2 P3) -(*-----------------------------------------------------------------------*) ⊢ - carr X ≡ list T. - -unification hint 0 ≔ SS : setoid; - S ≟ carr SS, - TT ≟ setoid1_of_setoid (LIST SS) -(*-----------------------------------------------------------------*) ⊢ - list S ≡ carr1 TT. - -unification hint 0 ≔ S:setoid,a,b:list S; - R ≟ eq0 (LIST S), - L ≟ (list S) -(* -------------------------------------------- *) ⊢ - eq_list S a b ≡ eq_rel L R a b. - -alias symbol "hint_decl" (instance 1) = "hint_decl_CProp2". -unification hint 0 ≔ S : setoid, x,y; - SS ≟ LIST S, - TT ≟ setoid1_of_setoid SS -(*-----------------------------------------*) ⊢ - eq_list S x y ≡ eq_rel1 ? (eq1 TT) x y. - -notation "hvbox(hd break :: tl)" - right associative with precedence 47 - for @{'cons $hd $tl}. - -notation "[ list0 x sep ; ]" - non associative with precedence 90 - for ${fold right @'nil rec acc @{'cons $x $acc}}. - -notation "hvbox(l1 break @ l2)" - right associative with precedence 47 - for @{'append $l1 $l2 }. - -interpretation "nil" 'nil = (nil ?). -interpretation "cons" 'cons hd tl = (cons ? hd tl). +(* XXX move somewere else *) +ndefinition if': ∀A,B:CPROP. A = B → A → B. +#A B; *; /2/. nqed. -nlet rec append A (l1: list A) l2 on l1 ≝ - match l1 with - [ nil ⇒ l2 - | cons hd tl ⇒ hd :: append A tl l2 ]. +ncoercion if : ∀A,B:CPROP. ∀p:A = B. A → B ≝ if' on _p : eq_rel1 ???? to ∀_:?.?. -interpretation "append" 'append l1 l2 = (append ? l1 l2). +(* XXX move to list-setoids-theory.ma *) ntheorem append_nil: ∀A:setoid.∀l:list A.l @ [] = l. #A;#l;nelim l;//; #a;#l1;#IH;nnormalize;/2/;nqed. @@ -106,57 +38,37 @@ ndefinition associative ≝ λA:setoid.λf:A → A → A.∀x,y,z.f x (f y z) = ntheorem associative_append: ∀A:setoid.associative (list A) (append A). #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 *) + +(* XXX to undestand what I want inside Alpha + the eqb part should be split away, but when available it should be + possible to obtain a leibnitz equality on lemmas proved on setoids +*) interpretation "iff" 'iff a b = (iff a b). -ninductive eq (A:Type[0]) (x:A) : A → CProp[0] ≝ refl: eq A x x. +ninductive eq (A:Type[0]) (x:A) : A → CProp[0] ≝ erefl: eq A x x. nlemma eq_rect_Type0_r': - ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → P x p. + ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[0]. P a (erefl A a) → P x p. #A; #a; #x; #p; ncases p; #P; #H; nassumption. nqed. nlemma eq_rect_Type0_r: - ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. + ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (erefl A a) → ∀x.∀p:eq ? x a.P x p. #A; #a; #P; #p; #x0; #p0; napply (eq_rect_Type0_r' ??? p0); nassumption. nqed. nlemma eq_rect_CProp0_r': - ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p. + ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (erefl A a) → P x p. #A; #a; #x; #p; ncases p; #P; #H; nassumption. nqed. nlemma eq_rect_CProp0_r: - ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. + ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (erefl A a) → ∀x.∀p:eq ? x a.P x p. #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption. nqed. -(* XXX move to bool *) -interpretation "bool eq" 'eq_low a b = (eq bool a b). - -ndefinition BOOL : setoid. -@bool; @(eq bool); nnormalize; //; #x y; ##[ #E; ncases E; ##| #y H; ncases H; ##] //; nqed. - -alias symbol "hint_decl" (instance 1) = "hint_decl_Type1". -alias id "refl" = "cic:/matita/ng/properties/relations/refl.fix(0,1,3)". -unification hint 0 ≔ ; - P1 ≟ refl ? (eq0 BOOL), - P2 ≟ sym ? (eq0 BOOL), - P3 ≟ trans ? (eq0 BOOL), - X ≟ mk_setoid bool (mk_equivalence_relation ? (eq bool) P1 P2 P3) -(*-----------------------------------------------------------------------*) ⊢ - carr X ≡ bool. - -unification hint 0 ≔ a,b; - R ≟ eq0 BOOL, - L ≟ bool -(* -------------------------------------------- *) ⊢ - eq bool a b ≡ eq_rel L R a b. - nrecord Alpha : Type[1] ≝ { acarr :> setoid; eqb: acarr → acarr → bool; @@ -164,7 +76,9 @@ nrecord Alpha : Type[1] ≝ { }. interpretation "eqb" 'eq_low a b = (eqb ? a b). +(* end alpha *) +(* re *) ninductive re (S: Type[0]) : Type[0] ≝ z: re S | e: re S @@ -173,6 +87,30 @@ ninductive re (S: Type[0]) : Type[0] ≝ | o: re S → re S → re S | k: re S → re S. +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). +interpretation "or" 'plus a b = (o ? a b). + +notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}. +interpretation "cat" 'pc a b = (c ? a b). + +(* to get rid of \middot *) +ncoercion c : ∀S.∀p:re S. re S → re S ≝ c on _p : re ? to ∀_:?.?. + +notation < "a" non associative with precedence 90 for @{ 'ps $a}. +notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}. +interpretation "atom" 'ps a = (s ? a). + +notation "ϵ" non associative with precedence 90 for @{ 'epsilon }. +interpretation "epsilon" 'epsilon = (e ?). + +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) }. + (* setoid support for re *) nlet rec eq_re (S:Alpha) (a,b : re S) on a : CProp[0] ≝ @@ -203,8 +141,6 @@ ndefinition RE : Alpha → setoid. #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, @@ -222,7 +158,7 @@ unification hint 0 ≔ A:Alpha,a,b:re A; eq_re A a b ≡ eq_rel L R a b. nlemma c_is_morph : ∀A:Alpha.(re A) ⇒_0 (re A) ⇒_0 (re A). -#A; napply (mk_binary_morphism … (λs1,s2:re A. c A s1 s2)); +#A; napply (mk_binary_morphism … (λs1,s2:re A. s1 · s2)); #a; nelim a; ##[##1,2: #a' b b'; ncases a'; nnormalize; /2/ by conj; ##|#x a' b b'; ncases a'; /2/ by conj; @@ -231,16 +167,17 @@ nlemma c_is_morph : ∀A:Alpha.(re A) ⇒_0 (re A) ⇒_0 (re A). nqed. (* XXX This is the good format for hints about morphisms, fix the others *) +alias symbol "hint_decl" (instance 1) = "hint_decl_Type0". unification hint 0 ≔ S:Alpha, A,B:re S; MM ≟ mk_unary_morphism ?? - (λA:re S.mk_unary_morphism ?? (λB.c ? A B) (prop1 ?? (c_is_morph S A))) + (λA:re S.mk_unary_morphism ?? (λB.A · B) (prop1 ?? (c_is_morph S A))) (prop1 ?? (c_is_morph S)), T ≟ RE S (*--------------------------------------------------------------------------*) ⊢ - fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ c S A B. + fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ A · B. nlemma o_is_morph : ∀A:Alpha.(re A) ⇒_0 (re A) ⇒_0 (re A). -#A; napply (mk_binary_morphism … (λs1,s2:re A. o A s1 s2)); +#A; napply (mk_binary_morphism … (λs1,s2:re A. s1 + s2)); #a; nelim a; ##[##1,2: #a' b b'; ncases a'; nnormalize; /2/ by conj; ##|#x a' b b'; ncases a'; /2/ by conj; @@ -250,47 +187,17 @@ nqed. unification hint 0 ≔ S:Alpha, A,B:re S; MM ≟ mk_unary_morphism ?? - (λA:re S.mk_unary_morphism ?? (λB.o ? A B) (prop1 ?? (o_is_morph S A))) + (λA:re S.mk_unary_morphism ?? (λB.A + B) (prop1 ?? (o_is_morph S A))) (prop1 ?? (o_is_morph S)), T ≟ RE S (*--------------------------------------------------------------------------*) ⊢ - fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ o S A B. - + fun1 T T (fun1 T (unary_morph_setoid T T) MM A) B ≡ A + B. (* end setoids support for re *) -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). -interpretation "or" 'plus a b = (o ? a b). - -notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}. -interpretation "cat" 'pc a b = (c ? a b). - -(* to get rid of \middot *) -ncoercion c : ∀S.∀p:re S. re S → re S ≝ c on _p : re ? to ∀_:?.?. - -notation < "a" non associative with precedence 90 for @{ 'ps $a}. -notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}. -interpretation "atom" 'ps a = (s ? a). - -notation "ϵ" non associative with precedence 90 for @{ 'epsilon }. -interpretation "epsilon" 'epsilon = (e ?). - -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 sing_lang : ∀A:setoid.∀x:A.Ω^A ≝ λS.λx.{ w | x = w }. -interpretation "sing lang" 'singl x = (sing_lang ? x). -*) - interpretation "subset construction with type" 'comprehension t \eta.x = (mk_powerclass t x). @@ -314,10 +221,6 @@ match r with notation "𝐋 term 70 E" non associative with precedence 75 for @{'L_re $E}. interpretation "in_l" 'L_re E = (L_re ? E). -notation "a || b" left associative with precedence 30 for @{'orb $a $b}. -ndefinition orb ≝ λa,b:bool. match a with [ true ⇒ true | _ ⇒ b ]. -interpretation "orb" 'orb a b = (orb a b). - ninductive pitem (S: Type[0]) : Type[0] ≝ pz: pitem S | pe: pitem S @@ -327,6 +230,19 @@ ninductive pitem (S: Type[0]) : Type[0] ≝ | po: pitem S → pitem S → pitem S | pk: pitem S → pitem S. +interpretation "pstar" 'pk a = (pk ? a). +interpretation "por" 'plus a b = (po ? a b). +interpretation "pcat" 'pc a b = (pc ? a b). +notation < ".a" non associative with precedence 90 for @{ 'pp $a}. +notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}. +interpretation "ppatom" 'pp a = (pp ? a). +(* to get rid of \middot *) +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_r = (pz ?). + +(* setoids for pitem *) nlet rec eq_pitem (S : Alpha) (p1, p2 : pitem S) on p1 : CProp[0] ≝ match p1 with [ pz ⇒ match p2 with [ pz ⇒ True | _ ⇒ False] @@ -372,40 +288,8 @@ unification hint 0 ≔ S:Alpha,a,b: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. +(* end setoids for pitem *) -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}. @@ -413,18 +297,6 @@ interpretation "fst" 'fst x = (fst ? ? x). notation > "\snd term 90 x" non associative with precedence 90 for @{'snd $x}. interpretation "snd" 'snd x = (snd ? ? x). -interpretation "pstar" 'pk a = (pk ? a). -interpretation "por" 'plus a b = (po ? a b). -interpretation "pcat" 'pc a b = (pc ? a b). -notation < ".a" non associative with precedence 90 for @{ 'pp $a}. -notation > "`. term 90 a" non associative with precedence 90 for @{ 'pp $a}. -interpretation "ppatom" 'pp a = (pp ? a). -(* to get rid of \middot *) -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_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 ≝ match l with @@ -435,6 +307,7 @@ nlet rec forget (S: Alpha) (l : pitem S) on l: re S ≝ | pc E1 E2 ⇒ (|E1| · |E2|) | po E1 E2 ⇒ (|E1| + |E2|) | pk E ⇒ |E|^* ]. + notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}. interpretation "forget" 'forget a = (forget ? a). @@ -452,6 +325,7 @@ notation > "𝐋\p term 70 E" non associative with precedence 75 for @{'L_pi $E} notation "𝐋\sub(\p) term 70 E" non associative with precedence 75 for @{'L_pi $E}. interpretation "in_pl" 'L_pi E = (L_pi ? E). +(* set support for 𝐋\p *) ndefinition L_pi_ext : ∀S:Alpha.∀r:pitem S.Elang S. #S r; @(𝐋\p r); #w1 w2 E; nelim r; ##[ ##1,2: /2/; @@ -479,6 +353,8 @@ unification hint 0 ≔ S : Alpha,e : pitem S; X ≟ (mk_ext_powerclass SS (𝐋\p e) (ext_prop SS (L_pi_ext S e))) (*-----------------------------------------------------------------*)⊢ ext_carr SS X ≡ 𝐋\p e. + +(* end set support for 𝐋\p *) ndefinition epsilon ≝ λS:Alpha.λb.match b return λ_.lang S with [ true ⇒ { [ ] } | _ ⇒ ∅ ]. @@ -494,10 +370,10 @@ interpretation "L_pr" 'L_pi E = (L_pr ? E). nlemma append_eq_nil : ∀S:setoid.∀w1,w2:list S. [ ] = w1 @ w2 → w1 = [ ]. #S w1; ncases w1; //. nqed. -(* lemma 12 *) +(* lemma 12 *) (* XXX: a case where Leibnitz equality could be exploited for H *) nlemma epsilon_in_true : ∀S:Alpha.∀e:pre S. [ ] ∈ 𝐋\p e = (\snd e = true). -#S r; ncases r; #e b; @; ##[##2: #H; nrewrite > H; @2; /2/; ##] ncases b;//; -*; ##[##2:*] nelim e; +#S r; ncases r; #e b; @; ##[##2: #H; ncases b in H; ##[##2:*] #; @2; /2/; ##] +ncases b; //; *; ##[##2:*] nelim e; ##[ ##1,2: *; ##| #c; *; ##| #c; *| ##7: #p H; ##| #r1 r2 H G; *; ##[##2: nassumption; ##] ##| #r1 r2 H1 H2; *; /2/ by {}] @@ -576,12 +452,6 @@ nchange in match (ϵ false) with ∅; ##| napply (.= (cup0 ? {[]})^-1); napply cupC; ##] nqed. -(* XXX move somewere else *) -ndefinition if': ∀A,B:CPROP. A = B → A → B. -#A B; *; /2/. nqed. - -ncoercion if : ∀A,B:CPROP. ∀p:A = B. A → B ≝ if' on _p : eq_rel1 ???? to ∀_:?.?. - (* theorem 16: 2 *) nlemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.𝐋\p (e1 ⊕ e2) = 𝐋\p e1 ∪ 𝐋\p e2. #S r1; ncases r1; #e1 b1 r2; ncases r2; #e2 b2; (* oh my! @@ -601,10 +471,12 @@ nqed. (* 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. +#S e1 e2 b2; ncases b2; @; /3/ by refl, conj, I; nqed. +(* nlemma LcatE : ∀S:Alpha.∀e1,e2:pitem S. 𝐋\p (e1 · e2) = 𝐋\p e1 · 𝐋 |e2| ∪ 𝐋\p e2. //; nqed. +*) 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; @; @@ -655,35 +527,39 @@ nlemma erase_bull : ∀S:Alpha.∀a:pitem S. |\fst (•a)| = |a|. ncases (•e1); ncases (•e2); //] nqed. +(* nlemma eta_lp : ∀S:Alpha.∀p:pre S. 𝐋\p p = 𝐋\p 〈\fst p, \snd p〉. #S p; ncases p; //; nqed. +*) -(* ext_carr non applica *) +(* XXX coercion ext_carr non applica *) nlemma epsilon_dot: ∀S:Alpha.∀p:Elang S. {[]} · (ext_carr ? p) = p. #S e; napply ext_set; #w; @; ##[##2: #Hw; @[]; @w; @; //; @; //; napply #; (* XXX auto *) ##] *; #w1; *; #w2; *; *; #defw defw1 Hw2; -napply (. defw╪_1#); -napply (. (defw1^-1 ╪_0 #)╪_1#); (* manca @ morfismo *) -napply Hw2; nqed. - -STOP +napply (. defw╪_1#); +napply (. ((defw1 : [ ] = ?)^-1 ╪_0 #)╪_1#); +napply Hw2; +nqed. (* theorem 16: 1 → 3 *) -nlemma odot_dot_aux : ∀S.∀e1,e2: pre S. - 𝐋\p (•(\fst e2)) = 𝐋\p (\fst e2) ∪ 𝐋 .|\fst e2| → - 𝐋\p (e1 ⊙ e2) = 𝐋\p e1 · 𝐋 .|\fst e2| ∪ 𝐋\p e2. +nlemma odot_dot_aux : ∀S:Alpha.∀e1,e2: pre S. + 𝐋\p (•(\fst e2)) = 𝐋\p (\fst e2) ∪ 𝐋 |\fst e2| → + 𝐋\p (e1 ⊙ e2) = 𝐋\p e1 · 𝐋 |\fst e2| ∪ 𝐋\p e2. #S e1 e2 th1; ncases e1; #e1' b1'; ncases b1'; -##[ nwhd in ⊢ (??(??%)?); nletin e2' ≝ (\fst e2); nletin b2' ≝ (\snd e2); +##[ nchange in match (〈?,true〉⊙?) with 〈?,?〉; + nletin e2' ≝ (\fst e2); nletin b2' ≝ (\snd e2); nletin e2'' ≝ (\fst (•(\fst e2))); nletin b2'' ≝ (\snd (•(\fst e2))); - nchange in ⊢ (??%?) with (?∪?); - nchange in ⊢ (??(??%?)?) with (?∪?); - nchange in match (𝐋\p 〈?,?〉) with (?∪?); - nrewrite > (epsilon_or …); nrewrite > (cupC ? (ϵ ?)…); - nrewrite > (cupA …);nrewrite < (cupA ?? (ϵ?)…); - nrewrite > (?: 𝐋\p e2'' ∪ ϵ b2'' = 𝐋\p e2' ∪ 𝐋 .|e2'|); ##[##2: - nchange with (𝐋\p 〈e2'',b2''〉 = 𝐋\p e2' ∪ 𝐋 .|e2'|); - ngeneralize in match th1; - nrewrite > (eta_lp…); #th1; nrewrite > th1; //;##] + napply (.=_1 (# ╪_1 (epsilon_or …))); (* XXX … is too slow if combined with .= *) + nchange in match b2'' with b2''; (* XXX some unfoldings happened *) + nchange in match b2' with b2'; + napply (.=_1 (# ╪_1 (cupC …))); napply (.=_1 (cupA …)); + napply (.=_1 (# ╪_1 (cupA …)^-1)); (* XXX slow, but not because of disamb! *) + ncut (𝐋\p e2'' ∪ ϵ b2'' = 𝐋\p e2' ∪ 𝐋 |e2'|); ##[ + nchange with (𝐋\p 〈e2'',b2''〉 = 𝐋\p e2' ∪ 𝐋 |e2'|); + napply (?^-1); napply (.=_1 th1^-1); //;##] #E; + napply (.=_1 (# ╪_1 (E ╪_1 #))); + STOP + nrewrite > (eta_lp ? e2); nchange in match (𝐋\p 〈\fst e2,?〉) with (𝐋\p e2'∪ ϵ b2'); nrewrite > (cup_dotD …); nrewrite > (epsilon_dot…); diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma index 376edc0ce..0516982cd 100644 --- a/helm/software/matita/nlibrary/sets/setoids.ma +++ b/helm/software/matita/nlibrary/sets/setoids.ma @@ -32,6 +32,10 @@ notation < "[\setoid\ensp\of term 19 x]" non associative with precedence 90 fo interpretation "mk_setoid" 'mk_setoid x = (mk_setoid x ?). interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y). +(* 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 }. notation > "hvbox(a break =_0 b)" non associative with precedence 45 for @{ eq_rel ? (eq0 ?) $a $b }.