--- /dev/null
+Require Export pc3_defs.
+
+(*#* #stop record *)
+
+ Record G : Set := {
+ f : nat -> nat;
+ f_inc : (n:?) (lt n (f n))
+ }.
+
+(*#* #start record *)
+
+(*#* #caption "typing",
+ "well formed context sort", "well formed context binder",
+ "conversion rule", "typed sort", "typed reference to abbreviation",
+ "typed reference to abstraction", "typed binder", "typed application",
+ "typed cast"
+*)
+ Inductive wf0 [g:G] : C -> Prop :=
+ | wf0_sort : (m:?) (wf0 g (CSort m))
+ | wf0_bind : (c:?; u,t:?) (ty0 g c u t) ->
+ (b:?) (wf0 g (CTail c (Bind b) u))
+ with ty0 [g:G] : C -> T -> T -> Prop :=
+(* structural rules *)
+ | ty0_conv : (c:?; t2,t:?) (ty0 g c t2 t) ->
+ (u,t1:?) (ty0 g c u t1) -> (pc3 c t1 t2) ->
+ (ty0 g c u t2)
+(* axiom rules *)
+ | ty0_sort : (c:?) (wf0 g c) ->
+ (m:?) (ty0 g c (TSort m) (TSort (f g m)))
+ | ty0_abbr : (c:?) (wf0 g c) ->
+ (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abbr) u)) ->
+ (t:?) (ty0 g d u t) ->
+ (ty0 g c (TBRef n) (lift (S n) (0) t))
+ | ty0_abst : (c:?) (wf0 g c) ->
+ (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abst) u)) ->
+ (t:?) (ty0 g d u t) ->
+ (ty0 g c (TBRef n) (lift (S n) (0) u))
+ | ty0_bind : (c:?; u,t:?) (ty0 g c u t) ->
+ (b:?; t1,t2:?) (ty0 g (CTail c (Bind b) u) t1 t2) ->
+ (t0:?) (ty0 g (CTail c (Bind b) u) t2 t0) ->
+ (ty0 g c (TTail (Bind b) u t1) (TTail (Bind b) u t2))
+ | ty0_appl : (c:?; w,u:?) (ty0 g c w u) ->
+ (v,t:?) (ty0 g c v (TTail (Bind Abst) u t)) ->
+ (ty0 g c (TTail (Flat Appl) w v)
+ (TTail (Flat Appl) w (TTail (Bind Abst) u t))
+ )
+ | ty0_cast : (c:?; t1,t2:?) (ty0 g c t1 t2) ->
+ (t0:?) (ty0 g c t2 t0) ->
+ (ty0 g c (TTail (Flat Cast) t2 t1) t2).
+
+ Hint wf0 : ltlc := Constructors wf0.
+
+ Hint ty0 : ltlc := Constructors ty0.
+
+(*#* #caption "generation lemma of typing" #clauses ty0_gen_base *)
+
+ Section ty0_gen_base. (***************************************************)
+
+(*#* #caption "generation lemma for sort" *)
+(*#* #cap #cap c #alpha x in T, n in h *)
+
+ Theorem ty0_gen_sort: (g:?; c:?; x:?; n:?)
+ (ty0 g c (TSort n) x) ->
+ (pc3 c (TSort (f g n)) x).
+
+(*#* #stop proof *)
+
+ Intros until 1; InsertEq H '(TSort n); XElim H; Intros.
+(* case 1 : ty0_conv *)
+ XEAuto.
+(* case 2 : ty0_sort *)
+ Inversion H0; XAuto.
+(* case 3 : ty0_abbr *)
+ Inversion H3.
+(* case 4 : ty0_abst *)
+ Inversion H3.
+(* case 5 : ty0_bind *)
+ Inversion H5.
+(* case 6 : ty0_appl *)
+ Inversion H3.
+(* case 7 : ty0_cast *)
+ Inversion H3.
+ Qed.
+
+(*#* #start proof *)
+
+(*#* #caption "generation lemma for bound reference" *)
+(*#* #cap #cap c, e #alpha x in T, t in U, u in V, n in i *)
+
+ Theorem ty0_gen_bref: (g:?; c:?; x:?; n:?) (ty0 g c (TBRef n) x) ->
+ (EX e u t | (pc3 c (lift (S n) (0) t) x) &
+ (drop n (0) c (CTail e (Bind Abbr) u)) &
+ (ty0 g e u t)
+ ) \/
+ (EX e u t | (pc3 c (lift (S n) (0) u) x) &
+ (drop n (0) c (CTail e (Bind Abst) u)) &
+ (ty0 g e u t)
+ ).
+
+(*#* #stop proof *)
+
+ Intros until 1; InsertEq H '(TBRef n); XElim H; Intros.
+(* case 1 : ty0_conv *)
+ LApply H2; [ Clear H2; Intros H2 | XAuto ].
+ XElim H2; Intros; XElim H2; XEAuto.
+(* case 2 : ty0_sort *)
+ Inversion H0.
+(* case 3 : ty0_abbr *)
+ Inversion H3 ; Rewrite H5 in H0; XEAuto.
+(* case 4 : ty0_abst *)
+ Inversion H3; Rewrite H5 in H0; XEAuto.
+(* case 5 : ty0_bind *)
+ Inversion H5.
+(* case 6 : ty0_appl *)
+ Inversion H3.
+(* case 7 : ty0_cast *)
+ Inversion H3.
+ Qed.
+
+(*#* #start proof *)
+
+(*#* #caption "generation lemma for binder" *)
+(*#* #cap #cap c #alpha x in T, t1 in U1, t2 in U2, u in V, t in U, t0 in U3 *)
+
+ Theorem ty0_gen_bind: (g:?; b:?; c:?; u,t1,x:?) (ty0 g c (TTail (Bind b) u t1) x) ->
+ (EX t2 t t0 | (pc3 c (TTail (Bind b) u t2) x) &
+ (ty0 g c u t) &
+ (ty0 g (CTail c (Bind b) u) t1 t2) &
+ (ty0 g (CTail c (Bind b) u) t2 t0)
+ ).
+
+(*#* #stop proof *)
+
+ Intros until 1; InsertEq H '(TTail (Bind b) u t1); XElim H; Intros.
+(* case 1 : ty0_conv *)
+ LApply H2; [ Clear H2; Intros H2 | XAuto ].
+ XElim H2; XEAuto.
+(* case 2 : ty0_sort *)
+ Inversion H0.
+(* case 3 : ty0_abbr *)
+ Inversion H3.
+(* case 4 : ty0_abst *)
+ Inversion H3.
+(* case 5 : ty0_bind *)
+ Inversion H5.
+ Rewrite H7 in H1; Rewrite H7 in H3.
+ Rewrite H8 in H; Rewrite H8 in H1; Rewrite H8 in H3.
+ Rewrite H9 in H1; XEAuto.
+(* case 6 : ty0_appl *)
+ Inversion H3.
+(* case 7 : ty0_cast *)
+ Inversion H3.
+ Qed.
+
+(*#* #start proof *)
+
+(*#* #caption "generation lemma for application" *)
+(*#* #cap #cap c #alpha x in T, v in U1, w in V1, u in V2, t in U2 *)
+
+ Theorem ty0_gen_appl: (g:?; c:?; w,v,x:?) (ty0 g c (TTail (Flat Appl) w v) x) ->
+ (EX u t | (pc3 c (TTail (Flat Appl) w (TTail (Bind Abst) u t)) x) &
+ (ty0 g c v (TTail (Bind Abst) u t)) &
+ (ty0 g c w u)
+ ).
+
+(*#* #stop proof *)
+
+ Intros until 1; InsertEq H '(TTail (Flat Appl) w v); XElim H; Intros.
+(* case 1 : ty0_conv *)
+ LApply H2; [ Clear H2; Intros H2 | XAuto ].
+ XElim H2; XEAuto.
+(* case 2 : ty0_sort *)
+ Inversion H0.
+(* case 3 : ty0_abbr *)
+ Inversion H3.
+(* case 4 : ty0_abst *)
+ Inversion H3.
+(* case 5 : ty0_bind *)
+ Inversion H5.
+(* case 6 : ty0_appl *)
+ Inversion H3; Rewrite H5 in H; Rewrite H6 in H1; XEAuto.
+(* case 7 : ty0_cast *)
+ Inversion H3.
+ Qed.
+
+(*#* #start proof *)
+
+(*#* #caption "generation lemma for cast" *)
+(*#* #cap #cap c #alpha x in T, t2 in V, t1 in U *)
+
+ Theorem ty0_gen_cast: (g:?; c:?; t1,t2,x:?)
+ (ty0 g c (TTail (Flat Cast) t2 t1) x) ->
+ (pc3 c t2 x) /\ (ty0 g c t1 t2).
+
+(*#* #stop proof *)
+
+ Intros until 1; InsertEq H '(TTail (Flat Cast) t2 t1); XElim H; Intros.
+(* case 1 : ty0_conv *)
+ LApply H2; [ Clear H2; Intros H2 | XAuto ].
+ XElim H2; XEAuto.
+(* case 2 : ty0_sort *)
+ Inversion H0.
+(* case 3 : ty0_abbr *)
+ Inversion H3.
+(* case 4 : ty0_abst *)
+ Inversion H3.
+(* case 5 : ty0_bind *)
+ Inversion H5.
+(* case 6 : ty0_appl *)
+ Inversion H3.
+(* case 7 : ty0_cast *)
+ Inversion H3; Rewrite H5 in H; Rewrite H5 in H1; Rewrite H6 in H; XAuto.
+ Qed.
+
+ End ty0_gen_base.
+
+ Tactic Definition Ty0GenBase :=
+ Match Context With
+ | [ H: (ty0 ?1 ?2 (TSort ?3) ?4) |- ? ] ->
+ LApply (ty0_gen_sort ?1 ?2 ?4 ?3); [ Clear H; Intros | XAuto ]
+ | [ H: (ty0 ?1 ?2 (TBRef ?3) ?4) |- ? ] ->
+ LApply (ty0_gen_bref ?1 ?2 ?4 ?3); [ Clear H; Intros H | XAuto ];
+ XElim H; Intros H; XElim H; Intros
+ | [ H: (ty0 ?1 ?2 (TTail (Bind ?3) ?4 ?5) ?6) |- ? ] ->
+ LApply (ty0_gen_bind ?1 ?3 ?2 ?4 ?5 ?6); [ Clear H; Intros H | XAuto ];
+ XElim H; Intros
+ | [ H: (ty0 ?1 ?2 (TTail (Flat Appl) ?3 ?4) ?5) |- ? ] ->
+ LApply (ty0_gen_appl ?1 ?2 ?3 ?4 ?5); [ Clear H; Intros H | XAuto ];
+ XElim H; Intros
+ | [ H: (ty0 ?1 ?2 (TTail (Flat Cast) ?3 ?4) ?5) |- ? ] ->
+ LApply (ty0_gen_cast ?1 ?2 ?4 ?3 ?5); [ Clear H; Intros H | XAuto ];
+ XElim H; Intros.
+
+ Section wf0_props. (******************************************************)
+
+ Theorem wf0_ty0 : (g:?; c:?; u,t:?) (ty0 g c u t) -> (wf0 g c).
+ Intros; XElim H; XAuto.
+ Qed.
+
+ Hints Resolve wf0_ty0 : ltlc.
+
+ Theorem wf0_drop_O : (c,e:?; h:?) (drop h (0) c e) ->
+ (g:?) (wf0 g c) -> (wf0 g e).
+ XElim c.
+(* case 1 : CSort *)
+ Intros; DropGenBase; Rewrite H; XAuto.
+(* case 2 : CTail k *)
+ Intros c IHc; XElim k; (
+ XElim h; Intros; DropGenBase;
+ [ Rewrite H in H0; XAuto | Inversion H1; XEAuto ] ).
+ Qed.
+
+ End wf0_props.
+
+ Hints Resolve wf0_ty0 wf0_drop_O : ltlc.
+
+ Tactic Definition Wf0Ty0 :=
+ Match Context With
+ [ _: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
+ LApply (wf0_ty0 ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
+ Inversion_clear H_x.
+
+ Tactic Definition Wf0DropO :=
+ Match Context With
+ | [ _: (drop ?1 (0) ?2 ?3); _: (wf0 ?4 ?2) |- ? ] ->
+ LApply (wf0_drop_O ?2 ?3 ?1); [ Intros H_x | XAuto ];
+ LApply (H_x ?4); [ Clear H_x; Intros | XAuto ].
+
+ Section wf0_facilities. (*************************************************)
+
+ Theorem wf0_drop_wf0 : (g:?; c:?) (wf0 g c) ->
+ (b:?; e:?; u:?; h:?)
+ (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
+ Intros.
+ Wf0DropO; Inversion H1; XEAuto.
+ Qed.
+
+ Theorem ty0_drop_wf0 : (g:?; c:?; t1,t2:?) (ty0 g c t1 t2) ->
+ (b:?; e:?; u:?; h:?)
+ (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
+ Intros.
+ EApply wf0_drop_wf0; [ Idtac | EApply H0 ]; XEAuto.
+ Qed.
+
+ End wf0_facilities.
+
+ Hints Resolve wf0_drop_wf0 ty0_drop_wf0 : ltlc.
+
+ Tactic Definition DropWf0 :=
+ Match Context With
+ | [ _: (ty0 ?1 ?2 ?3 ?4);
+ _: (drop ?5 (0) ?2 (CTail ?6 (Bind ?7) ?8)) |- ? ] ->
+ LApply (ty0_drop_wf0 ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
+ LApply (H_x ?7 ?6 ?8 ?5); [ Clear H_x; Intros | XAuto ]
+ | [ _: (wf0 ?1 ?2);
+ _: (drop ?5 (0) ?2 (CTail ?6 (Bind ?7) ?8)) |- ? ] ->
+ LApply (wf0_drop_wf0 ?1 ?2); [ Intros H_x | XAuto ];
+ LApply (H_x ?7 ?6 ?8 ?5); [ Clear H_x; Intros | XAuto ].
+
+(*#* #start file *)
+
+(*#* #single *)
projects / helm.git / blobdiff