X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2FMONADS%2Fsperanza.ma;h=e0c6cc77539274d68652f65dfbdaa69398184c97;hb=0e3962b42f821bd7a2b30345a02488958d70fa2f;hp=95d4dda94e966970816621656e07cb82dcde6f84;hpb=ab09955e069a1b7191a1f8189a1d5f78ae014b57;p=helm.git

diff --git a/matita/matita/lib/MONADS/speranza.ma b/matita/matita/lib/MONADS/speranza.ma
index 95d4dda94..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.
@@ -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,21 +105,27 @@ 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.
-
 theorem update_correct2:
  ∀A,v,p1,p2,k,t.
   admissible t (reverse … p2 @ p1) = true →
@@ -127,33 +133,18 @@ theorem update_correct2:
 #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 change with (reverse ? (?::ptl)) in match (rev_append ???); >reverse_cons
-      >associative_append #H normalize >IH //
-
- normalize change with (reverse ? (true::ptl)) in match (rev_append bool ptl [true]);
-[>(reverse_cons … true ptl) | >(reverse_cons … false ptl)]
-[ >(associative_append ??[?]) 
-  
-
-
-theorem update_correct:
+|*: #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 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