matita/matita/broken_lib/finite_lambda/confluence.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "finite_lambda/reduction.ma".
  13
  14
  15 axiom canonical_to_T: ∀O,D.∀M:T O D.∀ty.(* type_of M ty → *)
  16   ∃a:FinSet_of_FType O D ty. star ? (red O D) M (to_T O D ty a).
  17
  18 axiom normal_to_T: ∀O,D,M,ty,a. red O D (to_T O D ty a) M → False.
  19
  20 axiom red_closed: ∀O,D,M,M1.
  21   is_closed O D 0 M → red O D M M1 → is_closed O D 0 M1.
  22
  23 lemma critical: ∀O,D,ty,M,N.
  24   ∃M3:T O D
  25   .star (T O D) (red O D) (subst O D M 0 N) M3
  26    ∧star (T O D) (red O D)
  27     (App O D
  28      (Vec O D ty
  29       (map (FinSet_of_FType O D ty) (T O D)
  30        (λa0:FinSet_of_FType O D ty.subst O D M 0 (to_T O D ty a0))
  31        (enum (FinSet_of_FType O D ty)))) N) M3.
  32 #O #D #ty #M #N
  33 lapply (canonical_to_T O D N ty) * #a #Ha
  34 %{(subst O D M 0 (to_T O D ty a))} (* CR-term *)
  35 %[@red_star_subst @Ha
  36  |@trans_star [|@(star_red_appr … Ha)] @R_to_star @riota
  37   lapply (enum_complete (FinSet_of_FType O D ty) a)
  38   elim (enum (FinSet_of_FType O D ty))
  39    [normalize #H1 destruct (H1)
  40    |#hd #tl #Hind #H cases (orb_true_l … H) -H #Hcase
  41      [normalize >Hcase >(\P Hcase) //
  42      |normalize cases (true_or_false (a==hd)) #Hcase1
  43        [normalize >Hcase1 >(\P Hcase1) // |>Hcase1 @Hind @Hcase]
  44      ]
  45    ]
  46  ]
  47 qed.
  48
  49 lemma critical2: ∀O,D,ty,a,M,M1,M2,v.
  50   red O D (Vec O D ty v) M →
  51   red O D (App O D (Vec O D ty v) (to_T O D ty a)) M1 →
  52   assoc (FinSet_of_FType O D ty) (T O D) a (enum (FinSet_of_FType O D ty)) v
  53     =Some (T O D) M2 →
  54   ∃M3:T O D
  55   .star (T O D) (red O D) M2 M3
  56    ∧star (T O D) (red O D) (App O D M (to_T O D ty a)) M3.
  57 #O #D #ty #a #M #M1 #M2 #v #redM #redM1 #Ha lapply (red_vec … redM) -redM
  58 * #N * #N1 * #v1 * #v2 * * #Hred1 #Hv #HM0 >HM0 -HM0 >Hv in Ha; #Ha
  59 cases (same_assoc … a (enum (FinSet_of_FType O D ty)) v1 v2 N N1)
  60   [* >Ha -Ha #H1 destruct (H1) #Ha
  61    %{N1} (* CR-term *) % [@R_to_star //|@R_to_star @(riota … Ha)]
  62   |#Ha1 %{M2} (* CR-term *) % [// | @R_to_star @riota <Ha1 @Ha]
  63   ]
  64 qed.
  65
  66
  67 lemma critical3: ∀O,D,ty,M1,M2. red O D M1 M2 →
  68   ∃M3:T O D.star (T O D) (red O D) (Lambda O D ty M2) M3
  69    ∧star (T O D) (red O D)
  70     (Vec O D ty
  71      (map (FinSet_of_FType O D ty) (T O D)
  72       (λa:FinSet_of_FType O D ty.subst O D M1 0 (to_T O D ty a))
  73       (enum (FinSet_of_FType O D ty)))) M3.
  74 #O #D #ty #M1 #M2 #Hred
  75  %{(Vec O D ty
  76     (map (FinSet_of_FType O D ty) (T O D)
  77     (λa:FinSet_of_FType O D ty.subst O D M2 0 (to_T O D ty a))
  78     (enum (FinSet_of_FType O D ty))))} (* CR-term *) %
  79   [@R_to_star @rmem
  80   |@star_red_vec2 [>length_map >length_map //] #n #M0
  81    cases (true_or_false (leb (|enum (FinSet_of_FType O D ty)|) n)) #Hcase
  82     [>nth_to_default [2:>length_map @(leb_true_to_le … Hcase)]
  83      >nth_to_default [2:>length_map @(leb_true_to_le … Hcase)] //
  84     |cut (n < |enum (FinSet_of_FType O D ty)|)
  85       [@not_le_to_lt @leb_false_to_not_le @Hcase] #Hlt
  86      cut (∃a:FinSet_of_FType O D ty.True)
  87       [lapply Hlt lapply (enum_complete (FinSet_of_FType O D ty))
  88        cases (enum (FinSet_of_FType O D ty))
  89         [#_ normalize #H @False_ind @(absurd … H) @lt_to_not_le //
  90         |#a #l #_ #_ %{a} //
  91         ]
  92       ] * #a #_
  93      >(nth_map ?????? a Hlt) >(nth_map ?????? a Hlt) #_
  94      @red_star_subst2 //
  95     ]
  96   ]
  97 qed.
  98
  99 (* we need to proceed by structural induction on the term and then
 100 by inversion on the two redexes. The problem are the moves in a
 101 same subterm, since we need an induction hypothesis, there *)
 102
 103 lemma local_confluence: ∀O,D,M,M1,M2. red O D M M1 → red O D M M2 →
 104 ∃M3. star ? (red O D) M1 M3 ∧ star ? (red O D) M2 M3.
 105 #O #D #M @(T_elim … M)
 106   [#o #a #M1 #M2 #H elim(red_val ????? H)
 107   |#n #M1 #M2 #H elim(red_rel ???? H)
 108   |(* app : this is the interesting case *)
 109    #P #Q #HindP #HindQ
 110    #M1 #M2 #H1 inversion H1 -H1
 111     [(* right redex is beta *)
 112      #ty #Q #N #Hc #HM >HM -HM #HM1 >HM1 - HM1 #Hl inversion Hl
 113       [#ty1 #Q1 #N1 #Hc1 #H1 destruct (H1) #H_
 114        %{(subst O D Q1 0 N1)} (* CR-term *) /2/
 115       |#ty #v #a #M0 #_ #H1 destruct (H1) (* vacuous *)
 116       |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #_ cases (red_lambda … redM0)
 117         [* #Q1 * #redQ #HM10 >HM10
 118          %{(subst O D Q1 0 N0)} (* CR-term *) %
 119           [@red_star_subst2 //|@R_to_star @rbeta @Hc]
 120         |#HM1 >HM1 @critical
 121         ]
 122       |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #HM2
 123        %{(subst O D Q 0 N1)} (* CR-term *)
 124        %[@red_star_subst @R_to_star //|@R_to_star @rbeta @(red_closed … Hc) //]
 125       |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
 126       |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
 127       |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
 128       ]
 129     |(* right redex is iota *)#ty #v #a #M3 #Ha #_ #_ #Hl inversion Hl
 130       [#P1 #M1 #N1 #_ #H1 destruct (H1) (* vacuous *)
 131       |#ty1 #v1 #a1 #M4 #Ha1 #H1 destruct (H1) -H1 #HM4 >(inj_to_T … e0) in Ha;
 132        >Ha1 #H1 destruct (H1) %{M3} (* CR-term *) /2/
 133       |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2 @(critical2 … redM0 Hl Ha)
 134       |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) elim (normal_to_T … redN0N1)
 135       |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
 136       |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
 137       |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
 138       ]
 139     |(* right redex is appl *)#M3 #M4 #N #redM3M4 #_ #H1 destruct (H1) #_
 140       #Hl inversion Hl
 141       [#ty1 #M1 #N1 #Hc #H1 destruct (H1) #HM2 lapply (red_lambda … redM3M4) *
 142         [* #M3 * #H1 #H2 >H2 %{(subst O D M3 0 N1)} %
 143           [@R_to_star @rbeta @Hc|@red_star_subst2 // ]
 144         |#H >H -H lapply (critical O D ty1 M1 N1) * #M3 * #H1 #H2
 145          %{M3} /2/
 146         ]
 147       |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct
 148        lapply (critical2 … redM3M4 Hl Ha1) * #M3 * #H1 #H2 %{M3} /2/
 149       |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2
 150        lapply (HindP … redM0 redM3M4) * #M3 * #H1 #H2
 151        %{(App O D M3 N0)} (* CR-term *) % [@star_red_appl //|@star_red_appl //]
 152       |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #_
 153        %{(App O D M4 N1)} % @R_to_star [@rappr //|@rappl //]
 154       |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
 155       |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
 156       |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
 157       ]
 158     |(* right redex is appr *)#M3 #N #N1 #redN #_ #H1 destruct (H1) #_
 159       #Hl inversion Hl
 160       [#ty1 #M0 #N0 #Hc #H1 destruct (H1) #HM2
 161        %{(subst O D M0 0 N1)} (* CR-term *) %
 162         [@R_to_star @rbeta @(red_closed … Hc) //|@red_star_subst @R_to_star // ]
 163       |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct (H1) elim (normal_to_T … redN)
 164       |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2
 165        %{(App O D M10 N1)} (* CR-term *) % @R_to_star [@rappl //|@rappr //]
 166       |#M0 #N0 #N10 #redN0 #_ #H1 destruct (H1) #_
 167        lapply (HindQ … redN0 redN) * #M3 * #H1 #H2
 168        %{(App O D M0 M3)} (* CR-term *) % [@star_red_appr //|@star_red_appr //]
 169       |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
 170       |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
 171       |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
 172       ]
 173     |(* right redex is rlam *) #ty #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
 174     |(* right redex is rmem *) #ty #M0 #H1 destruct (H1) (* vacuous *)
 175     |(* right redex is vec *) #ty #N #N1 #v #v1 #_ #_
 176      #H1 destruct (H1) (* vacuous *)
 177     ]
 178   |#ty #M1 #Hind #M2 #M3 #H1 #H2 (* this case is not trivial any more *)
 179    lapply (red_lambda … H1) *
 180     [* #M4 * #H3 #H4 >H4 lapply (red_lambda … H2) *
 181       [* #M5 * #H5 #H6 >H6 lapply(Hind … H3 H5) * #M6 * #H7 #H8
 182        %{(Lambda O D ty M6)} (* CR-term *) % @star_red_lambda //
 183       |#H5 >H5 @critical3 //
 184       ]
 185     |#HM2 >HM2 lapply (red_lambda … H2) *
 186       [* #M4 * #Hred #HM3 >HM3 lapply (critical3 … ty ?? Hred) * #M5
 187        * #H3 #H4 %{M5} (* CR-term *) % //
 188       |#HM3 >HM3 %{M3} (* CR-term *) % //
 189       ]
 190     ]
 191   |#ty #v1 #Hind #M1 #M2 #H1 #H2
 192    lapply (red_vec … H1) * #N11 * #N12 * #v11 * #v12 * * #redN11 #Hv1 #HM1
 193    lapply (red_vec … H2) * #N21* #N22 * #v21 * #v22 * * #redN21 #Hv2 #HM2
 194    >Hv1 in Hv2; #Hvv lapply (compare_append … Hvv) -Hvv *
 195    (* we must proceed by cases on the list *) * normalize
 196     [(* N11 = N21 *) *
 197       [>append_nil * #Hl1 #Hl2 destruct lapply(Hind N11 … redN11 redN21)
 198         [@mem_append_l2 %1 //]
 199        * #M3 * #HM31 #HM32
 200        %{(Vec O D ty (v21@M3::v12))} (* CR-term *)
 201        % [@star_red_vec //|@star_red_vec //]
 202       |>append_nil * #Hl1 #Hl2 destruct lapply(Hind N21 … redN21 redN11)
 203         [@mem_append_l2 %1 //]
 204        * #M3 * #HM31 #HM32
 205        %{(Vec O D ty (v11@M3::v22))} (* CR-term *)
 206        % [@star_red_vec //|@star_red_vec //]
 207       ]
 208     |(* N11 ≠  N21 *) -Hind #P #l *
 209       [* #Hv11 #Hv22 destruct
 210        %{((Vec O D ty ((v21@N22::l)@N12::v12)))} (* CR-term *) % @R_to_star
 211         [>associative_append >associative_append normalize @rvec //
 212         |>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
 213         ]
 214       |* #Hv11 #Hv22 destruct
 215        %{((Vec O D ty ((v11@N12::l)@N22::v22)))} (* CR-term *) % @R_to_star
 216         [>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
 217         |>associative_append >associative_append normalize @rvec //
 218         ]
 219       ]
 220     ]
 221   ]
 222 qed.
 223
 224
 225
 226