1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basics/types.ma".
16 include "arithmetics/nat.ma".
17 include "basics/lists/list.ma".
19 inductive t : Type[0] ≝
23 definition path ≝ list bool.
25 definition tp ≝ t × path.
27 let rec setleaf_fun (v:nat) (x:t) (p:path) on p : t × bool ≝
31 [ leaf _ ⇒ 〈leaf v,true〉
32 | node x1 x2 ⇒ 〈node x1 x2,false〉 ]
35 [ leaf n ⇒ 〈leaf n,false〉
38 let 〈x2',res〉 ≝ setleaf_fun v x2 tl in
41 let 〈x1',res〉 ≝ setleaf_fun v x1 tl in
42 〈node x1' x2, res〉 ]].
44 let rec admissible (x:t) (p:path) on p : bool ≝
51 if b then admissible x2 tl else admissible x1 tl ]].
53 definition left: ∀A:Type[0]. (bool → tp → A) → tp → A ≝
57 k (admissible t p') 〈t,p'〉.
59 definition right: ∀A:Type[0]. (bool → tp → A) → tp → A ≝
63 k (admissible t p') 〈t,p'〉.
65 definition reset: ∀A:Type[0]. (tp → A) → tp → A ≝
70 definition setleaf: ∀A:Type[0]. nat → (bool → tp → A) → tp → A ≝
73 let 〈t',res〉 ≝ setleaf_fun v t (reverse … p) in
76 (*****************************)
78 let rec update (A:Type[0]) (v:nat) (k: bool → tp → A) (p:path) on p:
82 [ nil ⇒ setleaf … v (λres. reset … (k res))
85 right … (λres1.update … v (λres2. k (res1 ∧ res2)) tl)
87 left … (λres1. update … v (λres2.k (res1 ∧ res2)) tl) ].
90 node (node (leaf 0) (leaf 1)) (node (leaf 2) (leaf 3)).
92 lemma test: update ? 5 (λres,x. 〈res,x〉) [false;false] 〈example,nil …〉 = ?.
96 lemma update_fun_correct:
98 admissible t p = false → setleaf_fun v t p = 〈t,false〉.
99 #v #p elim p normalize [#t #abs destruct ]
100 #hd #tl #IH * normalize // #x1 #x2 cases hd normalize #H >IH //
103 lemma rev_append_cons:
104 ∀A,x,l1,l2. rev_append A (x::l1) [] @ l2 = rev_append A l1 []@x::l2.
105 #A #x #l1 #l2 <(associative_append ?? [?]) <reverse_cons //
108 theorem update_correct1:
110 admissible t (reverse … p2 @ p1) = false →
111 update A v k p1 〈t,p2〉 = k false 〈t,[]〉.
112 #A #v #p1 elim p1 normalize
113 [ #p2 #k #t #H >update_fun_correct //
114 | #hd #tl #IH #p2 #k #t cases hd normalize nodelta
115 cases t normalize [1,3:#n|2,4:#x1 #x2] #H >IH // cases (admissible ??) //
118 lemma admissible_leaf_cons:
119 ∀n,p1,dir,p2. admissible (leaf n) (p1@dir::p2) = false.
124 lemma admissible_node_cons:
126 admissible (node x1 x2) (rev_append bool p1 [true]@p2)=true →
127 admissible x2 p1=true.
128 #x1 #x2 #p1 elim p1 normalize // #dir #tl #IH #p2 cases x2 normalize
131 theorem update_correct2:
133 admissible t (p2 @ reverse … p1) = true →
134 update A v k p1 〈t,p2〉 = update … v k [] 〈t,reverse … p1 @ p2〉.
135 #A #v #p1 elim p1 normalize //
136 #dir #ptl #IH #p2 #k #t cases dir normalize nodelta cases t normalize nodelta
137 [1,3: #n >admissible_leaf_cons #abs destruct
138 |*: #x1 #x2 #H >IH // >rev_append_cons >(?:admissible ? p2 = true) try %
139 <rev_append_cons in H; change with (reverse ??) in match (rev_append ???);
143 theorem update_correct:
145 let 〈t',res〉 ≝ setleaf_fun v t (reverse … p1 @ p2) in
146 update ? v (λres,x.〈res,x〉) p2 〈t,p1〉 = 〈res,〈t',nil …〉〉.
147 #v #p1 elim p1 normalize
148 [ #p2 elim p2 normalize
149 [ #x cases x normalize //
150 | #dir #path #IH #x elim x normalize
151 [ #n cases dir normalize
155 [ #t elim t normalize //
160 #path #IH #x elim x normalize
161 [ #v cases res normalize lapply (IH (leaf v)) -IH elim path
162 normalize // * normalize
163 [2: #path' #IH #IH2 @IH