]> matita.cs.unibo.it Git - helm.git/commitdiff
- relation between native type and atomic arity proced
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 15 Jun 2012 21:22:03 +0000 (21:22 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 15 Jun 2012 21:22:03 +0000 (21:22 +0000)
- higher order native typing defined
- some minor results towards subject reduction for native typing

16 files changed:
matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_aaa.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_nta.ma
matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_thin.ma
matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs_cpcs.ma
matita/matita/contribs/lambda_delta/basic_2/hod/ntas.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/hod/ntas_lift.ma [new file with mode: 0644]
matita/matita/contribs/lambda_delta/basic_2/notation.ma
matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma
matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml
matita/matita/contribs/lambda_delta/ground_2/xoa.ma
matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma

index 544232544fbe7a7bfafc5db1005da0365e3738c1..c5fe6def0932a2c8fcf2db186caa9c28cdca7b8f 100644 (file)
@@ -209,9 +209,7 @@ ty3/arity ty3_arity
 ty3/arity_props ty3_predicative
 ty3/arity_props ty3_repellent
 ty3/arity_props ty3_acyclic
-ty3/arity_props ty3_sn3
 ty3/dec ty3_inference
-ty3/fwd ty3_gen_appl
 ty3/fwd tys3_gen_nil
 ty3/fwd tys3_gen_cons
 ty3/fwd_nf2 ty3_gen_appl_nf2
index a71c773bc9a40a3fff886b39fbc5decac4f73f1e..5d4d74399a2efc959c448d0093bce6de4d8f0306 100644 (file)
@@ -130,6 +130,16 @@ lapply (IHV1 T1 T1 ?) -IHV1 // #HV1
 @(cprs_trans … HV1) -HV1 /2 width=1/
 qed.
 
+lemma cprs_beta_dx: ∀L,V1,V2,W,T1,T2.
+                    L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡* T2 → L ⊢ ⓐV1.ⓛW.T1 ➡* ⓓV2.T2.
+#L #V1 #V2 #W #T1 #T2 #HV12 #HT12 @(cprs_ind … HT12) -T2
+[ /3 width=1/
+| -HV12 #T #T2 #_ #HT2 #IHT1
+  lapply (cpr_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+  @(cprs_trans … IHT1) -V1 -W -T1 /3 width=1/
+]
+qed.
+
 (* Basic_1: was only: pr3_pr2_pr3_t pr3_wcpr0_t *)
 lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 →
                        ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_aaa.ma
new file mode 100644 (file)
index 0000000..9628569
--- /dev/null
@@ -0,0 +1,49 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/computation/csn_aaa.ma".
+include "basic_2/equivalence/lcpcs_aaa.ma".
+include "basic_2/dynamic/nta.ma".
+
+(* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Forward lemmas on atomic arity assignment for terms **********************)
+
+lemma nta_fwd_aaa: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃∃A. L ⊢ T ⁝ A & L ⊢ U ⁝ A.
+#h #L #T #U #H elim H -L -T -U
+[ /2 width=3/
+| #L #K #V #W #U #i #HLK #_ #HWU * #B #HV #HW
+  lapply (ldrop_fwd_ldrop2 … HLK) /3 width=9/
+| #L #K #W #V #U #i #HLK #_ #HWU * #B #HW #_ -V
+  lapply (ldrop_fwd_ldrop2 … HLK) /3 width=9/
+| * #L #V #W #T #U #_ #_ * #B #HV #HW * #A #HT #HU
+  [ /3 width=3/ | /3 width=5/ ]
+| #L #V #W #T #U #_ #_ * #B #HV #HW * #X #H1 #H2
+  elim (aaa_inv_abst … H1) -H1 #B1 #A1 #HW1 #HT #H destruct
+  elim (aaa_inv_abst … H2) -H2 #B2 #A #_ #HU #H destruct
+  lapply (aaa_mono … HW1 … HW) -HW1 #H destruct /4 width=5/
+| #L #V #W #T #U #_ #_ * #X #HT #HUX * #A #H #_ -W
+  elim (aaa_inv_appl … H) -H #B #HV #HUA
+  lapply (aaa_mono … HUA … HUX) -HUX #H destruct /3 width=5/
+| #L #T #U #_ * #A #HT #HU /3 width=3/
+| #L #T #U1 #U2 #V2 #_ #HU12 #_ * #X #HT #HU1 * #A #HU2 #_
+  lapply (aaa_cpcs_mono … HU12 … HU1 … HU2) -U1 #H destruct /2 width=3/
+]
+qed-.
+
+(* Note: this is the stong normalization property *)
+(* Basic_1: was only: ty3_sn3 *)
+theorem nta_fwd_csn: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → L ⊢ ⬇* T ∧ L ⊢ ⬇* U.
+#h #L #T #U #H elim (nta_fwd_aaa … H) -H /3 width=2/
+qed-. 
index 0631ca4f2f3b59c4596f0d8b167f0dfcb1f614d1..57e06a1e9aaff1c1c38a2900686ca414d8e18069 100644 (file)
@@ -99,7 +99,7 @@ lemma nta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓝY.X : U →  ⦃h, L⦄ ⊢
 
 (* Advanced forvard lemmas **************************************************)
 
-fact nta_fwd_appl1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓐY.X →
+fact nta_fwd_pure1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓐY.X →
                         ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
 #h #L #T #U #H elim H -L -T -U
 [ #L #k #X #Y #H destruct
@@ -116,7 +116,7 @@ fact nta_fwd_appl1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓐY.X
 ]
 qed.
 
-lemma nta_fwd_appl1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓐY.X : U →
+lemma nta_fwd_pure1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓐY.X : U →
                      ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
 /2 width=3/ qed-.
 
index 6ecc0bb81c7a7dcfbd7b9884176c5044d9d5626c..3799dcbb808dd148930bd28905607a47c6d0d0e1 100644 (file)
 (*                                                                        *)
 (**************************************************************************)
 
+(* FRAGMENT 0 
+include "basic_2/unfold/delift_lift.ma".
+
+  
+include "basic_2/equivalence/cpcs_cpcs.ma".
+include "basic_2/unfold/delift_delift.ma".
+
+
+
+axiom pippo1: ∀T1,V. ∃∃T2. ⓓV.T1 ➡ T2 & ⋆.ⓓV ⊢ T1 ▼*[0, 1] ≡ T2.
+(*
+#T1 #V elim (pippo0 (⋆.ⓓV) 0 1 ? T1)
+[ #T2 #HT12 @(ex2_1_intro … HT12)
+  @tpr
+*)
+
+axiom pippo: ∀L,V,T1. ∃∃T2. L ⊢ ⓓV.T1 ➡ T2 & L.ⓓV ⊢ T1 ▼*[0, 1] ≡ T2.
+
+axiom cprs_inv_appl1_cpcs: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 → (
+                           ∃∃V2,T2.  L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 &
+                                     L ⊢ U2 ➡* ⓐV2. T2
+                           ) ∨
+                           ∃∃V2,W,T. L ⊢ V1 ➡* V2 &
+                                     L ⊢ T1 ➡* ⓛW. T & L ⊢ ⓓV2. T ⬌* U2.
+#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+#U #U2 #_ #HU2 * *
+[ #V0 #T0 #HV10 #HT10 #HUT0
+  elim (cprs_strip … HUT0 … HU2) -U #U #H #HU2
+  elim (cpr_inv_appl1 … H) -H *
+  [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
+  | #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct
+    lapply (cprs_strap1 … HV10 HV02) -V0 #HV12
+    lapply (cprs_div ? (ⓓV2.T) ? ? ? HU2) -HU2 /2 width=1/ /3 width=6/
+  | #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct
+    lapply (cprs_strap1 … HV10 HV0) -V0 #HV1
+    lapply (cprs_trans … HT10 (ⓓW2.T2) ?) -HT10 /2 width=1/ -W0 -T #HT1
+    elim (pippo L W2 T2) #T3 #H1T3 #H2T3
+    elim (pippo L W2 (ⓐV2.T2)) #X #H1X #H
+    elim (delift_inv_flat1 … H) -H #V3 #Y #HV23 #HY #H destruct
+      
+  
+    @or_introl @(ex3_2_intro … HV1 HT1) -HV1 -HT1  
+      
+  ]
+| /4 width=8/
+]
+qed-.
+
+
+include "basic_2/computation/cprs_lcprs.ma".
+include "basic_2/dynamic/nta.ma".
+
+axiom cprs_inv_appl_abst: ∀L,V,T,W,U. L ⊢ ⓐV.T ➡* ⓛW.U →
+                          ∃∃V0,W0,T0,W1,U1. ⇧[O, 1] W ≡ W1 &
+                                            ⇧[O + 1, 1] U ≡ U1 &
+                                            L ⊢ V ➡* V0 & L ⊢ T ➡* ⓛW0.T0 &
+                                            L.ⓓV0 ⊢ T0 ➡* ⓛW1.U1.
+#L #V #T #W #U #H
+elim (cprs_inv_appl1 … H) -H *
+[ #V0 #T0 #_ #_ #H destruct
+| #V0 #W0 #T0 #HV0 #HT0 #H
+  elim (cprs_inv_abbr1 … H) -H *
+  [ #V1 #T1 #_ #_ #H destruct
+  | #X #H #HT01
+    elim (lift_inv_bind1 … H) -H #W1 #U1 #HW1 #HU1 #H destruct /2 width=10/ 
+  ]
+| #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #H
+  elim (cprs_inv_abbr1 … H) -H *
+  [ #V3 #T3 #_ #_ #H destruct
+  | #X #H #HT3
+    elim (lift_inv_bind1 … H) -H #W3 #U3 #HW3 #HU3 #H destruct /2 width=10/ 
+
+axiom pippo: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. L ⊢ T ➡* ⓛX.Y →
+             ∃Z. L ⊢ U ➡* ⓛX.Z.
+#h #L #T #U #H elim H -L -T -U
+[
+|
+|
+|
+|
+| #L #V #W #T #U #HTU #HUW #IHTU #IHUW #X #Y #HTY
+  elim (cprs_inv_appl1 … HTY) -HTY *
+  [ #V0 #T0 #_ #_ #H destruct
+  | #V0 #W0 #T0 #HV0 #HT0 #HTY
+    elim (IHTU … HT0) -IHTU -HT0 #Z #HUZ
+    elim (cprs_inv_abbr1 … HTY) -HTY *
+    [ #V1 #T1 #_ #_ #H destruct #X0  
+
+
 include "basic_2/dynamic/nta_ltpss.ma".
 include "basic_2/dynamic/nta_thin.ma".
 include "basic_2/dynamic/lsubn_nta.ma".
 
-lemma cpr_beta: ∀L,V1,V2,W,T1,T2.
-                V1 ➡ V2 → L.ⓛW ⊢ T1 ➡ T2 → L ⊢ ⓐV1.ⓛW.T1 ➡ ⓓV2.T2.
-#L #V1 #V2 #W #T1 #T2 #HV12 * #T #HT1 #HT2
-lapply (tpss_inv_S2 … HT2 L W ?) -HT2 // #HT2
-lapply (tpss_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
-@(ex2_1_intro … (ⓓV2.T)) /2 width=1/ (**) (* explicit constructor, /3/ is too skow *)
-qed.
-
-lemma cpr_beta2: ∀L,V1,V2,W,T1,T2.
-                 L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡ T2 → L ⊢ ⓐV1.ⓛW.T1 ➡ ⓓV2.T2.
-#L #V1 #V2 #W #T1 #T2 * #V #HV1 #HV2 * #T #HT1 #HT2
-lapply (tpss_inv_S2 … HT2 L W ?) -HT2 // #HT2
-lapply (tpss_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
-@(ex2_1_intro … (ⓓV.T)) /2 width=1/ (**) (* explicit constructor, /3/ is too skow *)
-qed.
+include "basic_2/hod/ntas_lift.ma".
 
+  
+  elim (nta_inv_pure1 … HUW) -HUW #V0 #U0 #U1 #HV0 #HU0 #HU0W #HU01
+  @(ex2_2_intro … HYW)
+  [2: 
+
+
+axiom pippo_aux: ∀h,L,Z,U. ⦃h, L⦄ ⊢ Z : U → ∀Y,X. Z = ⓐY.X →
+                 ∀W,T. L ⊢ X ➡* ⓛW.T → ⦃h, L⦄ ⊢ Y : W.
+#h #L #Z #U #H elim H -L -Z -U
+[
+|
+|
+|
+|
+| #L #V #W #T #U #HTU #_ #_ #IHUW #Y #X #H #W0 #T0 #HX destruct 
+  lapply (IHUW Y U ? ?) -IHUW -W // #T 
+  @(ex2_2_intro … HYW)
+  [2: 
+
+axiom pippo: ∀h,L,V,X,U. ⦃h, L⦄ ⊢ ⓐV.X : U →
+             ∃∃W,T. L ⊢ X ➡* ⓛW.T & ⦃h, L⦄ ⊢ V : W.
+#h #L #V #X #Y #H 
+
+*)
 (* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
 
 (* Properties on context-free parallel reduction for local environments ******)
-
-lemma nta_ltpr_tpr_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 →
+(*
+axiom nta_ltpr_cprs_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 →
+                          ∀T2. L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 : U.
+#h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U
+[ #L1 #k #L2 #_ #T2 #H
+  >(cprs_inv_sort1 … H) -H //
+|
+|
+|
+|
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #HL12 #T2 #H
+  elim (cprs_inv_appl1 … H) -H *
+  [ #V2 #T0 #HV12 #HT10 #H destruct
+    elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=2/ ] #U
+    @(nta_conv … (ⓐV2.U1)) (* /2 width=1/*) [ /4 width=2/] (**) (* explicit constructor, /5 width=5/ is too slow *)
+  | #V2 #W2 #T0 #HV12 #HT10 #HT02
+    lapply (IHTU1 … HL12 (ⓛW2.T0) ?) -IHTU1 /2 width=1/ -HT10 #H
+    elim (nta_inv_bind1 … H) -H #W #U0 #HW2 #HTU0 #HU01
+    elim (cpcs_inv_abst1 … HU01) -HU01 #W #U #HU1 #HU0
+    lapply (IHUW1 … HL12 (ⓐV2.ⓛW.U) ?) -IHUW1 -HL12 /2 width=1/ -HV12 #H
+    
+    
+    
+    elim (nta_fwd_pure1 … H) -H #W0 #U2 #HVU2 #H #HW01
+    elim (nta_inv_bind1 … H) -H #W3 #U3 #HW3 #HU3 #H
+    elim (cpcs_inv_abst1 … H) -H #W4 #U4  
+*)      
+(*
+axiom nta_ltpr_tpr_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 →
                          ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U.
 #h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U
 [ #L1 #k #L2 #_ #T2 #H
@@ -92,25 +218,36 @@ lemma nta_ltpr_tpr_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡
     elim (nta_fwd_correct … H1) #T #H2
     elim (nta_inv_bind1 … H1) -H1 #W #U2 #HW2 #HTU2 #H
     elim (cpcs_inv_abst … H Abst W2) -H #_ #HU21
-    elim (nta_inv_bind1 … H2) -H2 #W0 #U0 #_ #H #_ -T -W0 
+    elim (nta_inv_bind1 … H2) -H2 #W0 #U0 #_ #H #_ -T -W0
     lapply (lsubn_nta_trans … HTU2 (L2.ⓓV2) ?) -HTU2 /2 width=1/ #HTU2
-    @(nta_conv … (ⓓV2.U2))
-    [2: /2 width=2/
-    |3: -h -L1 -T0 -T2 -W -U0
-    |4: /3 width=2/ 
-    ]
+    @(nta_conv … (ⓓV2.U2)) /2 width=2/ /3 width=2/ (**) (* explicit constructor, /4 width=5/ is too slow *)
   | #V0 #V2 #W0 #W2 #T0 #T2 #_ #_ #_ #_ #H destruct
   ]
-
-
-
-
-
-| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H
-  elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
-  lapply (cpr_tpss … HV12) #HV
-  elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=4/ ] #U #HU
-  @(nta_conv … (ⓐV2.U1)) // /3 width=1/ /4 width=5/ (**) (* explicit constructor, /5 width=5/ is too slow *)
+| #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #HL12 #X #H
+  elim (tpr_inv_appl1 … H) -H *
+  [ #V2 #T2 #HV12 #HT12 #H destruct
+    elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=2/ ] #U
+    @(nta_conv … (ⓐV2.U1)) /2 width=1/ /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *)
+  | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
+    lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 /2 width=1/ -T0 #H
+    elim (nta_inv_bind1 … H) -H #W #U2 #HW2 #HTU2 #HU21
+    lapply (IHUW1 … HL12 (ⓐV2.U1) ?) -IHUW1 -HL12 /2 width=1/ #H
+    elim (nta_inv_pure1 … H) -H #V0 #U0 #U #HV20 #HU10 #HU0W1 #HU0
+    @(nta_conv … (ⓓV2.U2))
+    [2: @nta_bind //
+        @(lsubn_nta_trans … HTU2) @lsubn_abbr //
+(*
+    lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
+    lapply (IH … HB0  … HL12 W2 ?) -HB0 /width=5/ #HB0
+    lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/
+*)
+*)
+(*
+axiom pippo: ⦃h, L⦄ ⊢ ⓐV.X : Y →
+             ∃∃W,T. L ⊢ X ➡* ⓛW.T & ⦃h, L⦄ ⊢ ⓐV : W.
+
+*)
+(* SEGMENT 2
 | #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H
   elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct
   lapply (cpr_tpss … HU12) /4 width=4/
@@ -118,39 +255,13 @@ lemma nta_ltpr_tpr_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡
   @(nta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *)
 ]
 qed.
+*)
 
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
+(* SEGMENT 3
 fact nta_ltpr_tpr_conf_aux: ∀h,L,T,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → L = L1 → T = T1 →
                             ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U.
   
   
-| #L1 #V1 #T1 #B #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct
-  elim (tpr_inv_appl1 … H) -H *
-  [ #V2 #T2 #HV12 #HT12 #H destruct
-    lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
-    lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ /2 width=3/
-  | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
-    elim (nta_inv_abst … HT1) -HT1 #B0 #A0 #HB0 #HA0 #H destruct
-    lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
-    lapply (IH … HB0  … HL12 W2 ?) -HB0 /width=5/ #HB0
-    lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/
   | #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct
     elim (nta_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0
     lapply (IH … HW0  … HL12 … HW02) -HW0 /width=5/ #HW2
@@ -172,8 +283,9 @@ qed.
 
 /2 width=9/ qed.
 
-lemma nta_ltpr_conf: ∀L1,T,A. L1 ⊢ T : A → ∀L2. L1 ➡ L2 → L2 ⊢ T : A.
+axiom nta_ltpr_conf: ∀L1,T,A. L1 ⊢ T : A → ∀L2. L1 ➡ L2 → L2 ⊢ T : A.
 /2 width=5/ qed.
 
-lemma nta_tpr_conf: ∀L,T1,A. L ⊢ T1 : A → ∀T2. T1 ➡ T2 → L ⊢ T2 : A.
+axiom nta_tpr_conf: ∀L,T1,A. L ⊢ T1 : A → ∀T2. T1 ➡ T2 → L ⊢ T2 : A.
 /2 width=5/ qed.
+*)
index b36725d92ffc54a1c24c275c5bb21730304db7ab..05eb6c55df0ae58fd6ae7a34f9431b60b0c81c26 100644 (file)
@@ -37,10 +37,10 @@ theorem nta_mono: ∀h,L,T,U1. ⦃h, L⦄ ⊢ T : U1 → ∀U2. ⦃h, L⦄ ⊢ T
   elim (nta_inv_bind1 … H) -H #W2 #U2 #_ #HTU2 #H
   @(cpcs_trans … H) -X /3 width=1/
 | #L #V #W1 #T #U1 #_ #_ #_ #IHTU1 #X #H
-  elim (nta_fwd_appl1 … H) -H #U2 #W2 #_ #HTU2 #H
+  elim (nta_fwd_pure1 … H) -H #U2 #W2 #_ #HTU2 #H
   @(cpcs_trans … H) -X /3 width=1/
 | #L #V #W1 #T #U1 #_ #_ #IHTU1 #_ #X #H
-  elim (nta_fwd_appl1 … H) -H #U2 #W2 #_ #HTU2 #H
+  elim (nta_fwd_pure1 … H) -H #U2 #W2 #_ #HTU2 #H
   @(cpcs_trans … H) -X /3 width=1/
 | #L #T #U1 #_ #_ #X #H
   elim (nta_inv_cast1 … H) -H //
index 96e84dd5196f69afee941bfe344a2e0aa5127f04..e2e568d3a33d04e4542e1bc580d2354b37bedb87 100644 (file)
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop_sfr.ma".
 include "basic_2/unfold/delift_lift.ma".
 include "basic_2/unfold/thin_ldrop.ma".
 include "basic_2/equivalence/cpcs_delift.ma".
index bbf70c7820a313a845d501ac3a86d46b328dccdd..d67e6663004cd4268b185d7831a3e4ffad502659 100644 (file)
@@ -65,6 +65,14 @@ lemma cpcs_inv_abst_shift: ∀L,W1,W2,T1,T2. L ⊢ ⓛW1.T1 ⬌* ⓛW2.T2 → 
 lapply (cpcs_inv_abst … H Abst W) -H //
 qed.
 
+lemma cpcs_inv_abst1: ∀L,W1,T1,T. L ⊢ ⓛW1.T1 ⬌* T →
+                      ∃∃W2,T2. L ⊢ T ➡* ⓛW2.T2 & L ⊢ ⓛW1.T1 ➡* ⓛW2.T2.
+#L #W1 #T1 #T #H
+elim (cpcs_inv_cprs … H) -H #X #H1 #H2
+elim (cprs_inv_abst1 Abst W1 … H1) -H1 #W2 #T2 #HW12 #HT12 #H destruct
+@(ex2_2_intro … H2) -H2 /2 width=2/ (**) (* explicit constructor, /3 width=6/ is slow *)
+qed-.
+
 (* Basic_1: was: pc3_gen_lift *)
 lemma cpcs_inv_lift: ∀L,K,d,e. ⇩[d, e] L ≡ K →
                      ∀T1,U1. ⇧[d, e] T1 ≡ U1 → ∀T2,U2. ⇧[d, e] T2 ≡ U2 →
@@ -86,6 +94,10 @@ elim (cpcs_inv_cprs … HV12) -HV12 #V #HV1 #HV2
 elim (cpcs_inv_cprs … HT12) -HT12 /3 width=5 by cprs_flat, cprs_div/ (**) (* /3 width=5/ is too slow *)
 qed.
 
+lemma cpcs_flat_dx_tpr_rev: ∀L,V1,V2. V2 ➡ V1 → ∀T1,T2. L ⊢ T1 ⬌* T2 →
+                            ∀I. L ⊢ ⓕ{I}V1. T1 ⬌* ⓕ{I}V2. T2.
+/3 width=1/ qed.
+
 lemma cpcs_abst: ∀L,V1,V2. L ⊢ V1 ⬌* V2 →
                  ∀V,T1,T2. L.ⓛV ⊢ T1 ⬌* T2 → L ⊢ ⓛV1. T1 ⬌* ⓛV2. T2.
 #L #V1 #V2 #HV12 #V #T1 #T2 #HT12
@@ -111,6 +123,20 @@ qed.
 lemma cpcs_bind_sn: ∀I,L,V1,V2,T. L ⊢ V1 ⬌* V2 → L ⊢ ⓑ{I}V1. T ⬌* ⓑ{I}V2. T.
 * /2 width=1/ /2 width=2/ qed.
 
+lemma cpcs_beta_dx: ∀L,V1,V2,W,T1,T2.
+                    L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ⬌* T2 → L ⊢ ⓐV1.ⓛW.T1 ⬌* ⓓV2.T2.
+#L #V1 #V2 #W #T1 #T2 #HV12 #HT12
+elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
+lapply (cprs_beta_dx … HV12 HT1) -HV12 -HT1 #HT1
+lapply (cprs_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+@(cprs_div … HT1) /2 width=1/
+qed.
+
+lemma cpcs_beta_dx_tpr_rev: ∀L,V1,V2,W,T1,T2.
+                            V1 ➡ V2 → L.ⓛW ⊢ T2 ⬌* T1 →
+                            L ⊢ ⓓV2.T2 ⬌* ⓐV1.ⓛW.T1.
+/4 width=1/ qed.
+
 (* Note: it does not hold replacing |L1| with |L2| *)
 lemma cpcs_lsubs_trans: ∀L1,T1,T2. L1 ⊢ T1 ⬌* T2 →
                         ∀L2. L2 ≼ [0, |L1|] L1 → L2 ⊢ T1 ⬌* T2.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/hod/ntas.ma b/matita/matita/contribs/lambda_delta/basic_2/hod/ntas.ma
new file mode 100644 (file)
index 0000000..c090997
--- /dev/null
@@ -0,0 +1,53 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/dynamic/nta.ma".
+
+(* HIGHER ORDER NATIVE TYPE ASSIGNMENT ON TERMS *****************************)
+
+definition ntas: sh → lenv → relation term ≝
+                 λh,L. star … (nta h L).
+
+interpretation "higher order native type assignment (term)"
+   'NativeTypeStar h L T U = (ntas h L T U).
+
+(* Basic eliminators ********************************************************)
+(*
+lemma cprs_ind: ∀L,T1. ∀R:predicate term. R T1 →
+                (∀T,T2. L ⊢ T1 ➡* T → L ⊢ T ➡ T2 → R T → R T2) →
+                ∀T2. L ⊢ T1 ➡* T2 → R T2.
+#L #T1 #R #HT1 #IHT1 #T2 #HT12
+@(TC_star_ind … HT1 IHT1 … HT12) //
+qed-.
+*)
+axiom ntas_ind_dx: ∀h,L,T2. ∀R:predicate term. R T2 →
+                   (∀T1,T. ⦃h, L⦄ ⊢ T1 : T → ⦃h, L⦄ ⊢ T :* T2 → R T → R T1) →
+                   ∀T1. ⦃h, L⦄ ⊢ T1 :* T2 → R T1.
+(*
+#h #L #T2 #R #HT2 #IHT2 #T1 #HT12
+@(star_ind_dx … HT2 IHT2 … HT12) //
+qed-.
+*)
+(* Basic properties *********************************************************)
+
+lemma ntas_refl: ∀h,L,T. ⦃h, L⦄ ⊢ T :* T.
+// qed.
+
+lemma ntas_strap1: ∀h,L,T1,T,T2.
+                   ⦃h, L⦄ ⊢ T1 :* T → ⦃h, L⦄  ⊢ T : T2 → ⦃h, L⦄  ⊢ T1 :* T2.
+/2 width=3/ qed.
+
+lemma ntas_strap2: ∀h,L,T1,T,T2.
+                   ⦃h, L⦄  ⊢ T1 : T → ⦃h, L⦄ ⊢ T :* T2 → ⦃h, L⦄ ⊢ T1 :* T2.
+/2 width=3/ qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/hod/ntas_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/hod/ntas_lift.ma
new file mode 100644 (file)
index 0000000..1adced7
--- /dev/null
@@ -0,0 +1,71 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/dynamic/nta_lift.ma".
+include "basic_2/hod/ntas.ma".
+
+(* HIGHER ORDER NATIVE TYPE ASSIGNMENT ON TERMS *****************************)
+
+(* Advanced properties on native type assignment for terms ******************)
+
+lemma nta_pure_ntas: ∀h,L,U,W,Y. ⦃h, L⦄ ⊢ U :* ⓛW.Y → ∀T. ⦃h, L⦄ ⊢ T : U →
+                     ∀V. ⦃h, L⦄ ⊢ V : W →  ⦃h, L⦄ ⊢ ⓐV.T : ⓐV.U.
+#h #L #U #W #Y #H @(ntas_ind_dx … H) -U /2 width=1/ /3 width=2/
+qed.
+
+axiom pippo: ∀h,L,T,W,Y. ⦃h, L⦄ ⊢ T :* ⓛW.Y → ∀U. ⦃h, L⦄ ⊢ T : U →
+             ∃Z. ⦃h, L⦄ ⊢ U :* ⓛW.Z.
+(* REQUIRES SUBJECT CONVERSION
+#h #L #T #W #Y #H @(ntas_ind_dx … H) -T
+[ #U #HYU
+  elim (nta_fwd_correct … HYU) #U0 #HU0 
+  elim (nta_inv_bind1 … HYU) #W0 #Y0 #HW0 #HY0 #HY0U
+*)
+
+(* Advanced inversion lemmas on native type assignment for terms ************)
+
+fact nta_inv_pure1_aux: ∀h,L,Z,U. ⦃h, L⦄ ⊢ Z : U → ∀X,Y. Z = ⓐY.X →
+                        ∃∃W,V,T. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V &
+                                 L ⊢ ⓐY.V ⬌* U & ⦃h, L⦄ ⊢ V :* ⓛW.T.
+#h #L #Z #U #H elim H -L -Z -U
+[ #L #k #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct
+| #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
+| #L #V #W #Z #U #HVW #HZU #_ #_ #X #Y #H destruct /2 width=7/
+| #L #V #W #Z #U #HZU #_ #_ #IHUW #X #Y #H destruct
+  elim (IHUW U Y ?) -IHUW // /3 width=9/
+| #L #Z #U #_ #_ #X #Y #H destruct
+| #L #Z #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
+  elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #W #V #T #HYW #HXV #HU1 #HVT
+  lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=7/
+]
+qed.
+
+(* Basic_1: was only: ty3_gen_appl *)
+lemma nta_inv_pure1: ∀h,L,Y,X,U. ⦃h, L⦄ ⊢ ⓐY.X : U →
+                     ∃∃W,V,T. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V &
+                              L ⊢ ⓐY.V ⬌* U & ⦃h, L⦄ ⊢ V :* ⓛW.T.
+/2 width=3/ qed-.
+
+axiom nta_inv_appl1: ∀h,L,Z,Y,X,U. ⦃h, L⦄ ⊢ ⓐZ.ⓛY.X : U →
+                     ∃∃W. ⦃h, L⦄ ⊢ Z : Y & ⦃h, L⦄ ⊢ ⓛY.X : ⓛY.W &
+                     L ⊢ ⓐZ.ⓛY.W ⬌* U.
+(* REQUIRES SUBJECT REDUCTION
+#h #L #Z #Y #X #U #H
+elim (nta_inv_pure1 … H) -H #W #V #T #HZW #HXV #HVU #HVT
+elim (nta_inv_bind1 … HXV) -HXV #Y0 #X0 #HY0 #HX0 #HX0V
+lapply (cpcs_trans … (ⓐZ.ⓛY.X0) … HVU) -HVU /2 width=1/ -HX0V #HX0U
+@(ex3_1_intro … HX0U) /2 width=2/
+*)
index 8a947e683f9ffadc53cf479ca0b796f65d5269d5..31126679ff7a34ea367f3fc2d18b30f496d20d61 100644 (file)
@@ -365,3 +365,9 @@ notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 :: break term 46 T2 )"
 notation "hvbox( h ⊢ break term 46 L1 : ⊑ break term 46 L2 )"
    non associative with precedence 45
    for @{ 'CrSubEqN $h $L1 $L2 }.
+
+(* Higher order dynamic typing **********************************************)
+
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 46 T1 :* break term 46 T2 )"
+   non associative with precedence 45
+   for @{ 'NativeTypeStar $h $L $T1 $T2 }.
index 9994fdd6be938ffaf49680bdc5108dd1d2e4df1f..6db1a47aa9c1f2ad09977a56adf6c6c1b1a04fc9 100644 (file)
@@ -32,11 +32,22 @@ lemma cpr_abst: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀V,T1,T2.
                 L.ⓛV ⊢ T1 ➡ T2 → L ⊢ ⓛV1. T1 ➡ ⓛV2. T2.
 #L #V1 #V2 * #V0 #HV10 #HV02 #V #T1 #T2 * #T0 #HT10 #HT02
 lapply (tpss_inv_S2 … HT02 L V ?) -HT02 // #HT02
-@(ex2_1_intro … (ⓛV0.T0)) /2 width=1/ -V1 -T1 (**) (* explicit constructors *)
-@tpss_bind // -V0
-@(tpss_lsubs_trans (L.ⓛV)) // -T0 -T2 /2 width=1/
+lapply (tpss_lsubs_trans … HT02 (L.ⓛV2) ?) -HT02 /2 width=1/ #HT02
+@(ex2_1_intro … (ⓛV0.T0)) /2 width=1/ (* explicit constructors *)
 qed.
 
+lemma cpr_beta: ∀L,V1,V2,W,T1,T2.
+                L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡ T2 → L ⊢ ⓐV1.ⓛW.T1 ➡ ⓓV2.T2.
+#L #V1 #V2 #W #T1 #T2 * #V #HV1 #HV2 * #T #HT1 #HT2
+lapply (tpss_inv_S2 … HT2 L W ?) -HT2 // #HT2
+lapply (tpss_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
+@(ex2_1_intro … (ⓓV.T)) /2 width=1/ (**) (* explicit constructor, /3/ is too slow *)
+qed.
+
+lemma cpr_beta_dx: ∀L,V1,V2,W,T1,T2.
+                   V1 ➡ V2 → L.ⓛW ⊢ T1 ➡ T2 → L ⊢ ⓐV1.ⓛW.T1 ➡ ⓓV2.T2.
+/3 width=1/ qed.
+
 (* Advanced inversion lemmas ************************************************)
 
 (* Basic_1: was: pr2_gen_lref *)
index a6846d3b870eebb61b2d10f6b0ca49d793b7d191..1fc544b1baebffb6fcb9c47c3babe3b4fc920c2e 100644 (file)
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/substitution/ldrop_sfr.ma".
 include "basic_2/unfold/tpss_lift.ma".
 include "basic_2/unfold/delift.ma".
 
@@ -28,7 +29,38 @@ lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus <plus_minus_m_m /
 lapply (lift_conf_be … HVU2 … HV2U ?) //
 >commutative_plus in ⊢ (??%??→?); <minus_plus_m_m /3 width=6/ 
 qed.
+
+fact sfr_delift_aux: ∀L,T,T1,d,e. d + e ≤ |L| → ≽ [d, e] L → T = T1 →
+                     ∃T2. L ⊢ T1 ▼*[d, e] ≡ T2.
+#L #T @(cw_wf_ind … L T) -L -T #L #T #IH * * /2 width=2/
+[ #i #d #e #Hde #HL #H destruct
+  elim (lt_or_ge i d) #Hdi [ /3 width=2/ ]
+  elim (lt_or_ge i (d+e)) #Hide [2: /3 width=2/ ]
+  lapply (lt_to_le_to_lt … Hide Hde) #Hi
+  elim (ldrop_O1 … Hi) -Hi #I #K #V1 #HLK
+  lapply (sfr_inv_ldrop … HLK … HL ? ?) // #H destruct
+  lapply (ldrop_pair2_fwd_cw … HLK (#i)) #HKL
+  lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
+  lapply (ldrop_fwd_O1_length … HLK0) #H
+  lapply (sfr_ldrop_trans_be_up … HLK0 … HL ? ?) -HLK0 -HL
+  [1,2: /2 width=1/ | <minus_n_O <minus_plus ] #HK
+  elim (IH … HKL … HK ?) -IH -HKL -HK
+  [3: // |2: skip |4: >H -H /2 width=1/ ] -Hde -H #V2 #V12 (**) (* H erased two times *)
+  elim (lift_total V2 0 d) /3 width=7/
+| #I #V1 #T1 #d #e #Hde #HL #H destruct
+  elim (IH … V1 … Hde HL ?) [2,4: // |3: skip ] #V2 #HV12
+  elim (IH (L.ⓑ{I}V1) T1 ? ? (d+1) e ? ? ?) -IH [3,6: // |2: skip |4,5: /2 width=1/ ] -Hde -HL #T2 #HT12
+  lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/ /3 width=4/
+| #I #V1 #T1 #d #e #Hde #HL #H destruct
+  elim (IH … V1 … Hde HL ?) [2,4: // |3: skip ] #V2 #HV12
+  elim (IH … T1 … Hde HL ?) -IH -Hde -HL [3,4: // |2: skip ] /3 width=2/
+]
+qed.
+
+lemma sfr_delift: ∀L,T1,d,e. d + e ≤ |L| → ≽ [d, e] L →
+                  ∃T2. L ⊢ T1 ▼*[d, e] ≡ T2.
+/2 width=2/ qed-.
+
 (* Advanced inversion lemmas ************************************************)
 
 lemma delift_inv_lref1_lt: ∀L,U2,i,d,e. L ⊢ #i ▼*[d, e] ≡ U2 → i < d → U2 = #i.
index fff92a290856e666455a8c84618343176750dbed..4aaba50b38e4b554a3dca141cefce2b1f5e59200 100644 (file)
@@ -28,6 +28,7 @@
     <key name="ex">5 2</key>
     <key name="ex">5 3</key>
     <key name="ex">5 4</key>
+    <key name="ex">5 5</key>
     <key name="ex">6 4</key>
     <key name="ex">6 6</key>
     <key name="ex">7 6</key>
index 6fe0ca0379a33b26b6ebfd0992aee742a5efe9bc..6214557bb7881406de4092f7d216efeb9988caad 100644 (file)
@@ -128,6 +128,14 @@ inductive ex5_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→Prop)
 
 interpretation "multiple existental quantifier (5, 4)" 'Ex P0 P1 P2 P3 P4 = (ex5_4 ? ? ? ? P0 P1 P2 P3 P4).
 
+(* multiple existental quantifier (5, 5) *)
+
+inductive ex5_5 (A0,A1,A2,A3,A4:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→A3→A4→Prop) : Prop ≝
+   | ex5_5_intro: ∀x0,x1,x2,x3,x4. P0 x0 x1 x2 x3 x4 → P1 x0 x1 x2 x3 x4 → P2 x0 x1 x2 x3 x4 → P3 x0 x1 x2 x3 x4 → P4 x0 x1 x2 x3 x4 → ex5_5 ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (5, 5)" 'Ex P0 P1 P2 P3 P4 = (ex5_5 ? ? ? ? ? P0 P1 P2 P3 P4).
+
 (* multiple existental quantifier (6, 4) *)
 
 inductive ex6_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2→A3→Prop) : Prop ≝
index 86f68b60833400b04bfafabe061c4e6578cad8f9..e1e2240ceb209339c23ebcbc6f4d5a75723889e3 100644 (file)
@@ -154,6 +154,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P4) }.
 
+(* multiple existental quantifier (5, 5) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.λ${ident x4}.$P4) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 , ident x4 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.λ${ident x4}:$T4.$P4) }.
+
 (* multiple existental quantifier (6, 4) *)
 
 notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5)"