--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.*)
+
(* *)
(**************************************************************************)
-include "arithmetics/nat.ma".
+include "logic/pts.ma".
ninductive list (A:Type[0]) : Type[0] ≝
| nil: list A
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 ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
-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
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
(* *)
(**************************************************************************)
-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".
(*
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.
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;
}.
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
| 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] ≝
#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,
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;
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;
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).
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
| 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]
(* -------------------------------------------- *) ⊢
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}.
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
| 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).
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/;
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 ⇒ { [ ] } | _ ⇒ ∅ ].
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 {}]
##| 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!
(* 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; @;
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…);
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 }.
projects / helm.git / commitdiff
