X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Fcnf.ma;h=02bbcf87a93df09cbae492289133846253f54aa7;hb=7bedf1797ba168f0742194b2add69575e5d4a5cd;hp=1156dcf68ff65ab85267a715e1e126f4154dd227;hpb=78d4844bcccb3deb58a3179151c3045298782b18;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma
index 1156dcf68..02bbcf87a 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma
@@ -20,18 +20,47 @@ definition cnf: lenv → predicate term ≝ λL. NF … (cpr L) (eq …).
 
 interpretation
    "context-sensitive normality (term)"
-   'Normal L T = (cnf L T). 
+   'Normal L T = (cnf L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cnf_inv_appl: ∀L,V,T. L ⊢ 𝐍⦃ⓐV.T⦄ → ∧∧ L ⊢ 𝐍⦃V⦄ & L ⊢ 𝐍⦃T⦄ & 𝐒⦃T⦄.
+#L #V1 #T1 #HVT1 @and3_intro
+[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+| generalize in match HVT1; -HVT1 elim T1 -T1 * // #a * #W1 #U1 #_ #_ #H
+  [ elim (lift_total V1 0 1) #V2 #HV12
+    lapply (H (ⓓ{a}W1.ⓐV2.U1) ?) -H /3 width=3/ -HV12 #H destruct
+  | lapply (H (ⓓ{a}V1.U1) ?) -H /3 width=1/ #H destruct
+]
+qed-.
+
+lemma cnf_inv_zeta: ∀L,V,T. L ⊢ 𝐍⦃+ⓓV.T⦄ → ⊥.
+#L #V #T #H elim (is_lift_dec T 0 1)
+[ * #U #HTU
+  lapply (H U ?) -H /3 width=3 by cpr_tpr, tpr_zeta/ #H destruct (**) (* auto too slow without trace *)
+  elim (lift_inv_pair_xy_y … HTU)
+| #HT
+  elim (tps_full (⋆) V T (⋆. ⓓV) 0 ?) // #T2 #T1 #HT2 #HT12
+  lapply (H (+ⓓV.T2) ?) -H /3 width=3 by cpr_tpr, tpr_delta/ -HT2 #H destruct /3 width=2/ (**) (* auto too slow without trace *)
+]
+qed.
+
+lemma cnf_inv_tau: ∀L,V,T. L ⊢ 𝐍⦃ⓝV.T⦄ → ⊥.
+#L #V #T #H lapply (H T ?) -H /2 width=1/ #H
+@discr_tpair_xy_y //
+qed-.
 
 (* Basic properties *********************************************************)
 
 (* Basic_1: was: nf2_sort *)
-lemma cnf_sort: ∀L,k. L ⊢ 𝐍[⋆k].
+lemma cnf_sort: ∀L,k. L ⊢ 𝐍⦃⋆k⦄.
 #L #k #X #H
 >(cpr_inv_sort1 … H) //
 qed.
 
 (* Basic_1: was: nf2_dec *)
-axiom cnf_dec: ∀L,T1. L ⊢ 𝐍[T1] ∨
+axiom cnf_dec: ∀L,T1. L ⊢ 𝐍⦃T1⦄ ∨
                ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → ⊥).
 
 (* Basic_1: removed theorems 1: nf2_abst_shift *)