weblib/tutorial/chapter6.ma

   1 include "basics/logic.ma".
   2
   3 (* Given a universe A, we can consider sets of elements of type A by means of their
   4 characteristic predicates A → Prop. *)
   5
   6 definition set ≝ λA:Type[0].A → Prop.
   7
   8 (* For instance, the empty set is the set defined by an always False predicate *)
   9
  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.
  11
  12 (* the singleton set {a} can be defined by the characteristic predicate stating
  13 equality with a *)
  14
  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.
  16
  17 (* Complement, union and intersection are easily defined, by means of logical
  18 connectives *)
  19
  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).
  21
  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).
  23
  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).
  25
  26
  27
  28
  29
  30
  31
  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
  35    t : A : s
  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
  41    p : Q : Prop
  42 should be read as p is a proof of the proposition Q.*)
  43
  44
  45
  46 include "arithmetics/nat.ma".
  47 include "basics/list.ma".
  48
  49 interpretation "iff" 'iff a b = (iff a b).
  50
  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)
  54 }.
  55
  56 notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
  57 interpretation "eqb" 'eqb a b = (eqb ? a b).
  58
  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.
  60
  61 inductive re (S: \ 5a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) : Type[0] ≝
  62    z: re S
  63  | e: re S
  64  | s: S → re S
  65  | c: re S → re S → re S
  66  | o: re S → re S → re S
  67  | k: re S → re S.
  68
  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).
  73
  74 notation "a · b" non associative with precedence 60 for @{ 'pc $a $b}.
  75 interpretation "cat" 'pc a b = (c ? a b).
  76
  77 (* to get rid of \middot
  78 coercion c  : ∀S:Alpha.∀p:re S.  re S →  re S   ≝ c  on _p : re ?  to ∀_:?.?. *)
  79
  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).
  83
  84 notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
  85 interpretation "epsilon" 'epsilon = (e ?).
  86
  87 notation "∅" non associative with precedence 90 for @{ 'empty }.
  88 interpretation "empty" 'empty = (z ?).
  89
  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 ].
  92
  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 ].
  95
  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