+include "basics/logic.ma".
+(**** a subset of A is just an object of type A→Prop ****)
-(**************************************************************************)
-(* ___ *)
-(* ||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 "basics/lists/list.ma".
-include "basics/sets.ma".
-
-definition word ≝ λS:DeqSet.list S.
-
-notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
-interpretation "epsilon" 'epsilon = (nil ?).
-
-(* concatenation *)
-definition cat : ∀S,l1,l2,w.Prop ≝
- λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2.
-notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
-interpretation "cat lang" 'middot a b = (cat ? a b).
-
-let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝
-match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
-
-let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝
-match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ].
-
-(* kleene's star *)
-definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l.
-notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
-interpretation "star lang" 'star l = (star ? l).
-
-lemma cat_ext_l: ∀S.∀A,B,C:word S →Prop.
- A =1 C → A · B =1 C · B.
-#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
-cases (H w1) /6/
+definition empty_set ≝ λA:Type[0].λa:A.False.
+notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
+interpretation "empty set" 'empty_set = (empty_set ?).
+
+definition singleton ≝ λA.λx,a:A.x=a.
+(* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
+interpretation "singleton" 'singl x = (singleton ? x).
+
+definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a ∨ Q a.
+interpretation "union" 'union a b = (union ? a b).
+
+definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a ∧ Q a.
+interpretation "intersection" 'intersects a b = (intersection ? a b).
+
+definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
+interpretation "complement" 'not a = (complement ? a).
+
+definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
+interpretation "substraction" 'minus a b = (substraction ? a b).
+
+definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
+interpretation "subset" 'subseteq a b = (subset ? a b).
+
+(* extensional equality *)
+definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
+notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
+interpretation "extensional equality" 'eqP a b = (eqP ? a b).
+
+lemma eqP_sym: ∀U.∀A,B:U →Prop.
+ A =1 B → B =1 A.
+#U #A #B #eqAB #a @iff_sym @eqAB qed.
+
+lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
+ A =1 B → B =1 C → A =1 C.
+#U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
+
+lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
+ A =1 C → A ∪ B =1 C ∪ B.
+#U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
+
+lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
+ B =1 C → A ∪ B =1 A ∪ C.
+#U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
+
+lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
+ A =1 C → A ∩ B =1 C ∩ B.
+#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+
+lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop.
+ B =1 C → A ∩ B =1 A ∩ C.
+#U #A #B #C #eqBC #a @iff_and_l @eqBC qed.
+
+lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
+ A =1 C → A - B =1 C - B.
+#U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
+
+lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
+ B =1 C → A - B =1 A - C.
+#U #A #B #C #eqBC #a @iff_and_l /2/ qed.
+
+(* set equalities *)
+lemma union_empty_r: ∀U.∀A:U→Prop.
+ A ∪ ∅ =1 A.
+#U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
qed.
-lemma cat_ext_r: ∀S.∀A,B,C:word S →Prop.
- B =1 C → A · B =1 A · C.
-#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
-cases (H w2) /6/
+lemma union_comm : ∀U.∀A,B:U →Prop.
+ A ∪ B =1 B ∪ A.
+#U #A #B #a % * /2/ qed.
+
+lemma union_assoc: ∀U.∀A,B,C:U → Prop.
+ A ∪ B ∪ C =1 A ∪ (B ∪ C).
+#S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/]
+qed.
+
+lemma cap_comm : ∀U.∀A,B:U →Prop.
+ A ∩ B =1 B ∩ A.
+#U #A #B #a % * /2/ qed.
+
+lemma union_idemp: ∀U.∀A:U →Prop.
+ A ∪ A =1 A.
+#U #A #a % [* // | /2/] qed.
+
+lemma cap_idemp: ∀U.∀A:U →Prop.
+ A ∩ A =1 A.
+#U #A #a % [* // | /2/] qed.
+
+(*distributivities *)
+
+lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
+ (A ∪ B) ∩ C =1 (A ∩ C) ∪ (B ∩ C).
+#U #A #B #C #w % [* * /3/ | * * /3/]
qed.
-lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop.
- (A ∪ B) · C =1 A · C ∪ B · C.
-#S #A #B #C #w %
- [* #w1 * #w2 * * #eqw * /6/ |* * #w1 * #w2 * * /6/]
+lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
+ (A ∪ B) - C =1 (A - C) ∪ (B - C).
+#U #A #B #C #w % [* * /3/ | * * /3/]
qed.
-lemma espilon_in_star: ∀S.∀A:word S → Prop.
- A^* ϵ.
-#S #A @(ex_intro … [ ]) normalize /2/
+(* substraction *)
+lemma substract_def:∀U.∀A,B:U→Prop. A-B =1 A ∩ ¬B.
+#U #A #B #w normalize /2/
qed.
-lemma cat_to_star:∀S.∀A:word S → Prop.
- ∀w1,w2. A w1 → A^* w2 → A^* (w1@w2).
-#S #A #w1 #w2 #Aw * #l * #H #H1 @(ex_intro … (w1::l))
-% normalize /2/
-qed.
+include "basics/types.ma".
+include "basics/bool.ma".
-lemma fix_star: ∀S.∀A:word S → Prop.
- A^* =1 A · A^* ∪ {ϵ}.
-#S #A #w %
- [* #l generalize in match w; -w cases l [normalize #w * /2/]
- #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
- #w1A #cw1 %1 @(ex_intro … w1) @(ex_intro … (flatten S tl))
- % /2/ whd @(ex_intro … tl) /2/
- |* [2: whd in ⊢ (%→?); #eqw <eqw //]
- * #w1 * #w2 * * #eqw <eqw @cat_to_star
- ]
-qed.
+(****** DeqSet: a set with a decidbale equality ******)
+
+record DeqSet : Type[1] ≝ { carr :> Type[0];
+ eqb: carr → carr → bool;
+ eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)
+}.
-lemma star_fix_eps : ∀S.∀A:word S → Prop.
- A^* =1 (A - {ϵ}) · A^* ∪ {ϵ}.
-#S #A #w %
- [* #l elim l
- [* whd in ⊢ ((??%?)→?); #eqw #_ %2 <eqw //
- |* [#tl #Hind * #H * #_ #H2 @Hind % [@H | //]
- |#a #w1 #tl #Hind * whd in ⊢ ((??%?)→?); #H1 * #H2 #H3 %1
- @(ex_intro … (a::w1)) @(ex_intro … (flatten S tl)) %
- [% [@H1 | normalize % /2/] |whd @(ex_intro … tl) /2/]
- ]
- ]
- |* [* #w1 * #w2 * * #eqw * #H1 #_ <eqw @cat_to_star //
- | whd in ⊢ (%→?); #H <H //
- ]
+notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
+interpretation "eqb" 'eqb a b = (eqb ? a b).
+
+notation "\P H" non associative with precedence 90
+ for @{(proj1 … (eqb_true ???) $H)}.
+
+notation "\b H" non associative with precedence 90
+ for @{(proj2 … (eqb_true ???) $H)}.
+
+lemma eqb_false: ∀S:DeqSet.∀a,b:S.
+ (eqb ? a b) = false ↔ a ≠ b.
+#S #a #b % #H
+ [@(not_to_not … not_eq_true_false) #H1 <H @sym_eq @(\b H1)
+ |cases (true_or_false (eqb ? a b)) // #H1 @False_ind @(absurd … (\P H1) H)
]
-qed.
-
-lemma star_epsilon: ∀S:DeqSet.∀A:word S → Prop.
- A^* ∪ {ϵ} =1 A^*.
-#S #A #w % /2/ * //
qed.
+
+notation "\Pf H" non associative with precedence 90
+ for @{(proj1 … (eqb_false ???) $H)}.
+
+notation "\bf H" non associative with precedence 90
+ for @{(proj2 … (eqb_false ???) $H)}.
-lemma epsilon_cat_r: ∀S.∀A:word S →Prop.
- A · {ϵ} =1 A.
-#S #A #w %
- [* #w1 * #w2 * * #eqw #inw1 normalize #eqw2 <eqw //
- |#inA @(ex_intro … w) @(ex_intro … [ ]) /3/
- ]
+lemma dec_eq: ∀S:DeqSet.∀a,b:S. a = b ∨ a ≠ b.
+#S #a #b cases (true_or_false (eqb ? a b)) #H
+ [%1 @(\P H) | %2 @(\Pf H)]
qed.
-lemma epsilon_cat_l: ∀S.∀A:word S →Prop.
- {ϵ} · A =1 A.
-#S #A #w %
- [* #w1 * #w2 * * #eqw normalize #eqw2 <eqw <eqw2 //
- |#inA @(ex_intro … ϵ) @(ex_intro … w) /3/
- ]
+definition beqb ≝ λb1,b2.
+ match b1 with [ true ⇒ b2 | false ⇒ notb b2].
+
+notation < "a == b" non associative with precedence 45 for @{beqb $a $b }.
+lemma beqb_true: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2).
+#b1 #b2 cases b1 cases b2 normalize /2/
+qed.
+
+definition DeqBool ≝ mk_DeqSet bool beqb beqb_true.
+
+unification hint 0 ≔ ;
+ X ≟ mk_DeqSet bool beqb beqb_true
+(* ---------------------------------------- *) ⊢
+ bool ≡ carr X.
+
+unification hint 0 ≔ b1,b2:bool;
+ X ≟ mk_DeqSet bool beqb beqb_true
+(* ---------------------------------------- *) ⊢
+ beqb b1 b2 ≡ eqb X b1 b2.
+
+example exhint: ∀b:bool. (b == false) = true → b = false.
+#b #H @(\P H).
qed.
-lemma distr_cat_r_eps: ∀S.∀A,C:word S →Prop.
- (A ∪ {ϵ}) · C =1 A · C ∪ C.
-#S #A #C @eqP_trans [|@distr_cat_r |@eqP_union_l @epsilon_cat_l]
+(* pairs *)
+definition eq_pairs ≝
+ λA,B:DeqSet.λp1,p2:A×B.(\fst p1 == \fst p2) ∧ (\snd p1 == \snd p2).
+
+lemma eq_pairs_true: ∀A,B:DeqSet.∀p1,p2:A×B.
+ eq_pairs A B p1 p2 = true ↔ p1 = p2.
+#A #B * #a1 #b1 * #a2 #b2 %
+ [#H cases (andb_true …H) #eqa #eqb >(\P eqa) >(\P eqb) //
+ |#H destruct normalize >(\b (refl … a2)) >(\b (refl … b2)) //
+ ]
qed.
+definition DeqProd ≝ λA,B:DeqSet.
+ mk_DeqSet (A×B) (eq_pairs A B) (eq_pairs_true A B).
+
+unification hint 0 ≔ C1,C2;
+ T1 ≟ carr C1,
+ T2 ≟ carr C2,
+ X ≟ DeqProd C1 C2
+(* ---------------------------------------- *) ⊢
+ T1×T2 ≡ carr X.
+
+unification hint 0 ≔ T1,T2,p1,p2;
+ X ≟ DeqProd T1 T2
+(* ---------------------------------------- *) ⊢
+ eq_pairs T1 T2 p1 p2 ≡ eqb X p1 p2.
+
+example hint2: ∀b1,b2.
+ 〈b1,true〉==〈false,b2〉=true → 〈b1,true〉=〈false,b2〉.
+#b1 #b2 #H @(\P H).
\ No newline at end of file
-(**************************************************************************)
-(* ___ *)
-(* ||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 *)
-(* *)
-(**************************************************************************)
+(* boolean functions over lists *)
-include "re/lang.ma".
+include "basics/list.ma".
+include "basics/sets.ma".
+include "basics/deqsets.ma".
-inductive re (S: DeqSet) : Type[0] ≝
- z: re S
- | e: re S
- | s: S → re S
- | c: re S → re S → re S
- | o: re S → re S → re S
- | k: re S → re S.
+(********* search *********)
-interpretation "re epsilon" 'epsilon = (e ?).
-interpretation "re or" 'plus a b = (o ? a b).
-interpretation "re cat" 'middot a b = (c ? a b).
-interpretation "re star" 'star a = (k ? a).
-
-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 @{ 'empty }.
-interpretation "empty" 'empty = (z ?).
-
-let rec in_l (S : DeqSet) (r : re S) on r : word S → Prop ≝
-match r with
-[ z ⇒ ∅
-| e ⇒ {ϵ}
-| s x ⇒ {[x]}
-| c r1 r2 ⇒ (in_l ? r1) · (in_l ? r2)
-| o r1 r2 ⇒ (in_l ? r1) ∪ (in_l ? r2)
-| k r1 ⇒ (in_l ? r1) ^*].
-
-notation "\sem{term 19 E}" non associative with precedence 75 for @{'in_l $E}.
-interpretation "in_l" 'in_l E = (in_l ? E).
-interpretation "in_l mem" 'mem w l = (in_l ? l w).
-
-lemma rsem_star : ∀S.∀r: re S. \sem{r^*} = \sem{r}^*.
-// qed.
-
-
-(* pointed items *)
-inductive pitem (S: DeqSet) : Type[0] ≝
- pz: pitem S
- | pe: pitem S
- | ps: S → pitem S
- | pp: S → pitem S
- | pc: pitem S → pitem S → pitem S
- | po: pitem S → pitem S → pitem S
- | pk: pitem S → pitem S.
-
-definition pre ≝ λS.pitem S × bool.
-
-interpretation "pitem star" 'star a = (pk ? a).
-interpretation "pitem or" 'plus a b = (po ? a b).
-interpretation "pitem cat" 'middot 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 "pitem pp" 'pp a = (pp ? a).
-interpretation "pitem ps" 'ps a = (ps ? a).
-interpretation "pitem epsilon" 'epsilon = (pe ?).
-interpretation "pitem empty" 'empty = (pz ?).
-
-let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝
- match l with
- [ pz ⇒ `∅
- | pe ⇒ ϵ
- | ps x ⇒ `x
- | pp x ⇒ `x
- | pc E1 E2 ⇒ (forget ? E1) · (forget ? E2)
- | po E1 E2 ⇒ (forget ? E1) + (forget ? E2)
- | pk E ⇒ (forget ? E)^* ].
-
-(* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*)
-interpretation "forget" 'norm a = (forget ? a).
-
-let rec in_pl (S : DeqSet) (r : pitem S) on r : word S → Prop ≝
-match r with
-[ pz ⇒ ∅
-| pe ⇒ ∅
-| ps _ ⇒ ∅
-| pp x ⇒ { [x] }
-| pc r1 r2 ⇒ (in_pl ? r1) · \sem{forget ? r2} ∪ (in_pl ? r2)
-| po r1 r2 ⇒ (in_pl ? r1) ∪ (in_pl ? r2)
-| pk r1 ⇒ (in_pl ? r1) · \sem{forget ? r1}^* ].
-
-interpretation "in_pl" 'in_l E = (in_pl ? E).
-interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
-
-definition in_prl ≝ λS : DeqSet.λp:pre S.
- if (\snd p) then \sem{\fst p} ∪ {ϵ} else \sem{\fst p}.
-
-interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
-interpretation "in_prl" 'in_l E = (in_prl ? E).
-
-lemma sem_pre_true : ∀S.∀i:pitem S.
- \sem{〈i,true〉} = \sem{i} ∪ {ϵ}.
-// qed.
-
-lemma sem_pre_false : ∀S.∀i:pitem S.
- \sem{〈i,false〉} = \sem{i}.
-// qed.
-
-lemma sem_cat: ∀S.∀i1,i2:pitem S.
- \sem{i1 · i2} = \sem{i1} · \sem{|i2|} ∪ \sem{i2}.
-// qed.
-
-lemma sem_cat_w: ∀S.∀i1,i2:pitem S.∀w.
- \sem{i1 · i2} w = ((\sem{i1} · \sem{|i2|}) w ∨ \sem{i2} w).
-// qed.
-
-lemma sem_plus: ∀S.∀i1,i2:pitem S.
- \sem{i1 + i2} = \sem{i1} ∪ \sem{i2}.
-// qed.
-
-lemma sem_plus_w: ∀S.∀i1,i2:pitem S.∀w.
- \sem{i1 + i2} w = (\sem{i1} w ∨ \sem{i2} w).
-// qed.
-
-lemma sem_star : ∀S.∀i:pitem S.
- \sem{i^*} = \sem{i} · \sem{|i|}^*.
-// qed.
-
-lemma sem_star_w : ∀S.∀i:pitem S.∀w.
- \sem{i^*} w = (∃w1,w2.w1 @ w2 = w ∧ \sem{i} w1 ∧ \sem{|i|}^* w2).
-// qed.
+let rec memb (S:DeqSet) (x:S) (l: list S) on l ≝
+ match l with
+ [ nil ⇒ false
+ | cons a tl ⇒ (x == a) ∨ memb S x tl
+ ].
-lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = ϵ → w1 = ϵ.
-#S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed.
+notation < "\memb x l" non associative with precedence 90 for @{'memb $x $l}.
+interpretation "boolean membership" 'memb a l = (memb ? a l).
-lemma not_epsilon_lp : ∀S:DeqSet.∀e:pitem S. ¬ (ϵ ∈ e).
-#S #e elim e normalize /2/
- [#r1 #r2 * #n1 #n2 % * /2/ * #w1 * #w2 * * #H
- >(append_eq_nil …H…) /2/
- |#r1 #r2 #n1 #n2 % * /2/
- |#r #n % * #w1 * #w2 * * #H >(append_eq_nil …H…) /2/
- ]
+lemma memb_hd: ∀S,a,l. memb S a (a::l) = true.
+#S #a #l normalize >(proj2 … (eqb_true S …) (refl S a)) //
qed.
-(* lemma 12 *)
-lemma epsilon_to_true : ∀S.∀e:pre S. ϵ ∈ e → \snd e = true.
-#S * #i #b cases b // normalize #H @False_ind /2/
+lemma memb_cons: ∀S,a,b,l.
+ memb S a l = true → memb S a (b::l) = true.
+#S #a #b #l normalize cases (a==b) normalize //
qed.
-lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → ϵ ∈ e.
-#S * #i #b #btrue normalize in btrue; >btrue %2 //
+lemma memb_single: ∀S,a,x. memb S a [x] = true → a = x.
+#S #a #x normalize cases (true_or_false … (a==x)) #H
+ [#_ >(\P H) // |>H normalize #abs @False_ind /2/]
qed.
-definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
-notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
-interpretation "oplus" 'oplus a b = (lo ? a b).
+lemma memb_append: ∀S,a,l1,l2.
+memb S a (l1@l2) = true →
+ memb S a l1= true ∨ memb S a l2 = true.
+#S #a #l1 elim l1 normalize [#l2 #H %2 //]
+#b #tl #Hind #l2 cases (a==b) normalize /2/
+qed.
-lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉.
-// qed.
+lemma memb_append_l1: ∀S,a,l1,l2.
+ memb S a l1= true → memb S a (l1@l2) = true.
+#S #a #l1 elim l1 normalize
+ [normalize #le #abs @False_ind /2/
+ |#b #tl #Hind #l2 cases (a==b) normalize /2/
+ ]
+qed.
+
+lemma memb_append_l2: ∀S,a,l1,l2.
+ memb S a l2= true → memb S a (l1@l2) = true.
+#S #a #l1 elim l1 normalize //
+#b #tl #Hind #l2 cases (a==b) normalize /2/
+qed.
+
+lemma memb_exists: ∀S,a,l.memb S a l = true →
+ ∃l1,l2.l=l1@(a::l2).
+#S #a #l elim l [normalize #abs @False_ind /2/]
+#b #tl #Hind #H cases (orb_true_l … H)
+ [#eqba @(ex_intro … (nil S)) @(ex_intro … tl) >(\P eqba) //
+ |#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl
+ @(ex_intro … (b::l1)) @(ex_intro … l2) >eqtl //
+ ]
+qed.
-definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S.
- match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉].
+lemma not_memb_to_not_eq: ∀S,a,b,l.
+ memb S a l = false → memb S b l = true → a==b = false.
+#S #a #b #l cases (true_or_false (a==b)) //
+#eqab >(\P eqab) #H >H #abs @False_ind /2/
+qed.
-notation "i ◂ e" left associative with precedence 60 for @{'ltrif $i $e}.
-interpretation "pre_concat_r" 'ltrif i e = (pre_concat_r ? i e).
-
-lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop.
- A = B → A =1 B.
-#S #A #B #H >H /2/ qed.
-
-lemma sem_pre_concat_r : ∀S,i.∀e:pre S.
- \sem{i ◂ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}.
-#S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //]
->sem_pre_true >sem_cat >sem_pre_true /2/
+lemma memb_map: ∀S1,S2,f,a,l. memb S1 a l= true →
+ memb S2 (f a) (map … f l) = true.
+#S1 #S2 #f #a #l elim l normalize [//]
+#x #tl #memba cases (true_or_false (a==x))
+ [#eqx >eqx >(\P eqx) >(\b (refl … (f x))) normalize //
+ |#eqx >eqx cases (f a==f x) normalize /2/
+ ]
qed.
-
-definition lc ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λi2:pitem S.
- match e1 with
- [ mk_Prod i1 b1 ⇒ match b1 with
- [ true ⇒ (i1 ◂ (bcast ? i2))
- | false ⇒ 〈i1 · i2,false〉
- ]
- ].
-
-definition lift ≝ λS.λf:pitem S →pre S.λe:pre S.
- match e with
- [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉].
-
-notation "a ▸ b" left associative with precedence 60 for @{'lc eclose $a $b}.
-interpretation "lc" 'lc op a b = (lc ? op a b).
-
-definition lk ≝ λS:DeqSet.λbcast:∀S:DeqSet.∀E:pitem S.pre S.λe:pre S.
- match e with
- [ mk_Prod i1 b1 ⇒
- match b1 with
- [true ⇒ 〈(\fst (bcast ? i1))^*, true〉
- |false ⇒ 〈i1^*,false〉
- ]
- ].
-
-(* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $op $a}.*)
-interpretation "lk" 'lk op a = (lk ? op a).
-notation "a^⊛" non associative with precedence 90 for @{'lk eclose $a}.
-
-notation "•" non associative with precedence 60 for @{eclose ?}.
-let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
- match i with
- [ pz ⇒ 〈 `∅, false 〉
- | pe ⇒ 〈 ϵ, true 〉
- | ps x ⇒ 〈 `.x, false〉
- | pp x ⇒ 〈 `.x, false 〉
- | po i1 i2 ⇒ •i1 ⊕ •i2
- | pc i1 i2 ⇒ •i1 ▸ i2
- | pk i ⇒ 〈(\fst (•i))^*,true〉].
-
-notation "• x" non associative with precedence 60 for @{'eclose $x}.
-interpretation "eclose" 'eclose x = (eclose ? x).
-
-lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S.
- •(i1 + i2) = •i1 ⊕ •i2.
-// qed.
-
-lemma eclose_dot: ∀S:DeqSet.∀i1,i2:pitem S.
- •(i1 · i2) = •i1 ▸ i2.
-// qed.
-
-lemma eclose_star: ∀S:DeqSet.∀i:pitem S.
- •i^* = 〈(\fst(•i))^*,true〉.
-// qed.
-
-definition reclose ≝ λS. lift S (eclose S).
-interpretation "reclose" 'eclose x = (reclose ? x).
-
-(* theorem 16: 2 *)
-lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
- \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
-#S * #i1 #b1 * #i2 #b2 #w %
- [cases b1 cases b2 normalize /2/ * /3/ * /3/
- |cases b1 cases b2 normalize /2/ * /3/ * /3/
+lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.
+ memb S1 a1 l1 = true → memb S2 a2 l2 = true →
+ memb S3 (op a1 a2) (compose S1 S2 S3 op l1 l2) = true.
+#S1 #S2 #S3 #op #a1 #a2 #l1 elim l1 [normalize //]
+#x #tl #Hind #l2 #memba1 #memba2 cases (orb_true_l … memba1)
+ [#eqa1 >(\P eqa1) @memb_append_l1 @memb_map //
+ |#membtl @memb_append_l2 @Hind //
]
qed.
-lemma odot_true :
- ∀S.∀i1,i2:pitem S.
- 〈i1,true〉 ▸ i2 = i1 ◂ (•i2).
-// qed.
-
-lemma odot_true_bis :
- ∀S.∀i1,i2:pitem S.
- 〈i1,true〉 ▸ i2 = 〈i1 · \fst (•i2), \snd (•i2)〉.
-#S #i1 #i2 normalize cases (•i2) // qed.
-
-lemma odot_false:
- ∀S.∀i1,i2:pitem S.
- 〈i1,false〉 ▸ i2 = 〈i1 · i2, false〉.
-// qed.
-
-lemma LcatE : ∀S.∀e1,e2:pitem S.
- \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}.
-// qed.
-
-lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
-// qed.
+(**************** unicity test *****************)
-lemma erase_plus : ∀S.∀i1,i2:pitem S.
- |i1 + i2| = |i1| + |i2|.
-// qed.
-
-lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*.
-// qed.
-
-lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|.
-#S #i elim i //
- [ #i1 #i2 #IH1 #IH2 >erase_dot <IH1 >eclose_dot
- cases (•i1) #i11 #b1 cases b1 // <IH2 >odot_true_bis //
- | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus … i1) <IH1 <IH2
- cases (•i1) #i11 #b1 cases (•i2) #i21 #b2 //
- | #i #IH >eclose_star >(erase_star … i) <IH cases (•i) //
- ]
-qed.
-
-lemma sem_eclose_star: ∀S:DeqSet.∀i:pitem S.
- \sem{〈i^*,true〉} =1 \sem{〈i,false〉}·\sem{|i|}^* ∪ {ϵ}.
-/2/ qed.
+let rec uniqueb (S:DeqSet) l on l : bool ≝
+ match l with
+ [ nil ⇒ true
+ | cons a tl ⇒ notb (memb S a tl) ∧ uniqueb S tl
+ ].
-(* theorem 16: 1 → 3 *)
-lemma odot_dot_aux : ∀S.∀e1:pre S.∀i2:pitem S.
- \sem{•i2} =1 \sem{i2} ∪ \sem{|i2|} →
- \sem{e1 ▸ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
-#S * #i1 #b1 #i2 cases b1
- [2:#th >odot_false >sem_pre_false >sem_pre_false >sem_cat /2/
- |#H >odot_true >sem_pre_true @(eqP_trans … (sem_pre_concat_r …))
- >erase_bull @eqP_trans [|@(eqP_union_l … H)]
- @eqP_trans [|@eqP_union_l[|@union_comm ]]
- @eqP_trans [|@eqP_sym @union_assoc ] /3/
- ]
-qed.
+(* unique_append l1 l2 add l1 in fornt of l2, but preserving unicity *)
-lemma sem_fst: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
-#S * #i *
- [>sem_pre_true normalize in ⊢ (??%?); #w %
- [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
- |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ]
- ]
-qed.
+let rec unique_append (S:DeqSet) (l1,l2: list S) on l1 ≝
+ match l1 with
+ [ nil ⇒ l2
+ | cons a tl ⇒
+ let r ≝ unique_append S tl l2 in
+ if memb S a r then r else a::r
+ ].
-lemma item_eps: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
-#S #i #w %
- [#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) //
- |* //
+axiom unique_append_elim: ∀S:DeqSet.∀P: S → Prop.∀l1,l2.
+(∀x. memb S x l1 = true → P x) → (∀x. memb S x l2 = true → P x) →
+∀x. memb S x (unique_append S l1 l2) = true → P x.
+
+lemma unique_append_unique: ∀S,l1,l2. uniqueb S l2 = true →
+ uniqueb S (unique_append S l1 l2) = true.
+#S #l1 elim l1 normalize // #a #tl #Hind #l2 #uniquel2
+cases (true_or_false … (memb S a (unique_append S tl l2)))
+#H >H normalize [@Hind //] >H normalize @Hind //
+qed.
+
+(******************* sublist *******************)
+definition sublist ≝
+ λS,l1,l2.∀a. memb S a l1 = true → memb S a l2 = true.
+
+lemma sublist_length: ∀S,l1,l2.
+ uniqueb S l1 = true → sublist S l1 l2 → |l1| ≤ |l2|.
+#S #l1 elim l1 //
+#a #tl #Hind #l2 #unique #sub
+cut (∃l3,l4.l2=l3@(a::l4)) [@memb_exists @sub //]
+* #l3 * #l4 #eql2 >eql2 >length_append normalize
+applyS le_S_S <length_append @Hind [@(andb_true_r … unique)]
+>eql2 in sub; #sub #x #membx
+cases (memb_append … (sub x (orb_true_r2 … membx)))
+ [#membxl3 @memb_append_l1 //
+ |#membxal4 cases (orb_true_l … membxal4)
+ [#eqxa @False_ind lapply (andb_true_l … unique)
+ <(\P eqxa) >membx normalize /2/ |#membxl4 @memb_append_l2 //
+ ]
]
qed.
-
-lemma sem_fst_aux: ∀S.∀e:pre S.∀i:pitem S.∀A.
- \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}).
-#S #e #i #A #seme
-@eqP_trans [|@sem_fst]
-@eqP_trans [||@eqP_union_r [|@eqP_sym @item_eps]]
-@eqP_trans [||@distribute_substract]
-@eqP_substract_r //
-qed.
-(* theorem 16: 1 *)
-theorem sem_bull: ∀S:DeqSet. ∀e:pitem S. \sem{•e} =1 \sem{e} ∪ \sem{|e|}.
-#S #e elim e
- [#w normalize % [/2/ | * //]
- |/2/
- |#x normalize #w % [ /2/ | * [@False_ind | //]]
- |#x normalize #w % [ /2/ | * // ]
- |#i1 #i2 #IH1 #IH2 >eclose_dot
- @eqP_trans [|@odot_dot_aux //] >sem_cat
- @eqP_trans
- [|@eqP_union_r
- [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]]
- @eqP_trans [|@union_assoc]
- @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_union_l //
- |#i1 #i2 #IH1 #IH2 >eclose_plus
- @eqP_trans [|@sem_oplus] >sem_plus >erase_plus
- @eqP_trans [|@(eqP_union_l … IH2)]
- @eqP_trans [|@eqP_sym @union_assoc]
- @eqP_trans [||@union_assoc] @eqP_union_r
- @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_trans [||@eqP_union_l [|@union_comm]]
- @eqP_trans [||@union_assoc] /2/
- |#i #H >sem_pre_true >sem_star >erase_bull >sem_star
- @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@sem_fst_aux //]]]
- @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
- @eqP_trans [|@union_assoc] @eqP_union_l >erase_star
- @eqP_sym @star_fix_eps
+lemma sublist_unique_append_l1:
+ ∀S,l1,l2. sublist S l1 (unique_append S l1 l2).
+#S #l1 elim l1 normalize [#l2 #S #abs @False_ind /2/]
+#x #tl #Hind #l2 #a
+normalize cases (true_or_false … (a==x)) #eqax >eqax
+[<(\P eqax) cases (true_or_false (memb S a (unique_append S tl l2)))
+ [#H >H normalize // | #H >H normalize >(\b (refl … a)) //]
+|cases (memb S x (unique_append S tl l2)) normalize
+ [/2/ |>eqax normalize /2/]
+]
+qed.
+
+lemma sublist_unique_append_l2:
+ ∀S,l1,l2. sublist S l2 (unique_append S l1 l2).
+#S #l1 elim l1 [normalize //] #x #tl #Hind normalize
+#l2 #a cases (memb S x (unique_append S tl l2)) normalize
+[@Hind | cases (a==x) normalize // @Hind]
+qed.
+
+lemma decidable_sublist:∀S,l1,l2.
+ (sublist S l1 l2) ∨ ¬(sublist S l1 l2).
+#S #l1 #l2 elim l1
+ [%1 #a normalize in ⊢ (%→?); #abs @False_ind /2/
+ |#a #tl * #subtl
+ [cases (true_or_false (memb S a l2)) #memba
+ [%1 whd #x #membx cases (orb_true_l … membx)
+ [#eqax >(\P eqax) // |@subtl]
+ |%2 @(not_to_not … (eqnot_to_noteq … true memba)) #H1 @H1 @memb_hd
+ ]
+ |%2 @(not_to_not … subtl) #H1 #x #H2 @H1 @memb_cons //
+ ]
]
qed.
-definition lifted_cat ≝ λS:DeqSet.λe:pre S.
- lift S (lc S eclose e).
+(********************* filtering *****************)
-notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}.
-
-interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2).
-
-lemma odot_true_b : ∀S.∀i1,i2:pitem S.∀b.
- 〈i1,true〉 ⊙ 〈i2,b〉 = 〈i1 · (\fst (•i2)),\snd (•i2) ∨ b〉.
-#S #i1 #i2 #b normalize in ⊢ (??%?); cases (•i2) //
-qed.
-
-lemma odot_false_b : ∀S.∀i1,i2:pitem S.∀b.
- 〈i1,false〉 ⊙ 〈i2,b〉 = 〈i1 · i2 ,b〉.
-//
-qed.
+lemma filter_true: ∀S,f,a,l.
+ memb S a (filter S f l) = true → f a = true.
+#S #f #a #l elim l [normalize #H @False_ind /2/]
+#b #tl #Hind cases (true_or_false (f b)) #H
+normalize >H normalize [2:@Hind]
+cases (true_or_false (a==b)) #eqab
+ [#_ >(\P eqab) // | >eqab normalize @Hind]
+qed.
-lemma erase_odot:∀S.∀e1,e2:pre S.
- |\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|).
-#S * #i1 * * #i2 #b2 // >odot_true_b //
+lemma memb_filter_memb: ∀S,f,a,l.
+ memb S a (filter S f l) = true → memb S a l = true.
+#S #f #a #l elim l [normalize //]
+#b #tl #Hind normalize (cases (f b)) normalize
+cases (a==b) normalize // @Hind
qed.
-
-lemma ostar_true: ∀S.∀i:pitem S.
- 〈i,true〉^⊛ = 〈(\fst (•i))^*, true〉.
-// qed.
-
-lemma ostar_false: ∀S.∀i:pitem S.
- 〈i,false〉^⊛ = 〈i^*, false〉.
-// qed.
-lemma erase_ostar: ∀S.∀e:pre S.
- |\fst (e^⊛)| = |\fst e|^*.
-#S * #i * // qed.
-
-lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i.
- \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▸ i} ∪ { [ ] }.
-#S #e1 #i
-cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▸ i), \snd(e1 ▸ i) ∨ true〉) [//]
-#H >H cases (e1 ▸ i) #i1 #b1 cases b1
- [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc]
- @eqP_union_l /2/
- |/2/
+lemma memb_filter: ∀S,f,l,x. memb S x (filter ? f l) = true →
+memb S x l = true ∧ (f x = true).
+/3/ qed.
+
+lemma memb_filter_l: ∀S,f,x,l. (f x = true) → memb S x l = true →
+memb S x (filter ? f l) = true.
+#S #f #x #l #fx elim l normalize //
+#b #tl #Hind cases (true_or_false (x==b)) #eqxb
+ [<(\P eqxb) >(\b (refl … x)) >fx normalize >(\b (refl … x)) normalize //
+ |>eqxb cases (f b) normalize [>eqxb normalize @Hind| @Hind]
]
-qed.
+qed.
-lemma eq_odot_false: ∀S:DeqSet.∀e1:pre S.∀i.
- e1 ⊙ 〈i,false〉 = e1 ▸ i.
-#S #e1 #i
-cut (e1 ⊙ 〈i,false〉 = 〈\fst (e1 ▸ i), \snd(e1 ▸ i) ∨ false〉) [//]
-cases (e1 ▸ i) #i1 #b1 cases b1 #H @H
-qed.
+(********************* exists *****************)
-lemma sem_odot:
- ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
-#S #e1 * #i2 *
- [>sem_pre_true
- @eqP_trans [|@sem_odot_true]
- @eqP_trans [||@union_assoc] @eqP_union_r @odot_dot_aux //
- |>sem_pre_false >eq_odot_false @odot_dot_aux //
- ]
-qed.
+let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝
+match l with
+[ nil ⇒ false
+| cons h t ⇒ orb (p h) (exists A p t)
+].
-(* theorem 16: 4 *)
-theorem sem_ostar: ∀S.∀e:pre S.
- \sem{e^⊛} =1 \sem{e} · \sem{|\fst e|}^*.
-#S * #i #b cases b
- [>sem_pre_true >sem_pre_true >sem_star >erase_bull
- @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@sem_fst_aux //]]]
- @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
- @eqP_trans [||@eqP_sym @distr_cat_r]
- @eqP_trans [|@union_assoc] @eqP_union_l
- @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps
- |>sem_pre_false >sem_pre_false >sem_star /2/
- ]
+lemma Exists_exists : ∀A,P,l.
+ Exists A P l →
+ ∃x. P x.
+#A #P #l elim l [ * | #hd #tl #IH * [ #H %{hd} @H | @IH ]
qed.
-
-include "basics/logic.ma".
-
-(* Given a universe A, we can consider sets of elements of type A by means of their
-characteristic predicates A → Prop. *)
-
-definition set ≝ λA:Type[0].A → Prop.
-
-(* For instance, the empty set is the set defined by an always False predicate *)
-
-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.
-
-(* the singleton set {a} can be defined by the characteristic predicate stating
-equality with a *)
-
-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.
-
-(* Complement, union and intersection are easily defined, by means of logical
-connectives *)
-
-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).
-
-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).
-
-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).
-
-
-
-
-
-
-
- (* The reader could probably wonder what is the difference between Prop and bool.
-In fact, they are quite distinct entities. In type theory, all objects are structured
-in a three levels hierarchy
- t : A : s
-where, t is a term, A is a type, and s is called a sort. Sorts are special, primitive
-constants used to give a type to types. Now, Prop is a primitive sort, while bool is
-just a user defined data type (whose sort his Type[0]). In particular, Prop is the
-sort of Propositions: its elements are logical statements in the usual sense. The important
-point is that statements are inhabited by their proofs: a triple of the kind
- p : Q : Prop
-should be read as p is a proof of the proposition Q.*)
-
-
-
-include "arithmetics/nat.ma".
include "basics/list.ma".
+include "basics/sets.ma".
+include "basics/deqsets.ma".
-interpretation "iff" 'iff a b = (iff a b).
-
-record Alpha : Type[1] ≝ { carr :> Type[0];
- eqb: carr → carr → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6;
- 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)
-}.
-
-notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
-interpretation "eqb" 'eqb a b = (eqb ? a b).
-
-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.
-
-inductive re (S: \ 5a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) : Type[0] ≝
- z: re S
- | e: re S
- | s: S → re S
- | c: re S → re S → 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 90 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
-coercion c : ∀S:Alpha.∀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).
+definition word ≝ λS:DeqSet.list S.
notation "ϵ" non associative with precedence 90 for @{ 'epsilon }.
-interpretation "epsilon" 'epsilon = (e ?).
-
-notation "∅" non associative with precedence 90 for @{ 'empty }.
-interpretation "empty" 'empty = (z ?).
-
-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 ≝
-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 ].
-
-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 ≝
-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 ].
+interpretation "epsilon" 'epsilon = (nil ?).
+
+(* concatenation *)
+definition cat : ∀S,l1,l2,w.Prop ≝
+ λS.λl1,l2.λw:word S.∃w1,w2.w1 @ w2 = w ∧ l1 w1 ∧ l2 w2.
+notation "a · b" non associative with precedence 60 for @{ 'middot $a $b}.
+interpretation "cat lang" 'middot a b = (cat ? a b).
+
+let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝
+match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
+
+let rec conjunct (S : DeqSet) (l : list (word S)) (r : word S → Prop) on l: Prop ≝
+match l with [ nil ⇒ True | cons w tl ⇒ r w ∧ conjunct ? tl r ].
+
+(* kleene's star *)
+definition star ≝ λS.λl.λw:word S.∃lw.flatten ? lw = w ∧ conjunct ? lw l.
+notation "a ^ *" non associative with precedence 90 for @{ 'star $a}.
+interpretation "star lang" 'star l = (star ? l).
+
+lemma cat_ext_l: ∀S.∀A,B,C:word S →Prop.
+ A =1 C → A · B =1 C · B.
+#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
+cases (H w1) /6/
+qed.
+
+lemma cat_ext_r: ∀S.∀A,B,C:word S →Prop.
+ B =1 C → A · B =1 A · C.
+#S #A #B #C #H #w % * #w1 * #w2 * * #eqw #inw1 #inw2
+cases (H w2) /6/
+qed.
+
+lemma cat_empty_l: ∀S.∀A:word S→Prop. ∅ · A =1 ∅.
+#S #A #w % [|*] * #w1 * #w2 * * #_ *
+qed.
+
+lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop.
+ (A ∪ B) · C =1 A · C ∪ B · C.
+#S #A #B #C #w %
+ [* #w1 * #w2 * * #eqw * /6/ |* * #w1 * #w2 * * /6/]
+qed.
+
+(* derivative *)
+
+definition deriv ≝ λS.λA:word S → Prop.λa,w. A (a::w).
+
+lemma deriv_middot: ∀S,A,B,a. ¬ A ϵ →
+ deriv S (A·B) a =1 (deriv S A a) · B.
+#S #A #B #a #noteps #w normalize %
+ [* #w1 cases w1
+ [* #w2 * * #_ #Aeps @False_ind /2/
+ |#b #w2 * #w3 * * whd in ⊢ ((??%?)→?); #H destruct
+ #H #H1 @(ex_intro … w2) @(ex_intro … w3) % // % //
+ ]
+ |* #w1 * #w2 * * #H #H1 #H2 @(ex_intro … (a::w1))
+ @(ex_intro … w2) % // % normalize //
+ ]
+qed.
+
+(* star properties *)
+lemma espilon_in_star: ∀S.∀A:word S → Prop.
+ A^* ϵ.
+#S #A @(ex_intro … [ ]) normalize /2/
+qed.
+
+lemma cat_to_star:∀S.∀A:word S → Prop.
+ ∀w1,w2. A w1 → A^* w2 → A^* (w1@w2).
+#S #A #w1 #w2 #Aw * #l * #H #H1 @(ex_intro … (w1::l))
+% normalize /2/
+qed.
+
+lemma fix_star: ∀S.∀A:word S → Prop.
+ A^* =1 A · A^* ∪ {ϵ}.
+#S #A #w %
+ [* #l generalize in match w; -w cases l [normalize #w * /2/]
+ #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
+ #w1A #cw1 %1 @(ex_intro … w1) @(ex_intro … (flatten S tl))
+ % /2/ whd @(ex_intro … tl) /2/
+ |* [2: whd in ⊢ (%→?); #eqw <eqw //]
+ * #w1 * #w2 * * #eqw <eqw @cat_to_star
+ ]
+qed.
+
+lemma star_fix_eps : ∀S.∀A:word S → Prop.
+ A^* =1 (A - {ϵ}) · A^* ∪ {ϵ}.
+#S #A #w %
+ [* #l elim l
+ [* whd in ⊢ ((??%?)→?); #eqw #_ %2 <eqw //
+ |* [#tl #Hind * #H * #_ #H2 @Hind % [@H | //]
+ |#a #w1 #tl #Hind * whd in ⊢ ((??%?)→?); #H1 * #H2 #H3 %1
+ @(ex_intro … (a::w1)) @(ex_intro … (flatten S tl)) %
+ [% [@H1 | normalize % /2/] |whd @(ex_intro … tl) /2/]
+ ]
+ ]
+ |* [* #w1 * #w2 * * #eqw * #H1 #_ <eqw @cat_to_star //
+ | whd in ⊢ (%→?); #H <H //
+ ]
+ ]
+qed.
+
+lemma star_epsilon: ∀S:DeqSet.∀A:word S → Prop.
+ A^* ∪ {ϵ} =1 A^*.
+#S #A #w % /2/ * //
+qed.
+
+lemma epsilon_cat_r: ∀S.∀A:word S →Prop.
+ A · {ϵ} =1 A.
+#S #A #w %
+ [* #w1 * #w2 * * #eqw #inw1 normalize #eqw2 <eqw //
+ |#inA @(ex_intro … w) @(ex_intro … [ ]) /3/
+ ]
+qed.
+
+lemma epsilon_cat_l: ∀S.∀A:word S →Prop.
+ {ϵ} · A =1 A.
+#S #A #w %
+ [* #w1 * #w2 * * #eqw normalize #eqw2 <eqw <eqw2 //
+ |#inA @(ex_intro … ϵ) @(ex_intro … w) /3/
+ ]
+qed.
+
+lemma distr_cat_r_eps: ∀S.∀A,C:word S →Prop.
+ (A ∪ {ϵ}) · C =1 A · C ∪ C.
+#S #A #C @eqP_trans [|@distr_cat_r |@eqP_union_l @epsilon_cat_l]
+qed.
-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.
-notation "{}" non associative with precedence 90 f
\ No newline at end of file
--- /dev/null
+include "lang.ma".
+
+inductive re (S: DeqSet) : Type[0] ≝
+ z: re S
+ | e: re S
+ | s: S → re S
+ | c: re S → re S → re S
+ | o: re S → re S → re S
+ | k: re S → re S.
+
+interpretation "re epsilon" 'epsilon = (e ?).
+interpretation "re or" 'plus a b = (o ? a b).
+interpretation "re cat" 'middot a b = (c ? a b).
+interpretation "re star" 'star a = (k ? a).
+
+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 @{ 'empty }.
+interpretation "empty" 'empty = (z ?).
+
+let rec in_l (S : DeqSet) (r : re S) on r : word S → Prop ≝
+match r with
+[ z ⇒ ∅
+| e ⇒ {ϵ}
+| s x ⇒ {[x]}
+| c r1 r2 ⇒ (in_l ? r1) · (in_l ? r2)
+| o r1 r2 ⇒ (in_l ? r1) ∪ (in_l ? r2)
+| k r1 ⇒ (in_l ? r1) ^*].
+
+notation "\sem{term 19 E}" non associative with precedence 75 for @{'in_l $E}.
+interpretation "in_l" 'in_l E = (in_l ? E).
+interpretation "in_l mem" 'mem w l = (in_l ? l w).
+
+lemma rsem_star : ∀S.∀r: re S. \sem{r^*} = \sem{r}^*.
+// qed.
+
+
+(* pointed items *)
+inductive pitem (S: DeqSet) : Type[0] ≝
+ pz: pitem S
+ | pe: pitem S
+ | ps: S → pitem S
+ | pp: S → pitem S
+ | pc: pitem S → pitem S → pitem S
+ | po: pitem S → pitem S → pitem S
+ | pk: pitem S → pitem S.
+
+definition pre ≝ λS.pitem S × bool.
+
+interpretation "pitem star" 'star a = (pk ? a).
+interpretation "pitem or" 'plus a b = (po ? a b).
+interpretation "pitem cat" 'middot 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 "pitem pp" 'pp a = (pp ? a).
+interpretation "pitem ps" 'ps a = (ps ? a).
+interpretation "pitem epsilon" 'epsilon = (pe ?).
+interpretation "pitem empty" 'empty = (pz ?).
+
+let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝
+ match l with
+ [ pz ⇒ `∅
+ | pe ⇒ ϵ
+ | ps x ⇒ `x
+ | pp x ⇒ `x
+ | pc E1 E2 ⇒ (forget ? E1) · (forget ? E2)
+ | po E1 E2 ⇒ (forget ? E1) + (forget ? E2)
+ | pk E ⇒ (forget ? E)^* ].
+
+(* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*)
+interpretation "forget" 'norm a = (forget ? a).
+
+lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
+// qed.
+
+lemma erase_plus : ∀S.∀i1,i2:pitem S.
+ |i1 + i2| = |i1| + |i2|.
+// qed.
+
+lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*.
+// qed.
+
+(* boolean equality *)
+let rec beqitem S (i1,i2: pitem S) on i1 ≝
+ match i1 with
+ [ pz ⇒ match i2 with [ pz ⇒ true | _ ⇒ false]
+ | pe ⇒ match i2 with [ pe ⇒ true | _ ⇒ false]
+ | ps y1 ⇒ match i2 with [ ps y2 ⇒ y1==y2 | _ ⇒ false]
+ | pp y1 ⇒ match i2 with [ pp y2 ⇒ y1==y2 | _ ⇒ false]
+ | po i11 i12 ⇒ match i2 with
+ [ po i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
+ | _ ⇒ false]
+ | pc i11 i12 ⇒ match i2 with
+ [ pc i21 i22 ⇒ beqitem S i11 i21 ∧ beqitem S i12 i22
+ | _ ⇒ false]
+ | pk i11 ⇒ match i2 with [ pk i21 ⇒ beqitem S i11 i21 | _ ⇒ false]
+ ].
+
+lemma beqitem_true: ∀S,i1,i2. iff (beqitem S i1 i2 = true) (i1 = i2).
+#S #i1 elim i1
+ [#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
+ |#i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % // normalize #H destruct
+ |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
+ [>(\P H) // | @(\b (refl …))]
+ |#x #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] % normalize #H destruct
+ [>(\P H) // | @(\b (refl …))]
+ |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
+ normalize #H destruct
+ [cases (true_or_false (beqitem S i11 i21)) #H1
+ [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
+ |>H1 in H; normalize #abs @False_ind /2/
+ ]
+ |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
+ ]
+ |#i11 #i12 #Hind1 #Hind2 #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i3] %
+ normalize #H destruct
+ [cases (true_or_false (beqitem S i11 i21)) #H1
+ [>(proj1 … (Hind1 i21) H1) >(proj1 … (Hind2 i22)) // >H1 in H; #H @H
+ |>H1 in H; normalize #abs @False_ind /2/
+ ]
+ |>(proj2 … (Hind1 i21) (refl …)) >(proj2 … (Hind2 i22) (refl …)) //
+ ]
+ |#i3 #Hind #i2 cases i2 [||#a|#a|#i21 #i22| #i21 #i22|#i4] %
+ normalize #H destruct
+ [>(proj1 … (Hind i4) H) // |>(proj2 … (Hind i4) (refl …)) //]
+ ]
+qed.
+
+definition DeqItem ≝ λS.
+ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S).
+
+unification hint 0 ≔ S;
+ X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
+(* ---------------------------------------- *) ⊢
+ pitem S ≡ carr X.
+
+unification hint 0 ≔ S,i1,i2;
+ X ≟ mk_DeqSet (pitem S) (beqitem S) (beqitem_true S)
+(* ---------------------------------------- *) ⊢
+ beqitem S i1 i2 ≡ eqb X i1 i2.
+
+(* semantics *)
+
+let rec in_pl (S : DeqSet) (r : pitem S) on r : word S → Prop ≝
+match r with
+[ pz ⇒ ∅
+| pe ⇒ ∅
+| ps _ ⇒ ∅
+| pp x ⇒ { [x] }
+| pc r1 r2 ⇒ (in_pl ? r1) · \sem{forget ? r2} ∪ (in_pl ? r2)
+| po r1 r2 ⇒ (in_pl ? r1) ∪ (in_pl ? r2)
+| pk r1 ⇒ (in_pl ? r1) · \sem{forget ? r1}^* ].
+
+interpretation "in_pl" 'in_l E = (in_pl ? E).
+interpretation "in_pl mem" 'mem w l = (in_pl ? l w).
+
+definition in_prl ≝ λS : DeqSet.λp:pre S.
+ if (\snd p) then \sem{\fst p} ∪ {ϵ} else \sem{\fst p}.
+
+interpretation "in_prl mem" 'mem w l = (in_prl ? l w).
+interpretation "in_prl" 'in_l E = (in_prl ? E).
+
+lemma sem_pre_true : ∀S.∀i:pitem S.
+ \sem{〈i,true〉} = \sem{i} ∪ {ϵ}.
+// qed.
+
+lemma sem_pre_false : ∀S.∀i:pitem S.
+ \sem{〈i,false〉} = \sem{i}.
+// qed.
+
+lemma sem_cat: ∀S.∀i1,i2:pitem S.
+ \sem{i1 · i2} = \sem{i1} · \sem{|i2|} ∪ \sem{i2}.
+// qed.
+
+lemma sem_cat_w: ∀S.∀i1,i2:pitem S.∀w.
+ \sem{i1 · i2} w = ((\sem{i1} · \sem{|i2|}) w ∨ \sem{i2} w).
+// qed.
+
+lemma sem_plus: ∀S.∀i1,i2:pitem S.
+ \sem{i1 + i2} = \sem{i1} ∪ \sem{i2}.
+// qed.
+
+lemma sem_plus_w: ∀S.∀i1,i2:pitem S.∀w.
+ \sem{i1 + i2} w = (\sem{i1} w ∨ \sem{i2} w).
+// qed.
+
+lemma sem_star : ∀S.∀i:pitem S.
+ \sem{i^*} = \sem{i} · \sem{|i|}^*.
+// qed.
+
+lemma sem_star_w : ∀S.∀i:pitem S.∀w.
+ \sem{i^*} w = (∃w1,w2.w1 @ w2 = w ∧ \sem{i} w1 ∧ \sem{|i|}^* w2).
+// qed.
+
+lemma append_eq_nil : ∀S.∀w1,w2:word S. w1 @ w2 = ϵ → w1 = ϵ.
+#S #w1 #w2 cases w1 // #a #tl normalize #H destruct qed.
+
+lemma not_epsilon_lp : ∀S:DeqSet.∀e:pitem S. ¬ (ϵ ∈ e).
+#S #e elim e normalize /2/
+ [#r1 #r2 * #n1 #n2 % * /2/ * #w1 * #w2 * * #H
+ >(append_eq_nil …H…) /2/
+ |#r1 #r2 #n1 #n2 % * /2/
+ |#r #n % * #w1 * #w2 * * #H >(append_eq_nil …H…) /2/
+ ]
+qed.
+
+(* lemma 12 *)
+lemma epsilon_to_true : ∀S.∀e:pre S. ϵ ∈ e → \snd e = true.
+#S * #i #b cases b // normalize #H @False_ind /2/
+qed.
+
+lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → ϵ ∈ e.
+#S * #i #b #btrue normalize in btrue; >btrue %2 //
+qed.
+
+lemma minus_eps_item: ∀S.∀i:pitem S. \sem{i} =1 \sem{i}-{[ ]}.
+#S #i #w %
+ [#H whd % // normalize @(not_to_not … (not_epsilon_lp …i)) //
+ |* //
+ ]
+qed.
+
+lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+#S * #i *
+ [>sem_pre_true normalize in ⊢ (??%?); #w %
+ [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
+ |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ]
+ ]
+qed.
+
+definition lo ≝ λS:DeqSet.λa,b:pre S.〈\fst a + \fst b,\snd a ∨ \snd b〉.
+notation "a ⊕ b" left associative with precedence 60 for @{'oplus $a $b}.
+interpretation "oplus" 'oplus a b = (lo ? a b).
+
+lemma lo_def: ∀S.∀i1,i2:pitem S.∀b1,b2. 〈i1,b1〉⊕〈i2,b2〉=〈i1+i2,b1∨b2〉.
+// qed.
+
+definition pre_concat_r ≝ λS:DeqSet.λi:pitem S.λe:pre S.
+ match e with [ mk_Prod i1 b ⇒ 〈i · i1, b〉].
+
+notation "i ◃ e" left associative with precedence 60 for @{'lhd $i $e}.
+interpretation "pre_concat_r" 'lhd i e = (pre_concat_r ? i e).
+
+lemma eq_to_ex_eq: ∀S.∀A,B:word S → Prop.
+ A = B → A =1 B.
+#S #A #B #H >H /2/ qed.
+
+lemma sem_pre_concat_r : ∀S,i.∀e:pre S.
+ \sem{i ◃ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}.
+#S #i * #i1 #b1 cases b1 [2: @eq_to_ex_eq //]
+>sem_pre_true >sem_cat >sem_pre_true /2/
+qed.
+
+definition pre_concat_l ≝ λS:DeqSet.λbcast:∀S:DeqSet.pitem S → pre S.λe1:pre S.λi2:pitem S.
+ match e1 with
+ [ mk_Prod i1 b1 ⇒ match b1 with
+ [ true ⇒ (i1 ◃ (bcast ? i2))
+ | false ⇒ 〈i1 · i2,false〉
+ ]
+ ].
+
+notation "a ▹ b" left associative with precedence 60 for @{'tril eclose $a $b}.
+interpretation "item-pre concat" 'tril op a b = (pre_concat_l ? op a b).
+
+notation "•" non associative with precedence 60 for @{eclose ?}.
+
+let rec eclose (S: DeqSet) (i: pitem S) on i : pre S ≝
+ match i with
+ [ pz ⇒ 〈 `∅, false 〉
+ | pe ⇒ 〈 ϵ, true 〉
+ | ps x ⇒ 〈 `.x, false〉
+ | pp x ⇒ 〈 `.x, false 〉
+ | po i1 i2 ⇒ •i1 ⊕ •i2
+ | pc i1 i2 ⇒ •i1 ▹ i2
+ | pk i ⇒ 〈(\fst (•i))^*,true〉].
+
+notation "• x" non associative with precedence 60 for @{'eclose $x}.
+interpretation "eclose" 'eclose x = (eclose ? x).
+
+lemma eclose_plus: ∀S:DeqSet.∀i1,i2:pitem S.
+ •(i1 + i2) = •i1 ⊕ •i2.
+// qed.
+
+lemma eclose_dot: ∀S:DeqSet.∀i1,i2:pitem S.
+ •(i1 · i2) = •i1 ▹ i2.
+// qed.
+
+lemma eclose_star: ∀S:DeqSet.∀i:pitem S.
+ •i^* = 〈(\fst(•i))^*,true〉.
+// qed.
+
+definition lift ≝ λS.λf:pitem S →pre S.λe:pre S.
+ match e with
+ [ mk_Prod i b ⇒ 〈\fst (f i), \snd (f i) ∨ b〉].
+
+definition preclose ≝ λS. lift S (eclose S).
+interpretation "preclose" 'eclose x = (preclose ? x).
+
+(* theorem 16: 2 *)
+lemma sem_oplus: ∀S:DeqSet.∀e1,e2:pre S.
+ \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
+#S * #i1 #b1 * #i2 #b2 #w %
+ [cases b1 cases b2 normalize /2/ * /3/ * /3/
+ |cases b1 cases b2 normalize /2/ * /3/ * /3/
+ ]
+qed.
+
+lemma odot_true :
+ ∀S.∀i1,i2:pitem S.
+ 〈i1,true〉 ▹ i2 = i1 ◃ (•i2).
+// qed.
+
+lemma odot_true_bis :
+ ∀S.∀i1,i2:pitem S.
+ 〈i1,true〉 ▹ i2 = 〈i1 · \fst (•i2), \snd (•i2)〉.
+#S #i1 #i2 normalize cases (•i2) // qed.
+
+lemma odot_false:
+ ∀S.∀i1,i2:pitem S.
+ 〈i1,false〉 ▹ i2 = 〈i1 · i2, false〉.
+// qed.
+
+lemma LcatE : ∀S.∀e1,e2:pitem S.
+ \sem{e1 · e2} = \sem{e1} · \sem{|e2|} ∪ \sem{e2}.
+// qed.
+
+lemma erase_bull : ∀S.∀i:pitem S. |\fst (•i)| = |i|.
+#S #i elim i //
+ [ #i1 #i2 #IH1 #IH2 >erase_dot <IH1 >eclose_dot
+ cases (•i1) #i11 #b1 cases b1 // <IH2 >odot_true_bis //
+ | #i1 #i2 #IH1 #IH2 >eclose_plus >(erase_plus … i1) <IH1 <IH2
+ cases (•i1) #i11 #b1 cases (•i2) #i21 #b2 //
+ | #i #IH >eclose_star >(erase_star … i) <IH cases (•i) //
+ ]
+qed.
+
+(*
+lemma sem_eclose_star: ∀S:DeqSet.∀i:pitem S.
+ \sem{〈i^*,true〉} =1 \sem{〈i,false〉}·\sem{|i|}^* ∪ {ϵ}.
+/2/ qed.
+*)
+
+(* theorem 16: 1 → 3 *)
+lemma odot_dot_aux : ∀S.∀e1:pre S.∀i2:pitem S.
+ \sem{•i2} =1 \sem{i2} ∪ \sem{|i2|} →
+ \sem{e1 ▹ i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
+#S * #i1 #b1 #i2 cases b1
+ [2:#th >odot_false >sem_pre_false >sem_pre_false >sem_cat /2/
+ |#H >odot_true >sem_pre_true @(eqP_trans … (sem_pre_concat_r …))
+ >erase_bull @eqP_trans [|@(eqP_union_l … H)]
+ @eqP_trans [|@eqP_union_l[|@union_comm ]]
+ @eqP_trans [|@eqP_sym @union_assoc ] /3/
+ ]
+qed.
+
+lemma minus_eps_pre_aux: ∀S.∀e:pre S.∀i:pitem S.∀A.
+ \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}).
+#S #e #i #A #seme
+@eqP_trans [|@minus_eps_pre]
+@eqP_trans [||@eqP_union_r [|@eqP_sym @minus_eps_item]]
+@eqP_trans [||@distribute_substract]
+@eqP_substract_r //
+qed.
+
+(* theorem 16: 1 *)
+theorem sem_bull: ∀S:DeqSet. ∀i:pitem S. \sem{•i} =1 \sem{i} ∪ \sem{|i|}.
+#S #e elim e
+ [#w normalize % [/2/ | * //]
+ |/2/
+ |#x normalize #w % [ /2/ | * [@False_ind | //]]
+ |#x normalize #w % [ /2/ | * // ]
+ |#i1 #i2 #IH1 #IH2 >eclose_dot
+ @eqP_trans [|@odot_dot_aux //] >sem_cat
+ @eqP_trans
+ [|@eqP_union_r
+ [|@eqP_trans [|@(cat_ext_l … IH1)] @distr_cat_r]]
+ @eqP_trans [|@union_assoc]
+ @eqP_trans [||@eqP_sym @union_assoc]
+ @eqP_union_l //
+ |#i1 #i2 #IH1 #IH2 >eclose_plus
+ @eqP_trans [|@sem_oplus] >sem_plus >erase_plus
+ @eqP_trans [|@(eqP_union_l … IH2)]
+ @eqP_trans [|@eqP_sym @union_assoc]
+ @eqP_trans [||@union_assoc] @eqP_union_r
+ @eqP_trans [||@eqP_sym @union_assoc]
+ @eqP_trans [||@eqP_union_l [|@union_comm]]
+ @eqP_trans [||@union_assoc] /2/
+ |#i #H >sem_pre_true >sem_star >erase_bull >sem_star
+ @eqP_trans [|@eqP_union_r [|@cat_ext_l [|@minus_eps_pre_aux //]]]
+ @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
+ @eqP_trans [|@union_assoc] @eqP_union_l >erase_star
+ @eqP_sym @star_fix_eps
+ ]
+qed.
+
+(* blank item *)
+let rec blank (S: DeqSet) (i: re S) on i :pitem S ≝
+ match i with
+ [ z ⇒ `∅
+ | e ⇒ ϵ
+ | s y ⇒ `y
+ | o e1 e2 ⇒ (blank S e1) + (blank S e2)
+ | c e1 e2 ⇒ (blank S e1) · (blank S e2)
+ | k e ⇒ (blank S e)^* ].
+
+lemma forget_blank: ∀S.∀e:re S.|blank S e| = e.
+#S #e elim e normalize //
+qed.
+
+lemma sem_blank: ∀S.∀e:re S.\sem{blank S e} =1 ∅.
+#S #e elim e
+ [1,2:@eq_to_ex_eq //
+ |#s @eq_to_ex_eq //
+ |#e1 #e2 #Hind1 #Hind2 >sem_cat
+ @eqP_trans [||@(union_empty_r … ∅)]
+ @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r
+ @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind1
+ |#e1 #e2 #Hind1 #Hind2 >sem_plus
+ @eqP_trans [||@(union_empty_r … ∅)]
+ @eqP_trans [|@eqP_union_l[|@Hind2]] @eqP_union_r @Hind1
+ |#e #Hind >sem_star
+ @eqP_trans [||@(cat_empty_l … ?)] @cat_ext_l @Hind
+ ]
+qed.
+
+theorem re_embedding: ∀S.∀e:re S.
+ \sem{•(blank S e)} =1 \sem{e}.
+#S #e @eqP_trans [|@sem_bull] >forget_blank
+@eqP_trans [|@eqP_union_r [|@sem_blank]]
+@eqP_trans [|@union_comm] @union_empty_r.
+qed.
+
+(* lefted operations *)
+definition lifted_cat ≝ λS:DeqSet.λe:pre S.
+ lift S (pre_concat_l S eclose e).
+
+notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}.
+
+interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2).
+
+lemma odot_true_b : ∀S.∀i1,i2:pitem S.∀b.
+ 〈i1,true〉 ⊙ 〈i2,b〉 = 〈i1 · (\fst (•i2)),\snd (•i2) ∨ b〉.
+#S #i1 #i2 #b normalize in ⊢ (??%?); cases (•i2) //
+qed.
+
+lemma odot_false_b : ∀S.∀i1,i2:pitem S.∀b.
+ 〈i1,false〉 ⊙ 〈i2,b〉 = 〈i1 · i2 ,b〉.
+//
+qed.
+
+lemma erase_odot:∀S.∀e1,e2:pre S.
+ |\fst (e1 ⊙ e2)| = |\fst e1| · (|\fst e2|).
+#S * #i1 * * #i2 #b2 // >odot_true_b >erase_dot //
+qed.
+
+definition lk ≝ λS:DeqSet.λe:pre S.
+ match e with
+ [ mk_Prod i1 b1 ⇒
+ match b1 with
+ [true ⇒ 〈(\fst (eclose ? i1))^*, true〉
+ |false ⇒ 〈i1^*,false〉
+ ]
+ ].
+
+(* notation < "a \sup ⊛" non associative with precedence 90 for @{'lk $a}.*)
+interpretation "lk" 'lk a = (lk ? a).
+notation "a^⊛" non associative with precedence 90 for @{'lk $a}.
+
+
+lemma ostar_true: ∀S.∀i:pitem S.
+ 〈i,true〉^⊛ = 〈(\fst (•i))^*, true〉.
+// qed.
+
+lemma ostar_false: ∀S.∀i:pitem S.
+ 〈i,false〉^⊛ = 〈i^*, false〉.
+// qed.
+
+lemma erase_ostar: ∀S.∀e:pre S.
+ |\fst (e^⊛)| = |\fst e|^*.
+#S * #i * // qed.
+
+lemma sem_odot_true: ∀S:DeqSet.∀e1:pre S.∀i.
+ \sem{e1 ⊙ 〈i,true〉} =1 \sem{e1 ▹ i} ∪ { [ ] }.
+#S #e1 #i
+cut (e1 ⊙ 〈i,true〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ true〉) [//]
+#H >H cases (e1 ▹ i) #i1 #b1 cases b1
+ [>sem_pre_true @eqP_trans [||@eqP_sym @union_assoc]
+ @eqP_union_l /2/
+ |/2/
+ ]
+qed.
+
+lemma eq_odot_false: ∀S:DeqSet.∀e1:pre S.∀i.
+ e1 ⊙ 〈i,false〉 = e1 ▹ i.
+#S #e1 #i
+cut (e1 ⊙ 〈i,false〉 = 〈\fst (e1 ▹ i), \snd(e1 ▹ i) ∨ false〉) [//]
+cases (e1 ▹ i) #i1 #b1 cases b1 #H @H
+qed.
+
+lemma sem_odot:
+ ∀S.∀e1,e2: pre S. \sem{e1 ⊙ e2} =1 \sem{e1}· \sem{|\fst e2|} ∪ \sem{e2}.
+#S #e1 * #i2 *
+ [>sem_pre_true
+ @eqP_trans [|@sem_odot_true]
+ @eqP_trans [||@union_assoc] @eqP_union_r @odot_dot_aux //
+ |>sem_pre_false >eq_odot_false @odot_dot_aux //
+ ]
+qed.
+
+(* theorem 16: 4 *)
+theorem sem_ostar: ∀S.∀e:pre S.
+ \sem{e^⊛} =1 \sem{e} · \sem{|\fst e|}^*.
+#S * #i #b cases b
+ [>sem_pre_true >sem_pre_true >sem_star >erase_bull
+ @eqP_trans [|@eqP_union_r[|@cat_ext_l [|@minus_eps_pre_aux //]]]
+ @eqP_trans [|@eqP_union_r [|@distr_cat_r]]
+ @eqP_trans [||@eqP_sym @distr_cat_r]
+ @eqP_trans [|@union_assoc] @eqP_union_l
+ @eqP_trans [||@eqP_sym @epsilon_cat_l] @eqP_sym @star_fix_eps
+ |>sem_pre_false >sem_pre_false >sem_star /2/
+ ]
+qed.
+
--- /dev/null
+include "re.ma".
+include "basics/listb.ma".
+
+let rec move (S: DeqSet) (x:S) (E: pitem S) on E : pre S ≝
+ match E with
+ [ pz ⇒ 〈 `∅, false 〉
+ | pe ⇒ 〈 ϵ, false 〉
+ | ps y ⇒ 〈 `y, false 〉
+ | pp y ⇒ 〈 `y, x == y 〉
+ | po e1 e2 ⇒ (move ? x e1) ⊕ (move ? x e2)
+ | pc e1 e2 ⇒ (move ? x e1) ⊙ (move ? x e2)
+ | pk e ⇒ (move ? x e)^⊛ ].
+
+lemma move_plus: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S.
+ move S x (i1 + i2) = (move ? x i1) ⊕ (move ? x i2).
+// qed.
+
+lemma move_cat: ∀S:DeqSet.∀x:S.∀i1,i2:pitem S.
+ move S x (i1 · i2) = (move ? x i1) ⊙ (move ? x i2).
+// qed.
+
+lemma move_star: ∀S:DeqSet.∀x:S.∀i:pitem S.
+ move S x i^* = (move ? x i)^⊛.
+// qed.
+
+definition pmove ≝ λS:DeqSet.λx:S.λe:pre S. move ? x (\fst e).
+
+lemma pmove_def : ∀S:DeqSet.∀x:S.∀i:pitem S.∀b.
+ pmove ? x 〈i,b〉 = move ? x i.
+// qed.
+
+lemma eq_to_eq_hd: ∀A.∀l1,l2:list A.∀a,b.
+ a::l1 = b::l2 → a = b.
+#A #l1 #l2 #a #b #H destruct //
+qed.
+
+lemma same_kernel: ∀S:DeqSet.∀a:S.∀i:pitem S.
+ |\fst (move ? a i)| = |i|.
+#S #a #i elim i //
+ [#i1 #i2 #H1 #H2 >move_cat >erase_odot //
+ |#i1 #i2 #H1 #H2 >move_plus whd in ⊢ (??%%); //
+ ]
+qed.
+
+theorem move_ok:
+ ∀S:DeqSet.∀a:S.∀i:pitem S.∀w: word S.
+ \sem{move ? a i} w ↔ \sem{i} (a::w).
+#S #a #i elim i
+ [normalize /2/
+ |normalize /2/
+ |normalize /2/
+ |normalize #x #w cases (true_or_false (a==x)) #H >H normalize
+ [>(\P H) % [* // #bot @False_ind //| #H1 destruct /2/]
+ |% [@False_ind |#H1 cases (\Pf H) #H2 @H2 destruct //]
+ ]
+ |#i1 #i2 #HI1 #HI2 #w >move_cat
+ @iff_trans[|@sem_odot] >same_kernel >sem_cat_w
+ @iff_trans[||@(iff_or_l … (HI2 w))] @iff_or_r
+ @iff_trans[||@iff_sym @deriv_middot //]
+ @cat_ext_l @HI1
+ |#i1 #i2 #HI1 #HI2 #w >(sem_plus S i1 i2) >move_plus >sem_plus_w
+ @iff_trans[|@sem_oplus]
+ @iff_trans[|@iff_or_l [|@HI2]| @iff_or_r //]
+ |#i1 #HI1 #w >move_star
+ @iff_trans[|@sem_ostar] >same_kernel >sem_star_w
+ @iff_trans[||@iff_sym @deriv_middot //]
+ @cat_ext_l @HI1
+ ]
+qed.
+
+notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
+let rec moves (S : DeqSet) w e on w : pre S ≝
+ match w with
+ [ nil ⇒ e
+ | cons x w' ⇒ w' ↦* (move S x (\fst e))].
+
+lemma moves_empty: ∀S:DeqSet.∀e:pre S.
+ moves ? [ ] e = e.
+// qed.
+
+lemma moves_cons: ∀S:DeqSet.∀a:S.∀w.∀e:pre S.
+ moves ? (a::w) e = moves ? w (move S a (\fst e)).
+// qed.
+
+lemma moves_left : ∀S,a,w,e.
+ moves S (w@[a]) e = move S a (\fst (moves S w e)).
+#S #a #w elim w // #x #tl #Hind #e >moves_cons >moves_cons //
+qed.
+
+lemma not_epsilon_sem: ∀S:DeqSet.∀a:S.∀w: word S. ∀e:pre S.
+ iff ((a::w) ∈ e) ((a::w) ∈ \fst e).
+#S #a #w * #i #b cases b normalize
+ [% /2/ * // #H destruct |% normalize /2/]
+qed.
+
+lemma same_kernel_moves: ∀S:DeqSet.∀w.∀e:pre S.
+ |\fst (moves ? w e)| = |\fst e|.
+#S #w elim w //
+qed.
+
+theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S.
+ (\snd (moves ? w e) = true) ↔ \sem{e} w.
+#S #w elim w
+ [* #i #b >moves_empty cases b % /2/
+ |#a #w1 #Hind #e >moves_cons
+ @iff_trans [||@iff_sym @not_epsilon_sem]
+ @iff_trans [||@move_ok] @Hind
+ ]
+qed.
+
+(************************ pit state ***************************)
+definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉.
+
+let rec occur (S: DeqSet) (i: re S) on i ≝
+ match i with
+ [ z ⇒ [ ]
+ | e ⇒ [ ]
+ | s y ⇒ [y]
+ | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
+ | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
+ | k e ⇒ occur S e].
+
+lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
+ move S a i = pit_pre S i.
+#S #a #i elim i //
+ [#x normalize cases (a==x) normalize // #H @False_ind /2/
+ |#i1 #i2 #Hind1 #Hind2 #H >move_cat
+ >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
+ >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
+ |#i1 #i2 #Hind1 #Hind2 #H >move_plus
+ >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
+ >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
+ |#i #Hind #H >move_star >Hind //
+ ]
+qed.
+
+lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
+#S #a #i elim i //
+ [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 //
+ |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 //
+ |#i #Hind >move_star >Hind //
+ ]
+qed.
+
+lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
+#S #w #i elim w //
+qed.
+
+lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
+ moves S w e = pit_pre S (\fst e).
+#S #w elim w
+ [#e * #H @False_ind @H normalize #a #abs @False_ind /2/
+ |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|\fst e|))))
+ [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a)
+ @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb)
+ [#H2 >(\P H2) // |#H2 @H1 //]
+ |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/
+ ]
+ ]
+qed.
+
+(* bisimulation *)
+definition cofinal ≝ λS.λp:(pre S)×(pre S).
+ \snd (\fst p) = \snd (\snd p).
+
+theorem equiv_sem: ∀S:DeqSet.∀e1,e2:pre S.
+ \sem{e1} =1 \sem{e2} ↔ ∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
+#S #e1 #e2 %
+[#same_sem #w
+ cut (∀b1,b2. iff (b1 = true) (b2 = true) → (b1 = b2))
+ [* * // * #H1 #H2 [@sym_eq @H1 //| @H2 //]]
+ #Hcut @Hcut @iff_trans [|@decidable_sem]
+ @iff_trans [|@same_sem] @iff_sym @decidable_sem
+|#H #w1 @iff_trans [||@decidable_sem] <H @iff_sym @decidable_sem]
+qed.
+
+definition occ ≝ λS.λe1,e2:pre S.
+ unique_append ? (occur S (|\fst e1|)) (occur S (|\fst e2|)).
+
+lemma occ_enough: ∀S.∀e1,e2:pre S.
+(∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
+ →∀w.cofinal ? 〈moves ? w e1,moves ? w e2〉.
+#S #e1 #e2 #H #w
+cases (decidable_sublist S w (occ S e1 e2)) [@H] -H #H
+ >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l1 @H1 //]
+ >to_pit [2: @(not_to_not … H) #H1 #a #memba @sublist_unique_append_l2 @H1 //]
+ //
+qed.
+
+lemma equiv_sem_occ: ∀S.∀e1,e2:pre S.
+(∀w.(sublist S w (occ S e1 e2))→ cofinal ? 〈moves ? w e1,moves ? w e2〉)
+→ \sem{e1}=1\sem{e2}.
+#S #e1 #e2 #H @(proj2 … (equiv_sem …)) @occ_enough #w @H
+qed.
+
+definition sons ≝ λS:DeqSet.λl:list S.λp:(pre S)×(pre S).
+ map ?? (λa.〈move S a (\fst (\fst p)),move S a (\fst (\snd p))〉) l.
+
+lemma memb_sons: ∀S,l.∀p,q:(pre S)×(pre S). memb ? p (sons ? l q) = true →
+ ∃a.(move ? a (\fst (\fst q)) = \fst p ∧
+ move ? a (\fst (\snd q)) = \snd p).
+#S #l elim l [#p #q normalize in ⊢ (%→?); #abs @False_ind /2/]
+#a #tl #Hind #p #q #H cases (orb_true_l … H) -H
+ [#H @(ex_intro … a) >(\P H) /2/ |#H @Hind @H]
+qed.
+
+definition is_bisim ≝ λS:DeqSet.λl:list ?.λalpha:list S.
+ ∀p:(pre S)×(pre S). memb ? p l = true → cofinal ? p ∧ (sublist ? (sons ? alpha p) l).
+
+lemma bisim_to_sem: ∀S:DeqSet.∀l:list ?.∀e1,e2: pre S.
+ is_bisim S l (occ S e1 e2) → memb ? 〈e1,e2〉 l = true → \sem{e1}=1\sem{e2}.
+#S #l #e1 #e2 #Hbisim #Hmemb @equiv_sem_occ
+#w #Hsub @(proj1 … (Hbisim 〈moves S w e1,moves S w e2〉 ?))
+lapply Hsub @(list_elim_left … w) [//]
+#a #w1 #Hind #Hsub >moves_left >moves_left @(proj2 …(Hbisim …(Hind ?)))
+ [#x #Hx @Hsub @memb_append_l1 //
+ |cut (memb S a (occ S e1 e2) = true) [@Hsub @memb_append_l2 //] #occa
+ @(memb_map … occa)
+ ]
+qed.
+
+(* the algorithm *)
+let rec bisim S l n (frontier,visited: list ?) on n ≝
+ match n with
+ [ O ⇒ 〈false,visited〉 (* assert false *)
+ | S m ⇒
+ match frontier with
+ [ nil ⇒ 〈true,visited〉
+ | cons hd tl ⇒
+ if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
+ bisim S l m (unique_append ? (filter ? (λx.notb (memb ? x (hd::visited)))
+ (sons S l hd)) tl) (hd::visited)
+ else 〈false,visited〉
+ ]
+ ].
+
+lemma unfold_bisim: ∀S,l,n.∀frontier,visited: list ?.
+ bisim S l n frontier visited =
+ match n with
+ [ O ⇒ 〈false,visited〉 (* assert false *)
+ | S m ⇒
+ match frontier with
+ [ nil ⇒ 〈true,visited〉
+ | cons hd tl ⇒
+ if beqb (\snd (\fst hd)) (\snd (\snd hd)) then
+ bisim S l m (unique_append ? (filter ? (λx.notb(memb ? x (hd::visited)))
+ (sons S l hd)) tl) (hd::visited)
+ else 〈false,visited〉
+ ]
+ ].
+#S #l #n cases n // qed.
+
+lemma bisim_never: ∀S,l.∀frontier,visited: list ?.
+ bisim S l O frontier visited = 〈false,visited〉.
+#frontier #visited >unfold_bisim //
+qed.
+
+lemma bisim_end: ∀Sig,l,m.∀visited: list ?.
+ bisim Sig l (S m) [] visited = 〈true,visited〉.
+#n #visisted >unfold_bisim //
+qed.
+
+lemma bisim_step_true: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
+beqb (\snd (\fst p)) (\snd (\snd p)) = true →
+ bisim Sig l (S m) (p::frontier) visited =
+ bisim Sig l m (unique_append ? (filter ? (λx.notb(memb ? x (p::visited)))
+ (sons Sig l p)) frontier) (p::visited).
+#Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test //
+qed.
+
+lemma bisim_step_false: ∀Sig,l,m.∀p.∀frontier,visited: list ?.
+beqb (\snd (\fst p)) (\snd (\snd p)) = false →
+ bisim Sig l (S m) (p::frontier) visited = 〈false,visited〉.
+#Sig #l #m #p #frontier #visited #test >unfold_bisim normalize nodelta >test //
+qed.
+
+lemma notb_eq_true_l: ∀b. notb b = true → b = false.
+#b cases b normalize //
+qed.
+
+let rec pitem_enum S (i:re S) on i ≝
+ match i with
+ [ z ⇒ [pz S]
+ | e ⇒ [pe S]
+ | s y ⇒ [ps S y; pp S y]
+ | o i1 i2 ⇒ compose ??? (po S) (pitem_enum S i1) (pitem_enum S i2)
+ | c i1 i2 ⇒ compose ??? (pc S) (pitem_enum S i1) (pitem_enum S i2)
+ | k i ⇒ map ?? (pk S) (pitem_enum S i)
+ ].
+
+lemma pitem_enum_complete : ∀S.∀i:pitem S.
+ memb (DeqItem S) i (pitem_enum S (|i|)) = true.
+#S #i elim i
+ [1,2://
+ |3,4:#c normalize >(\b (refl … c)) //
+ |5,6:#i1 #i2 #Hind1 #Hind2 @(memb_compose (DeqItem S) (DeqItem S)) //
+ |#i #Hind @(memb_map (DeqItem S)) //
+ ]
+qed.
+
+definition pre_enum ≝ λS.λi:re S.
+ compose ??? (λi,b.〈i,b〉) (pitem_enum S i) [true;false].
+
+lemma pre_enum_complete : ∀S.∀e:pre S.
+ memb ? e (pre_enum S (|\fst e|)) = true.
+#S * #i #b @(memb_compose (DeqItem S) DeqBool ? (λi,b.〈i,b〉))
+// cases b normalize //
+qed.
+
+definition space_enum ≝ λS.λi1,i2:re S.
+ compose ??? (λe1,e2.〈e1,e2〉) (pre_enum S i1) (pre_enum S i2).
+
+lemma space_enum_complete : ∀S.∀e1,e2: pre S.
+ memb ? 〈e1,e2〉 (space_enum S (|\fst e1|) (|\fst e2|)) = true.
+#S #e1 #e2 @(memb_compose … (λi,b.〈i,b〉))
+// qed.
+
+definition all_reachable ≝ λS.λe1,e2:pre S.λl: list ?.
+uniqueb ? l = true ∧
+ ∀p. memb ? p l = true →
+ ∃w.(moves S w e1 = \fst p) ∧ (moves S w e2 = \snd p).
+
+definition disjoint ≝ λS:DeqSet.λl1,l2.
+ ∀p:S. memb S p l1 = true → memb S p l2 = false.
+
+lemma bisim_correct: ∀S.∀e1,e2:pre S.\sem{e1}=1\sem{e2} →
+ ∀l,n.∀frontier,visited:list ((pre S)×(pre S)).
+ |space_enum S (|\fst e1|) (|\fst e2|)| < n + |visited|→
+ all_reachable S e1 e2 visited →
+ all_reachable S e1 e2 frontier →
+ disjoint ? frontier visited →
+ \fst (bisim S l n frontier visited) = true.
+#Sig #e1 #e2 #same #l #n elim n
+ [#frontier #visited #abs * #unique #H @False_ind @(absurd … abs)
+ @le_to_not_lt @sublist_length // * #e11 #e21 #membp
+ cut ((|\fst e11| = |\fst e1|) ∧ (|\fst e21| = |\fst e2|))
+ [|* #H1 #H2 <H1 <H2 @space_enum_complete]
+ cases (H … membp) #w * #we1 #we2 <we1 <we2 % >same_kernel_moves //
+ |#m #HI * [#visited #vinv #finv >bisim_end //]
+ #p #front_tl #visited #Hn * #u_visited #r_visited * #u_frontier #r_frontier
+ #disjoint
+ cut (∃w.(moves ? w e1 = \fst p) ∧ (moves ? w e2 = \snd p))
+ [@(r_frontier … (memb_hd … ))] #rp
+ cut (beqb (\snd (\fst p)) (\snd (\snd p)) = true)
+ [cases rp #w * #fstp #sndp <fstp <sndp @(\b ?)
+ @(proj1 … (equiv_sem … )) @same] #ptest
+ >(bisim_step_true … ptest) @HI -HI
+ [<plus_n_Sm //
+ |% [whd in ⊢ (??%?); >(disjoint … (memb_hd …)) whd in ⊢ (??%?); //
+ |#p1 #H (cases (orb_true_l … H)) [#eqp >(\P eqp) // |@r_visited]
+ ]
+ |whd % [@unique_append_unique @(andb_true_r … u_frontier)]
+ @unique_append_elim #q #H
+ [cases (memb_sons … (memb_filter_memb … H)) -H
+ #a * #m1 #m2 cases rp #w1 * #mw1 #mw2 @(ex_intro … (w1@[a]))
+ >moves_left >moves_left >mw1 >mw2 >m1 >m2 % //
+ |@r_frontier @memb_cons //
+ ]
+ |@unique_append_elim #q #H
+ [@injective_notb @(filter_true … H)
+ |cut ((q==p) = false)
+ [|#Hpq whd in ⊢ (??%?); >Hpq @disjoint @memb_cons //]
+ cases (andb_true … u_frontier) #notp #_ @(\bf ?)
+ @(not_to_not … not_eq_true_false) #eqqp <notp <eqqp >H //
+ ]
+ ]
+ ]
+qed.
+
+definition all_true ≝ λS.λl.∀p:(pre S) × (pre S). memb ? p l = true →
+ (beqb (\snd (\fst p)) (\snd (\snd p)) = true).
+
+definition sub_sons ≝ λS,l,l1,l2.∀x:(pre S) × (pre S).
+memb ? x l1 = true → sublist ? (sons ? l x) l2.
+
+lemma bisim_complete:
+ ∀S,l,n.∀frontier,visited,visited_res:list ?.
+ all_true S visited →
+ sub_sons S l visited (frontier@visited) →
+ bisim S l n frontier visited = 〈true,visited_res〉 →
+ is_bisim S visited_res l ∧ sublist ? (frontier@visited) visited_res.
+#S #l #n elim n
+ [#fron #vis #vis_res #_ #_ >bisim_never #H destruct
+ |#m #Hind *
+ [(* case empty frontier *)
+ -Hind #vis #vis_res #allv #H normalize in ⊢ (%→?);
+ #H1 destruct % #p
+ [#membp % [@(\P ?) @allv //| @H //]|#H1 @H1]
+ |#hd cases (true_or_false (beqb (\snd (\fst hd)) (\snd (\snd hd))))
+ [|(* case head of the frontier is non ok (absurd) *)
+ #H #tl #vis #vis_res #allv >(bisim_step_false … H) #_ #H1 destruct]
+ (* frontier = hd:: tl and hd is ok *)
+ #H #tl #visited #visited_res #allv >(bisim_step_true … H)
+ (* new_visited = hd::visited are all ok *)
+ cut (all_true S (hd::visited))
+ [#p #H1 cases (orb_true_l … H1) [#eqp >(\P eqp) @H |@allv]]
+ (* we now exploit the induction hypothesis *)
+ #allh #subH #bisim cases (Hind … allh … bisim) -bisim -Hind
+ [#H1 #H2 % // #p #membp @H2 -H2 cases (memb_append … membp) -membp #membp
+ [cases (orb_true_l … membp) -membp #membp
+ [@memb_append_l2 >(\P membp) @memb_hd
+ |@memb_append_l1 @sublist_unique_append_l2 //
+ ]
+ |@memb_append_l2 @memb_cons //
+ ]
+ |(* the only thing left to prove is the sub_sons invariant *)
+ #x #membx cases (orb_true_l … membx)
+ [(* case x = hd *)
+ #eqhdx <(\P eqhdx) #xa #membxa
+ (* xa is a son of x; we must distinguish the case xa
+ was already visited form the case xa is new *)
+ cases (true_or_false … (memb ? xa (x::visited)))
+ [(* xa visited - trivial *) #membxa @memb_append_l2 //
+ |(* xa new *) #membxa @memb_append_l1 @sublist_unique_append_l1 @memb_filter_l
+ [>membxa //|//]
+ ]
+ |(* case x in visited *)
+ #H1 #xa #membxa cases (memb_append … (subH x … H1 … membxa))
+ [#H2 (cases (orb_true_l … H2))
+ [#H3 @memb_append_l2 <(\P H3) @memb_hd
+ |#H3 @memb_append_l1 @sublist_unique_append_l2 @H3
+ ]
+ |#H2 @memb_append_l2 @memb_cons @H2
+ ]
+ ]
+ ]
+ ]
+qed.
+
+definition equiv ≝ λSig.λre1,re2:re Sig.
+ let e1 ≝ •(blank ? re1) in
+ let e2 ≝ •(blank ? re2) in
+ let n ≝ S (length ? (space_enum Sig (|\fst e1|) (|\fst e2|))) in
+ let sig ≝ (occ Sig e1 e2) in
+ (bisim ? sig n [〈e1,e2〉] []).
+
+theorem euqiv_sem : ∀Sig.∀e1,e2:re Sig.
+ \fst (equiv ? e1 e2) = true ↔ \sem{e1} =1 \sem{e2}.
+#Sig #re1 #re2 %
+ [#H @eqP_trans [|@eqP_sym @re_embedding] @eqP_trans [||@re_embedding]
+ cut (equiv ? re1 re2 = 〈true,\snd (equiv ? re1 re2)〉)
+ [<H //] #Hcut
+ cases (bisim_complete … Hcut)
+ [2,3: #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/]
+ #Hbisim #Hsub @(bisim_to_sem … Hbisim)
+ @Hsub @memb_hd
+ |#H @(bisim_correct ? (•(blank ? re1)) (•(blank ? re2)))
+ [@eqP_trans [|@re_embedding] @eqP_trans [|@H] @eqP_sym @re_embedding
+ |//
+ |% // #p whd in ⊢ ((??%?)→?); #abs @False_ind /2/
+ |% // #p #H >(memb_single … H) @(ex_intro … ϵ) /2/
+ |#p #_ normalize //
+ ]
+ ]
+qed.
+
+lemma eqbnat_true : ∀n,m. eqbnat n m = true ↔ n = m.
+#n #m % [@eqbnat_true_to_eq | @eq_to_eqbnat_true]
+qed.
+
+definition DeqNat ≝ mk_DeqSet nat eqbnat eqbnat_true.
+
+definition a ≝ s DeqNat O.
+definition b ≝ s DeqNat (S O).
+definition c ≝ s DeqNat (S (S O)).
+
+definition exp1 ≝ ((a·b)^*·a).
+definition exp2 ≝ a·(b·a)^*.
+definition exp4 ≝ (b·a)^*.
+
+definition exp6 ≝ a·(a ·a ·b^* + b^* ).
+definition exp7 ≝ a · a^* · b^*.
+
+definition exp8 ≝ a·a·a·a·a·a·a·a·(a^* ).
+definition exp9 ≝ (a·a·a + a·a·a·a·a)^*.
+
+example ex1 : \fst (equiv ? (exp8+exp9) exp9) = true.
+normalize // qed.
+
+
+
+
+
+
+
+++ /dev/null
-include "basics/logic.ma".
-
-(* Given a universe A, we can consider sets of elements of type A by means of their
-characteristic predicates A → Prop. *)
-
-definition set ≝ λA:Type[0].A → Prop.
-
-(* For instance, the empty set is the set defined by an always False predicate *)
-
-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.
-
-(* the singleton set {a} can be defined by the characteristic predicate stating
-equality with a *)
-
-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.
-
-(* Complement, union and intersection are easily defined, by means of logical
-connectives *)
-
-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).
-
-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).
-
-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).
-
-
-
-
-
-
-
- (* The reader could probably wonder what is the difference between Prop and bool.
-In fact, they are quite distinct entities. In type theory, all objects are structured
-in a three levels hierarchy
- t : A : s
-where, t is a term, A is a type, and s is called a sort. Sorts are special, primitive
-constants used to give a type to types. Now, Prop is a primitive sort, while bool is
-just a user defined data type (whose sort his Type[0]). In particular, Prop is the
-sort of Propositions: its elements are logical statements in the usual sense. The important
-point is that statements are inhabited by their proofs: a triple of the kind
- p : Q : Prop
-should be read as p is a proof of the proposition Q.*)
-
-
-
-include "arithmetics/nat.ma".
-include "basics/list.ma".
-
-interpretation "iff" 'iff a b = (iff a b).
-
-record Alpha : Type[1] ≝ { carr :> Type[0];
- eqb: carr → carr → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6;
- 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)
-}.
-
-notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }.
-interpretation "eqb" 'eqb a b = (eqb ? a b).
-
-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.
-
-inductive re (S: \ 5a href="cic:/matita/tutorial/re/Alpha.ind(1,0,0)"\ 6Alpha\ 5/a\ 6) : Type[0] ≝
- z: re S
- | e: re S
- | s: S → re S
- | c: re S → re S → 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 90 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
-coercion c : ∀S:Alpha.∀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 "∅" non associative with precedence 90 for @{ 'empty }.
-interpretation "empty" 'empty = (z ?).
-
-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 ≝
-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 ].
-
-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 ≝
-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 ].
-
-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.
-notation "{}" non associative with precedence 90 f
\ No newline at end of file
projects / helm.git / commitdiff