--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "apps_2/MLTT1_1/syntax.ma".
+
+(* PRIMITIVE GLOBAL CONSTANTS **********************************************)
+
+(* symbolic names for referring the primitive global constants *)
+
+definition empty ≝ 0. (* empty type *)
+
+definition erec ≝ 1. (* empty eliminator *)
+
+definition one ≝ 2. (* unit type *)
+
+definition tt ≝ 3. (* unit constructor *)
+
+definition orec ≝ 4. (* unit eliminator *)
+
+definition nat ≝ 5. (* natural numbers type *)
+
+definition zero ≝ 6. (* natural numbers constructor: zero *)
+
+definition succ ≝ 7. (* natural numbers constructor: successor *)
+
+definition nrec ≝ 8. (* natural numbers eliminator *)
+
+definition ii ≝ 9. (* intensional identity type *)
+
+definition refl ≝ 10. (* intensional identity constructor *)
+
+definition irec ≝ 11. (* intensional identity eliminator *)
+
+definition sum ≝ 12. (* disjoint sum type *)
+
+definition sn ≝ 13. (* disjoint sum constructor: left *)
+
+definition dx ≝ 14. (* disjoint sum constructor: right *)
+
+definition srec ≝ 15. (* disjoint sum eliminator *)
+
+definition prod ≝ 16. (* dependent product type *)
+
+definition pair ≝ 17. (* dependent product constructor *)
+
+definition prec ≝ 18. (* dependent product eliminator *)
+
+definition fun ≝ 19. (* dependent function type *)
+
+definition abst ≝ 20. (* dependent function constructor *)
+
+definition ap ≝ 21. (* dependent function eliminator *)
+
+definition univ ≝ 22. (* first universe type *)
+
+definition ue ≝ 23. (* first universe constructor: empty *)
+
+definition uo ≝ 24. (* first universe constructor: one *)
+
+definition un ≝ 25. (* first universe constructor: nat *)
+
+definition ui ≝ 26. (* first universe constructor: ii *)
+
+definition us ≝ 27. (* first universe constructor: sum *)
+
+definition up ≝ 28. (* first universe constructor: union *)
+
+definition uf ≝ 29. (* first universe constructor: fun *)
+
+definition urec ≝ 30. (* first universe eliminator *)
+
+definition primitives ≝ 31. (* number of primitive constants *)
+
+(* primitive global environment *)
+
+definition Gp: lenv ≝
+ ⋆
+ Λ □ (* empty *)
+ Λ □ ⤏ □ (* erec *)
+ Λ □ (* one *)
+ Λ □ (* tt *)
+ Λ □ ⤏ □ ⤏ □ (* orec *)
+ Λ □ (* nat *)
+ Λ □ (* zero *)
+ Λ □ ⤏ □ (* succ *)
+ Λ □ ⤏ □ ⤏ (□ ⤏ □ ⤏ □) ⤏ □ (* nrec *)
+ Λ □ ⤏ □ ⤏ □ ⤏ □ (* ii *)
+ Λ □ ⤏ □ (* refl *)
+ Λ □ ⤏ (□ ⤏ □) ⤏ □ (* irec *)
+ Λ □ ⤏ □ ⤏ □ (* sum *)
+ Λ □ ⤏ □ (* sn *)
+ Λ □ ⤏ □ (* dx *)
+ Λ □ ⤏ (□ ⤏ □) ⤏ (□ ⤏ □) ⤏ □ (* srec *)
+ Λ □ ⤏ (□ ⤏ □) ⤏ □ (* prod *)
+ Λ □ ⤏ □ ⤏ □ (* pair *)
+ Λ □ ⤏ (□ ⤏ □ ⤏ □) ⤏ □ (* prec *)
+ Λ □ ⤏ (□ ⤏ □) ⤏ □ (* fun *)
+ Λ (□ ⤏ □) ⤏ □ (* abst *)
+ Λ □ ⤏ □ ⤏ □ (* ap *)
+ Λ □ (* univ *)
+ Λ □ (* ue *)
+ Λ □ (* uo *)
+ Λ □ (* un *)
+ Λ □ ⤏ □ ⤏ □ ⤏ □ (* ui *)
+ Λ □ ⤏ □ ⤏ □ (* us *)
+ Λ □ ⤏ (□ ⤏ □) ⤏ □ (* up *)
+ Λ □ ⤏ (□ ⤏ □) ⤏ □ (* uf *)
+ Λ □ ⤏ □ (* urec *)
+.
+
+(* notation for applying the primitive constants *)
+
+interpretation
+ "empty type (MLTT)"
+ 'Empty = (TAtom (GRef empty)).
+
+interpretation
+ "empty eliminator (MLTT)"
+ 'ERec T = (TPair Appl T (TAtom (GRef erec))).
+
+interpretation
+ "unit type (MLTT)"
+ 'One = (TAtom (GRef one)).
+
+interpretation
+ "unit constructor (MLTT)"
+ 'TT = (TAtom (GRef tt)).
+
+interpretation
+ "unit eliminator (MLTT)"
+ 'SRec T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef srec)))).
+
+interpretation
+ "natural numbers type (MLTT)"
+ 'Nat = (TAtom (GRef nat)).
+
+interpretation
+ "natural numbers constructor: zero (MLTT)"
+ 'Zero = (TAtom (GRef zero)).
+
+interpretation
+ "natural numbers constructor: successor (MLTT)"
+ 'Succ T = (TPair Appl T (TAtom (GRef succ))).
+
+interpretation
+ "natural numbers eliminator (MLTT)"
+ 'NRec T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef nrec))))).
+
+interpretation
+ "intensional identity type (MLTT)"
+ 'II T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef ii))))).
+
+interpretation
+ "intensional identity constructor (MLTT)"
+ 'Refl T = (TPair Appl T (TAtom (GRef refl))).
+
+interpretation
+ "intensional identity eliminator (MLTT)"
+ 'IRec T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef irec)))).
+
+interpretation
+ "sum type (MLTT)"
+ 'Sum T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef sum)))).
+
+interpretation
+ "sum constructorL left (MLTT)"
+ 'Sn T = (TPair Appl T (TAtom (GRef sn))).
+
+interpretation
+ "sum constructor: right (MLTT)"
+ 'Dx T = (TPair Appl T (TAtom (GRef dx))).
+
+interpretation
+ "sum eliminator (MLTT)"
+ 'SRec T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef srec))))).
+
+interpretation
+ "product type (MLTT)"
+ 'Prod T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef prod)))).
+
+interpretation
+ "product constructor (MLTT)"
+ 'Pair T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef pair)))).
+
+interpretation
+ "product eliminator (MLTT)"
+ 'PRec T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef prec)))).
+
+interpretation
+ "function type (MLTT)"
+ 'Fun T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef fun)))).
+
+interpretation
+ "function constructor (MLTT)"
+ 'Abst T = (TPair Appl T (TAtom (GRef abst))).
+
+interpretation
+ "function eliminator (MLTT)"
+ 'AP T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef ap)))).
+
+interpretation
+ "first universe type (MLTT)"
+ 'Univ = (TAtom (GRef univ)).
+
+interpretation
+ "first universe constructor: empty (MLTT)"
+ 'UE = (TAtom (GRef ue)).
+
+interpretation
+ "first universe constructor: one (MLTT)"
+ 'UO = (TAtom (GRef us)).
+
+interpretation
+ "first universe constructor: nat (MLTT)"
+ 'UN = (TAtom (GRef un)).
+
+interpretation
+ "first universe constructor: ii (MLTT)"
+ 'UI T1 T2 T3 = (TPair Appl T3 (TPair Appl T2 (TPair Appl T1 (TAtom (GRef ui))))).
+
+interpretation
+ "first universe constructor: sum (MLTT)"
+ 'US T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef us)))).
+
+interpretation
+ "first universe constructor: product (MLTT)"
+ 'UP T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef up)))).
+
+interpretation
+ "first universe constructor: function (MLTT)"
+ 'UF T1 T2 = (TPair Appl T2 (TPair Appl T1 (TAtom (GRef uf)))).
+
+interpretation
+ "first universe eliminator (MLTT)"
+ 'URec T = (TPair Appl T (TAtom (GRef urec))).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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/unfold/delift.ma".
+include "apps_2/MLTT1_1/genv_primitive.ma".
+
+(* JUDJEMENTS ***************************************************************)
+
+(* type judgement *)
+inductive TJ: lenv → predicate term ≝
+| tj_weak : ∀L,V,T1,T2. TJ L V → TJ L T1 → ⇧[0,1] T1 ≡ T2 → TJ (L Λ V) T2
+| tj_empty: TJ (⋆) 𝔼
+| tj_one : TJ (⋆) 𝕆
+| tj_sum : ∀G,A,B. TJ G A → TJ G B → TJ G (A ⊕ B)
+.
+
+(* element judgement *)
+inductive EJ: lenv → relation term ≝
+| tj_erec: ∀L,V,T1,T2.
+ EJ L V 𝔼 → TJ (L Λ 𝔼) T1 → L Δ V ⊢ T1 [0,1] ≡ T2 → EJ L 𝕖𝕣[V] T2
+| tj_tt : EJ (⋆) 𝕥 𝕆
+.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* NOTATION FOR MARTIN-LÖF TYPE THEORY WITH ONE UNIVERSE (MLTT1) ************)
+
+(* Syntax extension *********************************************************)
+
+notation "hvbox( □ )"
+ non associative with precedence 90
+ for @{ 'Box }.
+
+notation "hvbox(T1 break ⤏ T2)"
+ right associative with precedence 65
+ for @{ 'TImp $T1 $T2 }.
+
+notation "hvbox( L break Λ T )"
+ left associative with precedence 60
+ for @{ 'LAbst $L $T }.
+
+notation "hvbox( L break Δ T )"
+ left associative with precedence 60
+ for @{ 'LAbbr $L $T }.
+
+notation "hvbox( Λ T )"
+ non associative with precedence 65
+ for @{ 'TAbst $T }.
+
+(* Primitive global constants ***********************************************)
+
+notation "hvbox( 𝔼 )"
+ non associative with precedence 90
+ for @{ 'Empty }.
+
+notation "hvbox( 𝕖𝕣 [ T ] )"
+ non associative with precedence 90
+ for @{ 'ERec $T }.
+
+notation "hvbox( 𝕆 )"
+ non associative with precedence 90
+ for @{ 'One }.
+
+notation "hvbox( 𝕥 )"
+ non associative with precedence 90
+ for @{ 'TT }.
+
+notation "hvbox( 𝕠𝕣 [ T1 , break T2 ] )"
+ non associative with precedence 90
+ for @{ 'ORec $T1 $T2 }.
+(*
+notation "hvbox( ℕ )"
+ non associative with precedence 90
+ for @{ 'Nat }.
+
+notation "hvbox( 𝕫 )"
+ non associative with precedence 90
+ for @{ 'Zero }.
+
+notation "hvbox( 𝕤 [ T ] )"
+ non associative with precedence 90
+ for @{ 'Succ $T }.
+
+notation "hvbox( 𝕟𝕣 [ T1 , break T2 , break T3 ] )"
+ non associative with precedence 90
+ for @{ 'NRec $T1 $T2 $3 }.
+*)
+notation "hvbox( T1 ⊕ T2 )"
+ left associative with precedence 70
+ for @{ 'Sum $T1 $T2 }.
+
+notation "hvbox( 𝕤𝕟 [ T ] )"
+ non associative with precedence 90
+ for @{ 'Sn $T }.
+
+notation "hvbox( 𝕕𝕩 [ T ] )"
+ non associative with precedence 90
+ for @{ 'Dx $T }.
+
+notation "hvbox( 𝕤𝕣 [ T1 , break T2 , break T3 ] )"
+ non associative with precedence 90
+ for @{ 'SRec $T1 $T2 $3 }.
+(*
+notation "hvbox( 𝕌 )"
+ non associative with precedence 90
+ for @{ 'Univ }.
+
+notation "hvbox( 𝕖 )"
+ non associative with precedence 90
+ for @{ 'UE }.
+
+notation "hvbox( 𝕠 )"
+ non associative with precedence 90
+ for @{ 'UO }.
+
+notation "hvbox( 𝕟 )"
+ non associative with precedence 90
+ for @{ 'UN }.
+*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+(* MARTIN-LÖF TYPE THEORY WITH ONE UNIVERSE (MLTT1): MATITA SOURCE FILES
+ * Specification started: 2011 December 12
+ * - Patience on me to gain peace and perfection! -
+ *)
+
+include "basic_2/grammar/lenv.ma".
+include "apps_2/MLTT1_1/notation.ma".
+
+(* EXTENDED NOTATION ********************************************************)
+
+definition sort ≝ 0.
+
+interpretation
+ "global definition"
+ 'LAbbr L T = (LPair L Abbr T).
+
+interpretation
+ "global declaration"
+ 'LAbst L T = (LPair L Abst T).
+
+interpretation
+ "atom (arity)"
+ 'Box = (TAtom (Sort sort)).
+
+interpretation
+ "function (arity)"
+ 'TImp T1 T2 = (TPair Abst T1 T2).
+
+interpretation
+ "function (term)"
+ 'TAbst T = (TPair Abst (TAtom (Sort sort)) T).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 *)
+(* *)
+(**************************************************************************)
+
+notation "hvbox( [ term 46 d ⬐ break term 46 V ] break term 46 T )"
+ non associative with precedence 46
+ for @{ 'DSubst $V $d $T }.
+
+include "basic_2/unfold/delift_lift.ma".
+include "apps_2/functional/lift.ma".
+
+(* FUNCTIONAL DELIFTING SUBSTITUTION ****************************************)
+
+let rec fdsubst W d U on U ≝ match U with
+[ TAtom I ⇒ match I with
+ [ Sort _ ⇒ U
+ | LRef i ⇒ tri … i d (#i) (↑[0, i] W) (#(i-1))
+ | GRef _ ⇒ U
+ ]
+| TPair I V T ⇒ match I with
+ [ Bind2 a I ⇒ ⓑ{a,I} (fdsubst W d V). (fdsubst W (d+1) T)
+ | Flat2 I ⇒ ⓕ{I} (fdsubst W d V). (fdsubst W d T)
+ ]
+].
+
+interpretation
+ "functional delifting substitution"
+ 'DSubst V d T = (fdsubst V d T).
+
+(* Main properties **********************************************************)
+
+theorem fdsubst_delift: ∀K,V,T,L,d.
+ ⇩[0, d] L ≡ K. ⓓV → L ⊢ ▼*[d, 1] T ≡ [d ⬐ V] T.
+#K #V #T elim T -T
+[ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/
+ elim (lt_or_eq_or_gt i d) #Hid
+ [ -HLK >(tri_lt ?????? Hid) /3 width=3/
+ | destruct >tri_eq /4 width=4 by tpss_strap2, tps_subst, le_n, ex2_intro/ (**) (* too slow without trace *)
+ | -HLK >(tri_gt ?????? Hid) /3 width=3/
+ ]
+| * /3 width=1/ /4 width=1/
+]
+qed.
+
+(* Main inversion properties ************************************************)
+
+theorem fdsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV →
+ L ⊢ ▼*[d, 1] T1 ≡ T2 → [d ⬐ V] T1 = T2.
+#K #V #T1 elim T1 -T1
+[ * #i #L #T2 #d #HLK #H
+ [ -HLK >(delift_inv_sort1 … H) -H //
+ | elim (lt_or_eq_or_gt i d) #Hid normalize
+ [ -HLK >(delift_inv_lref1_lt … H) -H // /2 width=1/
+ | destruct
+ elim (delift_inv_lref1_be … H ? ?) -H // #K0 #V0 #V2 #HLK0
+ lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H >minus_plus <minus_n_n #HV2 #HVT2 destruct
+ >(delift_inv_refl_O2 … HV2) -V >(flift_inv_lift … HVT2) -V2 //
+ | -HLK >(delift_inv_lref1_ge … H) -H // /2 width=1/
+ ]
+ | -HLK >(delift_inv_gref1 … H) -H //
+ ]
+| * [ #a ] #I #V1 #T1 #IHV1 #IHT1 #L #X #d #HLK #H
+ [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/
+ | elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
+ <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 //
+ ]
+]
+qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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/unfold/delift_lift.ma".
-include "apps_2/functional/lift.ma".
-
-(* FUNCTIONAL DELIFTING SUBSTITUTION ****************************************)
-
-let rec fdsubst W d U on U ≝ match U with
-[ TAtom I ⇒ match I with
- [ Sort _ ⇒ U
- | LRef i ⇒ tri … i d (#i) (↑[0, i] W) (#(i-1))
- | GRef _ ⇒ U
- ]
-| TPair I V T ⇒ match I with
- [ Bind2 a I ⇒ ⓑ{a,I} (fdsubst W d V). (fdsubst W (d+1) T)
- | Flat2 I ⇒ ⓕ{I} (fdsubst W d V). (fdsubst W d T)
- ]
-].
-
-interpretation
- "functional delifting substitution"
- 'DSubst V d T = (fdsubst V d T).
-
-(* Main properties **********************************************************)
-
-theorem fdsubst_delift: ∀K,V,T,L,d.
- ⇩[0, d] L ≡ K. ⓓV → L ⊢ ▼*[d, 1] T ≡ [d ⬐ V] T.
-#K #V #T elim T -T
-[ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/
- elim (lt_or_eq_or_gt i d) #Hid
- [ -HLK >(tri_lt ?????? Hid) /3 width=3/
- | destruct >tri_eq /4 width=4 by tpss_strap2, tps_subst, le_n, ex2_intro/ (**) (* too slow without trace *)
- | -HLK >(tri_gt ?????? Hid) /3 width=3/
- ]
-| * /3 width=1/ /4 width=1/
-]
-qed.
-
-(* Main inversion properties ************************************************)
-
-theorem fdsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV →
- L ⊢ ▼*[d, 1] T1 ≡ T2 → [d ⬐ V] T1 = T2.
-#K #V #T1 elim T1 -T1
-[ * #i #L #T2 #d #HLK #H
- [ -HLK >(delift_inv_sort1 … H) -H //
- | elim (lt_or_eq_or_gt i d) #Hid normalize
- [ -HLK >(delift_inv_lref1_lt … H) -H // /2 width=1/
- | destruct
- elim (delift_inv_lref1_be … H ? ?) -H // #K0 #V0 #V2 #HLK0
- lapply (ldrop_mono … HLK0 … HLK) -HLK0 -HLK #H >minus_plus <minus_n_n #HV2 #HVT2 destruct
- >(delift_inv_refl_O2 … HV2) -V >(flift_inv_lift … HVT2) -V2 //
- | -HLK >(delift_inv_lref1_ge … H) -H // /2 width=1/
- ]
- | -HLK >(delift_inv_gref1 … H) -H //
- ]
-| * [ #a ] #I #V1 #T1 #IHV1 #IHT1 #L #X #d #HLK #H
- [ elim (delift_inv_bind1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/
- | elim (delift_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
- <(IHV1 … HV12) -IHV1 -HV12 // <(IHT1 … HT12) -IHT1 -HT12 //
- ]
-]
-qed-.
(* *)
(**************************************************************************)
-include "basic_2/substitution/lift.ma".
+include "basic_2/relocation/lift.ma".
include "apps_2/functional/notation.ma".
(* FUNCTIONAL RELOCATION ****************************************************)
non associative with precedence 46
for @{ 'Lift $d $e $T }.
-notation "hvbox( [ term 46 d ⬐ break term 46 V ] break term 46 T )"
- non associative with precedence 46
- for @{ 'DSubst $V $d $T }.
-
notation "hvbox( T1 ⇨ break term 46 T2 )"
non associative with precedence 45
for @{ 'SRed $T1 $T2 }.
include "basic_2/grammar/term_vector.ma".
include "basic_2/grammar/genv.ma".
+include "apps_2/functional/notation.ma".
(* REDUCTION AND TYPE MACHINE ***********************************************)
]
}
]
- class "yellow"
+(*
+ class "orange"
[ { "MLTT1" * } {
[ { "" * } {
[ "genv_primitive" "judgement" * ]
]
}
]
- class "orange"
+*)
+ class "red"
[ { "functional" * } {
[ { "reduction and type machine" * } {
[ "rtm" "rtm_step ( ? ⇨ ? )" * ]
}
]
- [ { "unfold" * } {
- [ "lift ( ↑[?,?] ? )" "subst ( [?←?] ? )" * ]
- }
- ]
- }
- ]
- class "red"
- [ { "examples" * } {
- [ { "" * } {
- [ "" * ]
+ [ { "relocation" * } {
+ [ "lift ( ↑[?,?] ? )" * ]
}
]
}
[ #i #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2
elim (snv_inv_lref … H) -H #I2 #K2 #W2 #HLK2 #HW2
elim (lsubsv_ldrop_O1_trans … HL12 … HLK2) -HL12 #X #H #HLK1
- lapply (ldrop_pair2_fwd_fw … HLK2 (#i)) -HLK2 #HLK2
elim (lsubsv_inv_pair2 … H) -H * #K1
- [ #HK12 #H destruct /4 width=8 by snv_lref, fw_ygt/ (**) (* auto too slow without trace *)
+ [ #HK12 #H destruct
+ /5 width=8 by snv_lref, fsupp_ygt, fsupp_lref/ (**) (* auto too slow without trace *)
| #W1 #V1 #V2 #l #HV1 #_ #_ #_ #_ #_ #H #_ destruct /2 width=5/
]
| #p #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2 -IH1
lapply (cpcs_cprs_strap1 … HW10 … HW0) -W0 #H
elim (cpcs_inv_cprs … H) -H #W0 #HW10 #HW0
lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU ?) [ /2 width=1/ ] -HTU -HW0
- /4 width=8 by snv_appl, fw_ygt/ (**) (* auto too slow without trace *)
+ /4 width=8 by snv_appl, fsupp_ygt/ (**) (* auto too slow without trace *)
| #W #T #HL0 #HT0 #H #L1 #HL12 destruct -IH4 -IH3 -IH2
elim (snv_inv_cast … H) -H #U #l #HW #HT #HTU #HUW
lapply (lsubsv_cpcs_trans … HL12 … HUW) -HUW #HUW
elim (lsubsv_ssta_trans … HTU … HL12) -HTU #U0 #HTU0 #HU0
- lapply (cpcs_trans … HU0 … HUW) -U /4 width=4 by snv_cast, fw_ygt/ (**) (* auto too slow without trace *)
+ lapply (cpcs_trans … HU0 … HUW) -U /4 width=4 by snv_cast, fsupp_ygt/ (**) (* auto too slow without trace *)
]
qed-.
[ #I1 #L1 #V1 #H
elim (snv_inv_lref … H) -H #I2 #L2 #V2 #H #HV2
lapply (ldrop_inv_refl … H) -H #H destruct //
-|2,3: #a #I #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H //
-|4,5: * #L1 #V1 #T1 #H
+|2: *
+|5: /3 width=7 by snv_inv_lift/
+]
+[1,3: #a #I #L1 #V1 #T1 #H elim (snv_inv_bind … H) -H //
+|2,4: * #L1 #V1 #T1 #H
[1,3: elim (snv_inv_appl … H) -H //
|2,4: elim (snv_inv_cast … H) -H //
]
-| /3 width=7 by snv_inv_lift/
]
qed-.
elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1
elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
- lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKL
+ lapply (fsupp_lref … HLK1) #HKL
elim (cpr_inv_lref1 … H2) -H2
[ #H destruct -HLK1
lapply (IH1 … HV12 … HK12) -IH1 -HV12 -HK12 // -HV1 [ /2 width=1/ ] -HKL /2 width=5/
| * #K0 #V0 #W0 #H #HVW0 #W0 -HV12
- lapply (ldrop_mono … H … HLK1) -HLK1 -H #H destruct
+ lapply (ldrop_mono … H … HLK1) -HLK1 -H #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2
lapply (IH1 … HVW0 … HK12) -IH1 -HVW0 -HK12 // -HV1 [ /2 width=1/ ] -HKL /3 width=7/
]
lapply (IH1 … HT20 … HT202 … (L2.ⓛW20) ?) [1,2: /2 width=1/ ] -HT20 #HT2
lapply (IH2 … HVW2) //
[ @(ygt_yprs_trans … L1 L1 … V1) (**) (* auto /4 width=5/ is a bit slow even with trace *)
- [ /2 width=1 by fw_ygt/
+ [ /2 width=1 by fsupp_ygt/
| /3 width=1 by cprs_lpr_yprs, cpr_cprs/
]
] #HW2
elim (snv_fwd_ssta … HW20) #l0 #U20 #HWU20
elim (ssta_fwd_correct … HVW2) <minus_plus_m_m #U2 #HWU2
elim (ssta_cpcs_lpr_aux … IH1 IH3 … HWU2 … HWU20 … HW220 … L2) // -IH3
- [2: /4 width=4 by ygt_yprs_trans, fw_ygt, ypr_yprs, ypr_lpr/
+ [2: /4 width=4 by ygt_yprs_trans, fsupp_ygt, ypr_yprs, ypr_lpr/
|3: @(ygt_yprs_trans … L1 L2 … V2) (**) (* auto not tried *)
[ @(ygt_yprs_trans … L1 L1 … V1)
- [ /2 width=1 by fw_ygt/
+ [ /2 width=1 by fsupp_ygt/
| /3 width=1 by cprs_lpr_yprs, cpr_cprs/
]
| /3 width=2 by ypr_ssta, ypr_yprs/
lapply (IH4 … HT2 (L2.ⓓV2) ?)
[ /2 width=6/
| @(ygt_yprs_trans … (L1.ⓛW20) … T2) (**) (* auto /5 width=5/ is too slow even with trace timeout=35 *)
- [ /4 width=4 by ygt_yprs_trans, fw_ygt, ypr_yprs, ypr_cpr/
+ [ /4 width=4 by ygt_yprs_trans, fsupp_ygt, ypr_yprs, ypr_cpr/
| /4 width=1 by ypr_yprs, ypr_lpr, lpr_pair/
]
] -L1 -V1 -W2 -T20 -U20 -W20 -l0 /2 width=1/
elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1
elim (ssta_inv_lref1 … H2) -H2 * #K0 #V0 #W1 [| #l ] #H #HVW1 #HX [| #_ ]
lapply (ldrop_mono … H … HLK1) -H #H destruct
- lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #H
+ lapply (fsupp_lref … HLK1) #H
lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /4 width=7/
| #p #HL0 #HT0 #H1 #X #l #H2 destruct -IH3 -IH2 -IH1
elim (snv_inv_gref … H1)
elim (ssta_inv_lref1 … H2) -H2 * #K1
#V1 #W1 [| #l0 ] #HLK1 #HVW1 #HWU1 [| #H destruct ]
lapply (ldrop_mono … H … HLK1) -H #H destruct
- lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1
+ lapply (fsupp_lref … HLK1) #HKV1
elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
lapply (ldrop_fwd_ldrop2 … HLK2) #H2
lapply (IH3 … HVW1) -IH3 // [ /2 width=1/ ] #HW1
elim (ssta_cpcs_lpr_aux … IH2 IH1 … HWX1 … HWV … L1) -IH2 -HWX1 //
[2: /2 width=1/
- |3: /4 width=4 by ygt_yprs_trans, fw_ygt, sstas_yprs, ssta_sstas/
+ |3: /4 width=4 by ygt_yprs_trans, fsupp_ygt, sstas_yprs, ssta_sstas/
] #H #_ destruct -X1
elim (IH1 … HVW1 … HV12 … HL12) -HVW1 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12
elim (IH1 … HWV W … HL12) -HWV // -HW [2: /2 width=1/ ] #V0 #HWV0 #_
/3 width=4 by ygt_strap2/
qed-.
-lemma fw_ygt: ∀h,g,L1,L2,T1,T2. ♯{L2, T2} < ♯{L1, T1} → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
-/3 width=1/ qed.
+lemma fsupp_ygt: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ >[g] ⦃L2, T2⦄.
+#h #g #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -L2 -T2 /3 width=1/ /3 width=4/
+qed.
lemma cprs_ygt: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) →
h ⊢ ⦃L, T1⦄ >[g] ⦃L, T2⦄.
(* *)
(**************************************************************************)
+include "basic_2/relocation/fsup.ma".
include "basic_2/reduction/lpr.ma".
include "basic_2/dynamic/lsubsv.ma".
(* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************)
inductive ypr (h) (g) (L1) (T1): relation2 lenv term ≝
-| ypr_fw : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ypr h g L1 T1 L2 T2
+| ypr_fsup : ∀L2,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ypr h g L1 T1 L2 T2
| ypr_lpr : ∀L2. L1 ⊢ ➡ L2 → ypr h g L1 T1 L2 T1
| ypr_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → ypr h g L1 T1 L1 T2
| ypr_ssta : ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ypr h g L1 T1 L1 T2
(* *)
(**************************************************************************)
+include "basic_2/substitution/fsupp.ma".
include "basic_2/computation/lprs.ma".
include "basic_2/dynamic/ypr.ma".
h ⊢ ⦃L, T⦄ ≥[g] ⦃L2, T2⦄ → h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
/2 width=4/ qed-.
-lemma fw_yprs: ∀h,g,L1,L2,T1,T2. ♯{L2, T2} < ♯{L1, T1} →
- h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
-/3 width=1/ qed.
+(* Note: this is a general property of bi_TC *)
+lemma fsupp_yprs: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ →
+ h ⊢ ⦃L1, T1⦄ ≥[g] ⦃L2, T2⦄.
+#h #g #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -L2 -T2 /3 width=1/ /3 width=4/
+qed.
lemma cprs_yprs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → h ⊢ ⦃L, T1⦄ ≥[g] ⦃L, T2⦄.
#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=4 by ypr_cpr, yprs_strap1/
(* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************)
inductive ysc (h) (g) (L1) (T1): relation2 lenv term ≝
-| ysc_fw : ∀L2,T2. ♯{L2, T2} < ♯{L1, T1} → ysc h g L1 T1 L2 T2
+| ysc_fsup : ∀L2,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ysc h g L1 T1 L2 T2
| ysc_cpr : ∀T2. L1 ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ysc h g L1 T1 L1 T2
| ysc_ssta : ∀T2,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, T2⦄ → ysc h g L1 T1 L1 T2
| ysc_lsubsv: ∀L2. h ⊢ L2 ¡⊑[g] L1 → (L1 = L2 → ⊥) → ysc h g L1 T1 L2 T1
inductive fsup: bi_relation lenv term ≝
| fsup_lref : ∀I,L,V. fsup (L.ⓑ{I}V) (#0) L V
-| fsup_bind_sn: ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) L V
+| fsup_pair_sn: ∀I,L,V,T. fsup L (②{I}V.T) L V
| fsup_bind_dx: ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
-| fsup_flat_sn: ∀I,L,V,T. fsup L (ⓕ{I}V.T) L V
| fsup_flat_dx: ∀I,L,V,T. fsup L (ⓕ{I}V.T) L T
| fsup_ldrop : ∀L1,K1,K2,T1,T2,U1,d,e.
⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 →
fact fsup_fwd_length_lref1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀i. T1 = #i → |L2| < |L1|.
#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2
-[ 6: #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct
- lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
- elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct
- @(lt_to_le_to_lt … HLK1) /2 width=2/
-| normalize // |2,3: #a
+[5: #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct
+ lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
+ elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct
+ @(lt_to_le_to_lt … HLK1) /2 width=2/
+| normalize // |3: #a
] #I #L #V #T #j #H destruct
qed-.
⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄.
/2 width=4/ qed.
+lemma fsupp_lref: ∀I,K,V,i,L. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃L, #i⦄ ⊃+ ⦃K, V⦄.
+/3 width=2/ qed.
+
+lemma fsupp_pair_sn: ∀I,L,V,T. ⦃L, ②{I}V.T⦄ ⊃+ ⦃L, V⦄.
+/2 width=1/ qed.
+
+lemma fsupp_bind_dx: ∀a,K,I,V,T. ⦃K, ⓑ{a,I}V.T⦄ ⊃+ ⦃K.ⓑ{I}V, T⦄.
+/2 width=1/ qed.
+
+lemma fsupp_flat_dx: ∀I,L,V,T. ⦃L, ⓕ{I}V.T⦄ ⊃+ ⦃L, T⦄.
+/2 width=1/ qed.
+
+lemma fsupp_flat_dx_pair_sn: ∀I1,I2,L,V1,V2,T. ⦃L, ⓕ{I1}V1.②{I2}V2.T⦄ ⊃+ ⦃L, V2⦄.
+/2 width=4/ qed.
+
+lemma fsupp_bind_dx_flat_dx: ∀a,I1,I2,L,V1,V2,T. ⦃L, ⓑ{a,I1}V1.ⓕ{I2}V2.T⦄ ⊃+ ⦃L.ⓑ{I1}V1, T⦄.
+/2 width=4/ qed.
+
+lemma fsupp_flat_dx_bind_dx: ∀a,I1,I2,L,V1,V2,T. ⦃L, ⓕ{I1}V1.ⓑ{a,I2}V2.T⦄ ⊃+ ⦃L.ⓑ{I2}V2, T⦄.
+/2 width=4/ qed.
+(*
+lemma fsupp_append_sn: ∀I,L,K,V,T. ⦃L.ⓑ{I}V@@K, T⦄ ⊃+ ⦃L, V⦄.
+#I #L #K #V *
+[ * #i
+normalize /3 width=1 by monotonic_lt_plus_l, monotonic_le_plus_r/ (**) (* auto too slow without trace *)
+qed.
+*)
(* Basic forward lemmas *****************************************************)
lemma fsupp_fwd_cw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}.
lemma fsupp_fsups_fsupp: ∀L1,L,L2,T1,T,T2. ⦃L1, T1⦄ ⊃+ ⦃L, T⦄ →
⦃L, T⦄ ⊃* ⦃L2, T2⦄ → ⦃L1, T1⦄ ⊃+ ⦃L2, T2⦄.
/2 width=4/ qed.
+(*
+lemma fsups_pippo: ∀L,T. ⦃L, T⦄ ⊃+ ⦃L, #0⦄.
+#L * *
+[ #i
+*)
(* Basic forward lemmas *****************************************************)
lemma fsup_cpss_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ▶* U2 →
∃∃L,U1. L1 ⊢ ▶* L & L ⊢ T1 ▶* U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄.
-#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ]
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [2: * ] [1,2,3,4,5: /3 width=5/ ]
#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2
elim (lift_total T d e) #U #HTU
lemma fsup_cpqs_trans: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ∀U2. L2 ⊢ T2 ➤* U2 →
∃∃L,U1. L1 ⊢ ➤* L & L ⊢ T1 ➤* U1 & ⦃L, U1⦄ ⊃ ⦃L2, U2⦄.
-#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1,2,3,4,5: /3 width=5/ ]
+#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [2: * ] [1,2,3,4,5: /3 width=5/ ]
#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
elim (IHT12 … HTU2) -IHT12 -HTU2 #K #T #HK1 #HT1 #HT2
elim (lift_total T d e) #U #HTU
}
]
(*
+ class "wine"
+ [ { "examples" * } {
+ [ { "" * } {
+ [ "" * ]
+ }
+ ]
+ }
+ ]
class "magenta"
[ { "higher order dynamic typing" * } {
[ { "higher order native type assignment" * } {
projects / helm.git / commitdiff