From: Enrico Tassi Date: Thu, 26 Mar 2009 12:29:35 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~4137 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e76b34f51e5677cbe3dbe3d8e89a34d13efe487a;p=helm.git ... --- diff --git a/helm/software/matita/contribs/ICC/lamla.ma b/helm/software/matita/contribs/ICC/lamla.ma index a036fe0fd..d54775375 100644 --- a/helm/software/matita/contribs/ICC/lamla.ma +++ b/helm/software/matita/contribs/ICC/lamla.ma @@ -152,43 +152,102 @@ let rec maps (l : list ctxe) : list ctxe ≝ | 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 + | Tl : ∀t,C. Tok t (Reg::C) → FO 1 t ≤ 1 → 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 + | Tb : ∀t,C.FOa 0 t ≤ 1 → 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 ≝ *Λ(§Λ𝟚(𝟚𝟙)). + | Tls: ∀t1,t2,C. Tok t1 C → Tok t2 (Sec::C) → FO 1 t2 ≤ 1 → Tok (LetS t1 t2) C. + +(* powerup! *) +include "decidable_kit/eqtype.ma". + +definition cmpC : ctxe → ctxe → bool ≝ + λc1,c2. + match c1 with + [ Reg ⇒ match c2 with [ Reg ⇒ true | _ ⇒ false ] + | Ban ⇒ match c2 with [ Ban ⇒ true | _ ⇒ false ] + | Sec ⇒ match c2 with [ Sec ⇒ true | _ ⇒ false ] + | Err ⇒ match c2 with [ Err ⇒ true | _ ⇒ false ]]. + +lemma cmpCP: ∀x,y.eq_compatible ? x y (cmpC x y). +intros; apply prove_reflect; cases x; cases y; simplify; intro; +destruct H; try reflexivity; intro W; destruct W; +qed. +definition ctxe_eqType ≝ mk_eqType ?? cmpCP. + +let rec Tok_dec (C:list ctxe) (t:PT) on t : bool ≝ + match t with + [ Var n ⇒ cmp ctxe_eqType (nth ? (Err::C) Err n) Reg + | Lam t ⇒ andb (Tok_dec (Reg::C) t) (leb (FO 1 t) 1) + | Appl t1 t2 ⇒ andb (Tok_dec C t1) (Tok_dec C t2) + | Bang t ⇒ andb (leb (FOa 0 t) 1) (Tok_dec (mapb C) t) + | Sect t ⇒ Tok_dec (maps C) t + | LetB t1 t2 ⇒ andb (Tok_dec C t1) (Tok_dec (Ban::C) t2) + | LetS t1 t2 ⇒ andb (Tok_dec C t1) (andb (Tok_dec (Sec::C) t2) (leb (FO 1 t2) 1)) + ]. + +(* (constructor ?) tactic *) 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 "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; + +lemma TokP : ∀t,C.reflect (Tok t C) (Tok_dec C t). +intros; apply prove_reflect; generalize in match C; elim t; intros; +[1,2,3,4,5,6,7: apply rule #; simplify in H H1 H2; + [1: apply (b2pT ?? (cmpCP ??) H); + |2,7: cases (b2pT ?? (andbP ??) H1); apply (b2pT ?? (lebP ??)); assumption; + |3,6: cases (b2pT ?? (andbP ??) H1); autobatch depth=2; + |4,5,9,10,13: cases (b2pT ?? (andbP ??) H2); autobatch depth=2; + |8: autobatch depth=2; + |11: cases (b2pT ?? (andbP ??) H2); cases (b2pT ?? (andbP ??) H4); + apply (b2pT ?? (lebP ??)); assumption; + |12,11: cases (b2pT ?? (andbP ??) H2); cases (b2pT ?? (andbP ??) H4); autobatch depth=2;] +|*: intro E; inversion E; clear E; intros; simplify in H; + [1: destruct H3; destruct H2; rewrite > H1 in H; normalize in H; destruct H; + |9: destruct H6; destruct H5; simplify in H1; + cases (b2pF ?? (andbP ??) H1); split[2:apply (p2bT ?? (lebP ??) H4);] + lapply depth=0 (H (Reg::l)) as W; cases (Tok_dec (Reg::l) p) in W; + intros; [reflexivity] cases (H5 ? H2); reflexivity; + |17: destruct H7; destruct H8; simplify in H2; apply (b2pF ?? (andbP ??) H2); + lapply depth=0 (H l) as W1; lapply depth=0 (H1 l) as W2; + cases (Tok_dec l p) in W1; cases (Tok_dec l p1) in W2; + intros; split; try reflexivity; + [1,3: cases (H7 ? H5); reflexivity;|*: cases (H8 ? H3); reflexivity;] + |25: destruct H6; destruct H5; simplify in H1; + apply (b2pF ?? (andbP ??) H1); rewrite > (p2bT ?? (lebP ??) H2); + split[reflexivity] lapply depth=0 (H (mapb l)) as W; + cases (Tok_dec (mapb l) p) in W; intros; [reflexivity] + cases (H5 ? H3); reflexivity; + |33: destruct H5; destruct H4; simplify in H1; exact (H ? H1 H2); + |41: destruct H8; destruct H6; destruct H7; clear H4 H6; simplify in H2; + lapply depth=0 (H l) as W1; lapply depth=0 (H1 (Ban::l)) as W2; + apply (b2pF ?? (andbP ??) H2); cases (Tok_dec l p) in W1; + cases (Tok_dec (Ban::l) p1) in W2; intros; split; try reflexivity; + [1,3: cases (H4 ? H5); reflexivity;|*: cases (H6 ? H3); reflexivity;] + |49: destruct H9; destruct H8; clear H6 H4; simplify in H2; + apply (b2pF ?? (andbP ??) H2); clear H2; rewrite > (p2bT ?? (lebP ??) H7); + rewrite > andb_sym; simplify; + lapply depth=0 (H l) as W1; lapply depth=0 (H1 (Sec::l)) as W2; + cases (Tok_dec l p) in W1; cases (Tok_dec (Sec::l) p1) in W2; + intros; split; try reflexivity; + [1,3: cases (H2 ? H5); reflexivity;|*: cases (H4 ? H3); reflexivity;] + |*: try solve[destruct H3]; try solve[destruct H4]; try solve[destruct H5]; + try solve[destruct H6]; try solve[destruct H7]; try solve[destruct H8]]] qed. +definition two : PT ≝ *Λ(§Λ𝟚(𝟚𝟙)). 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. +lemma two_Tok : Tok two [ ]. apply (b2pT ?? (TokP ??)); reflexivity; qed. +lemma succ_Tok : Tok succ [ ]. apply (b2pT ?? (TokP ??)); reflexivity; qed. +lemma three_Tok : Tok three [ ]. apply (b2pT ?? (TokP ??)); reflexivity; qed. definition foldl ≝ λA,B:Type.λf:A → B → B.