| 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.
projects / helm.git / commitdiff