1. more bugs fixed

2. correctness proof completed

diff --git a/matita/matita/lib/MONADS/speranza.ma b/matita/matita/lib/MONADS/speranza.ma
index 99f60c26348bad39c190e9187aa62fdc1130370b..e0c6cc77539274d68652f65dfbdaa69398184c97 100644 (file)
--- 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.
@@ -93,7 +93,7 @@ lemma test: update ? 5 (λres,x. 〈res,x〉) [false;false] 〈example,nil …
  normalize //
 qed.
 
-lemma update_fun_correct:
+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 ]
@@ -105,60 +105,46 @@ lemma rev_append_cons:
  #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 >update_fun_correct //
+ [ #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.
 
-lemma admissible_leaf_cons:
- ∀n,p1,dir,p2. admissible (leaf n) (p1@dir::p2) = false.
- #n #p1 elim p1 //
-qed.
-
-(*
-lemma admissible_node_cons:
- ∀x1,x2,p1,p2.
-  admissible (node x1 x2) (rev_append bool p1 [true]@p2)=true →
-   admissible x2 p1=true.
- #x1 #x2 #p1 elim p1 normalize // #dir #tl #IH #p2 cases x2 normalize
- [ #n *)
-
 theorem update_correct2:
  ∀A,v,p1,p2,k,t.
-  admissible t (p2 @ reverse … p1) = true →
+  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 // >rev_append_cons >(?:admissible ? p2 = true) try %
-    <rev_append_cons in H; change with (reverse ??) in match (rev_append ???);
+|*: #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.
     
-
-(* OLD
-theorem update_correct:
+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 elim p1 normalize
-  [ #p2 elim p2 normalize
-    [ #x cases x normalize //
-    | #dir #path #IH #x elim x normalize
-      [ #n cases dir normalize
- 
- 
-  #p2 elim p normalize
-  [ #t elim t normalize //
-  | * normalize 
-    [ #path #IH
-  
-  
-  #path #IH #x elim x normalize
-    [ #v cases res normalize lapply (IH (leaf v)) -IH elim path
-      normalize // * normalize
-      [2: #path' #IH #IH2 @IH
-*)
\ No newline at end of file
+ #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