matita/matita/lib/MONADS/speranza2.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 option_map: ∀A,B:Type[0]. (A → option B) → option A → option B ≝
  26  λA,B,f,x. match x with [ None ⇒ None … | Some v ⇒ f v ].
  27
  28 definition left: ∀A:Type[0]. (T → option T) → (T → option A) → T → option A ≝
  29  λA,kl,k,t.
  30   match t with
  31   [ leaf _ ⇒ None ?
  32   | node l r ⇒ option_map … (λl'. k (node l' r)) (kl l) ].
  33
  34 definition right: ∀A:Type[0]. (T → option T) → (T → option A) → T → option A ≝
  35  λA,kr,k,t.
  36   match t with
  37   [ leaf _ ⇒ None ?
  38   | node l r ⇒ option_map … (λr'. k (node l r')) (kr r) ].
  39
  40 definition setleaf: ∀A:Type[0]. (nat → option nat) → (T → option A) → T → option A ≝
  41  λA,kv,k,t.
  42   match t with
  43   [ leaf n ⇒ option_map … (λn'. k (leaf n')) (kv n)
  44   | node l r ⇒ None ? ].
  45
  46 definition stop: T → option T ≝
  47  λt. Some … t.
  48
  49 (*****************************)
  50
  51 let rec setleaf_fun (v:nat) (x:T) (p:path) on p : option T ≝
  52  match p with
  53  [ nil ⇒
  54     match x with
  55     [ leaf _ ⇒ Some … (leaf v)
  56     | node x1 x2 ⇒ None ? ]
  57  | cons b tl ⇒
  58     match x with
  59     [ leaf n ⇒ None …
  60     | node x1 x2 ⇒
  61        if b then
  62         option_map … (λx2'. Some … (node x1 x2')) (setleaf_fun v x2 tl)
  63        else
  64         option_map … (λx1'. Some … (node x1' x2)) (setleaf_fun v x1 tl) ]].
  65
  66 let rec update (A:Type[0]) (v:nat) (k: T → option A) (p:path) on p: T → option A ≝
  67  match p with
  68  [ nil ⇒ setleaf … (λ_. Some … v) k
  69  | cons b tl ⇒
  70     if b then right … (update T v stop tl) k else left … (update T v stop tl) k ].
  71
  72 let rec add_fun (t1:T) (t2:T) on t2 : option T ≝
  73  match t1 with
  74  [ leaf m ⇒ match t2 with [ leaf n ⇒ Some … (leaf (m+n)) | _ ⇒ None ? ]
  75  | node l1 r1 ⇒
  76     match t2 with
  77     [ node l2 r2 ⇒
  78        option_map … (λl'.
  79         option_map … (λr'. Some … (node l' r')) (add_fun r1 r2)) (add_fun l1 l2)
  80     | _ ⇒ None … ]].
  81
  82 let rec add (A:Type[0]) (k: T → option A) (t1:T) on t1 : T → option A ≝
  83  match t1 with
  84  [ leaf n ⇒ setleaf … (λm.Some … (n+m)) k
  85  | node l r ⇒
  86     left … (add … stop l) (right … (add … stop r) k) ].
  87
  88 definition example ≝
  89  node (node (leaf 0) (leaf 1)) (node (leaf 2) (leaf 3)).
  90
  91 lemma test: add … stop example example = ?.
  92  normalize //
  93 qed.
  94
  95 lemma test1: update ? 5 stop [false;false] example = ?.
  96  normalize //
  97 qed.
  98
  99 theorem update_correct:
 100  ∀v,p,t. setleaf_fun v t p =  update ? v stop p t.
 101 #v #p elim p normalize [* normalize // ]
 102 #hd #tl #IH * normalize
 103  [ cases hd normalize //
 104  | cases hd normalize #l #r >IH // ]
 105 qed.
 106
 107 theorem add_correct: ∀t1,t2. add_fun t1 t2 = add … stop t1 t2.
 108  #t1 elim t1 normalize
 109   [ #n * normalize //
 110   | #l1 #r1 #IHl #IHr * normalize // #l2 #r2 >IHl >IHr // ]
 111 qed.