Require subst0_subst0.
Require pr0_subst0.
+Require cpr0_defs.
Require pr3_defs.
Require pr3_props.
Require pr3_confluence.
-Require cpr0_defs.
-Require cpr0_props.
Require pc3_defs.
- Section pc3_confluence. (*************************************************)
+ Section pc3_trans. (******************************************************)
- Theorem pc3_confluence : (c:?; t1,t2:?) (pc3 c t1 t2) ->
- (EX t0 | (pr3 c t1 t0) & (pr3 c t2 t0)).
- Intros; XElim H; Intros.
-(* case 1 : pc3_r *)
- XEAuto.
-(* case 2 : pc3_u *)
- Clear H0; XElim H1; Intros.
- Inversion_clear H; [ XEAuto | Pr3Confluence; XEAuto ].
+ Theorem pc3_t: (t2,c,t1:?) (pc3 c t1 t2) ->
+ (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
+ Intros; Repeat Pc3Unfold; Pr3Confluence; XEAuto.
Qed.
- End pc3_confluence.
+ Theorem pc3_pr2_u2: (c:?; t0,t1:?) (pr2 c t0 t1) ->
+ (t2:?) (pc3 c t0 t2) -> (pc3 c t1 t2).
+ Intros; Apply (pc3_t t0); XAuto.
+ Qed.
- Tactic Definition Pc3Confluence :=
+ Theorem pc3_tail_12: (c:?; u1,u2:?) (pc3 c u1 u2) ->
+ (k:?; t1,t2:?) (pc3 (CTail c k u2) t1 t2) ->
+ (pc3 c (TTail k u1 t1) (TTail k u2 t2)).
+ Intros.
+ EApply pc3_t; [ Apply pc3_tail_1 | Apply pc3_tail_2 ]; XAuto.
+ Qed.
+
+ Theorem pc3_tail_21: (c:?; u1,u2:?) (pc3 c u1 u2) ->
+ (k:?; t1,t2:?) (pc3 (CTail c k u1) t1 t2) ->
+ (pc3 c (TTail k u1 t1) (TTail k u2 t2)).
+ Intros.
+ EApply pc3_t; [ Apply pc3_tail_2 | Apply pc3_tail_1 ]; XAuto.
+ Qed.
+
+ End pc3_trans.
+
+ Hints Resolve pc3_t pc3_tail_12 pc3_tail_21 : ltlc.
+
+ Tactic Definition Pc3T :=
Match Context With
- [ H: (pc3 ?1 ?2 ?3) |- ? ] ->
- LApply (pc3_confluence ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
- XElim H; Intros.
+ | [ _: (pr3 ?1 ?2 (TTail ?3 ?4 ?5)); _: (pc3 ?1 ?6 ?4) |- ? ] ->
+ LApply (pc3_t (TTail ?3 ?4 ?5) ?1 ?2); [ Intros H_x | XAuto ];
+ LApply (H_x (TTail ?3 ?6 ?5)); [ Clear H_x; Intros | Apply pc3_s; XAuto ]
+ | [ _: (pc3 ?1 ?2 ?3); _: (pr3 ?1 ?3 ?4) |- ? ] ->
+ LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
+ LApply (H_x ?4); [ Clear H_x; Intros | XAuto ]
+ | [ _: (pc3 ?1 ?2 ?3); _: (pc3 ?1 ?4 ?3) |- ? ] ->
+ LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
+ LApply (H_x ?4); [ Clear H_x; Intros | XAuto ].
Section pc3_context. (****************************************************)
- Theorem pc3_pr0_pr2_t : (u1,u2:?) (pr0 u2 u1) ->
- (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
- (pc3 (CTail c k u1) t1 t2).
+ Theorem pc3_pr0_pr2_t: (u1,u2:?) (pr0 u2 u1) ->
+ (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
+ (pc3 (CTail c k u1) t1 t2).
Intros.
Inversion H0; Clear H0; [ XAuto | NewInduction i ].
-(* case 1 : pr2_delta i = 0 *)
- DropGenBase; Inversion H0; Clear H0 H3 H4 c k.
- Rewrite H5 in H; Clear H5 u2.
- Pr0Subst0; XEAuto.
-(* case 2 : pr2_delta i > 0 *)
+(* case 1: pr2_delta i = 0 *)
+ DropGenBase; Inversion H0; Clear H0 H4 H5 H6 c k t.
+ Rewrite H7 in H; Clear H7 u2.
+ Pr0Subst0; Apply pc3_pr3_t with t0:=x; XEAuto.
+(* case 2: pr2_delta i > 0 *)
NewInduction k; DropGenBase; XEAuto.
Qed.
- Theorem pc3_pr2_pr2_t : (c:?; u1,u2:?) (pr2 c u2 u1) ->
- (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
- (pc3 (CTail c k u1) t1 t2).
+ Theorem pc3_pr2_pr2_t: (c:?; u1,u2:?) (pr2 c u2 u1) ->
+ (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
+ (pc3 (CTail c k u1) t1 t2).
Intros until 1; Inversion H; Clear H; Intros.
-(* case 1 : pr2_pr0 *)
+(* case 1: pr2_free *)
EApply pc3_pr0_pr2_t; [ Apply H0 | XAuto ].
-(* case 2 : pr2_delta *)
+(* case 2: pr2_delta *)
Inversion H; [ XAuto | NewInduction i0 ].
-(* case 2.1 : i0 = 0 *)
- DropGenBase; Inversion H2; Clear H2.
- Rewrite <- H5; Rewrite H6 in H; Rewrite <- H7 in H3; Clear H5 H6 H7 d0 k u0.
- Subst0Subst0; Arith9'In H4 i.
- EApply pc3_pr3_u.
+(* case 2.1: i0 = 0 *)
+ DropGenBase; Inversion H4; Clear H3 H4 H7 t t4.
+ Rewrite <- H9; Rewrite H10 in H; Rewrite <- H11 in H6; Clear H9 H10 H11 d0 k u0.
+ Pr0Subst0; Subst0Subst0; Arith9'In H6 i.
+ EApply pc3_pr2_u.
EApply pr2_delta; XEAuto.
- Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XEAuto ]; XEAuto.
-(* case 2.2 : i0 > 0 *)
+ Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XEAuto | XEAuto ]; XEAuto.
+(* case 2.2: i0 > 0 *)
Clear IHi0; NewInduction k; DropGenBase; XEAuto.
Qed.
- Theorem pc3_pr2_pr3_t : (c:?; u2,t1,t2:?; k:?)
- (pr3 (CTail c k u2) t1 t2) ->
- (u1:?) (pr2 c u2 u1) ->
- (pc3 (CTail c k u1) t1 t2).
+ Theorem pc3_pr2_pr3_t: (c:?; u2,t1,t2:?; k:?)
+ (pr3 (CTail c k u2) t1 t2) ->
+ (u1:?) (pr2 c u2 u1) ->
+ (pc3 (CTail c k u1) t1 t2).
Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1: pr3_refl *)
XAuto.
-(* case 2 : pr3_u *)
+(* case 2: pr3_sing *)
EApply pc3_t.
EApply pc3_pr2_pr2_t; [ Apply H2 | Apply H ].
XAuto.
Qed.
- Theorem pc3_pr3_pc3_t : (c:?; u1,u2:?) (pr3 c u2 u1) ->
- (t1,t2:?; k:?) (pc3 (CTail c k u2) t1 t2) ->
- (pc3 (CTail c k u1) t1 t2).
+ Theorem pc3_pr3_pc3_t: (c:?; u1,u2:?) (pr3 c u2 u1) ->
+ (t1,t2:?; k:?) (pc3 (CTail c k u2) t1 t2) ->
+ (pc3 (CTail c k u1) t1 t2).
Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1: pr3_refl *)
XAuto.
-(* case 2 : pr3_u *)
- Apply H1; Pc3Confluence.
+(* case 2: pr3_sing *)
+ Apply H1; Pc3Unfold.
EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_pr2_pr3_t; XEAuto.
Qed.
Section pc3_lift. (*******************************************************)
- Theorem pc3_lift : (c,e:?; h,d:?) (drop h d c e) ->
- (t1,t2:?) (pc3 e t1 t2) ->
- (pc3 c (lift h d t1) (lift h d t2)).
+ Theorem pc3_lift: (c,e:?; h,d:?) (drop h d c e) ->
+ (t1,t2:?) (pc3 e t1 t2) ->
+ (pc3 c (lift h d t1) (lift h d t2)).
Intros.
- Pc3Confluence.
- EApply pc3_pr3_t; (EApply pr3_lift; [ XEAuto | Apply H0 Orelse Apply H1 ]).
+ Pc3Unfold.
+ EApply pc3_pr3_t; (EApply pr3_lift; [ XEAuto | Apply H1 Orelse Apply H2 ]).
Qed.
End pc3_lift.
Section pc3_cpr0. (*******************************************************)
- Remark pc3_cpr0_t_aux : (c1,c2:?) (cpr0 c1 c2) ->
- (k:?; u,t1,t2:?) (pr3 (CTail c1 k u) t1 t2) ->
- (pc3 (CTail c2 k u) t1 t2).
+ Remark pc3_cpr0_t_aux: (c1,c2:?) (cpr0 c1 c2) ->
+ (k:?; u,t1,t2:?) (pr3 (CTail c1 k u) t1 t2) ->
+ (pc3 (CTail c2 k u) t1 t2).
Intros; XElim H0; Intros.
-(* case 1.1 : pr3_r *)
+(* case 1.1: pr3_refl *)
XAuto.
-(* case 1.2 : pr3_u *)
+(* case 1.2: pr3_sing *)
EApply pc3_t; [ Idtac | XEAuto ]. Clear H2 t1 t2.
Inversion_clear H0.
-(* case 1.2.1 : pr2_pr0 *)
+(* case 1.2.1: pr2_free *)
XAuto.
-(* case 1.2.2 : pr2_delta *)
+(* case 1.2.2: pr2_delta *)
Cpr0Drop; Pr0Subst0.
- EApply pc3_pr3_u; [ EApply pr2_delta; XEAuto | XAuto ].
+ EApply pc3_pr2_u; [ EApply pr2_delta; XEAuto | XAuto ].
Qed.
- Theorem pc3_cpr0_t : (c1,c2:?) (cpr0 c1 c2) ->
- (t1,t2:?) (pr3 c1 t1 t2) ->
- (pc3 c2 t1 t2).
+ Theorem pc3_cpr0_t: (c1,c2:?) (cpr0 c1 c2) ->
+ (t1,t2:?) (pr3 c1 t1 t2) ->
+ (pc3 c2 t1 t2).
Intros until 1; XElim H; Intros.
-(* case 1 : cpr0_refl *)
+(* case 1: cpr0_refl *)
XAuto.
-(* case 2 : cpr0_cont *)
- Pc3Context; Pc3Confluence.
+(* case 2: cpr0_comp *)
+ Pc3Context; Pc3Unfold.
EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t_aux; XEAuto.
Qed.
- Theorem pc3_cpr0 : (c1,c2:?) (cpr0 c1 c2) -> (t1,t2:?) (pc3 c1 t1 t2) ->
- (pc3 c2 t1 t2).
- Intros; Pc3Confluence.
+ Theorem pc3_cpr0: (c1,c2:?) (cpr0 c1 c2) -> (t1,t2:?) (pc3 c1 t1 t2) ->
+ (pc3 c2 t1 t2).
+ Intros; Pc3Unfold.
EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t; XEAuto.
Qed.
End pc3_cpr0.
Hints Resolve pc3_cpr0 : ltlc.
+
+ Section pc3_ind_left. (***************************************************)
+
+ Inductive pc3_left [c:C] : T -> T -> Prop :=
+ | pc3_left_r : (t:?) (pc3_left c t t)
+ | pc3_left_ur: (t1,t2:?) (pr2 c t1 t2) -> (t3:?) (pc3_left c t2 t3) ->
+ (pc3_left c t1 t3)
+ | pc3_left_ux: (t1,t2:?) (pr2 c t1 t2) -> (t3:?) (pc3_left c t1 t3) ->
+ (pc3_left c t2 t3).
+
+ Hint pc3_left: ltlc := Constructors pc3_left.
+
+ Remark pc3_left_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) -> (pc3_left c t1 t2).
+ Intros; XElim H; XEAuto.
+ Qed.
+
+ Remark pc3_left_trans: (c:?; t1,t2:?) (pc3_left c t1 t2) ->
+ (t3:?) (pc3_left c t2 t3) -> (pc3_left c t1 t3).
+ Intros until 1; XElim H; XEAuto.
+ Qed.
+
+ Hints Resolve pc3_left_trans : ltlc.
+
+ Remark pc3_left_sym: (c:?; t1,t2:?) (pc3_left c t1 t2) ->
+ (pc3_left c t2 t1).
+ Intros; XElim H; XEAuto.
+ Qed.
+
+ Hints Resolve pc3_left_sym pc3_left_pr3 : ltlc.
+
+ Remark pc3_left_pc3: (c:?; t1,t2:?) (pc3 c t1 t2) -> (pc3_left c t1 t2).
+ Intros; Pc3Unfold; XEAuto.
+ Qed.
+
+ Remark pc3_pc3_left: (c:?; t1,t2:?) (pc3_left c t1 t2) -> (pc3 c t1 t2).
+ Intros; XElim H; XEAuto.
+ Qed.
+
+ Hints Resolve pc3_left_pc3 pc3_pc3_left : ltlc.
+
+ Theorem pc3_ind_left: (c:C; P:(T->T->Prop))
+ ((t:T) (P t t)) ->
+ ((t1,t2:T) (pr2 c t1 t2) -> (t3:T) (pc3 c t2 t3) -> (P t2 t3) -> (P t1 t3)) ->
+ ((t1,t2:T) (pr2 c t1 t2) -> (t3:T) (pc3 c t1 t3) -> (P t1 t3) -> (P t2 t3)) ->
+ (t,t0:T) (pc3 c t t0) -> (P t t0).
+ Intros; ElimType (pc3_left c t t0); XEAuto.
+ Qed.
+
+ End pc3_ind_left.
projects / helm.git / blobdiff