matita/matita/contribs/lambdadelta/basic_1/nf2/fwd.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "basic_1/nf2/defs.ma".
  18
  19 include "basic_1/pr2/clen.ma".
  20
  21 include "basic_1/subst0/dec.ma".
  22
  23 include "basic_1/T/props.ma".
  24
  25 lemma nf2_gen_lref:
  26  \forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c
  27 (CHead d (Bind Abbr) u)) \to ((nf2 c (TLRef i)) \to (\forall (P: Prop).P))))))
  28 \def
  29  \lambda (c: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
  30 (H: (getl i c (CHead d (Bind Abbr) u))).(\lambda (H0: ((\forall (t2: T).((pr2
  31 c (TLRef i) t2) \to (eq T (TLRef i) t2))))).(\lambda (P:
  32 Prop).(lift_gen_lref_false (S i) O i (le_O_n i) (le_n (plus O (S i))) u (H0
  33 (lift (S i) O u) (pr2_delta c d u i H (TLRef i) (TLRef i) (pr0_refl (TLRef
  34 i)) (lift (S i) O u) (subst0_lref u i))) P))))))).
  35
  36 lemma nf2_gen_abst:
  37  \forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c (THead (Bind Abst) u
  38 t)) \to (land (nf2 c u) (nf2 (CHead c (Bind Abst) u) t)))))
  39 \def
  40  \lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H: ((\forall (t2:
  41 T).((pr2 c (THead (Bind Abst) u t) t2) \to (eq T (THead (Bind Abst) u t)
  42 t2))))).(conj (\forall (t2: T).((pr2 c u t2) \to (eq T u t2))) (\forall (t2:
  43 T).((pr2 (CHead c (Bind Abst) u) t t2) \to (eq T t t2))) (\lambda (t2:
  44 T).(\lambda (H0: (pr2 c u t2)).(let H1 \def (f_equal T T (\lambda (e:
  45 T).(match e with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | (THead
  46 _ t0 _) \Rightarrow t0])) (THead (Bind Abst) u t) (THead (Bind Abst) t2 t) (H
  47 (THead (Bind Abst) t2 t) (pr2_head_1 c u t2 H0 (Bind Abst) t))) in (let H2
  48 \def (eq_ind_r T t2 (\lambda (t0: T).(pr2 c u t0)) H0 u H1) in (eq_ind T u
  49 (\lambda (t0: T).(eq T u t0)) (refl_equal T u) t2 H1))))) (\lambda (t2:
  50 T).(\lambda (H0: (pr2 (CHead c (Bind Abst) u) t t2)).(let H1 \def (f_equal T
  51 T (\lambda (e: T).(match e with [(TSort _) \Rightarrow t | (TLRef _)
  52 \Rightarrow t | (THead _ _ t0) \Rightarrow t0])) (THead (Bind Abst) u t)
  53 (THead (Bind Abst) u t2) (H (THead (Bind Abst) u t2) (let H_y \def
  54 (pr2_gen_cbind Abst c u t t2 H0) in H_y))) in (let H2 \def (eq_ind_r T t2
  55 (\lambda (t0: T).(pr2 (CHead c (Bind Abst) u) t t0)) H0 t H1) in (eq_ind T t
  56 (\lambda (t0: T).(eq T t t0)) (refl_equal T t) t2 H1))))))))).
  57
  58 lemma nf2_gen_cast:
  59  \forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c (THead (Flat Cast) u
  60 t)) \to (\forall (P: Prop).P))))
  61 \def
  62  \lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (nf2 c (THead
  63 (Flat Cast) u t))).(\lambda (P: Prop).(thead_x_y_y (Flat Cast) u t (H t
  64 (pr2_free c (THead (Flat Cast) u t) t (pr0_tau t t (pr0_refl t) u))) P))))).
  65
  66 lemma nf2_gen_beta:
  67  \forall (c: C).(\forall (u: T).(\forall (v: T).(\forall (t: T).((nf2 c
  68 (THead (Flat Appl) u (THead (Bind Abst) v t))) \to (\forall (P: Prop).P)))))
  69 \def
  70  \lambda (c: C).(\lambda (u: T).(\lambda (v: T).(\lambda (t: T).(\lambda (H:
  71 ((\forall (t2: T).((pr2 c (THead (Flat Appl) u (THead (Bind Abst) v t)) t2)
  72 \to (eq T (THead (Flat Appl) u (THead (Bind Abst) v t)) t2))))).(\lambda (P:
  73 Prop).(let H0 \def (eq_ind T (THead (Flat Appl) u (THead (Bind Abst) v t))
  74 (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
  75 \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _)
  76 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind Abbr) u t)
  77 (H (THead (Bind Abbr) u t) (pr2_free c (THead (Flat Appl) u (THead (Bind
  78 Abst) v t)) (THead (Bind Abbr) u t) (pr0_beta v u u (pr0_refl u) t t
  79 (pr0_refl t))))) in (False_ind P H0))))))).
  80
  81 lemma nf2_gen_flat:
  82  \forall (f: F).(\forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c
  83 (THead (Flat f) u t)) \to (land (nf2 c u) (nf2 c t))))))
  84 \def
  85  \lambda (f: F).(\lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H:
  86 ((\forall (t2: T).((pr2 c (THead (Flat f) u t) t2) \to (eq T (THead (Flat f)
  87 u t) t2))))).(conj (\forall (t2: T).((pr2 c u t2) \to (eq T u t2))) (\forall
  88 (t2: T).((pr2 c t t2) \to (eq T t t2))) (\lambda (t2: T).(\lambda (H0: (pr2 c
  89 u t2)).(let H1 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
  90 \Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t0 _) \Rightarrow t0]))
  91 (THead (Flat f) u t) (THead (Flat f) t2 t) (H (THead (Flat f) t2 t)
  92 (pr2_head_1 c u t2 H0 (Flat f) t))) in H1))) (\lambda (t2: T).(\lambda (H0:
  93 (pr2 c t t2)).(let H1 \def (f_equal T T (\lambda (e: T).(match e with [(TSort
  94 _) \Rightarrow t | (TLRef _) \Rightarrow t | (THead _ _ t0) \Rightarrow t0]))
  95 (THead (Flat f) u t) (THead (Flat f) u t2) (H (THead (Flat f) u t2)
  96 (pr2_head_2 c u t t2 (Flat f) (pr2_cflat c t t2 H0 f u)))) in H1)))))))).
  97
  98 fact nf2_gen__nf2_gen_aux:
  99  \forall (b: B).(\forall (x: T).(\forall (u: T).(\forall (d: nat).((eq T
 100 (THead (Bind b) u (lift (S O) d x)) x) \to (\forall (P: Prop).P)))))
 101 \def
 102  \lambda (b: B).(\lambda (x: T).(T_ind (\lambda (t: T).(\forall (u:
 103 T).(\forall (d: nat).((eq T (THead (Bind b) u (lift (S O) d t)) t) \to
 104 (\forall (P: Prop).P))))) (\lambda (n: nat).(\lambda (u: T).(\lambda (d:
 105 nat).(\lambda (H: (eq T (THead (Bind b) u (lift (S O) d (TSort n))) (TSort
 106 n))).(\lambda (P: Prop).(let H0 \def (eq_ind T (THead (Bind b) u (lift (S O)
 107 d (TSort n))) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False |
 108 (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TSort n)
 109 H) in (False_ind P H0))))))) (\lambda (n: nat).(\lambda (u: T).(\lambda (d:
 110 nat).(\lambda (H: (eq T (THead (Bind b) u (lift (S O) d (TLRef n))) (TLRef
 111 n))).(\lambda (P: Prop).(let H0 \def (eq_ind T (THead (Bind b) u (lift (S O)
 112 d (TLRef n))) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False |
 113 (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow True])) I (TLRef n)
 114 H) in (False_ind P H0))))))) (\lambda (k: K).(\lambda (t: T).(\lambda (_:
 115 ((\forall (u: T).(\forall (d: nat).((eq T (THead (Bind b) u (lift (S O) d t))
 116 t) \to (\forall (P: Prop).P)))))).(\lambda (t0: T).(\lambda (H0: ((\forall
 117 (u: T).(\forall (d: nat).((eq T (THead (Bind b) u (lift (S O) d t0)) t0) \to
 118 (\forall (P: Prop).P)))))).(\lambda (u: T).(\lambda (d: nat).(\lambda (H1:
 119 (eq T (THead (Bind b) u (lift (S O) d (THead k t t0))) (THead k t
 120 t0))).(\lambda (P: Prop).(let H2 \def (f_equal T K (\lambda (e: T).(match e
 121 with [(TSort _) \Rightarrow (Bind b) | (TLRef _) \Rightarrow (Bind b) |
 122 (THead k0 _ _) \Rightarrow k0])) (THead (Bind b) u (lift (S O) d (THead k t
 123 t0))) (THead k t t0) H1) in ((let H3 \def (f_equal T T (\lambda (e: T).(match
 124 e with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t1 _)
 125 \Rightarrow t1])) (THead (Bind b) u (lift (S O) d (THead k t t0))) (THead k t
 126 t0) H1) in ((let H4 \def (f_equal T T (\lambda (e: T).(match e with [(TSort
 127 _) \Rightarrow (THead k (lref_map (\lambda (x0: nat).(plus x0 (S O))) d t)
 128 (lref_map (\lambda (x0: nat).(plus x0 (S O))) (s k d) t0)) | (TLRef _)
 129 \Rightarrow (THead k (lref_map (\lambda (x0: nat).(plus x0 (S O))) d t)
 130 (lref_map (\lambda (x0: nat).(plus x0 (S O))) (s k d) t0)) | (THead _ _ t1)
 131 \Rightarrow t1])) (THead (Bind b) u (lift (S O) d (THead k t t0))) (THead k t
 132 t0) H1) in (\lambda (_: (eq T u t)).(\lambda (H6: (eq K (Bind b) k)).(let H7
 133 \def (eq_ind_r K k (\lambda (k0: K).(eq T (lift (S O) d (THead k0 t t0)) t0))
 134 H4 (Bind b) H6) in (let H8 \def (eq_ind T (lift (S O) d (THead (Bind b) t
 135 t0)) (\lambda (t1: T).(eq T t1 t0)) H7 (THead (Bind b) (lift (S O) d t) (lift
 136 (S O) (S d) t0)) (lift_bind b t t0 (S O) d)) in (H0 (lift (S O) d t) (S d) H8
 137 P)))))) H3)) H2))))))))))) x)).
 138
 139 lemma nf2_gen_abbr:
 140  \forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c (THead (Bind Abbr) u
 141 t)) \to (\forall (P: Prop).P))))
 142 \def
 143  \lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H: ((\forall (t2:
 144 T).((pr2 c (THead (Bind Abbr) u t) t2) \to (eq T (THead (Bind Abbr) u t)
 145 t2))))).(\lambda (P: Prop).(let H_x \def (dnf_dec u t O) in (let H0 \def H_x
 146 in (ex_ind T (\lambda (v: T).(or (subst0 O u t (lift (S O) O v)) (eq T t
 147 (lift (S O) O v)))) P (\lambda (x: T).(\lambda (H1: (or (subst0 O u t (lift
 148 (S O) O x)) (eq T t (lift (S O) O x)))).(or_ind (subst0 O u t (lift (S O) O
 149 x)) (eq T t (lift (S O) O x)) P (\lambda (H2: (subst0 O u t (lift (S O) O
 150 x))).(let H3 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
 151 \Rightarrow t | (TLRef _) \Rightarrow t | (THead _ _ t0) \Rightarrow t0]))
 152 (THead (Bind Abbr) u t) (THead (Bind Abbr) u (lift (S O) O x)) (H (THead
 153 (Bind Abbr) u (lift (S O) O x)) (pr2_free c (THead (Bind Abbr) u t) (THead
 154 (Bind Abbr) u (lift (S O) O x)) (pr0_delta u u (pr0_refl u) t t (pr0_refl t)
 155 (lift (S O) O x) H2)))) in (let H4 \def (eq_ind T t (\lambda (t0: T).(subst0
 156 O u t0 (lift (S O) O x))) H2 (lift (S O) O x) H3) in (subst0_refl u (lift (S
 157 O) O x) O H4 P)))) (\lambda (H2: (eq T t (lift (S O) O x))).(let H3 \def
 158 (eq_ind T t (\lambda (t0: T).(\forall (t2: T).((pr2 c (THead (Bind Abbr) u
 159 t0) t2) \to (eq T (THead (Bind Abbr) u t0) t2)))) H (lift (S O) O x) H2) in
 160 (nf2_gen__nf2_gen_aux Abbr x u O (H3 x (pr2_free c (THead (Bind Abbr) u (lift
 161 (S O) O x)) x (pr0_zeta Abbr not_abbr_abst x x (pr0_refl x) u))) P))) H1)))
 162 H0))))))).
 163
 164 lemma nf2_gen_void:
 165  \forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c (THead (Bind Void) u
 166 (lift (S O) O t))) \to (\forall (P: Prop).P))))
 167 \def
 168  \lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H: ((\forall (t2:
 169 T).((pr2 c (THead (Bind Void) u (lift (S O) O t)) t2) \to (eq T (THead (Bind
 170 Void) u (lift (S O) O t)) t2))))).(\lambda (P: Prop).(nf2_gen__nf2_gen_aux
 171 Void t u O (H t (pr2_free c (THead (Bind Void) u (lift (S O) O t)) t
 172 (pr0_zeta Void not_void_abst t t (pr0_refl t) u))) P))))).
 173