1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "nat/compare.ma".
16 include "nat/plus.ma".
17 include "list/list.ma".
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 ] }.
30 | LetS : PT → PT → PT.
32 variant appl : PT → PT → PT ≝ Appl.
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).
58 let rec lift (from:nat) (amount:nat) (what:PT) on what : PT ≝
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) ].
68 let rec subst (ww : PT) (fw:nat) (w:PT) on w : PT ≝
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) ].
78 definition path ≝ list bool.
80 definition fire ≝ λt:PT.
84 [ Lam bo ⇒ subst arg 1 bo
88 [ Bang t ⇒ subst t 1 bo
92 [ Sect t ⇒ subst t 1 bo
93 | LetS def2 bo2 ⇒ LetS def2 (LetS bo2 bo)
97 let rec follow (p:path) (t:PT) (f : PT → PT) on p : PT ≝
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 ]].
110 definition reduce ≝ λp,t.follow p t fire.
112 let rec FO (w:nat) (t:PT) on t : nat ≝
114 [ Var n ⇒ if eqb w n then 1 else 0 fi
116 | Appl t1 t2 ⇒ FO w t1 + FO w t2
119 | LetB t1 t2 ⇒ FO w t1 + FO (1+w) t2
120 | LetS t1 t2 ⇒ FO w t1 + FO (1+w) t2 ].
122 let rec FOa (w:nat) (t:PT) on t : nat ≝
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
129 | LetB t1 t2 ⇒ FOa w t1 + FOa (1+w) t2
130 | LetS t1 t2 ⇒ FOa w t1 + FOa (1+w) t2 ].
132 inductive ctxe : Type ≝
138 let rec mapb (l : list ctxe) : list ctxe ≝
144 | _ ⇒ Err ] :: mapb xs].
146 let rec maps (l : list ctxe) : list ctxe ≝
153 | _ ⇒ Err ] :: maps xs].
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
166 definition two : PT ≝ *Λ(§Λ𝟚(𝟚𝟙)).
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.
177 lemma two_ok : Tok two [ ].
178 unfold two; autobatch depth=8 width=4 size=15;
181 definition succ : PT ≝ Λ*Λ(LetS (𝟛 (!𝟙)) §(Λ𝟛 (𝟚 𝟙))).
183 lemma succ_ok : Tok succ [ ].
184 unfold succ; autobatch depth=18 width=8 size=35;
187 definition three : PT ≝ *Λ(§Λ𝟚(𝟚(𝟚 𝟙))).
189 lemma three_ok : Tok three [ ].
190 unfold three. autobatch depth=9 width=4 size=17;
194 λA,B:Type.λf:A → B → B.
195 let rec aux (acc: B) (l:list A) on l ≝
198 | cons x xs ⇒ aux (f x acc) xs]
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;]