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 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 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 update_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 theorem update_correct1:
 109  ∀A,v,p1,p2,k,t.
 110   admissible t (reverse … p2 @ p1) = false →
 111    update A v k p1 〈t,p2〉 = k false 〈t,[]〉.
 112  #A #v #p1 elim p1 normalize
 113  [ #p2 #k #t #H >update_fun_correct //
 114  | #hd #tl #IH #p2 #k #t cases hd normalize nodelta
 115   cases t normalize [1,3:#n|2,4:#x1 #x2] #H >IH // cases (admissible ??) //
 116 qed.
 117
 118 lemma admissible_leaf_cons:
 119  ∀n,p1,dir,p2. admissible (leaf n) (p1@dir::p2) = false.
 120  #n #p1 elim p1 //
 121 qed.
 122
 123 (*
 124 lemma admissible_node_cons:
 125  ∀x1,x2,p1,p2.
 126   admissible (node x1 x2) (rev_append bool p1 [true]@p2)=true →
 127    admissible x2 p1=true.
 128  #x1 #x2 #p1 elim p1 normalize // #dir #tl #IH #p2 cases x2 normalize
 129  [ #n *)
 130
 131 theorem update_correct2:
 132  ∀A,v,p1,p2,k,t.
 133   admissible t (p2 @ reverse … p1) = true →
 134    update A v k p1 〈t,p2〉 = update … v k [] 〈t,reverse … p1 @ p2〉.
 135 #A #v #p1 elim p1 normalize //
 136 #dir #ptl #IH #p2 #k #t cases dir normalize nodelta cases t normalize nodelta
 137 [1,3: #n >admissible_leaf_cons #abs destruct
 138 |*: #x1 #x2 #H >IH // >rev_append_cons >(?:admissible ? p2 = true) try %
 139     <rev_append_cons in H; change with (reverse ??) in match (rev_append ???);
 140
 141
 142 (* OLD
 143 theorem update_correct:
 144  ∀v,p1,p2,t.
 145   let 〈t',res〉 ≝ setleaf_fun v t (reverse … p1 @ p2) in
 146   update ? v (λres,x.〈res,x〉) p2 〈t,p1〉 = 〈res,〈t',nil …〉〉.
 147  #v #p1 elim p1 normalize
 148   [ #p2 elim p2 normalize
 149     [ #x cases x normalize //
 150     | #dir #path #IH #x elim x normalize
 151       [ #n cases dir normalize
 152
 153
 154   #p2 elim p normalize
 155   [ #t elim t normalize //
 156   | * normalize
 157     [ #path #IH
 158
 159
 160   #path #IH #x elim x normalize
 161     [ #v cases res normalize lapply (IH (leaf v)) -IH elim path
 162       normalize // * normalize
 163       [2: #path' #IH #IH2 @IH
 164 *)