From f6753c1245b9824178b23f5d4d80bedc231b1107 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 2 Dec 2013 21:00:51 +0000 Subject: [PATCH] 1. more bugs fixed 2. correctness proof completed --- matita/matita/lib/MONADS/speranza.ma | 68 +++++++++++----------------- 1 file changed, 27 insertions(+), 41 deletions(-) diff --git a/matita/matita/lib/MONADS/speranza.ma b/matita/matita/lib/MONADS/speranza.ma index 99f60c263..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,60 +105,46 @@ lemma rev_append_cons: #A #x #l1 #l2 <(associative_append ?? [?]) 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 % - 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 -- 2.39.2