sn3/props sn3_appl_lref
sn3/props sn3_appl_abbr
sn3/props sn3_appl_cast
-sn3/props sn3_appl_appl
sn3/props sn3_appl_beta
sn3/props sn3_appl_appls
sn3/props sn3_appls_lref
--- /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/grammar/tstc.ma".
+include "Basic_2/reducibility/cpr_lift.ma".
+include "Basic_2/reducibility/lcpr_cpr.ma".
+include "Basic_2/computation/cprs_cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Forward lemmas involving same top term constructor ***********************)
+
+lemma cpr_fwd_theta: ∀L,V1,V,T,U. L ⊢ ⓐV1. ⓓV. T ➡ U →
+ ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1. ⓓV. T ≃ U ∨
+ L ⊢ ⓓV. ⓐV2. T ➡* U.
+#L #V1 #V #T #U #H #V2 #HV12
+elim (cpr_inv_appl1 … H) -H *
+[ -HV12 #V0 #X #_ #_ #H destruct /2 width=1/
+| -HV12 #V0 #W #T1 #T2 #_ #_ #H destruct
+| #V0 #V3 #W1 #W2 #T1 #T2 #HV10 #HW12 #HT12 #HV03 #H1 #H2 destruct
+ lapply (cpr_lift (L.ⓓW1) … HV12 … HV03 … HV10) -V0 -HV12 /2 width=1/ #HV23
+ lapply (lcpr_cpr_trans (L. ⓓW1) … HT12) -HT12 /2 width=1/ #HT12
+ /4 width=1/
+]
+qed-.
@csn_intro #X #H1 #H2
elim (cpr_inv_cast1 … H1) -H1
[ * #W0 #T0 #HLW0 #HLT0 #H destruct
- elim (eq_false_inv_tpair … H2) -H2
+ elim (eq_false_inv_tpair_sn … H2) -H2
[ /3 width=3/
| -HLW0 * #H destruct /3 width=1/
]
(**************************************************************************)
include "Basic_2/computation/acp_cr.ma".
-include "Basic_2/computation/csn_lift.ma".
+include "Basic_2/computation/csn_lcpr.ma".
+include "Basic_2/computation/csn_vector.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
(* Advanced properties ******************************************************)
+(*
+lemma csn_applv_theta: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+ ∀V,T. L ⊢ ⬇* ⓓV. ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T.
+#L #V1s #V2s * -V1s -V2s /2 width=1/
+#V1s #V2s #V1 #V2 #HV12 * -V1s -V2s /2 width=3/
+#V1s #V2s #W1 #W2 #HW12 #HV12s #V #T #H #HV
+lapply (csn_appl_theta … HV12 … H) -H -HV12 #H
+lapply (csn_fwd_pair_sn … H) #HV1
+@csn_appl_simple // #X #H1 #H2
+whd in ⊢ (? ? %);
+*)
+(*
+lemma csn_S5: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+ ∀V,T. L. ⓓV ⊢ ⬇* ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T.
+#L #V1s #V2s #H elim H -V1s -V2s /2 width=1/
+*)
axiom csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T).
[ #V0 #V1 #T1 #HLV0 #HLV01 #HLT1 #H destruct
lapply (cpr_intro … HLV0 HLV01) -HLV01 #HLV1
lapply (ltpr_cpr_trans (L. ⓓV) … HLT1) /2 width=1/ -V0 #HLT1
- elim (eq_false_inv_tpair … H2) -H2
+ elim (eq_false_inv_tpair_sn … H2) -H2
[ #HV1 @IHV // /2 width=1/ -HV1
@(csn_lcpr_conf (L. ⓓV)) /2 width=1/ -HLV1 /2 width=3/
| -IHV -HLV1 * #H destruct /3 width=1/
elim (lift_total V0 0 1) #V5 #HV05
elim (term_eq_dec (ⓓV.ⓐV2.T) (ⓓV4.ⓐV5.T3))
[ -IHVT #H0 destruct
- elim (eq_false_inv_tpair … H) -H
+ elim (eq_false_inv_tpair_sn … H) -H
[ -HLV10 -HLV34 -HV3 -HLT3 -HVT
>(lift_inj … HV12 … HV05) -V5
#H elim (H ?) //
@csn_intro #X #H1 #H2
elim (cpr_inv_abst1 … H1 I V) -H1
#W0 #T0 #HLW0 #HLT0 #H destruct
-elim (eq_false_inv_tpair … H2) -H2
+elim (eq_false_inv_tpair_sn … H2) -H2
[ /3 width=5/
| -HLW0 * #H destruct /3 width=1/
]
qed.
-(*
-axiom eq_false_inv_tpair_dx: ∀I,V1,T1,V2,T2.
- (②{I} V1. T1 = ②{I} V2. T2 → False) →
- (T1 = T2 → False) ∨ (T1 = T2 ∧ (V1 = V2 → False)).
-
-#I #V1 #T1 #V2 #T2 #H
-elim (term_eq_dec V1 V2) /3 width=1/ #HV12 destruct
-@or_intror @conj // #HT12 destruct /2 width=1/
-qed-.
-lemma csn_appl_simple: ∀L,T. L ⊢ ⬇* T → 𝐒[T] → ∀V. L ⊢ ⬇* V → L ⊢ ⬇* ⓐV. T.
-#L #T #H elim H -T #T #_ #IHT #HT #V #H @(csn_ind … H) -V #V #HV #IHV
+(* Basic_1: was only: sn3_appl_appl *)
+lemma csn_appl_simple: ∀L,V. L ⊢ ⬇* V → ∀T1.
+ (∀T2. L ⊢ T1 ➡ T2 → (T1 = T2 → False) → L ⊢ ⬇* ⓐV. T2) →
+ 𝐒[T1] → L ⊢ ⬇* ⓐV. T1.
+#L #V #H @(csn_ind … H) -V #V #_ #IHV #T1 #IHT1 #HT1
@csn_intro #X #H1 #H2
elim (cpr_inv_appl1_simple … H1 ?) // -H1
-#V0 #T0 #HLV0 #HLT0 #H destruct
+#V0 #T0 #HLV0 #HLT10 #H destruct
elim (eq_false_inv_tpair_dx … H2) -H2
-[ -IHV #HT0 @IHT -IHT // -HLT0 /2 width=1/ -HT0 /2 width=3/
-| -HV -HT -IHT -HLT0 * #H #HV0 destruct /3 width=1/
+[ -IHV -HT1 #HT10
+ @(csn_cpr_trans … (ⓐV.T0)) /2 width=1/ -HLV0
+ @IHT1 -IHT1 // /2 width=1/
+| -HLT10 * #H #HV0 destruct
+ @IHV -IHV // -HT1 /2 width=1/ -HV0
+ #T2 #HLT02 #HT02
+ @(csn_cpr_trans … (ⓐV.T2)) /2 width=1/ -HLV0
+ @IHT1 -IHT1 // -HLT02 /2 width=1/
+]
+qed.
+
+(* Basic_1: was only: sn3_appl_appls *)
+lemma csn_appl_appls_simple: ∀L,V. L ⊢ ⬇* V → ∀Vs,T1.
+ (∀T2. L ⊢ ⒶVs.T1 ➡ T2 → (ⒶVs.T1 = T2 → False) → L ⊢ ⬇* ⓐV. T2) →
+ 𝐒[T1] → L ⊢ ⬇* ⓐV. ⒶVs. T1.
+#L #V #HV #Vs elim Vs -Vs
+[ @csn_appl_simple //
+| #V0 #Vs #_ #T1 #HT1 #_
+ @csn_appl_simple // -HV @HT1
]
qed.
-*)
\ No newline at end of file
--- /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/grammar/term_vector.ma".
+include "Basic_2/computation/csn.ma".
+
+(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************)
+
+inductive csnv (L:lenv): predicate (list term) ≝
+| csnv_nil: csnv L ◊
+| csn_cons: ∀Ts,T. L ⊢ ⬇* T → csnv L Ts → csnv L (T :: Ts)
+.
+
+interpretation
+ "context-sensitive strong normalization (term vector)"
+ 'SN L Ts = (csnv L Ts).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact csnv_inv_cons_aux: ∀L,Ts. L ⊢ ⬇* Ts → ∀U,Us. Ts = U :: Us →
+ L ⊢ ⬇* U ∧ L ⊢ ⬇* Us.
+#L #Ts * -Ts
+[ #U #Us #H destruct
+| #Ts #T #HT #HTs #U #Us #H destruct /2 width=1/
+]
+qed.
+
+lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬇* T :: Ts → L ⊢ ⬇* T ∧ L ⊢ ⬇* Ts.
+/2 width=3/ qed-.
+
+include "Basic_2/computation/csn_cpr.ma".
+
+lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬇* Ⓐ Vs. T → L ⊢ ⬇* Vs ∧ L ⊢ ⬇* T.
+#L #T #Vs elim Vs -Vs /2 width=1/
+#V #Vs #IHVs #HVs
+lapply (csn_fwd_pair_sn … HVs) #HV
+lapply (csn_fwd_flat_dx … HVs) -HVs #HVs
+elim (IHVs HVs) -IHVs -HVs /3 width=1/
+qed-.
]
qed-.
-lemma eq_false_inv_tpair: ∀I,V1,T1,V2,T2.
- (②{I} V1. T1 = ②{I} V2. T2 → False) →
- (V1 = V2 → False) ∨ (V1 = V2 ∧ (T1 = T2 → False)).
+lemma eq_false_inv_tpair_sn: ∀I,V1,T1,V2,T2.
+ (②{I} V1. T1 = ②{I} V2. T2 → False) →
+ (V1 = V2 → False) ∨ (V1 = V2 ∧ (T1 = T2 → False)).
#I #V1 #T1 #V2 #T2 #H
elim (term_eq_dec V1 V2) /3 width=1/ #HV12 destruct
@or_intror @conj // #HT12 destruct /2 width=1/
qed-.
+lemma eq_false_inv_tpair_dx: ∀I,V1,T1,V2,T2.
+ (②{I} V1. T1 = ②{I} V2. T2 → False) →
+ (T1 = T2 → False) ∨ (T1 = T2 ∧ (V1 = V2 → False)).
+#I #V1 #T1 #V2 #T2 #H
+elim (term_eq_dec T1 T2) /3 width=1/ #HT12 destruct
+@or_intror @conj // #HT12 destruct /2 width=1/
+qed-.
+
lemma eq_false_inv_beta: ∀V1,V2,W1,W2,T1,T2.
(ⓐV1. ⓛW1. T1 = ⓐV2. ⓛW2 .T2 →False) →
(W1 = W2 → False) ∨
(W1 = W2 ∧ (ⓓV1. T1 = ⓓV2. T2 → False)).
#V1 #V2 #W1 #W2 #T1 #T2 #H
-elim (eq_false_inv_tpair … H) -H
+elim (eq_false_inv_tpair_sn … H) -H
[ #HV12 elim (term_eq_dec W1 W2) /3 width=1/
#H destruct @or_intror @conj // #H destruct /2 width=1/
| * #H1 #H2 destruct
- elim (eq_false_inv_tpair … H2) -H2 /3 width=1/
+ elim (eq_false_inv_tpair_sn … H2) -H2 /3 width=1/
* #H #HT12 destruct
@or_intror @conj // #H destruct /2 width=1/
]
∃∃W2,U2. U1 ≈ U2 & 𝐒[U1] & 𝐒[U2] &
I = Appl & T2 = ⓐW2. U2.
/2 width=4/ qed-.
-
-(* Basic_1: removed theorems 7:
- iso_gen_sort iso_gen_lref iso_gen_head iso_refl iso_trans
- iso_flats_lref_bind_false iso_flats_flat_bind_false
-*)
--- /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/grammar/term.ma".
+
+(* SAME TOP TERM CONSTRUCTOR ************************************************)
+
+inductive tstc: relation term ≝
+ | tstc_atom: ∀I. tstc (⓪{I}) (⓪{I})
+ | tstc_pair: ∀I,V1,V2,T1,T2. tstc (②{I} V1. T1) (②{I} V2. T2)
+.
+
+interpretation "same top constructor (term)" 'Iso T1 T2 = (tstc T1 T2).
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: iso_refl *)
+lemma tstc_refl: ∀T. T ≃ T.
+#T elim T -T //
+qed.
+
+lemma tstc_sym: ∀T1,T2. T1 ≃ T2 → T2 ≃ T1.
+#T1 #T2 #H elim H -T1 -T2 //
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact tstc_inv_atom1_aux: ∀T1,T2. T1 ≃ T2 → ∀I. T1 = ⓪{I} → T2 = ⓪{I}.
+#T1 #T2 * -T1 -T2 //
+#J #V1 #V2 #T1 #T2 #I #H destruct
+qed.
+
+(* Basic_1: was: iso_gen_sort iso_gen_lref *)
+lemma tstc_inv_atom1: ∀I,T2. ⓪{I} ≃ T2 → T2 = ⓪{I}.
+/2 width=3/ qed-.
+
+fact tstc_inv_pair1_aux: ∀T1,T2. T1 ≃ T2 → ∀I,W1,U1. T1 = ②{I}W1.U1 →
+ ∃∃W2,U2. T2 = ②{I}W2. U2.
+#T1 #T2 * -T1 -T2
+[ #J #I #W1 #U1 #H destruct
+| #J #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3/
+]
+qed.
+
+(* Basic_1: was: iso_gen_head *)
+lemma tstc_inv_pair1: ∀I,W1,U1,T2. ②{I}W1.U1 ≃ T2 →
+ ∃∃W2,U2. T2 = ②{I}W2. U2.
+/2 width=5/ qed-.
+
+fact tstc_inv_atom2_aux: ∀T1,T2. T1 ≃ T2 → ∀I. T2 = ⓪{I} → T1 = ⓪{I}.
+#T1 #T2 * -T1 -T2 //
+#J #V1 #V2 #T1 #T2 #I #H destruct
+qed.
+
+lemma tstc_inv_atom2: ∀I,T1. T1 ≃ ⓪{I} → T1 = ⓪{I}.
+/2 width=3/ qed-.
+
+fact tstc_inv_pair2_aux: ∀T1,T2. T1 ≃ T2 → ∀I,W2,U2. T2 = ②{I}W2.U2 →
+ ∃∃W1,U1. T1 = ②{I}W1. U1.
+#T1 #T2 * -T1 -T2
+[ #J #I #W2 #U2 #H destruct
+| #J #V1 #V2 #T1 #T2 #I #W2 #U2 #H destruct /2 width=3/
+]
+qed.
+
+lemma tstc_inv_pair2: ∀I,T1,W2,U2. T1 ≃ ②{I}W2.U2 →
+ ∃∃W1,U1. T1 = ②{I}W1. U1.
+/2 width=5/ qed-.
+
+(* Basic_1: removed theorems 2:
+ iso_flats_lref_bind_false iso_flats_flat_bind_false
+*)
--- /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/grammar/tstc.ma".
+
+(* SAME TOP TERM CONSTRUCTOR ************************************************)
+
+(* Main properties **********************************************************)
+
+(* Basic_1: was: iso_trans *)
+theorem tstc_trans: ∀T1,T. T1 ≃ T → ∀T2. T ≃ T2 → T1 ≃ T2.
+#T1 #T * -T1 -T //
+#I #V1 #V #T1 #T #X #H
+elim (tstc_inv_pair1 … H) -H #V2 #T2 #H destruct //
+qed.
+
+theorem tstc_canc_sn: ∀T,T1. T ≃ T1 → ∀T2. T ≃ T2 → T1 ≃ T2.
+/3 width=3/ qed.
+
+theorem tstc_canc_dx: ∀T1,T. T1 ≃ T → ∀T2. T2 ≃ T → T1 ≃ T2.
+/3 width=3/ qed.
non associative with precedence 45
for @{ 'Hom $L $T1 $T2 }.
+notation "hvbox( T1 ≃ break T2 )"
+ non associative with precedence 45
+ for @{ 'Iso $T1 $T2 }.
+
notation "hvbox( T1 break [ d , break e ] ≼ break T2 )"
non associative with precedence 45
for @{ 'SubEq $T1 $d $e $T2 }.
<key name="objects">xoa</key>
<key name="notations">xoa_notation</key>
<key name="include">basics/pts.ma</key>
+ <key name="ex">1 2</key>
<key name="ex">2 1</key>
<key name="ex">2 2</key>
<key name="ex">2 3</key>
include "basics/pts.ma".
+(* multiple existental quantifier (1, 2) *)
+
+inductive ex1_2 (A0,A1:Type[0]) (P0:A0→A1→Prop) : Prop ≝
+ | ex1_2_intro: ∀x0,x1. P0 x0 x1 → ex1_2 ? ? ?
+.
+
+interpretation "multiple existental quantifier (1, 2)" 'Ex P0 = (ex1_2 ? ? P0).
+
(* multiple existental quantifier (2, 1) *)
inductive ex2_1 (A0:Type[0]) (P0,P1:A0→Prop) : Prop ≝
(* This file was generated by xoa.native: do not edit *********************)
+(* multiple existental quantifier (1, 2) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) }.
+
(* multiple existental quantifier (2, 1) *)
notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1)"
let predefined_classes = [
["-"; "÷"; "⊢"; ];
- ["="; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ];
+ ["="; "â\89\83"; "â\89\88"; "â\89\9d"; "â\89¡"; "â\89\85"; "â\89\90"; "â\89\91"; ];
["→"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;
["⇒"; "➾"; "⇨"; "➡"; "⇉"; "⥤"; "⥰"; ] ;
["⇑"; "⇧"; "⬆"; ] ;
projects / helm.git / commitdiff