helm/software/matita/contribs/ICC/lamla.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 "nat/compare.ma".
  16 include "nat/plus.ma".
  17 include "list/list.ma".
  18
  19 notation > "'if' term 19 E 'then' term 19 T 'else' term 19 F 'fi'"
  20 non associative with precedence 90
  21 for @{ match $E with [ true ⇒ $T | false ⇒ $F ] }.
  22
  23 inductive PT : Type ≝
  24   | Var : nat → PT
  25   | Lam : PT → PT
  26   | Appl : PT → PT → PT
  27   | Bang : PT → PT
  28   | Sect : PT → PT
  29   | LetB : PT → PT → PT
  30   | LetS : PT → PT → PT.
  31
  32 variant appl : PT → PT → PT ≝ Appl.
  33 coercion appl 1.
  34
  35 notation > "! term 90 t" non associative with precedence 90 for @{ 'bang $t }.
  36 notation < "! term 90 t" non associative with precedence 90 for @{ 'bang $t }.
  37 interpretation "bang" 'bang t = (Bang t).
  38 notation > "§ t" non associative with precedence 90 for @{ 'sect $t }.
  39 notation < "§ t" non associative with precedence 90 for @{ 'sect $t }.
  40 interpretation "sect" 'sect t = (Sect t).
  41 notation > "Λ t" non associative with precedence 90 for @{ 'lam $t }.
  42 notation < "Λ t" non associative with precedence 90 for @{ 'lam $t }.
  43 interpretation "lam" 'lam t = (Lam t).
  44 notation < "Λ \sup ! t" non associative with precedence 90 for @{ 'lamb $t}.
  45 notation > "*Λ t" non associative with precedence 90 for @{ 'lamb $t}.
  46 interpretation "lamb" 'lamb t = (Lam (LetB (Var (S O)) t)).
  47 notation "𝟙" non associative with precedence 90 for @{ 'one }.
  48 interpretation "one" 'one = (Var (S O)).
  49 notation "𝟚" non associative with precedence 90 for @{ 'two }.
  50 interpretation "two" 'two = (Var (S (S O))).
  51 notation "𝟛" non associative with precedence 90 for @{ 'three }.
  52 interpretation "three" 'three = (Var (S (S (S O)))).
  53 notation "𝟜" non associative with precedence 90 for @{ 'four }.
  54 interpretation "four" 'four = (Var (S (S (S (S O))))).
  55 notation < "a b" left associative with precedence 60 for @{ 'appl $a $b }.
  56 interpretation "appl" 'appl a b = (Appl a b).
  57
  58 let rec lift (from:nat) (amount:nat) (what:PT) on what : PT ≝
  59   match what with
  60   [ Var n ⇒ if leb from n then Var (n+amount) else what fi
  61   | Lam t ⇒ Lam (lift (1+from) amount t)
  62   | Appl t1 t2 ⇒ Appl (lift from amount t1) (lift from amount t2)
  63   | Bang t ⇒ Bang (lift from amount t)
  64   | Sect t ⇒ Sect (lift from amount t)
  65   | LetB t1 t2 ⇒ LetB (lift from amount t1) (lift (1+from) amount t2)
  66   | LetS t1 t2 ⇒ LetS (lift from amount t1) (lift (1+from) amount t2) ].
  67
  68 let rec subst (ww : PT) (fw:nat) (w:PT) on w : PT ≝
  69   match w with
  70   [ Var n ⇒  if eqb n fw then ww else if ltb fw n then Var (pred n) else w fi fi
  71   | Lam t ⇒ Lam (subst (lift 1 1 ww) (1+fw) t)
  72   | Appl t1 t2 ⇒ Appl (subst ww fw t1) (subst ww fw t2)
  73   | Bang t ⇒ Bang (subst ww fw t)
  74   | Sect t ⇒ Sect (subst ww fw t)
  75   | LetB t1 t2 ⇒ LetB (subst ww fw t1) (subst (lift 1 1 ww) (1+fw) t2)
  76   | LetS t1 t2 ⇒ LetS (subst ww fw t1) (subst (lift 1 1 ww) (1+fw) t2) ].
  77
  78 definition path ≝ list bool.
  79
  80 definition fire ≝ λt:PT.
  81   match t with
  82   [ Appl hd arg ⇒
  83       match hd with
  84       [ Lam bo ⇒ subst arg 1 bo
  85       | _ ⇒ t ]
  86   | LetB def bo ⇒
  87       match def with
  88       [ Bang t ⇒ subst t 1 bo
  89       | _ ⇒ t ]
  90   | LetS def bo ⇒
  91       match def with
  92       [ Sect t ⇒ subst t 1 bo
  93       | LetS def2 bo2 ⇒ LetS def2 (LetS bo2 bo)
  94       | _ ⇒ t ]
  95   | _ ⇒ t ].
  96
  97 let rec follow (p:path) (t:PT) (f : PT → PT) on p : PT ≝
  98   match p with
  99   [ nil ⇒ f t
 100   | cons b tl ⇒
 101       match t with
 102       [ Var _ ⇒ t
 103       | Lam t1 ⇒ if b then t else Lam (follow tl t1 f) fi
 104       | Appl t1 t2 ⇒ if b then Appl t1 (follow tl t2 f) else Appl (follow tl t1 f) t2 fi
 105       | Bang t1 ⇒ if b then t else Bang (follow tl t1 f) fi
 106       | Sect t1 ⇒ if b then t else Sect (follow tl t1 f) fi
 107       | LetB t1 t2 ⇒ if b then LetB t1 (follow tl t2 f) else LetB (follow tl t1 f) t2 fi
 108       | LetS t1 t2 ⇒ if b then LetS t1 (follow tl t2 f) else LetS (follow tl t1 f) t2 fi ]].
 109
 110 definition reduce ≝ λp,t.follow p t fire.
 111
 112 let rec FO (w:nat) (t:PT) on t : nat ≝
 113   match t with
 114   [ Var n ⇒ if eqb w n then 1 else 0 fi
 115   | Lam t ⇒ FO (1+w) t
 116   | Appl t1 t2 ⇒ FO w t1 + FO w t2
 117   | Bang t ⇒ FO w t
 118   | Sect t ⇒ FO w t
 119   | LetB t1 t2 ⇒ FO w t1 + FO (1+w) t2
 120   | LetS t1 t2 ⇒ FO w t1 + FO (1+w) t2 ].
 121
 122 let rec FOa (w:nat) (t:PT) on t : nat ≝
 123   match t with
 124   [ Var n ⇒ if ltb w n then 1 else 0 fi
 125   | Lam t ⇒ FOa (1+w) t
 126   | Appl t1 t2 ⇒ FOa w t1 + FOa w t2
 127   | Bang t ⇒ FOa w t
 128   | Sect t ⇒ FOa w t
 129   | LetB t1 t2 ⇒ FOa w t1 + FOa (1+w) t2
 130   | LetS t1 t2 ⇒ FOa w t1 + FOa (1+w) t2 ].
 131
 132 inductive ctxe : Type ≝
 133   | Reg: ctxe
 134   | Ban: ctxe
 135   | Sec: ctxe
 136   | Err: ctxe.
 137
 138 let rec mapb (l : list ctxe) : list ctxe ≝
 139   match l with
 140   [ nil ⇒ nil ?
 141   | cons x xs ⇒
 142       match x with
 143       [ Ban ⇒ Reg
 144       | _ ⇒ Err ] :: mapb xs].
 145
 146 let rec maps (l : list ctxe) : list ctxe ≝
 147   match l with
 148   [ nil ⇒ nil ?
 149   | cons x xs ⇒
 150       match x with
 151       [ Ban ⇒ Reg
 152       | Sec ⇒ Reg
 153       | _ ⇒ Err ] :: maps xs].
 154
 155
 156 inductive Tok : PT → list ctxe → Prop ≝
 157   | Tv : ∀n,C. nth ? (Err::C) Err n = Reg → Tok (Var n) C
 158   | Tl : ∀t,C. Tok t (Reg::C) → leb (FO 1 t) 1 = true → Tok (Lam t) C
 159   | Ta : ∀t1,t2,C. Tok t1 C → Tok t2 C → Tok (Appl t1 t2) C
 160   | Tb : ∀t,C.leb (FOa 0 t) 1 = true → Tok t (mapb C)  → Tok (Bang t) C
 161   | Ts : ∀t,C.Tok t (maps C)  → Tok (Sect t) C
 162   | Tlb: ∀t1,t2,C. Tok t1 C → Tok t2 (Ban::C) → Tok (LetB t1 t2) C
 163   | Tls: ∀t1,t2,C. Tok t1 C → Tok t2 (Sec::C) → leb (FO 1 t2) 1 = true → Tok (LetS t1 t2) C
 164   .
 165
 166 definition two : PT ≝ *Λ(§Λ𝟚(𝟚𝟙)).
 167
 168 notation "#" non associative with precedence 90 for @{ 'Tok }.
 169 interpretation "Tv" 'Tok = Tv.
 170 interpretation "Tl" 'Tok = Tl.
 171 interpretation "Ta" 'Tok = Ta.
 172 interpretation "Tb" 'Tok = Tb.
 173 interpretation "Ts" 'Tok = Ts.
 174 interpretation "Tlb" 'Tok = Tlb.
 175 interpretation "Tls" 'Tok = Tls.
 176
 177 lemma two_ok : Tok two [ ].
 178 unfold two; autobatch depth=8 width=4 size=15;
 179 qed.
 180
 181 definition succ : PT ≝ Λ*Λ(LetS (𝟛 (!𝟙)) §(Λ𝟛 (𝟚 𝟙))).
 182
 183 lemma succ_ok : Tok succ [ ].
 184 unfold succ; autobatch depth=18 width=8 size=35;
 185 qed.
 186
 187 definition three : PT ≝ *Λ(§Λ𝟚(𝟚(𝟚 𝟙))).
 188
 189 lemma three_ok : Tok three [ ].
 190 unfold three. autobatch depth=9 width=4 size=17;
 191 qed.
 192
 193 definition foldl ≝
 194   λA,B:Type.λf:A → B → B.
 195   let rec aux (acc: B) (l:list A) on l  ≝
 196     match l with
 197     [ nil ⇒  acc
 198     | cons x xs ⇒ aux (f x acc) xs]
 199   in
 200     aux.
 201
 202 lemma obvious : ∃pl.foldl ?? reduce (succ two) pl = three.
 203 unfold succ; unfold two; exists;
 204 [apply ([ ] :: ?);| simplify;]
 205 [apply ([false;true;false] :: ?);| simplify;]
 206 [apply ([false;true;false] :: ?);| simplify;]
 207 [apply ([false;true] :: ?);| simplify;]
 208 [apply ([false;true;false;false;true] :: ?);| simplify;]
 209 [apply ([ ]);| simplify;]
 210 reflexivity;
 211 qed.