matita/matita/lib/MONADS/speranza.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "basics/types.ma".
  16 include "arithmetics/nat.ma".
  17 include "basics/lists/list.ma".
  18
  19 inductive t : Type[0] ≝
  20    leaf: nat → t
  21  | node: t → t → t.
  22
  23 definition path ≝ list bool.
  24
  25 definition tp ≝ t × path.
  26
  27 let rec setleaf_fun (v:nat) (x:t) (p:path) on p : t × bool ≝
  28  match p with
  29  [ nil ⇒
  30     match x with
  31     [ leaf _ ⇒ 〈leaf v,true〉
  32     | node x1 x2 ⇒ 〈node x1 x2,false〉 ]
  33  | cons b tl ⇒
  34     match x with
  35     [ leaf n ⇒ 〈leaf n,false〉
  36     | node x1 x2 ⇒
  37        if b then
  38         let 〈x2',res〉 ≝ setleaf_fun v x2 tl in
  39          〈node x1 x2', res〉
  40        else
  41         let 〈x1',res〉 ≝ setleaf_fun v x1 tl in
  42          〈node x1' x2, res〉 ]].
  43
  44 let rec admissible (x:t) (p:path) on p : bool ≝
  45  match p with
  46  [ nil ⇒ true
  47  | cons b tl ⇒
  48     match x with
  49     [ leaf _ ⇒ false
  50     | node x1 x2 ⇒
  51        if b then admissible x2 tl else admissible x1 tl ]].
  52
  53 definition left: ∀A:Type[0]. (bool → tp → A) → tp → A ≝
  54  λA,k,x.
  55   let 〈t,p〉 ≝ x in
  56   let p' ≝ false::p in
  57    k (admissible t (reverse … p')) 〈t,p'〉.
  58
  59 definition right: ∀A:Type[0]. (bool → tp → A) → tp → A ≝
  60  λA,k,x.
  61   let 〈t,p〉 ≝ x in
  62   let p' ≝ true::p in
  63    k (admissible t (reverse … p')) 〈t,p'〉.
  64
  65 definition reset: ∀A:Type[0]. (tp → A) → tp → A ≝
  66  λA,k,x.
  67   let 〈t,p〉 ≝ x in
  68    k 〈t,nil …〉.
  69
  70 definition setleaf: ∀A:Type[0]. nat → (bool → tp → A) → tp → A ≝
  71  λA,v,k,x.
  72   let 〈t,p〉 ≝ x in
  73   let 〈t',res〉 ≝ setleaf_fun v t (reverse … p) in
  74    k res 〈t',p〉.
  75
  76 (*****************************)
  77
  78 let rec update (A:Type[0]) (v:nat) (k: bool → tp → A) (p:path) on p:
  79  tp → A
  80 ≝
  81  match p with
  82  [ nil ⇒ setleaf … v (λres. reset … (k res))
  83  | cons b tl ⇒
  84     if b then
  85      right … (λres1.update … v (λres2. k (res1 ∧ res2)) tl)
  86     else
  87      left … (λres1. update … v (λres2.k (res1 ∧ res2)) tl) ].
  88
  89 definition example ≝
  90  node (node (leaf 0) (leaf 1)) (node (leaf 2) (leaf 3)).
  91
  92 lemma test: update ? 5 (λres,x. 〈res,x〉) [false;false] 〈example,nil …〉 = ?.
  93  normalize //
  94 qed.
  95
  96 lemma setleaf_fun_correct:
  97  ∀v,p,t.
  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 //
 101 qed.
 102
 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 //
 106 qed.
 107
 108 lemma admissible_leaf_cons:
 109  ∀n,p1,dir,p2. admissible (leaf n) (p1@dir::p2) = false.
 110  #n #p1 elim p1 //
 111 qed.
 112
 113 lemma admissible_append_true:
 114  ∀p1,p2,t. admissible t (p1@p2)=true → admissible t p1=true.
 115  #p1 elim p1 normalize // #hd #tl #IH #p2 * normalize //
 116  #x1 #x2 cases hd normalize @IH
 117 qed.
 118
 119 theorem update_correct1:
 120  ∀A,v,p1,p2,k,t.
 121   admissible t (reverse … p2 @ p1) = false →
 122    update A v k p1 〈t,p2〉 = k false 〈t,[]〉.
 123  #A #v #p1 elim p1 normalize
 124  [ #p2 #k #t #H >setleaf_fun_correct //
 125  | #hd #tl #IH #p2 #k #t cases hd normalize nodelta
 126   cases t normalize [1,3:#n|2,4:#x1 #x2] #H >IH // cases (admissible ??) //
 127 qed.
 128
 129 theorem update_correct2:
 130  ∀A,v,p1,p2,k,t.
 131   admissible t (reverse … p2 @ p1) = true →
 132    update A v k p1 〈t,p2〉 = update … v k [] 〈t,reverse … p1 @ p2〉.
 133 #A #v #p1 elim p1 normalize //
 134 #dir #ptl #IH #p2 #k #t cases dir normalize nodelta cases t normalize nodelta
 135 [1,3: #n >admissible_leaf_cons #abs destruct
 136 |*: #x1 #x2 #H >IH
 137     [2,4: normalize >rev_append_def >associative_append //
 138     |*: >(rev_append_def … ptl [?]) >associative_append
 139         >(?:admissible ?? = true) // @(admissible_append_true … ptl) // ]]
 140 qed.
 141
 142 theorem final_update_correct:
 143  ∀v,p1,p2,t.
 144   let 〈t',res〉 ≝ setleaf_fun v t (reverse … p1 @ p2) in
 145   update ? v (λres,x.〈res,x〉) p2 〈t,p1〉 = 〈res,〈t',nil …〉〉.
 146  #v #p1 #p2 #t @pair_elim #t' #res #EQ inversion (admissible t (reverse … p1 @ p2))
 147  [ #H >update_correct2 // whd in ⊢ (??%?);
 148    >(reverse_append ? (reverse ? p2) p1) >reverse_reverse >EQ %
 149  | #H >update_correct1 // >setleaf_fun_correct in EQ; // ]
 150 qed.