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 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.