--- /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 "re/re.ma".
+
+let rec move (S: Alpha) (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:Alpha.∀x:S.∀i1,i2:pitem S.
+ move S x (i1 + i2) = (move ? x i1) ⊕ (move ? x i2).
+// qed.
+
+lemma move_cat: ∀S:Alpha.∀x:S.∀i1,i2:pitem S.
+ move S x (i1 · i2) = (move ? x i1) ⊙ (move ? x i2).
+// qed.
+
+lemma move_star: ∀S:Alpha.∀x:S.∀i:pitem S.
+ move S x i^* = (move ? x i)^⊛.
+// qed.
+
+lemma fst_eq : ∀A,B.∀a:A.∀b:B. \fst 〈a,b〉 = a.
+// qed.
+
+lemma snd_eq : ∀A,B.∀a:A.∀b:B. \snd 〈a,b〉 = b.
+// qed.
+
+definition pmove ≝ λS:Alpha.λx:S.λe:pre S. move ? x (\fst e).
+
+lemma pmove_def : ∀S:Alpha.∀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.
+
+axiom same_kernel: ∀S:Alpha.∀a:S.∀i:pitem S.
+ |\fst (move ? a i)| = |i|.
+(* #S #a #i elim i //
+ [#i1 #i2 >move_cat
+ cases (move S a i1) #i11 #b1 >fst_eq #IH1
+ cases (move S a i2) #i21 #b2 >fst_eq #IH2
+ normalize *)
+
+axiom iff_trans:∀A,B,C. A ↔ B → B ↔ C → A ↔ C.
+axiom iff_or_l: ∀A,B,C. A ↔ B → C ∨ A ↔ C ∨ B.
+axiom iff_or_r: ∀A,B,C. A ↔ B → A ∨ C ↔ B ∨ C.
+
+axiom epsilon_in_star: ∀S.∀A:word S → Prop. A^* [ ].
+
+theorem move_ok:
+ ∀S:Alpha.∀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
+ [>(proj1 … (eqb_true …) H) %
+ [* // #bot @False_ind //| #H1 destruct /2/]
+ |% [#bot @False_ind //
+ | #H1 destruct @(absurd ((a==a)=true))
+ [>(proj2 … (eqb_true …) (refl …)) // | /2/]
+ ]
+ ]
+ |#i1 #i2 #HI1 #HI2 #w >(sem_cat S i1 i2) >move_cat
+ @iff_trans[|@sem_odot] >same_kernel >sem_cat_w
+ @iff_trans[||@(iff_or_l … (HI2 w))] @iff_or_r %
+ [* #w1 * #w2 * * #eqw #w1in #w2in @(ex_intro … (a::w1))
+ @(ex_intro … w2) % // % normalize // cases (HI1 w1) /2/
+ |* #w1 * #w2 * cases w1
+ [* #_ #H @False_ind /2/
+ |#x #w3 * #eqaw normalize in eqaw; destruct #w3in #w2in
+ @(ex_intro … w3) @(ex_intro … w2) % // % // cases (HI1 w3) /2/
+ ]
+ ]
+ |#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 %
+ [* #w1 * #w2 * * #eqw #w1in #w2in
+ @(ex_intro … (a::w1)) @(ex_intro … w2) % // % normalize //
+ cases (HI1 w1 ) /2/
+ |* #w1 * #w2 * cases w1
+ [* #_ #H @False_ind /2/
+ |#x #w3 * #eqaw normalize in eqaw; destruct #w3in #w2in
+ @(ex_intro … w3) @(ex_intro … w2) % // % // cases (HI1 w3) /2/
+ ]
+ ]
+ ]
+qed.
+
+notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
+let rec moves (S : Alpha) w e on w : pre S ≝
+ match w with
+ [ nil ⇒ e
+ | cons x w' ⇒ w' ↦* (move S x (\fst e))].
+
+lemma moves_empty: ∀S:Alpha.∀e:pre S.
+ moves ? [ ] e = e.
+// qed.
+
+lemma moves_cons: ∀S:Alpha.∀a:S.∀w.∀e:pre S.
+ moves ? (a::w) e = moves ? w (move S a (\fst e)).
+// qed.
+
+lemma not_epsilon_sem: ∀S:Alpha.∀a:S.∀w: word S. ∀e:pre S.
+ iff ((a::w) ∈ e) ((a::w) ∈ \fst e).
+#S #a #w * #i #b >fst_eq cases b normalize
+ [% /2/ * // #H destruct |% normalize /2/]
+qed.
+
+lemma same_kernel_moves: ∀S:Alpha.∀w.∀e:pre S.
+ |\fst (moves ? w e)| = |\fst e|.
+#S #w elim w //
+qed.
+
+axiom iff_not: ∀A,B. (iff A B) →(iff (¬A) (¬B)).
+
+axiom iff_sym: ∀A,B. (iff A B) →(iff B A).
+
+theorem decidable_sem: ∀S:Alpha.∀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.
+
+lemma not_true_to_false: ∀b.b≠true → b =false.
+#b * cases b // #H @False_ind /2/
+qed.
+
+theorem equiv_sem: ∀S:Alpha.∀e1,e2:pre S.
+ iff (\sem{e1} =1 \sem{e2}) (∀w.\snd (moves ? w e1) = \snd (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.
+
+axiom moves_left : ∀S,a,w,e.
+ moves S (w@[a]) e = move S a (\fst (moves S w e)).
+
+definition in_moves ≝ λS:Alpha.λw.λe:pre S. \snd(w ↦* e).
+
+coinductive equiv (S:Alpha) : pre S → pre S → Prop ≝
+ mk_equiv:
+ ∀e1,e2: pre S.
+ \snd e1 = \snd e2 →
+ (∀x. equiv S (move ? x (\fst e1)) (move ? x (\fst e2))) →
+ equiv S e1 e2.
+
+definition beqb ≝ λb1,b2.
+ match b1 with
+ [ true ⇒ b2
+ | false ⇒ notb b2
+ ].
+
+lemma beqb_ok: ∀b1,b2. iff (beqb b1 b2 = true) (b1 = b2).
+#b1 #b2 cases b1 cases b2 normalize /2/
+qed.
+
+definition Bin ≝ mk_Alpha bool beqb beqb_ok.
+
+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]
+ ].
+
+axiom beqitem_ok: ∀S,i1,i2. iff (beqitem S i1 i2 = true) (i1 = i2).
+
+definition BinItem ≝
+ mk_Alpha (pitem Bin) (beqitem Bin) (beqitem_ok Bin).
+
+definition beqpre ≝ λS:Alpha.λe1,e2:pre S.
+ beqitem S (\fst e1) (\fst e2) ∧ beqb (\snd e1) (\snd e2).
+
+definition beqpairs ≝ λS:Alpha.λp1,p2:(pre S)×(pre S).
+ beqpre S (\fst p1) (\fst p2) ∧ beqpre S (\snd p1) (\snd p2).
+
+axiom beqpairs_ok: ∀S,p1,p2. iff (beqpairs S p1 p2 = true) (p1 = p2).
+
+definition space ≝ λS.mk_Alpha ((pre S)×(pre S)) (beqpairs S) (beqpairs_ok S).
+
+let rec memb (S:Alpha) (x:S) (l: list S) on l ≝
+ match l with
+ [ nil ⇒ false
+ | cons a tl ⇒ (a == x) || memb S x tl
+ ].
+
+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 memb_cons: ∀S,a,b,l.
+ memb S a l = true → memb S a (b::l) = true.
+#S #a #b #l normalize cases (b==a) normalize //
+qed.
+
+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 [/2/] #b #tl #Hind
+#l2 cases (b==a) normalize /2/
+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 (b==a) 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 (b==a) normalize /2/
+qed.
+
+let rec uniqueb (S:Alpha) l on l : bool ≝
+ match l with
+ [ nil ⇒ true
+ | cons a tl ⇒ notb (memb S a tl) ∧ uniqueb S tl
+ ].
+
+definition sons ≝ λp:space Bin.
+ [〈move Bin true (\fst (\fst p)), move Bin true (\fst (\snd p))〉;
+ 〈move Bin false (\fst (\fst p)), move Bin false (\fst (\snd p))〉
+ ].
+
+axiom memb_sons: ∀p,q. memb (space Bin) p (sons q) = true →
+ ∃a.(move ? a (\fst (\fst q)) = \fst p ∧
+ move ? a (\fst (\snd q)) = \snd p).
+
+(*
+let rec test_sons (l:list (space Bin)) ≝
+ match l with
+ [ nil ⇒ true
+ | cons hd tl ⇒
+ beqb (\snd (\fst hd)) (\snd (\snd hd)) ∧ test_sons tl
+ ]. *)
+
+let rec unique_append (S:Alpha) (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 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.
+
+let rec bisim (n:nat) (frontier,visited: list (space Bin)) ≝
+ 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 m (unique_append ? (filter ? (λx.notb (memb ? x (hd::visited)))
+ (sons hd)) tl) (hd::visited)
+ else 〈false,visited〉
+ ]
+ ].
+
+lemma unfold_bisim: ∀n.∀frontier,visited: list (space Bin).
+ bisim 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 m (unique_append ? (filter ? (λx.notb(memb ? x (hd::visited))) (sons hd)) tl) (hd::visited)
+ else 〈false,visited〉
+ ]
+ ].
+#n cases n // qed.
+
+lemma bisim_never: ∀frontier,visited: list (space Bin).
+ bisim O frontier visited = 〈false,visited〉.
+#frontier #visited >unfold_bisim //
+qed.
+
+lemma bisim_end: ∀m.∀visited: list (space Bin).
+ bisim (S m) [] visited = 〈true,visited〉.
+#n #visisted >unfold_bisim //
+qed.
+
+lemma bisim_step_true: ∀m.∀p.∀frontier,visited: list (space Bin).
+beqb (\snd (\fst p)) (\snd (\snd p)) = true →
+ bisim (S m) (p::frontier) visited =
+ bisim m (unique_append ? (filter ? (λx.notb(memb (space Bin) x (p::visited))) (sons p)) frontier) (p::visited).
+#m #p #frontier #visited #test >unfold_bisim normalize nodelta >test //
+qed.
+
+lemma bisim_step_false: ∀m.∀p.∀frontier,visited: list (space Bin).
+beqb (\snd (\fst p)) (\snd (\snd p)) = false →
+ bisim (S m) (p::frontier) visited = 〈false,visited〉.
+#m #p #frontier #visited #test >unfold_bisim normalize nodelta >test //
+qed.
+
+definition visited_inv ≝ λe1,e2:pre Bin.λvisited: list (space Bin).
+uniqueb ? visited = true ∧
+ ∀p. memb ? p visited = true →
+ (∃w.(moves Bin w e1 = \fst p) ∧ (moves Bin w e2 = \snd p)) ∧
+ (beqb (\snd (\fst p)) (\snd (\snd p)) = true).
+
+definition frontier_inv ≝ λfrontier,visited: list (space Bin).
+uniqueb ? frontier = true ∧
+∀p. memb ? p frontier = true →
+ memb ? p visited = false ∧
+ ∃p1.((memb ? p1 visited = true) ∧
+ (∃a. move ? a (\fst (\fst p1)) = \fst p ∧
+ move ? a (\fst (\snd p1)) = \snd p)).
+
+definition orb_true_r1: ∀b1,b2:bool.
+ b1 = true → (b1 ∨ b2) = true.
+#b1 #b2 #H >H // qed.
+
+definition orb_true_r2: ∀b1,b2:bool.
+ b2 = true → (b1 ∨ b2) = true.
+#b1 #b2 #H >H cases b1 // qed.
+
+definition orb_true_l: ∀b1,b2:bool.
+ (b1 ∨ b2) = true → (b1 = true) ∨ (b2 = true).
+* normalize /2/ qed.
+
+definition andb_true_l1: ∀b1,b2:bool.
+ (b1 ∧ b2) = true → (b1 = true).
+#b1 #b2 cases b1 normalize //.
+qed.
+
+definition andb_true_l2: ∀b1,b2:bool.
+ (b1 ∧ b2) = true → (b2 = true).
+#b1 #b2 cases b1 cases b2 normalize //.
+qed.
+
+definition andb_true_l: ∀b1,b2:bool.
+ (b1 ∧ b2) = true → (b1 = true) ∧ (b2 = true).
+#b1 #b2 cases b1 normalize #H [>H /2/ |@False_ind /2/].
+qed.
+
+definition andb_true_r: ∀b1,b2:bool.
+ (b1 = true) ∧ (b2 = true) → (b1 ∧ b2) = true.
+#b1 #b2 cases b1 normalize * //
+qed.
+
+lemma notb_eq_true_l: ∀b. notb b = true → b = false.
+#b cases b normalize //
+qed.
+
+lemma notb_eq_true_r: ∀b. b = false → notb b = true.
+#b cases b normalize //
+qed.
+
+lemma notb_eq_false_l:∀b. notb b = false → b = true.
+#b cases b normalize //
+qed.
+
+lemma notb_eq_false_r:∀b. b = true → notb b = false.
+#b cases b normalize //
+qed.
+
+
+axiom 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 normalize cases (f b) normalize *)
+
+axiom memb_filter_memb: ∀S,f,a,l.
+ memb S a (filter S f l) = true → memb S a l = true.
+
+axiom unique_append_elim: ∀S:Alpha.∀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.
+
+axiom not_memb_to_not_eq: ∀S,a,b,l.
+ memb S a l = false → memb S b l = true → a==b = false.
+
+include "arithmetics/exp.ma".
+
+let rec pos S (i:re S) on i ≝
+ match i with
+ [ z ⇒ 0
+ | e ⇒ 0
+ | s y ⇒ 1
+ | o i1 i2 ⇒ pos S i1 + pos S i2
+ | c i1 i2 ⇒ pos S i1 + pos S i2
+ | k i ⇒ pos S i
+ ].
+
+definition sublist ≝
+ λS,l1,l2.∀a. memb S a l1 = true → memb S a l2 = true.
+
+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)
+ >(proj1 … (eqb_true …) eqba) //
+ |#mem_tl cases (Hind mem_tl) #l1 * #l2 #eqtl
+ @(ex_intro … (b::l1)) @(ex_intro … l2) >eqtl //
+ ]
+qed.
+
+lemma length_append: ∀A.∀l1,l2:list A.
+ |l1@l2| = |l1|+|l2|.
+#A #l1 elim l1 // normalize /2/
+qed.
+
+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_l2 … 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)
+ [#eqax @False_ind cases (andb_true_l … unique)
+ >(proj1 … (eqb_true …) eqax) >membx normalize /2/
+ |#membxl4 @memb_append_l2 //
+ ]
+ ]
+qed.
+
+axiom memb_filter: ∀S,f,l,x. memb S x (filter ? f l) = true →
+memb S x l = true ∧ (f x = true).
+
+axiom memb_filter_l: ∀S,f,l,x. memb S x l = true → (f x = true) →
+memb S x (filter ? f l) = true.
+
+axiom sublist_unique_append_l1:
+ ∀S,l1,l2. sublist S l1 (unique_append S l1 l2).
+
+axiom sublist_unique_append_l2:
+ ∀S,l1,l2. sublist S l2 (unique_append S l1 l2).
+
+definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
+ foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
+
+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)
+ ].
+
+axiom 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.
+(* #S #op #a1 #a2 #l1 elim l1 [normalize //]
+#x #tl #Hind #l2 elim l2 [#_ normalize #abs @False_ind /2/]
+#y #tl2 #Hind2 #membx #memby normalize *)
+
+axiom pitem_enum_complete: ∀i: pitem Bin.
+ memb BinItem i (pitem_enum ? (forget ? i)) = true.
+(*
+#i elim i
+ [//
+ |//
+ |* //
+ |* //
+ |#i1 #i2 #Hind1 #Hind2 @memb_compose //
+ |#i1 #i2 #Hind1 #Hind2 @memb_compose //
+ |
+*)
+
+definition pre_enum ≝ λS.λi:re S.
+ compose ??? (λi,b.〈i,b〉) (pitem_enum S i) [true;false].
+
+definition space_enum ≝ λS.λi1,i2:re S.
+ compose ??? (λe1,e2.〈e1,e2〉) (pre_enum S i1) (pre_enum S i1).
+
+axiom space_enum_complete : ∀S.∀e1,e2: pre S.
+ memb (space S) 〈e1,e2〉 (space_enum S (|\fst e1|) (|\fst e2|)) = true.
+
+lemma bisim_ok1: ∀e1,e2:pre Bin.\sem{e1}=1\sem{e2} →
+ ∀n.∀frontier,visited:list (space Bin).
+ |space_enum Bin (|\fst e1|) (|\fst e2|)| < n + |visited|→
+ visited_inv e1 e2 visited → frontier_inv frontier visited →
+ \fst (bisim n frontier visited) = true.
+#e1 #e2 #same #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 * >fst_eq >snd_eq #we1 #we2 #_
+ <we1 <we2 % //
+ |#m #HI * [#visited #vinv #finv >bisim_end //]
+ #p #front_tl #visited #Hn * #u_visited #vinv * #u_frontier #finv
+ cases (finv p (memb_hd …)) #Hp * #p2 * #visited_p2
+ * #a * #movea1 #movea2
+ cut (∃w.(moves Bin w e1 = \fst p) ∧ (moves Bin w e2 = \snd p))
+ [cases (vinv … visited_p2) -vinv * #w1 * #mw1 #mw2 #_
+ @(ex_intro … (w1@[a])) /2/]
+ -movea2 -movea1 -a -visited_p2 -p2 #reachp
+ cut (beqb (\snd (\fst p)) (\snd (\snd p)) = true)
+ [cases reachp #w * #move_e1 #move_e2 <move_e1 <move_e2
+ @(proj2 … (beqb_ok … )) @(proj1 … (equiv_sem … )) @same
+ |#ptest >(bisim_step_true … ptest) @HI -HI
+ [<plus_n_Sm //
+ |% [@andb_true_r % [@notb_eq_false_l // | // ]]
+ #p1 #H (cases (orb_true_l … H))
+ [#eqp <(proj1 … (eqb_true (space Bin) ? p1) eqp) % //
+ |#visited_p1 @(vinv … visited_p1)
+ ]
+ |whd % [@unique_append_unique @(andb_true_l2 … u_frontier)]
+ @unique_append_elim #q #H
+ [%
+ [@notb_eq_true_l @(filter_true … H)
+ |@(ex_intro … p) % //
+ @(memb_sons … (memb_filter_memb … H))
+ ]
+ |cases (finv q ?) [|@memb_cons //]
+ #nvq * #p1 * #Hp1 #reach %
+ [cut ((p==q) = false) [|#Hpq whd in ⊢ (??%?); >Hpq @nvq]
+ cases (andb_true_l … u_frontier) #notp #_
+ @(not_memb_to_not_eq … H) @notb_eq_true_l @notp
+ |cases (proj2 … (finv q ?))
+ [#p1 * #Hp1 #reach @(ex_intro … p1) % // @memb_cons //
+ |@memb_cons //
+ ]
+ ]
+ ]
+ ]
+ ]
+ ]
+qed.
+
+definition all_true ≝ λl.∀p. memb (space Bin) p l = true →
+ (beqb (\snd (\fst p)) (\snd (\snd p)) = true).
+
+definition sub_sons ≝ λl1,l2.∀x,a.
+memb (space Bin) x l1 = true →
+ memb (space Bin) 〈move ? a (\fst (\fst x)), move ? a (\fst (\snd x))〉 l2 = true.
+
+lemma reachable_bisim:
+ ∀n.∀frontier,visited,visited_res:list (space Bin).
+ all_true visited →
+ sub_sons visited (frontier@visited) →
+ bisim n frontier visited = 〈true,visited_res〉 →
+ (sub_sons visited_res visited_res ∧
+ sublist ? visited visited_res ∧
+ all_true visited_res).
+#n elim n
+ [#fron #vis #vis_res #_ #_ >bisim_never #H destruct
+ |#m #Hind *
+ [-Hind #vis #vis_res #allv #H normalize in ⊢ (%→?);
+ #H1 destruct % // % // #p /2/
+ |#hd cases (true_or_false (beqb (\snd (\fst hd)) (\snd (\snd hd))))
+ [|#H #tl #vis #vis_res #allv >(bisim_step_false … H) #_ #H1 destruct]
+ #H #tl #visited #visited_res #allv >(bisim_step_true … H)
+ cut (all_true (hd::visited))
+ [#p #H cases (orb_true_l … H)
+ [#eqp <(proj1 … (eqb_true …) eqp) // |@allv]]
+ #allh #subH #bisim cases (Hind … allh … bisim) -Hind
+ [* #H1 #H2 #H3 % // % // #p #H4 @H2 @memb_cons //]
+ #x #a #membx
+ cases (orb_true_l … membx)
+ [#eqhdx >(proj1 … (eqb_true …) eqhdx)
+ letin xa ≝ 〈move Bin a (\fst (\fst x)), move Bin a (\fst (\snd x))〉
+ cases (true_or_false … (memb (space Bin) xa (x::visited)))
+ [#membxa @memb_append_l2 //
+ |#membxa @memb_append_l1 @sublist_unique_append_l1 @memb_filter_l
+ [whd in ⊢ (??(??%%)?); cases a [@memb_hd |@memb_cons @memb_hd]
+ |>membxa //
+ ]
+ ]
+ |#H1 letin xa ≝ 〈move Bin a (\fst (\fst x)), move Bin a (\fst (\snd x))〉
+ cases (memb_append … (subH x a H1))
+ [#H2 (cases (orb_true_l … H2))
+ [#H3 @memb_append_l2 >(proj1 … (eqb_true …) H3) @memb_hd
+ |#H3 @memb_append_l1 @sublist_unique_append_l2 @H3
+ ]
+ |#H2 @memb_append_l2 @memb_cons @H2
+ ]
+ ]
+ ]
+ ]
+qed.
+
+axiom bisim_char: ∀e1,e2:pre Bin.
+(∀w.(beqb (\snd (moves ? w e1)) (\snd (moves ? w e2))) = true) →
+\sem{e1}=1\sem{e2}.
+
+lemma bisim_ok2: ∀e1,e2:pre Bin.
+ (beqb (\snd e1) (\snd e2) = true) →
+ ∀n.∀frontier:list (space Bin).
+ sub_sons [〈e1,e2〉] (frontier@[〈e1,e2〉]) →
+ \fst (bisim n frontier [〈e1,e2〉]) = true → \sem{e1}=1\sem{e2}.
+#e1 #e2 #Hnil #n #frontier #init #bisim_true
+letin visited_res ≝ (\snd (bisim n frontier [〈e1,e2〉]))
+cut (bisim n frontier [〈e1,e2〉] = 〈true,visited_res〉)
+ [<bisim_true <eq_pair_fst_snd //] #H
+cut (all_true [〈e1,e2〉])
+ [#p #Hp cases (orb_true_l … Hp)
+ [#eqp <(proj1 … (eqb_true …) eqp) //
+ | whd in ⊢ ((??%?)→?); #abs @False_ind /2/
+ ]] #allH
+cases (reachable_bisim … allH init … H) * #H1 #H2 #H3
+cut (∀w,p.memb (space Bin) p visited_res = true →
+ memb (space Bin) 〈moves ? w (\fst p), moves ? w (\snd p)〉 visited_res = true)
+ [#w elim w [* //]
+ #a #w1 #Hind * #e11 #e21 #visp >fst_eq >snd_eq >moves_cons >moves_cons
+ @(Hind 〈?,?〉) @(H1 〈?,?〉) //] #all_reach
+@bisim_char #w @(H3 〈?,?〉) @(all_reach w 〈?,?〉) @H2 //
+qed.
+
+definition tt ≝ ps Bin true.
+definition ff ≝ ps Bin false.
+definition eps ≝ pe Bin.
+definition exp1 ≝ (ff + tt · ff).
+definition exp2 ≝ ff · (eps + tt).
+
+definition exp3 ≝ move Bin true (\fst (•exp1)).
+definition exp4 ≝ move Bin true (\fst (•exp2)).
+definition exp5 ≝ move Bin false (\fst (•exp1)).
+definition exp6 ≝ move Bin false (\fst (•exp2)).
+
+example comp1 : bequiv 15 (•exp1) (•exp2) [ ] = false .
+normalize //
+qed.
+
+
-
-
(**************************************************************************)
(* ___ *)
(* ||M|| *)
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.
+
notation "a || b" left associative with precedence 30 for @{'orb $a $b}.
interpretation "orb" 'orb a b = (orb 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 = (pz ?).
(* notation < "|term 19 e|" non associative with precedence 70 for @{'forget $e}.*)
interpretation "forget" 'norm a = (forget ? a).
-
let rec in_pl (S : Alpha) (r : pitem S) on r : word S → Prop ≝
match r with
[ pz ⇒ {}
\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.
qed.
lemma true_to_epsilon : ∀S.∀e:pre S. \snd e = true → [ ] ∈ e.
-#S * #i #b #btrue normalize in btrue >btrue %2 //
+#S * #i #b #btrue normalize in btrue; >btrue %2 //
qed.
definition lo ≝ λS:Alpha.λa,b:pre S.〈\fst a + \fst b,\snd a || \snd b〉.
definition pre_concat_r ≝ λS:Alpha.λi:pitem S.λe:pre S.
match e with [ pair i1 b ⇒ 〈i · i1, b〉].
-notation "i â\96¸ e" left associative with precedence 60 for @{'trir $i $e}.
-interpretation "pre_concat_r" 'trir i e = (pre_concat_r ? i e).
+notation "i â\97\82 e" left associative with precedence 60 for @{'ltrif $i $e}.
+interpretation "pre_concat_r" 'ltrif i e = (pre_concat_r ? i e).
definition eq_f1 ≝ λS.λa,b:word S → Prop.∀w.a w ↔ b w.
notation "A =1 B" non associative with precedence 45 for @{'eq_f1 $A $B}.
qed.
lemma sem_pre_concat_r : ∀S,i.∀e:pre S.
- \sem{i â\96¸ e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}.
+ \sem{i â\97\82 e} =1 \sem{i} · \sem{|\fst e|} ∪ \sem{e}.
#S #i * #i1 #b1 cases b1 /2/
>sem_pre_true >sem_cat >sem_pre_true /2/
qed.
definition lc ≝ λS:Alpha.λbcast:∀S:Alpha.pitem S → pre S.λe1:pre S.λi2:pitem S.
match e1 with
[ pair i1 b1 ⇒ match b1 with
- [ true â\87\92 (i1 â\96¸ (bcast ? i2))
+ [ true â\87\92 (i1 â\97\82 (bcast ? i2))
| false ⇒ 〈i1 · i2,false〉
]
].
-definition lift ≝ λf:∀S.pitem S →pre S.λS.λe:pre S.
+definition lift ≝ λS.λf:pitem S →pre S.λe:pre S.
match e with
- [ pair i b ⇒ 〈\fst (f S i), \snd (f S i) || b〉].
+ [ pair i b ⇒ 〈\fst (f i), \snd (f i) || b〉].
-notation < "a ⊙ b" left associative with precedence 60 for @{'lc $op $a $b}.
+notation "a ▸ b" left associative with precedence 60 for @{'lc eclose $a $b}.
interpretation "lc" 'lc op a b = (lc ? op a b).
-notation > "a ⊙ b" left associative with precedence 60 for @{'lc eclose $a $b}.
definition lk ≝ λS:Alpha.λbcast:∀S:Alpha.∀E:pitem S.pre S.λe:pre S.
match e with
[ pair i1 b1 ⇒
match b1 with
[true ⇒ 〈(\fst (bcast ? i1))^*, true〉
- |false ⇒ 〈i1^*,true〉
+ |false ⇒ 〈i1^*,false〉
]
- ].
+ ].
+
+(*
+lemma oplus_tt : ∀S: Alpha.∀i1,i2:pitem S.
+ 〈i1,true〉 ⊕ 〈i2,true〉 = 〈i1 + i2,true〉.
+// qed.
+
+lemma oplus_tf : ∀S: Alpha.∀i1,i2:pitem S.
+ 〈i1,true〉 ⊕ 〈i2,false〉 = 〈i1 + i2,true〉.
+// qed.
+
+lemma oplus_ft : ∀S: Alpha.∀i1,i2:pitem S.
+ 〈i1,false〉 ⊕ 〈i2,true〉 = 〈i1 + i2,true〉.
+// qed.
+
+lemma oplus_ff : ∀S: Alpha.∀i1,i2:pitem S.
+ 〈i1,false〉 ⊕ 〈i2,false〉 = 〈i1 + i2,false〉.
+// qed. *)
(* 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 "a^⊛" non associative with precedence 90 for @{'lk eclose $a}.
-notation > "•" non associative with precedence 60 for @{eclose ?}.
+notation "•" non associative with precedence 60 for @{eclose ?}.
let rec eclose (S: Alpha) (i: pitem S) on i : pre S ≝
match i with
| ps x ⇒ 〈 `.x, false〉
| pp x ⇒ 〈 `.x, false 〉
| po i1 i2 ⇒ •i1 ⊕ •i2
- | pc i1 i2 ⇒ •i1 ⊙ i2
- | pk i ⇒ 〈(\fst(•i))^*,true〉].
-
+ | 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).
// qed.
lemma eclose_dot: ∀S:Alpha.∀i1,i2:pitem S.
- â\80¢(i1 · i2) = â\80¢i1 â\8a\99 i2.
+ â\80¢(i1 · i2) = â\80¢i1 â\96¸ i2.
// qed.
lemma eclose_star: ∀S:Alpha.∀i:pitem S.
•i^* = 〈(\fst(•i))^*,true〉.
// qed.
-definition reclose ≝ lift eclose.
+definition reclose ≝ λS. lift S (eclose S).
interpretation "reclose" 'eclose x = (reclose ? x).
lemma epsilon_or : ∀S:Alpha.∀b1,b2. epsilon S (b1 || b2) =1 ϵ b1 ∪ ϵ b2.
#S a b; napply extP; #w; @; *; nnormalize; /2/; nqed.*)
(* theorem 16: 2 *)
-(*
-lemma oplus_cup : ∀S:Alpha.∀e1,e2:pre S.
- \sem{e1 ⊕ e2} =1 \sem{e1} ∪ \sem{e2}.
-#S * #i1 #b1 * #i2 #b2 #w %
-[normalize * [* /3/ | cases b1 cases b2 normalize /3/ ]
-|normalize * * /3/ cases b1 cases b2 normalize /3/ *]
-qed. *)
+lemma sem_oplus: ∀S:Alpha.∀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.
- â\8c©i1,trueâ\8cª â\8a\99 i2 = i1 â\96¸ (•i2).
+ â\8c©i1,trueâ\8cª â\96¸ i2 = i1 â\97\82 (•i2).
// qed.
lemma odot_true_bis :
∀S.∀i1,i2:pitem S.
- â\8c©i1,trueâ\8cª â\8a\99 i2 = 〈i1 · \fst (•i2), \snd (•i2)〉.
+ â\8c©i1,trueâ\8cª â\96¸ i2 = 〈i1 · \fst (•i2), \snd (•i2)〉.
#S #i1 #i2 normalize cases (•i2) // qed.
lemma odot_false:
∀S.∀i1,i2:pitem S.
- â\8c©i1,falseâ\8cª â\8a\99 i2 = 〈i1 · i2, false〉.
+ â\8c©i1,falseâ\8cª â\96¸ i2 = 〈i1 · i2, false〉.
// qed.
lemma LcatE : ∀S.∀e1,e2:pitem S.
lemma erase_star : ∀S.∀i:pitem S.|i^*| = |i|^*.
// qed.
-(*
definition substract := λS.λp,q:word S → Prop.λw.p w ∧ ¬ q w.
interpretation "substract" 'minus a b = (substract ? a b).
-nlemma cup_sub: ∀S.∀a,b:word S → Prop. ¬ (a []) → a ∪ (b - {[]}) = (a ∪ b) - {[]}.
+(* nlemma cup_sub: ∀S.∀a,b:word S → Prop. ¬ (a []) → a ∪ (b - {[]}) = (a ∪ b) - {[]}.
#S a b c; napply extP; #w; nnormalize; @; *; /4/; *; /4/; nqed.
nlemma sub0 : ∀S.∀a:word S → Prop. a - {} = a.
axiom union_comm : ∀S.∀A,B:word S →Prop.
A ∪ B =1 B ∪ A.
+
+axiom union_idemp: ∀S.∀A:word S →Prop.
+ A ∪ A =1 A.
+
+axiom cat_ext_l: ∀S.∀A,B,C:word S →Prop.
+ A =1 C → A · B =1 C · B.
+
+axiom cat_ext_r: ∀S.∀A,B,C:word S →Prop.
+ B =1 C → A · B =1 A · C.
lemma distr_cat_r: ∀S.∀A,B,C:word S →Prop.
(A ∪ B) · C =1 A · C ∪ B · C.
[* #w1 * #w2 * * #eqw * /6/ |* * #w1 * #w2 * * /6/]
qed.
+axiom fix_star: ∀S.∀A:word S → Prop.
+ A^* =1 A · A^* ∪ { [ ] }.
+
+axiom star_epsilon: ∀S:Alpha.∀A:word S → Prop.
+ A^* ∪ { [ ] } =1 A^*.
+
+lemma sem_eclose_star: ∀S:Alpha.∀i:pitem S.
+ \sem{〈i^*,true〉} =1 \sem{〈i,false〉}·\sem{|i|}^* ∪ { [ ] }.
+/2/ qed.
+
+(*
+lemma sem_eclose_star: ∀S:Alpha.∀i:pitem S.
+ \sem{〈i^*,true〉} =1 \sem{〈i,true〉}·\sem{|i|}^* ∪ { [ ] }.
+/2/ qed.
+
+#S #i #b cases b
+ [>sem_pre_true >sem_star
+ |/2/
+ ] *)
+
(* this kind of results are pretty bad for automation;
better not index them *)
lemma epsilon_cat_r: ∀S.∀A:word S →Prop.
(* theorem 16: 1 → 3 *)
lemma odot_dot_aux : ∀S.∀e1:pre S.∀i2:pitem S.
\sem{•i2} =1 \sem{i2} ∪ \sem{|i2|} →
- \sem{e1 â\8a\99 i2} =1 \sem{e1} · \sem{|i2|} ∪ \sem{i2}.
+ \sem{e1 â\96¸ 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 @(ext_eq_trans … (sem_pre_concat_r …))
- >erase_bull
- @ext_eq_trans
- [|@(union_ext_r … H)
- |@ext_eq_trans
- [|@union_ext_r [|@union_comm ]
- |@ext_eq_trans (* /3 by eq_ext_sym, union_ext_l/; *)
- [|@eq_ext_sym @union_assoc
- |/3/
- (*
- by eq_ext_sym, union_ext_l; @union_ext_l /3
- /3/ ext_eq_trans /2/
- /3 width=5 by eq_ext_sym, union_ext_r/ *)
- ]
- ]
- ]
- ]
+ >erase_bull @ext_eq_trans [|@(union_ext_r … H)]
+ @ext_eq_trans [|@union_ext_r [|@union_comm ]]
+ @ext_eq_trans [|@eq_ext_sym @union_assoc ] /3/
+ ]
qed.
-(* nlemma sub_dot_star :
- ∀S.∀X:word S → Prop.∀b. (X - ϵ b) · X^* ∪ {[]} = X^*.
-#S X b; napply extP; #w; @;
-##[ *; ##[##2: nnormalize; #defw; nrewrite < defw; @[]; @; //]
- *; #w1; *; #w2; *; *; #defw sube; *; #lw; *; #flx cj;
- @ (w1 :: lw); nrewrite < defw; nrewrite < flx; @; //;
- @; //; napply (subW … sube);
-##| *; #wl; *; #defw Pwl; nrewrite < defw; nelim wl in Pwl; ##[ #_; @2; //]
- #w' wl' IH; *; #Pw' IHp; nlapply (IH IHp); *;
- ##[ *; #w1; *; #w2; *; *; #defwl' H1 H2;
- @; ncases b in H1; #H1;
- ##[##2: nrewrite > (sub0…); @w'; @(w1@w2);
- nrewrite > (associative_append ? w' w1 w2);
- nrewrite > defwl'; @; ##[@;//] @(wl'); @; //;
- ##| ncases w' in Pw';
- ##[ #ne; @w1; @w2; nrewrite > defwl'; @; //; @; //;
- ##| #x xs Px; @(x::xs); @(w1@w2);
- nrewrite > (defwl'); @; ##[@; //; @; //; @; nnormalize; #; ndestruct]
- @wl'; @; //; ##] ##]
- ##| #wlnil; nchange in match (flatten ? (w'::wl')) with (w' @ flatten ? wl');
- nrewrite < (wlnil); nrewrite > (append_nil…); ncases b;
- ##[ ncases w' in Pw'; /2/; #x xs Pxs; @; @(x::xs); @([]);
- nrewrite > (append_nil…); @; ##[ @; //;@; //; nnormalize; @; #; ndestruct]
- @[]; @; //;
- ##| @; @w'; @[]; nrewrite > (append_nil…); @; ##[##2: @[]; @; //]
- @; //; @; //; @; *;##]##]##]
-nqed. *)
+axiom star_fix :
+ ∀S.∀X:word S → Prop.(X - {[ ]}) · X^* ∪ {[ ]} =1 X^*.
+
+axiom sem_fst: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
+
+axiom sem_fst_aux: ∀S.∀e:pre S.∀i:pitem S.∀A.
+ \sem{e} =1 \sem{i} ∪ A → \sem{\fst e} =1 \sem{i} ∪ (A - {[ ]}).
(* theorem 16: 1 *)
-alias symbol "pc" (instance 13) = "cat lang".
-alias symbol "in_pl" (instance 23) = "in_pl".
-alias symbol "in_pl" (instance 5) = "in_pl".
-alias symbol "eclose" (instance 21) = "eclose".
-ntheorem bull_cup : ∀S:Alpha. ∀e:pitem S. 𝐋\p (•e) = 𝐋\p e ∪ 𝐋 |e|.
-#S e; nelim e; //;
- ##[ #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl, or_intror;
- ##| #a; napply extP; #w; nnormalize; @; *; /3/ by or_introl; *;
- ##| #e1 e2 IH1 IH2;
- nchange in ⊢ (??(??(%))?) with (•e1 ⊙ 〈e2,false〉);
- nrewrite > (odot_dot_aux S (•e1) 〈e2,false〉 IH2);
- nrewrite > (IH1 …); nrewrite > (cup_dotD …);
- nrewrite > (cupA …); nrewrite > (cupC ?? (𝐋\p ?) …);
- nchange in match (𝐋\p 〈?,?〉) with (𝐋\p e2 ∪ {}); nrewrite > (cup0 …);
- nrewrite < (erase_dot …); nrewrite < (cupA …); //;
- ##| #e1 e2 IH1 IH2;
- nchange in match (•(?+?)) with (•e1 ⊕ •e2); nrewrite > (oplus_cup …);
- nrewrite > (IH1 …); nrewrite > (IH2 …); nrewrite > (cupA …);
- nrewrite > (cupC ? (𝐋\p e2)…);nrewrite < (cupA ??? (𝐋\p e2)…);
- nrewrite > (cupC ?? (𝐋\p e2)…); nrewrite < (cupA …);
- nrewrite < (erase_plus …); //.
- ##| #e; nletin e' ≝ (\fst (•e)); nletin b' ≝ (\snd (•e)); #IH;
- nchange in match (𝐋\p ?) with (𝐋\p 〈e'^*,true〉);
- nchange in match (𝐋\p ?) with (𝐋\p (e'^* ) ∪ {[ ]});
- nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 |e'|^* );
- nrewrite > (erase_bull…e);
- nrewrite > (erase_star …);
- nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 |e| - ϵ b')); ##[##2:
- nchange in IH : (??%?) with (𝐋\p e' ∪ ϵ b'); ncases b' in IH;
- ##[ #IH; nrewrite > (cup_sub…); //; nrewrite < IH;
- nrewrite < (cup_sub…); //; nrewrite > (subK…); nrewrite > (cup0…);//;
- ##| nrewrite > (sub0 …); #IH; nrewrite < IH; nrewrite > (cup0 …);//; ##]##]
- nrewrite > (cup_dotD…); nrewrite > (cupA…);
- nrewrite > (?: ((?·?)∪{[]} = 𝐋 |e^*|)); //;
- nchange in match (𝐋 |e^*|) with ((𝐋 |e|)^* ); napply sub_dot_star;##]
- nqed.
+theorem sem_bull: ∀S:Alpha. ∀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
+ @ext_eq_trans [|@odot_dot_aux //] >sem_cat
+ @ext_eq_trans
+ [|@union_ext_l
+ [|@ext_eq_trans [|@(cat_ext_l … IH1)] @distr_cat_r]]
+ @ext_eq_trans [|@union_assoc]
+ @ext_eq_trans [||@eq_ext_sym @union_assoc]
+ @union_ext_r //
+ |#i1 #i2 #IH1 #IH2 >eclose_plus
+ @ext_eq_trans [|@sem_oplus] >sem_plus >erase_plus
+ @ext_eq_trans [|@(union_ext_r … IH2)]
+ @ext_eq_trans [|@eq_ext_sym @union_assoc]
+ @ext_eq_trans [||@union_assoc] @union_ext_l
+ @ext_eq_trans [||@eq_ext_sym @union_assoc]
+ @ext_eq_trans [||@union_ext_r [|@union_comm]]
+ @ext_eq_trans [||@union_assoc] /3/
+ |#i #H >sem_pre_true >sem_star >erase_bull >sem_star
+ @ext_eq_trans [|@union_ext_l [|@cat_ext_l [|@sem_fst_aux //]]]
+ @ext_eq_trans [|@union_ext_l [|@distr_cat_r]]
+ @ext_eq_trans [|@union_assoc] @union_ext_r >erase_star @star_fix
+ ]
+qed.
+
+definition lifted_cat ≝ λS:Alpha.λe:pre S.
+ lift S (lc S eclose e).
-(* theorem 16: 3 *)
-nlemma odot_dot:
- ∀S.∀e1,e2: pre S. 𝐋\p (e1 ⊙ e2) = 𝐋\p e1 · 𝐋 |\fst e2| ∪ 𝐋\p e2.
-#S e1 e2; napply odot_dot_aux; napply (bull_cup S (\fst e2)); nqed.
+notation "e1 ⊙ e2" left associative with precedence 70 for @{'odot $e1 $e2}.
+interpretation "lifted cat" 'odot e1 e2 = (lifted_cat ? e1 e2).
+
+lemma sem_odot_true: ∀S:Alpha.∀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 @ext_eq_trans [||@eq_ext_sym @union_assoc]
+ @union_ext_r /2/
+ |/2/
+ ]
+qed.
+
+lemma eq_odot_false: ∀S:Alpha.∀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
+ @ext_eq_trans [|@sem_odot_true]
+ @ext_eq_trans [||@union_assoc] @union_ext_l @odot_dot_aux //
+ |>sem_pre_false >eq_odot_false @odot_dot_aux //
+ ]
+qed.
+
+(*
nlemma dot_star_epsilon : ∀S.∀e:re S.𝐋 e · 𝐋 e^* ∪ {[]} = 𝐋 e^*.
#S e; napply extP; #w; nnormalize; @;
##[ *; ##[##2: #H; nrewrite < H; @[]; /3/] *; #w1; *; #w2;
#S A C b nbA defC; nrewrite < defC; napply extP; #w; @;
##[ #Aw; /3/| *; *; //; #H nH; ncases nH; #abs; nlapply (abs H); *]
nqed.
+*)
(* theorem 16: 4 *)
-nlemma star_dot: ∀S.∀e:pre S. 𝐋\p (e^⊛) = 𝐋\p e · (𝐋 |\fst e|)^*.
-#S p; ncases p; #e b; ncases b;
-##[ nchange in match (〈e,true〉^⊛) with 〈?,?〉;
- nletin e' ≝ (\fst (•e)); nletin b' ≝ (\snd (•e));
- nchange in ⊢ (??%?) with (?∪?);
- nchange in ⊢ (??(??%?)?) with (𝐋\p e' · 𝐋 |e'|^* );
- nrewrite > (?: 𝐋\p e' = 𝐋\p e ∪ (𝐋 |e| - ϵ b' )); ##[##2:
- nlapply (bull_cup ? e); #bc;
- nchange in match (𝐋\p (•e)) in bc with (?∪?);
- nchange in match b' in bc with b';
- ncases b' in bc; ##[##2: nrewrite > (cup0…); nrewrite > (sub0…); //]
- nrewrite > (cup_sub…); ##[napply rcanc_sing] //;##]
- nrewrite > (cup_dotD…); nrewrite > (cupA…);nrewrite > (erase_bull…);
- nrewrite > (sub_dot_star…);
- nchange in match (𝐋\p 〈?,?〉) with (?∪?);
- nrewrite > (cup_dotD…); nrewrite > (epsilon_dot…); //;
-##| nwhd in match (〈e,false〉^⊛); nchange in match (𝐋\p 〈?,?〉) with (?∪?);
- nrewrite > (cup0…);
- nchange in ⊢ (??%?) with (𝐋\p e · 𝐋 |e|^* );
- nrewrite < (cup0 ? (𝐋\p e)); //;##]
-nqed.
-
+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
+ @ext_eq_trans [|@union_ext_l [|@cat_ext_l [|@sem_fst_aux //]]]
+ @ext_eq_trans [|@union_ext_l [|@distr_cat_r]]
+ @ext_eq_trans [||@eq_ext_sym @distr_cat_r]
+ @ext_eq_trans [|@union_assoc] @union_ext_r
+ @ext_eq_trans [||@eq_ext_sym @epsilon_cat_l] @star_fix
+ |>sem_pre_false >sem_pre_false >sem_star /2/
+ ]
+qed.
+
+(*
nlet rec pre_of_re (S : Alpha) (e : re S) on e : pitem S ≝
match e with
[ z ⇒ pz ?
nrewrite > defsnde; #H;
nlapply (Pext ??? H [ ] ?); ##[ @2; //] *; //;
-STOP
-
-notation > "\move term 90 x term 90 E"
-non associative with precedence 60 for @{move ? $x $E}.
-nlet rec move (S: Alpha) (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)^⊛ ].
-notation < "\move\shy x\shy E" non associative with precedence 60 for @{'move $x $E}.
-notation > "\move term 90 x term 90 E" non associative with precedence 60 for @{'move $x $E}.
-interpretation "move" 'move x E = (move ? x E).
-
-ndefinition rmove ≝ λS:Alpha.λx:S.λe:pre S. \move x (\fst e).
-interpretation "rmove" 'move x E = (rmove ? x E).
-
-nlemma XXz : ∀S:Alpha.∀w:word S. w ∈ ∅ → False.
-#S w abs; ninversion abs; #; ndestruct;
-nqed.
-
-
-nlemma XXe : ∀S:Alpha.∀w:word S. w .∈ ϵ → False.
-#S w abs; ninversion abs; #; ndestruct;
-nqed.
-
-nlemma XXze : ∀S:Alpha.∀w:word S. w .∈ (∅ · ϵ) → False.
-#S w abs; ninversion abs; #; ndestruct; /2/ by XXz,XXe;
-nqed.
-
-
-naxiom in_move_cat:
- ∀S.∀w:word S.∀x.∀E1,E2:pitem S. w .∈ \move x (E1 · E2) →
- (∃w1.∃w2. w = w1@w2 ∧ w1 .∈ \move x E1 ∧ w2 ∈ .|E2|) ∨ w .∈ \move x E2.
-#S w x e1 e2 H; nchange in H with (w .∈ \move x e1 ⊙ \move x e2);
-ncases e1 in H; ncases e2;
-##[##1: *; ##[*; nnormalize; #; ndestruct]
- #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
- nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze;
-##|##2: *; ##[*; nnormalize; #; ndestruct]
- #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
- nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz,XXze;
-##| #r; *; ##[ *; nnormalize; #; ndestruct]
- #H; ninversion H; ##[##1,4,5,6: nnormalize; #; ndestruct]
- ##[##2: nnormalize; #; ndestruct; @2; @2; //.##]
- nnormalize; #; ndestruct; ncases (?:False); /2/ by XXz;
-##| #y; *; ##[ *; nnormalize; #defw defx; ndestruct; @2; @1; /2/ by conj;##]
- #H; ninversion H; nnormalize; #; ndestruct;
- ##[ncases (?:False); /2/ by XXz] /3/ by or_intror;
-##| #r1 r2; *; ##[ *; #defw]
- ...
-nqed.
-
-ntheorem move_ok:
- ∀S:Alpha.∀E:pre S.∀a,w.w .∈ \move a E ↔ (a :: w) .∈ E.
-#S E; ncases E; #r b; nelim r;
-##[##1,2: #a w; @;
- ##[##1,3: nnormalize; *; ##[##1,3: *; #; ndestruct; ##| #abs; ncases (XXz … abs); ##]
- #H; ninversion H; #; ndestruct;
- ##|##*:nnormalize; *; ##[##1,3: *; #; ndestruct; ##| #H1; ncases (XXz … H1); ##]
- #H; ninversion H; #; ndestruct;##]
-##|#a c w; @; nnormalize; ##[*; ##[*; #; ndestruct; ##] #abs; ninversion abs; #; ndestruct;##]
- *; ##[##2: #abs; ninversion abs; #; ndestruct; ##] *; #; ndestruct;
-##|#a c w; @; nnormalize;
- ##[ *; ##[ *; #defw; nrewrite > defw; #ca; @2; nrewrite > (eqb_t … ca); @; ##]
- #H; ninversion H; #; ndestruct;
- ##| *; ##[ *; #; ndestruct; ##] #H; ninversion H; ##[##2,3,4,5,6: #; ndestruct]
- #d defw defa; ndestruct; @1; @; //; nrewrite > (eqb_true S d d); //. ##]
-##|#r1 r2 H1 H2 a w; @;
- ##[ #H; ncases (in_move_cat … H);
- ##[ *; #w1; *; #w2; *; *; #defw w1m w2m;
- ncases (H1 a w1); #H1w1; #_; nlapply (H1w1 w1m); #good;
- nrewrite > defw; @2; @2 (a::w1); //; ncases good; ##[ *; #; ndestruct] //.
- ##|
- ...
-##|
-##|
-##]
-nqed.
-
-
-notation > "x ↦* E" non associative with precedence 60 for @{move_star ? $x $E}.
-nlet rec move_star (S : decidable) w E on w : bool × (pre S) ≝
- match w with
- [ nil ⇒ E
- | cons x w' ⇒ w' ↦* (x ↦ \snd E)].
-
-ndefinition in_moves ≝ λS:decidable.λw.λE:bool × (pre S). \fst(w ↦* E).
-
-ncoinductive equiv (S:decidable) : bool × (pre S) → bool × (pre S) → Prop ≝
- mk_equiv:
- ∀E1,E2: bool × (pre S).
- \fst E1 = \fst E2 →
- (∀x. equiv S (x ↦ \snd E1) (x ↦ \snd E2)) →
- equiv S E1 E2.
-
-ndefinition NAT: decidable.
- @ nat eqb; /2/.
-nqed.
-
-include "hints_declaration.ma".
-
-alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
-unification hint 0 ≔ ; X ≟ NAT ⊢ carr X ≡ nat.
-
-ninductive unit: Type[0] ≝ I: unit.
-
-nlet corec foo_nop (b: bool):
- equiv ?
- 〈 b, pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0))) 〉
- 〈 b, pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0) 〉 ≝ ?.
- @; //; #x; ncases x
- [ nnormalize in ⊢ (??%%); napply (foo_nop false)
- | #y; ncases y
- [ nnormalize in ⊢ (??%%); napply (foo_nop false)
- | #w; nnormalize in ⊢ (??%%); napply (foo_nop false) ]##]
-nqed.
-
-(*
-nlet corec foo (a: unit):
- equiv NAT
- (eclose NAT (pc ? (ps ? 0) (pk ? (pc ? (ps ? 1) (ps ? 0)))))
- (eclose NAT (pc ? (pk ? (pc ? (ps ? 0) (ps ? 1))) (ps ? 0)))
-≝ ?.
- @;
- ##[ nnormalize; //
- ##| #x; ncases x
- [ nnormalize in ⊢ (??%%);
- nnormalize in foo: (? → ??%%);
- @; //; #y; ncases y
- [ nnormalize in ⊢ (??%%); napply foo_nop
- | #y; ncases y
- [ nnormalize in ⊢ (??%%);
-
- ##| #z; nnormalize in ⊢ (??%%); napply foo_nop ]##]
- ##| #y; nnormalize in ⊢ (??%%); napply foo_nop
- ##]
-nqed.
*)
-ndefinition test1 : pre ? ≝ ❨ `0 | `1 ❩^* `0.
-ndefinition test2 : pre ? ≝ ❨ (`0`1)^* `0 | (`0`1)^* `1 ❩.
-ndefinition test3 : pre ? ≝ (`0 (`0`1)^* `1)^*.
-
-nlemma foo: in_moves ? [0;0;1;0;1;1] (ɛ test3) = true.
- nnormalize in match test3;
- nnormalize;
-//;
-nqed.
-
-(**********************************************************)
-
-ninductive der (S: Type[0]) (a: S) : re S → re S → CProp[0] ≝
- der_z: der S a (z S) (z S)
- | der_e: der S a (e S) (z S)
- | der_s1: der S a (s S a) (e ?)
- | der_s2: ∀b. a ≠ b → der S a (s S b) (z S)
- | der_c1: ∀e1,e2,e1',e2'. in_l S [] e1 → der S a e1 e1' → der S a e2 e2' →
- der S a (c ? e1 e2) (o ? (c ? e1' e2) e2')
- | der_c2: ∀e1,e2,e1'. Not (in_l S [] e1) → der S a e1 e1' →
- der S a (c ? e1 e2) (c ? e1' e2)
- | der_o: ∀e1,e2,e1',e2'. der S a e1 e1' → der S a e2 e2' →
- der S a (o ? e1 e2) (o ? e1' e2').
-
-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; ncases p; #P; #H; nassumption.
-nqed.
-
-nlemma append1: ∀A.∀a:A.∀l. [a] @ l = a::l. //. nqed.
-
-naxiom in_l1: ∀S,r1,r2,w. in_l S [ ] r1 → in_l S w r2 → in_l S w (c S r1 r2).
-(* #S; #r1; #r2; #w; nelim r1
- [ #K; ninversion K
- | #H1; #H2; napply (in_c ? []); //
- | (* tutti casi assurdi *) *)
-
-ninductive in_l' (S: Type[0]) : word S → re S → CProp[0] ≝
- in_l_empty1: ∀E.in_l S [] E → in_l' S [] E
- | in_l_cons: ∀a,w,e,e'. in_l' S w e' → der S a e e' → in_l' S (a::w) e.
-
-ncoinductive eq_re (S: Type[0]) : re S → re S → CProp[0] ≝
- mk_eq_re: ∀E1,E2.
- (in_l S [] E1 → in_l S [] E2) →
- (in_l S [] E2 → in_l S [] E1) →
- (∀a,E1',E2'. der S a E1 E1' → der S a E2 E2' → eq_re S E1' E2') →
- eq_re S E1 E2.
-
-(* serve il lemma dopo? *)
-ntheorem eq_re_is_eq: ∀S.∀E1,E2. eq_re S E1 E2 → ∀w. in_l ? w E1 → in_l ? w E2.
- #S; #E1; #E2; #H1; #w; #H2; nelim H2 in E2 H1 ⊢ %
- [ #r; #K (* ok *)
- | #a; #w; #R1; #R2; #K1; #K2; #K3; #R3; #K4; @2 R2; //; ncases K4;
-
-(* IL VICEVERSA NON VALE *)
-naxiom in_l_to_in_l: ∀S,w,E. in_l' S w E → in_l S w E.
-(* #S; #w; #E; #H; nelim H
- [ //
- | #a; #w'; #r; #r'; #H1; (* e si cade qua sotto! *)
- ]
-nqed. *)
-
-ntheorem der1: ∀S,a,e,e',w. der S a e e' → in_l S w e' → in_l S (a::w) e.
- #S; #a; #E; #E'; #w; #H; nelim H
- [##1,2: #H1; ninversion H1
- [##1,8: #_; #K; (* non va ndestruct K; *) ncases (?:False); (* perche' due goal?*) /2/
- |##2,9: #X; #Y; #K; ncases (?:False); /2/
- |##3,10: #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
- |##4,11: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
- |##5,12: #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
- |##6,13: #x; #y; #K; ncases (?:False); /2/
- |##7,14: #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/]
-##| #H1; ninversion H1
- [ //
- | #X; #Y; #K; ncases (?:False); /2/
- | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
- | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
- | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
- | #x; #y; #K; ncases (?:False); /2/
- | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
-##| #H1; #H2; #H3; ninversion H3
- [ #_; #K; ncases (?:False); /2/
- | #X; #Y; #K; ncases (?:False); /2/
- | #x; #y; #z; #w; #a; #b; #c; #d; #e; #K; ncases (?:False); /2/
- | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
- | #x; #y; #z; #w; #a; #b; #K; ncases (?:False); /2/
- | #x; #y; #K; ncases (?:False); /2/
- | #x; #y; #z; #w; #a; #b; #c; #d; #K; ncases (?:False); /2/ ]
-##| #r1; #r2; #r1'; #r2'; #H1; #H2; #H3; #H4; #H5; #H6;
-
-lemma
\ No newline at end of file
projects / helm.git / commitdiff