From 7aaaee610ab145cb419de016fb69c633fdaa6cb4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 11 Feb 2009 10:30:15 +0000 Subject: [PATCH] ... --- helm/software/matita/contribs/ICC/depends | 4 + helm/software/matita/contribs/ICC/lamla.ma | 211 +++++++++++++++++++++ helm/software/matita/contribs/ICC/root | 1 + 3 files changed, 216 insertions(+) create mode 100644 helm/software/matita/contribs/ICC/depends create mode 100644 helm/software/matita/contribs/ICC/lamla.ma create mode 100644 helm/software/matita/contribs/ICC/root diff --git a/helm/software/matita/contribs/ICC/depends b/helm/software/matita/contribs/ICC/depends new file mode 100644 index 000000000..75ad60ed7 --- /dev/null +++ b/helm/software/matita/contribs/ICC/depends @@ -0,0 +1,4 @@ +lamla.ma list/list.ma nat/compare.ma nat/plus.ma +list/list.ma +nat/compare.ma +nat/plus.ma diff --git a/helm/software/matita/contribs/ICC/lamla.ma b/helm/software/matita/contribs/ICC/lamla.ma new file mode 100644 index 000000000..a036fe0fd --- /dev/null +++ b/helm/software/matita/contribs/ICC/lamla.ma @@ -0,0 +1,211 @@ +(**************************************************************************) +(* ___ *) +(* ||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 diff --git a/helm/software/matita/contribs/ICC/root b/helm/software/matita/contribs/ICC/root new file mode 100644 index 000000000..4e7f33883 --- /dev/null +++ b/helm/software/matita/contribs/ICC/root @@ -0,0 +1 @@ +baseuri=cic:/matita/ICC -- 2.39.2