matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpms_tdeq.etc

   1 (*
   2 axiom cpms_tdneq_fwd_step_sn (n) (h) (o) (G) (L):
   3                              ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → (T1 ≛[h,o] T2 → ⊥) →
   4                              ∃∃n1,n2,T,T0. ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T ➡*[n2,h] T0 & T0 ≛[h,o] T2 & n1+n2 = n.
   5 axiom plus_Sxy_y_false: ∀y,x. ↑(x+y) = y → ⊥.
   6
   7 lemma cnv_cpm_tdeq_trans (a) (h) (o) (G) (L):
   8                          ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
   9                          ∀n,T2.  ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 → ⦃G,L⦄ ⊢ T2 ![a,h].
  10 #a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1
  11 #G0 #L0 #T0 #IH #G #L * [| * [| * ]]
  12 [ #I #_ #_ #_ #H0 #n #X #H1X #H2X -G0 -L0 -T0
  13   elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
  14   [ #H #_ destruct //
  15   | #s #H #_ #_ #_ destruct //
  16   ]
  17 | #p #I #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct
  18   elim (cnv_inv_bind … H0) #HV1 #_
  19   elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct
  20   /3 width=6 by cnv_bind/
  21 | #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct
  22   elim (cnv_inv_appl … H0) #m #p #W1 #U1 #Hm #HV1 #_ #HVW1 #HTU1
  23   elim (cpm_tdeq_inv_appl_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct
  24   @(cnv_appl … Hm … HVW1)
  25
  26 (* Properties with restricted rt-transition for terms ***********************)
  27
  28 lemma pippo (a) (h) (o) (G) (L):
  29             ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
  30             ∀n1,T.  ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → T1 ≛[h,o] T →
  31             ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
  32             ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[n1,h] T2 & T0 ≛[h,o] T2.
  33 #a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1
  34 #G0 #L0 #T0 #IH #G #L * [| * [| * ]]
  35 [ #I #_ #_ #_ #_ #n1 #X1 #H1X #H2X #n2 #X2 #HX2 -G0 -L0 -T0
  36   elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
  37   [ #H1 #H2 destruct /2 width=4 by ex3_intro/
  38   | #s #H1 #H2 #H3 #Hs destruct
  39     elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn2 destruct >iter_n_Sm
  40     /5 width=6 by cpm_sort_iter, tdeq_sort, deg_iter, deg_next, ex3_intro/
  41   ]
  42 | #p #I #V1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct
  43   elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T #H1T1 #H2T1 #H3T1 #H destruct
  44   elim (cpm_inv_bind1 … HX2) -HX2 *
  45   [ #V2 #T2 #HV12 #HT2 #H destruct
  46     elim (IH … H1T1 … H2T1 H3T1 … HT2) -IH -H1T1 -H2T1 -H3T1 -HT2 [2: // ] #T0 #HT10 #H1T02 #H2T02
  47     @(ex3_intro … (ⓑ{p,I}V2.T0))
  48     [ /2 width=1 by cpm_bind/
  49     |
  50     | /2 width=1 by tdeq_pair/
  51
  52 *)