--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "nat/compare.ma".
+include "nat/plus.ma".
+include "list/list.ma".
+
+notation > "'if' term 19 E 'then' term 19 T 'else' term 19 F 'fi'"
+non associative with precedence 90
+for @{ match $E with [ true ⇒ $T | false ⇒ $F ] }.
+
+inductive PT : Type ≝
+ | Var : nat → PT
+ | Lam : PT → PT
+ | Appl : PT → PT → PT
+ | Bang : PT → PT
+ | Sect : PT → PT
+ | LetB : PT → PT → PT
+ | LetS : PT → PT → PT.
+
+variant appl : PT → PT → PT ≝ Appl.
+coercion appl 1.
+
+notation > "! term 90 t" non associative with precedence 90 for @{ 'bang $t }.
+notation < "! term 90 t" non associative with precedence 90 for @{ 'bang $t }.
+interpretation "bang" 'bang t = (Bang t).
+notation > "§ t" non associative with precedence 90 for @{ 'sect $t }.
+notation < "§ t" non associative with precedence 90 for @{ 'sect $t }.
+interpretation "sect" 'sect t = (Sect t).
+notation > "Λ t" non associative with precedence 90 for @{ 'lam $t }.
+notation < "Λ t" non associative with precedence 90 for @{ 'lam $t }.
+interpretation "lam" 'lam t = (Lam t).
+notation < "Λ \sup ! t" non associative with precedence 90 for @{ 'lamb $t}.
+notation > "*Λ t" non associative with precedence 90 for @{ 'lamb $t}.
+interpretation "lamb" 'lamb t = (Lam (LetB (Var (S O)) t)).
+notation "𝟙" non associative with precedence 90 for @{ 'one }.
+interpretation "one" 'one = (Var (S O)).
+notation "𝟚" non associative with precedence 90 for @{ 'two }.
+interpretation "two" 'two = (Var (S (S O))).
+notation "𝟛" non associative with precedence 90 for @{ 'three }.
+interpretation "three" 'three = (Var (S (S (S O)))).
+notation "𝟜" non associative with precedence 90 for @{ 'four }.
+interpretation "four" 'four = (Var (S (S (S (S O))))).
+notation < "a b" left associative with precedence 60 for @{ 'appl $a $b }.
+interpretation "appl" 'appl a b = (Appl a b).
+
+let rec lift (from:nat) (amount:nat) (what:PT) on what : PT ≝
+ match what with
+ [ Var n ⇒ if leb from n then Var (n+amount) else what fi
+ | Lam t ⇒ Lam (lift (1+from) amount t)
+ | Appl t1 t2 ⇒ Appl (lift from amount t1) (lift from amount t2)
+ | Bang t ⇒ Bang (lift from amount t)
+ | Sect t ⇒ Sect (lift from amount t)
+ | LetB t1 t2 ⇒ LetB (lift from amount t1) (lift (1+from) amount t2)
+ | LetS t1 t2 ⇒ LetS (lift from amount t1) (lift (1+from) amount t2) ].
+
+let rec subst (ww : PT) (fw:nat) (w:PT) on w : PT ≝
+ match w with
+ [ Var n ⇒ if eqb n fw then ww else if ltb fw n then Var (pred n) else w fi fi
+ | Lam t ⇒ Lam (subst (lift 1 1 ww) (1+fw) t)
+ | Appl t1 t2 ⇒ Appl (subst ww fw t1) (subst ww fw t2)
+ | Bang t ⇒ Bang (subst ww fw t)
+ | Sect t ⇒ Sect (subst ww fw t)
+ | LetB t1 t2 ⇒ LetB (subst ww fw t1) (subst (lift 1 1 ww) (1+fw) t2)
+ | LetS t1 t2 ⇒ LetS (subst ww fw t1) (subst (lift 1 1 ww) (1+fw) t2) ].
+
+definition path ≝ list bool.
+
+definition fire ≝ λt:PT.
+ match t with
+ [ Appl hd arg ⇒
+ match hd with
+ [ Lam bo ⇒ subst arg 1 bo
+ | _ ⇒ t ]
+ | LetB def bo ⇒
+ match def with
+ [ Bang t ⇒ subst t 1 bo
+ | _ ⇒ t ]
+ | LetS def bo ⇒
+ match def with
+ [ Sect t ⇒ subst t 1 bo
+ | LetS def2 bo2 ⇒ LetS def2 (LetS bo2 bo)
+ | _ ⇒ t ]
+ | _ ⇒ t ].
+
+let rec follow (p:path) (t:PT) (f : PT → PT) on p : PT ≝
+ match p with
+ [ nil ⇒ f t
+ | cons b tl ⇒
+ match t with
+ [ Var _ ⇒ t
+ | Lam t1 ⇒ if b then t else Lam (follow tl t1 f) fi
+ | Appl t1 t2 ⇒ if b then Appl t1 (follow tl t2 f) else Appl (follow tl t1 f) t2 fi
+ | Bang t1 ⇒ if b then t else Bang (follow tl t1 f) fi
+ | Sect t1 ⇒ if b then t else Sect (follow tl t1 f) fi
+ | LetB t1 t2 ⇒ if b then LetB t1 (follow tl t2 f) else LetB (follow tl t1 f) t2 fi
+ | LetS t1 t2 ⇒ if b then LetS t1 (follow tl t2 f) else LetS (follow tl t1 f) t2 fi ]].
+
+definition reduce ≝ λp,t.follow p t fire.
+
+let rec FO (w:nat) (t:PT) on t : nat ≝
+ match t with
+ [ Var n ⇒ if eqb w n then 1 else 0 fi
+ | Lam t ⇒ FO (1+w) t
+ | Appl t1 t2 ⇒ FO w t1 + FO w t2
+ | Bang t ⇒ FO w t
+ | Sect t ⇒ FO w t
+ | LetB t1 t2 ⇒ FO w t1 + FO (1+w) t2
+ | LetS t1 t2 ⇒ FO w t1 + FO (1+w) t2 ].
+
+let rec FOa (w:nat) (t:PT) on t : nat ≝
+ match t with
+ [ Var n ⇒ if ltb w n then 1 else 0 fi
+ | Lam t ⇒ FOa (1+w) t
+ | Appl t1 t2 ⇒ FOa w t1 + FOa w t2
+ | Bang t ⇒ FOa w t
+ | Sect t ⇒ FOa w t
+ | LetB t1 t2 ⇒ FOa w t1 + FOa (1+w) t2
+ | LetS t1 t2 ⇒ FOa w t1 + FOa (1+w) t2 ].
+
+inductive ctxe : Type ≝
+ | Reg: ctxe
+ | Ban: ctxe
+ | Sec: ctxe
+ | Err: ctxe.
+
+let rec mapb (l : list ctxe) : list ctxe ≝
+ match l with
+ [ nil ⇒ nil ?
+ | cons x xs ⇒
+ match x with
+ [ Ban ⇒ Reg
+ | _ ⇒ Err ] :: mapb xs].
+
+let rec maps (l : list ctxe) : list ctxe ≝
+ match l with
+ [ nil ⇒ nil ?
+ | cons x xs ⇒
+ match x with
+ [ Ban ⇒ Reg
+ | Sec ⇒ Reg
+ | _ ⇒ Err ] :: maps xs].
+
+
+inductive Tok : PT → list ctxe → Prop ≝
+ | Tv : ∀n,C. nth ? (Err::C) Err n = Reg → Tok (Var n) C
+ | Tl : ∀t,C. Tok t (Reg::C) → leb (FO 1 t) 1 = true → Tok (Lam t) C
+ | Ta : ∀t1,t2,C. Tok t1 C → Tok t2 C → Tok (Appl t1 t2) C
+ | Tb : ∀t,C.leb (FOa 0 t) 1 = true → Tok t (mapb C) → Tok (Bang t) C
+ | Ts : ∀t,C.Tok t (maps C) → Tok (Sect t) C
+ | Tlb: ∀t1,t2,C. Tok t1 C → Tok t2 (Ban::C) → Tok (LetB t1 t2) C
+ | Tls: ∀t1,t2,C. Tok t1 C → Tok t2 (Sec::C) → leb (FO 1 t2) 1 = true → Tok (LetS t1 t2) C
+ .
+
+definition two : PT ≝ *Λ(§Λ𝟚(𝟚𝟙)).
+
+notation "#" non associative with precedence 90 for @{ 'Tok }.
+interpretation "Tv" 'Tok = Tv.
+interpretation "Tl" 'Tok = Tl.
+interpretation "Ta" 'Tok = Ta.
+interpretation "Tb" 'Tok = Tb.
+interpretation "Ts" 'Tok = Ts.
+interpretation "Tlb" 'Tok = Tlb.
+interpretation "Tls" 'Tok = Tls.
+
+lemma two_ok : Tok two [ ].
+unfold two; autobatch depth=8 width=4 size=15;
+qed.
+
+definition succ : PT ≝ Λ*Λ(LetS (𝟛 (!𝟙)) §(Λ𝟛 (𝟚 𝟙))).
+
+lemma succ_ok : Tok succ [ ].
+unfold succ; autobatch depth=18 width=8 size=35;
+qed.
+
+definition three : PT ≝ *Λ(§Λ𝟚(𝟚(𝟚 𝟙))).
+
+lemma three_ok : Tok three [ ].
+unfold three. autobatch depth=9 width=4 size=17;
+qed.
+
+definition foldl ≝
+ λA,B:Type.λf:A → B → B.
+ let rec aux (acc: B) (l:list A) on l ≝
+ match l with
+ [ nil ⇒ acc
+ | cons x xs ⇒ aux (f x acc) xs]
+ in
+ aux.
+
+lemma obvious : ∃pl.foldl ?? reduce (succ two) pl = three.
+unfold succ; unfold two; exists;
+[apply ([ ] :: ?);| simplify;]
+[apply ([false;true;false] :: ?);| simplify;]
+[apply ([false;true;false] :: ?);| simplify;]
+[apply ([false;true] :: ?);| simplify;]
+[apply ([false;true;false;false;true] :: ?);| simplify;]
+[apply ([ ]);| simplify;]
+reflexivity;
+qed.
\ No newline at end of file
projects / helm.git / commitdiff