1 include "basics/logic.ma".
3 (* Given a universe A, we can consider sets of elements of type A by means of their
4 characteristic predicates A → Prop. *)
6 definition set ≝ λA:Type[0].A → Prop.
8 (* For instance, the empty set is the set defined by an always False predicate *)
10 definition empty : ∀A.
\ 5a href="cic:/matita/tutorial/chapter4/set.def(1)"
\ 6set
\ 5/a
\ 6 A ≝ λA.λa:A.
\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"
\ 6False
\ 5/a
\ 6.
12 (* the singleton set {a} can be defined by the characteristic predicate stating
15 definition singleton: ∀A.A →
\ 5a href="cic:/matita/tutorial/chapter4/set.def(1)"
\ 6set
\ 5/a
\ 6 A ≝ λA.λa,x.a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6x.
17 (* Complement, union and intersection are easily defined, by means of logical
20 definition complement: ∀A.
\ 5a href="cic:/matita/tutorial/chapter4/set.def(1)"
\ 6set
\ 5/a
\ 6 A →
\ 5a href="cic:/matita/tutorial/chapter4/set.def(1)"
\ 6set
\ 5/a
\ 6 A ≝ λA,P,x.
\ 5a title="logical not" href="cic:/fakeuri.def(1)"
\ 6¬
\ 5/a
\ 6(P x).
22 definition intersection: ∀A.
\ 5a href="cic:/matita/tutorial/chapter4/set.def(1)"
\ 6set
\ 5/a
\ 6 A →
\ 5a href="cic:/matita/tutorial/chapter4/set.def(1)"
\ 6set
\ 5/a
\ 6 A →
\ 5a href="cic:/matita/tutorial/chapter4/set.def(1)"
\ 6set
\ 5/a
\ 6 A ≝ λA,P,Q,x.(P x)
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 (Q x).
24 definition union: ∀A.
\ 5a href="cic:/matita/tutorial/chapter4/set.def(1)"
\ 6set
\ 5/a
\ 6 A →
\ 5a href="cic:/matita/tutorial/chapter4/set.def(1)"
\ 6set
\ 5/a
\ 6 A →
\ 5a href="cic:/matita/tutorial/chapter4/set.def(1)"
\ 6set
\ 5/a
\ 6 A ≝ λA,P,Q,x.(P x)
\ 5a title="logical or" href="cic:/fakeuri.def(1)"
\ 6∨
\ 5/a
\ 6 (Q x).
32 (* The reader could probably wonder what is the difference between Prop and bool.
33 In fact, they are quite distinct entities. In type theory, all objects are structured
34 in a three levels hierarchy
36 where, t is a term, A is a type, and s is called a sort. Sorts are special, primitive
37 constants used to give a type to types. Now, Prop is a primitive sort, while bool is
38 just a user defined data type (whose sort his Type[0]). In particular, Prop is the
39 sort of Propositions: its elements are logical statements in the usual sense. The important
40 point is that statements are inhabited by their proofs: a triple of the kind
42 should be read as p is a proof of the proposition Q.*)
46 include "arithmetics/nat.ma".
47 include "basics/list.ma".
49 interpretation "iff" 'iff a b = (iff a b).
51 record Alpha : Type[1] ≝ { carr :> Type[0];
52 eqb: carr → carr →
\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6;
53 eqb_true: ∀x,y. (eqb x y
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"
\ 6true
\ 5/a
\ 6)
\ 5a title="iff" href="cic:/fakeuri.def(1)"
\ 6↔
\ 5/a
\ 6 (x
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 y)
56 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
57 interpretation "eqb" 'eqb a b = (eqb ? a b).
59 definition word ≝ λS:
\ 5a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"
\ 6Alpha
\ 5/a
\ 6.
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 S.
61 inductive re (S:
\ 5a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"
\ 6Alpha
\ 5/a
\ 6) : Type[0] ≝
65 | c: re S → re S → re S
66 | o: re S → re S → re S
69 notation < "a \sup ⋇" non associative with precedence 90 for @{ 'pk $a}.
70 notation > "a ^ *" non associative with precedence 90 for @{ 'pk $a}.
71 interpretation "star" 'pk a = (k ? a).
72 interpretation "or" 'plus a b = (o ? a b).
74 notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
75 interpretation "cat" 'pc a b = (c ? a b).
77 (* to get rid of \middot
78 coercion c : ∀S:Alpha.∀p:re S. re S → re S ≝ c on _p : re ? to ∀_:?.?. *)
80 notation < "a" non associative with precedence 90 for @{ 'ps $a}.
81 notation > "` term 90 a" non associative with precedence 90 for @{ 'ps $a}.
82 interpretation "atom" 'ps a = (s ? a).
84 notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
85 interpretation "epsilon" 'epsilon = (e ?).
87 notation "∅" non associative with precedence 90 for @{ 'empty }.
88 interpretation "empty" 'empty = (z ?).
90 let rec flatten (S :
\ 5a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"
\ 6Alpha
\ 5/a
\ 6) (l :
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/re/word.def(3)"
\ 6word
\ 5/a
\ 6 S)) on l :
\ 5a href="cic:/matita/tutorial/re/word.def(3)"
\ 6word
\ 5/a
\ 6 S ≝
91 match l with [ nil ⇒
\ 5a title="nil" href="cic:/fakeuri.def(1)"
\ 6[
\ 5/a
\ 6 ] | cons w tl ⇒ w
\ 5a title="append" href="cic:/fakeuri.def(1)"
\ 6@
\ 5/a
\ 6 flatten ? tl ].
93 let rec conjunct (S :
\ 5a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"
\ 6Alpha
\ 5/a
\ 6) (l :
\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"
\ 6list
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/re/word.def(3)"
\ 6word
\ 5/a
\ 6 S)) (r :
\ 5a href="cic:/matita/tutorial/re/word.def(3)"
\ 6word
\ 5/a
\ 6 S → Prop) on l: Prop ≝
94 match l with [ nil ⇒
\ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"
\ 6True
\ 5/a
\ 6 | cons w tl ⇒ r w
\ 5a title="logical and" href="cic:/fakeuri.def(1)"
\ 6∧
\ 5/a
\ 6 conjunct ? tl r ].
96 definition empty_lang ≝ λS.λw:
\ 5a href="cic:/matita/tutorial/re/word.def(3)"
\ 6word
\ 5/a
\ 6 S.
\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"
\ 6False
\ 5/a
\ 6.
97 notation "{}" non associative with precedence 90 f