-(*#* #stop file *)
-
Require Export subst0_defs.
+(*#* #caption "axioms for the relation $\\PrZ{}{}$",
+ "reflexivity", "compatibility", "$\\beta$-contraction", "$\\upsilon$-swap",
+ "$\\delta$-expansion", "$\\zeta$-contraction", "$\\epsilon$-contraction"
+*)
+(*#* #cap #cap t, t1, t2 #alpha u in V, u1 in V1, u2 in V2, v1 in W1, v2 in W2, w in T, k in z *)
+
Inductive pr0 : T -> T -> Prop :=
(* structural rules *)
- | pr0_refl : (t:?) (pr0 t t)
- | pr0_thin : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
- (k:?) (pr0 (TTail k u1 t1) (TTail k u2 t2))
+ | pr0_refl : (t:?) (pr0 t t)
+ | pr0_comp : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
+ (k:?) (pr0 (TTail k u1 t1) (TTail k u2 t2))
(* axiom rules *)
- | pr0_beta : (k,v1,v2:?) (pr0 v1 v2) -> (t1,t2:?) (pr0 t1 t2) ->
- (pr0 (TTail (Flat Appl) v1 (TTail (Bind Abst) k t1))
- (TTail (Bind Abbr) v2 t2))
- | pr0_gamma : (b:?) ~b=Abst -> (v1,v2:?) (pr0 v1 v2) ->
- (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
- (pr0 (TTail (Flat Appl) v1 (TTail (Bind b) u1 t1))
- (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)))
- | pr0_delta : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
- (w:?) (subst0 (0) u2 t2 w) ->
- (pr0 (TTail (Bind Abbr) u1 t1) (TTail (Bind Abbr) u2 w))
- | pr0_zeta : (b:?) ~b=Abst -> (t1,t2:?) (pr0 t1 t2) ->
- (u:?) (pr0 (TTail (Bind b) u (lift (1) (0) t1)) t2)
- | pr0_eps : (t1,t2:?) (pr0 t1 t2) ->
- (u:?) (pr0 (TTail (Flat Cast) u t1) t2).
+ | pr0_beta : (u,v1,v2:?) (pr0 v1 v2) -> (t1,t2:?) (pr0 t1 t2) ->
+ (pr0 (TTail (Flat Appl) v1 (TTail (Bind Abst) u t1))
+ (TTail (Bind Abbr) v2 t2))
+ | pr0_upsilon: (b:?) ~b=Abst -> (v1,v2:?) (pr0 v1 v2) ->
+ (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
+ (pr0 (TTail (Flat Appl) v1 (TTail (Bind b) u1 t1))
+ (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)))
+ | pr0_delta : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
+ (w:?) (subst0 (0) u2 t2 w) ->
+ (pr0 (TTail (Bind Abbr) u1 t1) (TTail (Bind Abbr) u2 w))
+ | pr0_zeta : (b:?) ~b=Abst -> (t1,t2:?) (pr0 t1 t2) ->
+ (u:?) (pr0 (TTail (Bind b) u (lift (1) (0) t1)) t2)
+ | pr0_epsilon: (t1,t2:?) (pr0 t1 t2) ->
+ (u:?) (pr0 (TTail (Flat Cast) u t1) t2).
+
+(*#* #stop file *)
Hint pr0 : ltlc := Constructors pr0.
- Section pr0_gen. (********************************************************)
+ Section pr0_gen_base. (***************************************************)
Theorem pr0_gen_sort : (x:?; n:?) (pr0 (TSort n) x) -> x = (TSort n).
Intros; Inversion H; XAuto.
Qed.
- Theorem pr0_gen_bref : (x:?; n:?) (pr0 (TBRef n) x) -> x = (TBRef n).
+ Theorem pr0_gen_lref : (x:?; n:?) (pr0 (TLRef n) x) -> x = (TLRef n).
Intros; Inversion H; XAuto.
Qed.
Intros; Inversion H; XEAuto.
Qed.
- End pr0_gen.
+ End pr0_gen_base.
- Hints Resolve pr0_gen_sort pr0_gen_bref : ltlc.
+ Hints Resolve pr0_gen_sort pr0_gen_lref : ltlc.
Tactic Definition Pr0GenBase :=
Match Context With
- | [ H: (pr0 (TTail (Bind Abst) ?1 ?2) ?3) |- ? ] ->
+ | [ H: (pr0 (TSort ?1) ?2) |- ? ] ->
+ LApply (pr0_gen_sort ?2 ?1); [ Clear H; Intros | XAuto ]
+ | [ H: (pr0 (TLRef ?1) ?2) |- ? ] ->
+ LApply (pr0_gen_lref ?2 ?1); [ Clear H; Intros | XAuto ]
+ | [ H: (pr0 (TTail (Bind Abst) ?1 ?2) ?3) |- ? ] ->
LApply (pr0_gen_abst ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
XElim H; Intros
| [ H: (pr0 (TTail (Flat Appl) ?1 ?2) ?3) |- ? ] ->