helm/coq-contribs/LAMBDA-TYPES/pr0_confluence.v

   1 (*#* #stop file *)
   2
   3 Require tlt_defs.
   4 Require lift_gen.
   5 Require lift_tlt.
   6 Require subst0_gen.
   7 Require subst0_confluence.
   8 Require pr0_defs.
   9 Require pr0_lift.
  10 Require pr0_gen.
  11 Require pr0_subst0.
  12
  13    Section pr0_confluence. (*************************************************)
  14
  15       Tactic Definition SSubstInv :=
  16          Match Context With
  17             | [ H0: (TTail ? ? ?) = (TTail ? ? ?) |- ? ] ->
  18                Inversion H0; Clear H0
  19             | [ H0: (pr0 (TTail (Bind ?) ? ?) ?) |- ? ] ->
  20                Inversion H0; Clear H0
  21             | _ -> EqFalse Orelse LiftGen Orelse Pr0Gen.
  22
  23       Tactic Definition SSubstBack :=
  24          Match Context With
  25             | [ H0: Abst = ?1; H1:? |- ? ] ->
  26                Rewrite <- H0 in H1 Orelse Rewrite <- H0 Orelse Clear H0 ?1
  27             | [ H0: Abbr = ?1; H1:? |- ? ] ->
  28                Rewrite <- H0 in H1 Orelse Rewrite <- H0 Orelse Clear H0 ?1
  29             | [ H0: (? ?) = ?1; H1:? |- ? ] ->
  30                Rewrite <- H0 in H1 Orelse Rewrite <- H0 Orelse Clear H0 ?1
  31             | [ H0: (? ? ? ?) = ?1; H1:? |- ? ] ->
  32                Rewrite <- H0 in H1 Orelse Rewrite <- H0 Orelse Clear H0 ?1.
  33
  34       Tactic Definition SSubst :=
  35          Match Context With
  36             [ H0: ?1 = ?; H1:? |- ? ] ->
  37                Rewrite H0 in H1 Orelse Rewrite H0 Orelse Clear H0 ?1.
  38
  39       Tactic Definition XSubst :=
  40          Repeat (SSubstInv Orelse SSubstBack Orelse SSubst).
  41
  42       Tactic Definition IH :=
  43          Match Context With
  44             | [ H0: (pr0 ?1 ?2); H1: (pr0 ?1 ?3) |- ? ] ->
  45                LApply (H ?1); [ Intros H_x | XEAuto ];
  46                LApply (H_x ?2); [ Clear H_x; Intros H_x | XAuto ];
  47                LApply (H_x ?3); [ Clear H_x; Intros H_x | XAuto ];
  48                XElim H_x; Clear H0 H1; Intros.
  49
  50 (* case pr0_cong pr0_upsilon pr0_refl ***************************************)
  51
  52       Remark pr0_cong_upsilon_refl: (b:?) ~ b = Abst ->
  53                                     (u0,u3:?) (pr0 u0 u3) ->
  54                                     (t4,t5:?) (pr0 t4 t5) ->
  55                                     (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
  56                                     (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind b) u0 t4)) t) &
  57                                               (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
  58       Intros.
  59       Apply ex2_intro with x:=(TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) x) t5)); XAuto.
  60       Qed.
  61
  62 (* case pr0_cong pr0_upsilon pr0_cong ***************************************)
  63
  64       Remark pr0_cong_upsilon_cong: (b:?) ~ b = Abst ->
  65                                     (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
  66                                     (t2,t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) ->
  67                                     (u5,u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) ->
  68                                     (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind b) u5 t2)) t) &
  69                                               (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
  70       Intros.
  71       Apply ex2_intro with x:=(TTail (Bind b) x1 (TTail (Flat Appl) (lift (1) (0) x) x0)); XAuto.
  72       Qed.
  73
  74 (* case pr0_cong pr0_upsilon pr0_delta **************************************)
  75
  76       Remark pr0_cong_upsilon_delta: ~ Abbr = Abst ->
  77                                      (u5,t2,w:?) (subst0 (0) u5 t2 w) ->
  78                                      (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) ->
  79                                      (t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) ->
  80                                      (u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) ->
  81                                      (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind Abbr) u5 w)) t) &
  82                                                (pr0 (TTail (Bind Abbr) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)).
  83       Intros; Pr0Subst0.
  84 (* case 1: x0 is a lift *)
  85       Apply ex2_intro with x:=(TTail (Bind Abbr) x1 (TTail (Flat Appl) (lift (1) (0) x) x0)); XAuto.
  86 (* case 2: x0 is not a lift *)
  87       Apply ex2_intro with x:=(TTail (Bind Abbr) x1 (TTail (Flat Appl) (lift (1) (0) x) x2)); XEAuto.
  88       Qed.
  89
  90 (* case pr0_cong pr0_upsilon pr0_zeta ***************************************)
  91
  92       Remark pr0_cong_upsilon_zeta: (b:?) ~ b = Abst ->
  93                                     (u0,u3:?) (pr0 u0 u3) ->
  94                                     (u2,v2,x0:?) (pr0 u2 x0) -> (pr0 v2 x0) ->
  95                                     (x,t3,x1:?) (pr0 x x1) -> (pr0 t3 x1) ->
  96                                     (EX t:T | (pr0 (TTail (Flat Appl) u2 t3) t) &
  97                                               (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) (lift (1) (0) x))) t)).
  98       Intros; LiftTailRwBack; XEAuto.
  99       Qed.
 100
 101 (* case pr0_cong pr0_delta **************************************************)
 102
 103       Remark pr0_cong_delta: (u3,t5,w:?) (subst0 (0) u3 t5 w) ->
 104                              (u2,x:?) (pr0 u2 x) -> (pr0 u3 x) ->
 105                              (t3,x0:?) (pr0 t3 x0) -> (pr0 t5 x0) ->
 106                              (EX t:T | (pr0 (TTail (Bind Abbr) u2 t3) t) &
 107                                        (pr0 (TTail (Bind Abbr) u3 w) t)).
 108       Intros; Pr0Subst0; XEAuto.
 109       Qed.
 110
 111 (* case pr0_upsilon pr0_upsilon *********************************************)
 112
 113       Remark pr0_upsilon_upsilon: (b:?) ~ b = Abst ->
 114                                   (v1,v2,x0:?) (pr0 v1 x0) -> (pr0 v2 x0) ->
 115                                   (u1,u2,x1:?) (pr0 u1 x1) -> (pr0 u2 x1) ->
 116                                   (t1,t2,x2:?) (pr0 t1 x2) -> (pr0 t2 x2) ->
 117                                   (EX t:T | (pr0 (TTail (Bind b) u1 (TTail (Flat Appl) (lift (1) (0) v1) t1)) t) &
 118                                             (pr0 (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)) t)).
 119       Intros.
 120       Apply ex2_intro with x:=(TTail (Bind b) x1 (TTail (Flat Appl) (lift (1) (0) x0) x2)); XAuto.
 121       Qed.
 122
 123 (* case pr0_delta pr0_delta *************************************************)
 124
 125       Remark pr0_delta_delta: (u2,t3,w:?) (subst0 (0) u2 t3 w) ->
 126                               (u3,t5,w0:?) (subst0 (0) u3 t5 w0) ->
 127                               (x:?) (pr0 u2 x) -> (pr0 u3 x) ->
 128                               (x0:?) (pr0 t3 x0) -> (pr0 t5 x0) ->
 129                               (EX t:T | (pr0 (TTail (Bind Abbr) u2 w) t) &
 130                                         (pr0 (TTail (Bind Abbr) u3 w0) t)).
 131       Intros; Pr0Subst0; Pr0Subst0; Try Subst0Confluence; XSubst; XEAuto.
 132       Qed.
 133
 134 (* case pr0_delta pr0_epsilon ***********************************************)
 135
 136       Remark pr0_delta_epsilon: (u2,t3,w:?) (subst0 (0) u2 t3 w) ->
 137                                 (t4:?) (pr0 (lift (1) (0) t4) t3) ->
 138                                 (t2:?) (EX t:T | (pr0 (TTail (Bind Abbr) u2 w) t) & (pr0 t2 t)).
 139       Intros; Pr0Gen; XSubst; Subst0Gen.
 140       Qed.
 141
 142 (* main *********************************************************************)
 143
 144       Hints Resolve pr0_cong_upsilon_refl pr0_cong_upsilon_cong : ltlc.
 145       Hints Resolve pr0_cong_upsilon_delta pr0_cong_upsilon_zeta : ltlc.
 146       Hints Resolve pr0_cong_delta : ltlc.
 147       Hints Resolve pr0_upsilon_upsilon : ltlc.
 148       Hints Resolve pr0_delta_delta pr0_delta_epsilon : ltlc.
 149
 150 (*#* #start file *)
 151
 152 (*#* #caption "confluence with itself: Church-Rosser property" *)
 153 (*#* #cap #cap t0, t1, t2, t *)
 154
 155       Theorem pr0_confluence: (t0,t1:?) (pr0 t0 t1) -> (t2:?) (pr0 t0 t2) ->
 156                               (EX t | (pr0 t1 t) & (pr0 t2 t)).
 157
 158 (*#* #stop file *)
 159
 160       XElimUsing tlt_wf_ind t0; Intros.
 161       Inversion H0; Inversion H1; Clear H0 H1;
 162       XSubst; Repeat IH; XDEAuto 4.
 163       Qed.
 164
 165    End pr0_confluence.
 166
 167       Tactic Definition Pr0Confluence :=
 168          Match Context With
 169             [ H1: (pr0 ?1 ?2); H2: (pr0 ?1 ?3) |-? ] ->
 170                LApply (pr0_confluence ?1 ?2); [ Clear H1; Intros H1 | XAuto ];
 171                LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ];
 172                XElim H1; Intros.
 173
 174 (*#* #start file *)
 175
 176 (*#* #single *)