X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2FMONADS%2Fsperanza.ma;h=e0c6cc77539274d68652f65dfbdaa69398184c97;hb=1f30483032488ac4df2310b68fe8146e05524fec;hp=db364d2eccf5aa5cd9662938dd54b520882e89e7;hpb=08141cb42e6caa637b062a645996f90fc4c8c166;p=helm.git

diff --git a/matita/matita/lib/MONADS/speranza.ma b/matita/matita/lib/MONADS/speranza.ma
index db364d2ec..e0c6cc775 100644
--- a/matita/matita/lib/MONADS/speranza.ma
+++ b/matita/matita/lib/MONADS/speranza.ma
@@ -54,13 +54,13 @@ definition left: ∀A:Type[0]. (bool → tp → A) → tp → A ≝
  λA,k,x.
   let 〈t,p〉 ≝ x in
   let p' ≝ false::p in
-   k (admissible t p') 〈t,p'〉.
+   k (admissible t (reverse … p')) 〈t,p'〉.
 
 definition right: ∀A:Type[0]. (bool → tp → A) → tp → A ≝
  λA,k,x.
   let 〈t,p〉 ≝ x in
   let p' ≝ true::p in
-   k (admissible t p') 〈t,p'〉.
+   k (admissible t (reverse … p')) 〈t,p'〉.
 
 definition reset: ∀A:Type[0]. (tp → A) → tp → A ≝
  λA,k,x.
@@ -70,7 +70,7 @@ definition reset: ∀A:Type[0]. (tp → A) → tp → A ≝
 definition setleaf: ∀A:Type[0]. nat → (bool → tp → A) → tp → A ≝
  λA,v,k,x.
   let 〈t,p〉 ≝ x in
-  let 〈t',res〉 ≝ setleaf_fun v t p in
+  let 〈t',res〉 ≝ setleaf_fun v t (reverse … p) in
    k res 〈t',p〉.
 
 (*****************************)
@@ -91,4 +91,60 @@ definition example ≝
 
 lemma test: update ? 5 (λres,x. 〈res,x〉) [false;false] 〈example,nil …〉 = ?.
  normalize //
+qed.
+
+lemma setleaf_fun_correct:
+ ∀v,p,t.
+  admissible t p = false → setleaf_fun v t p = 〈t,false〉.
+ #v #p elim p normalize [#t #abs destruct ]
+ #hd #tl #IH * normalize // #x1 #x2 cases hd normalize #H >IH //
+qed.
+
+lemma rev_append_cons:
+ ∀A,x,l1,l2. rev_append A (x::l1) [] @ l2 = rev_append A l1 []@x::l2.
+ #A #x #l1 #l2 <(associative_append ?? [?]) <reverse_cons //
+qed.
+
+lemma admissible_leaf_cons:
+ ∀n,p1,dir,p2. admissible (leaf n) (p1@dir::p2) = false.
+ #n #p1 elim p1 //
+qed.
+
+lemma admissible_append_true:
+ ∀p1,p2,t. admissible t (p1@p2)=true → admissible t p1=true.
+ #p1 elim p1 normalize // #hd #tl #IH #p2 * normalize //
+ #x1 #x2 cases hd normalize @IH
+qed.
+
+theorem update_correct1:
+ ∀A,v,p1,p2,k,t.
+  admissible t (reverse … p2 @ p1) = false →
+   update A v k p1 〈t,p2〉 = k false 〈t,[]〉.
+ #A #v #p1 elim p1 normalize
+ [ #p2 #k #t #H >setleaf_fun_correct //
+ | #hd #tl #IH #p2 #k #t cases hd normalize nodelta
+  cases t normalize [1,3:#n|2,4:#x1 #x2] #H >IH // cases (admissible ??) //
+qed.
+
+theorem update_correct2:
+ ∀A,v,p1,p2,k,t.
+  admissible t (reverse … p2 @ p1) = true →
+   update A v k p1 〈t,p2〉 = update … v k [] 〈t,reverse … p1 @ p2〉.
+#A #v #p1 elim p1 normalize //
+#dir #ptl #IH #p2 #k #t cases dir normalize nodelta cases t normalize nodelta
+[1,3: #n >admissible_leaf_cons #abs destruct
+|*: #x1 #x2 #H >IH
+    [2,4: normalize >rev_append_def >associative_append //
+    |*: >(rev_append_def … ptl [?]) >associative_append
+        >(?:admissible ?? = true) // @(admissible_append_true … ptl) // ]]
+qed.
+    
+theorem final_update_correct:
+ ∀v,p1,p2,t.
+  let 〈t',res〉 ≝ setleaf_fun v t (reverse … p1 @ p2) in 
+  update ? v (λres,x.〈res,x〉) p2 〈t,p1〉 = 〈res,〈t',nil …〉〉.
+ #v #p1 #p2 #t @pair_elim #t' #res #EQ inversion (admissible t (reverse … p1 @ p2))
+ [ #H >update_correct2 // whd in ⊢ (??%?);
+   >(reverse_append ? (reverse ? p2) p1) >reverse_reverse >EQ %
+ | #H >update_correct1 // >setleaf_fun_correct in EQ; // ]
 qed.
\ No newline at end of file