(*#* #stop record *)
Record G : Set := {
- f : nat -> nat;
- f_inc : (n:?) (lt n (f n))
+ next : nat -> nat;
+ base : nat;
+ next_lt : (n:?) (lt n (next n));
+ base_next: (n:?) (le base n) -> (next n) = (S n)
}.
(*#* #start record *)
-(*#* #caption "typing",
+(*#* #caption "current axioms for 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"
*)
+(*#* #cap #cap c, d, t, t0, t1, t2, w #alpha m in h, n in i, u in V, v in U *)
+
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))
+ | 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)
+ | 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 (TLRef 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 (TLRef 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).
+ | ty0_sort: (c:?) (wf0 g c) ->
+ (m:?) (ty0 g c (TSort m) (TSort (next 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 (TLRef 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 (TLRef 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).
+
+(*#* #stop file *)
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_lref: (g:?; c:?; x:?; n:?) (ty0 g c (TLRef 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 '(TLRef 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 (TLRef ?3) ?4) |- ? ] ->
- LApply (ty0_gen_lref ?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).
+ 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).
+ 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.
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).
+ 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).
+ 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.
_: (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