we are switching from context-free to context-sensitive reducible terms
- basics/star: star constructor refl renamed to srefl to avoid name clash with id constructor refl
(* WEIGHT OF A CLOSURE ******************************************************)
-definition cw: lenv → term → ? ≝ λL,T. #[L] + #[T].
+definition cw: lenv → term → ? ≝ λL,T. #{L} + #{T}.
interpretation "weight (closure)" 'Weight L T = (cw L T).
(* Basic_1: was: flt_wf_ind *)
axiom cw_wf_ind: ∀R:lenv→predicate term.
- (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → R L1 T1) → R L2 T2) →
+ (∀L2,T2. (∀L1,T1. #{L1,T1} < #{L2,T2} → R L1 T1) → R L2 T2) →
∀L,T. R L T.
(* Basic_1: was: flt_shift *)
-lemma cw_shift: ∀a,K,I,V,T. #[K. ⓑ{I} V, T] < #[K, ⓑ{a,I} V. T].
+lemma cw_shift: ∀a,K,I,V,T. #{K. ⓑ{I} V, T} < #{K, ⓑ{a,I} V. T}.
normalize //
qed.
-lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @@ T].
+lemma tw_shift: ∀L,T. #{L, T} ≤ #{L @@ T}.
#L elim L //
#K #I #V #IHL #T
@transitive_le [3: @IHL |2: /2 width=2/ | skip ]
qed.
-lemma cw_tpair_sn: ∀I,L,V,T. #[L, V] < #[L, ②{I}V.T].
+lemma cw_tpair_sn: ∀I,L,V,T. #{L, V} < #{L, ②{I}V.T}.
#I #L #V #T normalize in ⊢ (? % %); //
qed.
-lemma cw_tpair_dx: ∀I,L,V,T. #[L, T] < #[L, ②{I}V.T].
+lemma cw_tpair_dx: ∀I,L,V,T. #{L, T} < #{L, ②{I}V.T}.
#I #L #V #T normalize in ⊢ (? % %); //
qed.
-lemma cw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. #[L, V2] < #[L, ②{I1}V1.②{I2}V2.T].
+lemma cw_tpair_dx_sn: ∀I1,I2,L,V1,V2,T. #{L, V2} < #{L, ②{I1}V1.②{I2}V2.T}.
#I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/
qed.
-lemma cw_tpair_dx_sn_shift: ∀a2,I1,I2,L,V1,V2,T. #[L.ⓑ{I2}V2, T] < #[L, ②{I1}V1.ⓑ{a2,I2}V2.T].
+lemma cw_tpair_dx_sn_shift: ∀a2,I1,I2,L,V1,V2,T.
+ #{L.ⓑ{I2}V2, T} < #{L, ②{I1}V1.ⓑ{a2,I2}V2.T}.
#a2 #I1 #I2 #L #V1 #V2 #T normalize in ⊢ (? % %); /2 width=1/
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/grammar/lenv_length.ma".
+
+(* LOCAL ENVIRONMENTS *******************************************************)
+
+let rec append L K on K ≝ match K with
+[ LAtom ⇒ L
+| LPair K I V ⇒ (append L K). ⓑ{I} V
+].
+
+interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2).
+
+(* Basic properties *********************************************************)
+
+lemma append_atom_sn: ∀L. ⋆ @@ L = L.
+#L elim L -L normalize //
+qed.
+
+lemma append_length: ∀L1,L2. |L1 @@ L2| = |L1| + |L2|.
+#L1 #L2 elim L2 -L2 normalize //
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+axiom discr_lpair_append_xy_x: ∀I,L,K,V. (L @@ K).ⓑ{I}V = L → ⊥.
+(*
+#I #L #K #V #H
+lapply (refl … (|L|)) <H in ⊢ (? ? % ? → ?); -H
+normalize >append_length -I -V #H
+*)
+lemma append_inv_sn: ∀L1,L2,L. L1 @@ L = L2 @@ L → L1 = L2.
+#L1 #L2 #L elim L -L normalize //
+#L #I #V #IHL #HL12 destruct /2 width=1/ (**) (* destruct does not simplify well *)
+qed.
+
+lemma append_inv_dx: ∀L1,L2,L. L @@ L1 = L @@ L2 → L1 = L2.
+#L1 elim L1 -L1
+[ * normalize //
+ #L2 #I2 #V2 #L #H
+ elim (discr_lpair_append_xy_x I2 L L2 V2 ?) //
+| #L1 #I1 #V1 #IHL1 * normalize
+ [ #L #H -IHL1 elim (discr_lpair_append_xy_x … H)
+ | #L2 #I2 #V2 #L normalize #H destruct (**) (* destruct does not simplify well *)
+ -H >e0 /3 width=2/
+ ]
+]
+qed.
let rec lw L ≝ match L with
[ LAtom ⇒ 0
-| LPair L _ V ⇒ lw L + #[V]
+| LPair L _ V ⇒ lw L + #{V}
].
interpretation "weight (local environment)" 'Weight L = (lw L).
(* Basic properties *********************************************************)
-lemma lw_pair: ∀I,L,V. #[L] < #[(L.ⓑ{I}V)].
+lemma lw_pair: ∀I,L,V. #{L} < #{(L.ⓑ{I}V)}.
/3 width=1/ qed.
(* Basic eliminators ********************************************************)
axiom lw_wf_ind: ∀R:predicate lenv.
- (∀L2. (∀L1. #[L1] < #[L2] → R L1) → R L2) →
+ (∀L2. (∀L1. #{L1} < #{L2} → R L1) → R L2) →
∀L. R L.
(* Basic_1: removed theorems 2: clt_cong clt_head clt_thead *)
(* Basic properties *********************************************************)
(* Basic_1: was: tweight_lt *)
-lemma tw_pos: ∀T. 1 ≤ #[T].
+lemma tw_pos: ∀T. 1 ≤ #{T}.
#T elim T -T //
qed.
(* Basic eliminators ********************************************************)
axiom tw_wf_ind: ∀R:predicate term.
- (∀T2. (∀T1. #[T1] < #[T2] → R T1) → R T2) →
+ (∀T2. (∀T1. #{T1} < #{T2} → R T1) → R T2) →
∀T. R T.
(* Basic_1: removed theorems 11:
non associative with precedence 50
for @{ 'DxItem4 $T $I $T1 $T2 $T3 }.
-notation "hvbox( # [ x ] )"
+notation "hvbox( # { x } )"
non associative with precedence 90
for @{ 'Weight $x }.
-notation "hvbox( # [ x , break y ] )"
+notation "hvbox( # { x , break y } )"
non associative with precedence 90
for @{ 'Weight $x $y }.
(* Substitution *************************************************************)
-notation "hvbox( L ⊢ break 𝐑 [ d , break e ] break ⦃ T ⦄ )"
- non associative with precedence 45
- for @{ 'Reducible $L $d $e $T }.
-
-notation "hvbox( L ⊢ break 𝐈 [ d , break e ] break ⦃ T ⦄ )"
- non associative with precedence 45
- for @{ 'NotReducible $L $d $e $T }.
-
-notation "hvbox( L ⊢ break 𝐍 [ d , break e ] break ⦃ T ⦄ )"
- non associative with precedence 45
- for @{ 'Normal $L $d $e $T }.
-
notation "hvbox( ⇧ [ d , break e ] break term 46 T1 ≡ break term 46 T2 )"
non associative with precedence 45
for @{ 'RLift $d $e $T1 $T2 }.
(* Unfold *******************************************************************)
-notation "hvbox( @ [ T1 ] break term 46 f ≡ break term 46 T2 )"
+notation "hvbox( @ ⦃ T1 , break f ⦄ ≡ break term 46 T2 )"
non associative with precedence 45
for @{ 'RAt $T1 $f $T2 }.
(* Unwind *******************************************************************)
-notation "hvbox( L1 ⊢ ⧫* break term 46 T ≡ break term 46 L2 )"
+notation "hvbox( L1 ⊢ ⧫ * break term 46 T ≡ break term 46 L2 )"
non associative with precedence 45
for @{ 'Unwind $L1 $T $L2 }.
(* Reducibility *************************************************************)
-notation "hvbox( 𝐑 ⦃ T ⦄ )"
- non associative with precedence 45
- for @{ 'Reducible $T }.
-
notation "hvbox( L ⊢ break 𝐑 ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'Reducible $L $T }.
-notation "hvbox( 𝐈 ⦃ T ⦄ )"
- non associative with precedence 45
- for @{ 'NotReducible $T }.
-
notation "hvbox( L ⊢ break 𝐈 ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'NotReducible $L $T }.
-notation "hvbox( 𝐍 ⦃ T ⦄ )"
- non associative with precedence 45
- for @{ 'Normal $T }.
-
notation "hvbox( L ⊢ break 𝐍 ⦃ T ⦄ )"
non associative with precedence 45
for @{ 'Normal $L $T }.
-notation "hvbox( 𝐖𝐇𝐑 ⦃ T ⦄ )"
+(* this might be removed *)
+notation "hvbox( 𝐇𝐑 ⦃ T ⦄ )"
non associative with precedence 45
- for @{ 'WHdReducible $T }.
+ for @{ 'HdReducible $T }.
-notation "hvbox( L ⊢ break 𝐖𝐇𝐑 ⦃ T ⦄ )"
+(* this might be removed *)
+notation "hvbox( L ⊢ break 𝐇𝐑 ⦃ T ⦄ )"
non associative with precedence 45
- for @{ 'WHdReducible $L $T }.
+ for @{ 'HdReducible $L $T }.
-notation "hvbox( 𝐖𝐇𝐈 ⦃ T ⦄ )"
+(* this might be removed *)
+notation "hvbox( 𝐇𝐈 ⦃ T ⦄ )"
non associative with precedence 45
- for @{ 'NotWHdReducible $T }.
+ for @{ 'NotHdReducible $T }.
-notation "hvbox( L ⊢ break 𝐖𝐇𝐈 ⦃ T ⦄ )"
+(* this might be removed *)
+notation "hvbox( L ⊢ break 𝐇𝐈 ⦃ T ⦄ )"
non associative with precedence 45
- for @{ 'NotWHdReducible $L $T }.
+ for @{ 'NotHdReducible $L $T }.
-notation "hvbox( 𝐖𝐇𝐍 ⦃ T ⦄ )"
+(* this might be removed *)
+notation "hvbox( 𝐇𝐍 ⦃ T ⦄ )"
non associative with precedence 45
- for @{ 'WHdNormal $T }.
+ for @{ 'HdNormal $T }.
-notation "hvbox( L ⊢ break 𝐖𝐇𝐍 ⦃ T ⦄ )"
+(* this might be removed *)
+notation "hvbox( L ⊢ break 𝐇𝐍 ⦃ T ⦄ )"
non associative with precedence 45
- for @{ 'WHdNormal $L $T }.
+ for @{ 'HdNormal $L $T }.
notation "hvbox( T1 ➡ break term 46 T2 )"
non associative with precedence 45
--- /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_simple.ma".
+include "basic_2/substitution/ldrop.ma".
+
+(* CONTEXT-SENSITIVE REDUCIBLE TERMS ****************************************)
+
+(* reducible binary items *)
+definition ri2: item2 → Prop ≝
+ λI. I = Bind2 true Abbr ∨ I = Flat2 Cast.
+
+(* irreducible binary binders *)
+definition ib2: bool → bind2 → Prop ≝
+ λa,I. I = Abst ∨ Bind2 a I = Bind2 false Abbr.
+
+(* reducible terms *)
+inductive crf: lenv → predicate term ≝
+| crf_delta : ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → crf L (#i)
+| crf_appl_sn: ∀L,V,T. crf L V → crf L (ⓐV. T)
+| crf_appl_dx: ∀L,V,T. crf L T → crf L (ⓐV. T)
+| crf_ri2 : ∀I,L,V,T. ri2 I → crf L (②{I}V. T)
+| crf_ib2_sn : ∀a,I,L,V,T. ib2 a I → crf L V → crf L (ⓑ{a,I}V. T)
+| crf_ib2_dx : ∀a,I,L,V,T. ib2 a I → crf (L.ⓑ{I}V) T → crf L (ⓑ{a,I}V. T)
+| crf_beta : ∀a,L,V,W,T. crf L (ⓐV. ⓛ{a}W. T)
+| crf_theta : ∀a,L,V,W,T. crf L (ⓐV. ⓓ{a}W. T)
+.
+
+interpretation
+ "context-sensitive reducibility (term)"
+ 'Reducible L T = (crf L T).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact trf_inv_atom_aux: ∀I,L,T. L ⊢ 𝐑⦃T⦄ → L = ⋆ → T = ⓪{I} → ⊥.
+#I #L #T * -L -T
+[ #L #K #V #i #HLK #H1 #H2 destruct
+ lapply (ldrop_inv_atom1 … HLK) -HLK #H destruct
+| #L #V #T #_ #_ #H destruct
+| #L #V #T #_ #_ #H destruct
+| #J #L #V #T #_ #_ #H destruct
+| #a #J #L #V #T #_ #_ #_ #H destruct
+| #a #J #L #V #T #_ #_ #_ #H destruct
+| #a #L #V #W #T #_ #H destruct
+| #a #L #V #W #T #_ #H destruct
+]
+qed.
+
+lemma trf_inv_atom: ∀I. ⋆ ⊢ 𝐑⦃⓪{I}⦄ → ⊥.
+/2 width=6/ qed-.
+
+fact crf_inv_abst_aux: ∀a,L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓛ{a}W. U →
+ L ⊢ 𝐑⦃W⦄ ∨ L.ⓛW ⊢ 𝐑⦃U⦄.
+#a #L #W #U #T * -T
+[ #L #K #V #i #_ #H destruct
+| #L #V #T #_ #H destruct
+| #L #V #T #_ #H destruct
+| #J #L #V #T #H1 #H2 destruct
+ elim H1 -H1 #H destruct
+| #b #J #L #V #T #_ #HV #H destruct /2 width=1/
+| #b #J #L #V #T #_ #HT #H destruct /2 width=1/
+| #b #L #V #W #T #H destruct
+| #b #L #V #W #T #H destruct
+]
+qed.
+
+lemma crf_inv_abst: ∀a,L,W,T. L ⊢ 𝐑⦃ⓛ{a}W.T⦄ → L ⊢ 𝐑⦃W⦄ ∨ L.ⓛW ⊢ 𝐑⦃T⦄.
+/2 width=4/ qed-.
+
+fact crf_inv_appl_aux: ∀L,W,U,T. L ⊢ 𝐑⦃T⦄ → T = ⓐW. U →
+ ∨∨ L ⊢ 𝐑⦃W⦄ | L ⊢ 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
+#L #W #U #T * -T
+[ #L #K #V #i #_ #H destruct
+| #L #V #T #HV #H destruct /2 width=1/
+| #L #V #T #HT #H destruct /2 width=1/
+| #J #L #V #T #H1 #H2 destruct
+ elim H1 -H1 #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #I #L #V #T #_ #_ #H destruct
+| #a #L #V #W0 #T #H destruct
+ @or3_intro2 #H elim (simple_inv_bind … H)
+| #a #L #V #W0 #T #H destruct
+ @or3_intro2 #H elim (simple_inv_bind … H)
+]
+qed.
+
+lemma crf_inv_appl: ∀L,V,T. L ⊢ 𝐑⦃ⓐV.T⦄ → ∨∨ L ⊢ 𝐑⦃V⦄ | L ⊢ 𝐑⦃T⦄ | (𝐒⦃T⦄ → ⊥).
+/2 width=3/ 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/grammar/tshf.ma".
+include "basic_2/reducibility/tpr.ma".
+
+(* CONTEXT-FREE WEAK HEAD NORMAL TERMS **************************************)
+
+definition thnf: predicate term ≝ NF … tpr tshf.
+
+interpretation
+ "context-free head normality (term)"
+ 'HdNormal T = (thnf T).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma twhnf_inv_tshf: ∀T. 𝐇𝐍⦃T⦄ → T ≈ T.
+normalize /2 width=1/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma tpr_tshf: ∀T1,T2. T1 ➡ T2 → T1 ≈ T1 → T1 ≈ T2.
+#T1 #T2 #H elim H -T1 -T2 //
+[ #I #V1 #V2 #T1 #T2 #_ #_ #_ #IHT12 #H
+ elim (tshf_inv_flat1 … H) -H #W2 #U2 #HT1U2 #HT1 #_ #H1 #H2 destruct
+ lapply (IHT12 HT1U2) -IHT12 -HT1U2 #HUT2
+ lapply (simple_tshf_repl_dx … HUT2 HT1) /2 width=1/
+| #a #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
+ elim (tshf_inv_flat1 … H) -H #W2 #U2 #_ #H
+ elim (simple_inv_bind … H)
+| #a #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #_ #_ #H
+ elim (tshf_inv_bind1 … H) -H #W2 #U2 #H1 * #H2 destruct //
+| #a #V2 #V1 #V #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
+ elim (tshf_inv_flat1 … H) -H #U1 #U2 #_ #H
+ elim (simple_inv_bind … H)
+| #V #T #T1 #T2 #_ #_ #_ #H
+ elim (tshf_inv_bind1 … H) -H #W2 #U2 #H1 * #H2 destruct
+| #V #T1 #T2 #_ #_ #H
+ elim (tshf_inv_flat1 … H) -H #W2 #U2 #_ #_ #_ #H destruct
+]
+qed.
+
+lemma twhnf_tshf: ∀T. T ≈ T → 𝐇𝐍⦃T⦄.
+/3 width=1/ qed.
fact tpr_conf_flat_flat:
∀I,V0,V1,T0,T1,V2,T2. (
- ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
+ ∀X0:term. #{X0} < #{V0} + #{T0} + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
fact tpr_conf_flat_beta:
∀a,V0,V1,T1,V2,W0,U0,T2. (
- ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 →
+ ∀X0:term. #{X0} < #{V0} + (#{W0} + #{U0} + 1) + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
*)
fact tpr_conf_flat_theta:
∀a,V0,V1,T1,V2,V,W0,W2,U0,U2. (
- ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 →
+ ∀X0:term. #{X0} < #{V0} + (#{W0} + #{U0} + 1) + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
fact tpr_conf_flat_cast:
∀X2,V0,V1,T0,T1. (
- ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
+ ∀X0:term. #{X0} < #{V0} + #{T0} + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
fact tpr_conf_beta_beta:
∀a. ∀W0:term. ∀V0,V1,T0,T1,V2,T2. (
- ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 →
+ ∀X0:term. #{X0} < #{V0} + (#{W0} + #{T0} + 1) + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
(* Basic_1: was: pr0_cong_delta pr0_delta_delta *)
fact tpr_conf_delta_delta:
∀a,I1,V0,V1,T0,T1,TT1,V2,T2,TT2. (
- ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
+ ∀X0:term. #{X0} < #{V0} + #{T0} + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
fact tpr_conf_delta_zeta:
∀X2,V0,V1,T0,T1,TT1,T2. (
- ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
+ ∀X0:term. #{X0} < #{V0} + #{T0} + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
(* Basic_1: was: pr0_upsilon_upsilon *)
fact tpr_conf_theta_theta:
∀a,VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. (
- ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 →
+ ∀X0:term. #{X0} < #{V0} + (#{W0} + #{T0} + 1) + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
fact tpr_conf_zeta_zeta:
∀V0:term. ∀X2,TT0,T0,T1,TT2. (
- ∀X0:term. #[X0] < #[V0] + #[TT0] + 1 →
+ ∀X0:term. #{X0} < #{V0} + #{TT0} + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
fact tpr_conf_tau_tau:
∀V0,T0:term. ∀X2,T1. (
- ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
+ ∀X0:term. #{X0} < #{V0} + #{T0} + 1 →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
fact tpr_conf_aux:
∀Y0:term. (
- ∀X0:term. #[X0] < #[Y0] →
+ ∀X0:term. #{X0} < #{Y0} →
∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
∃∃X. X1 ➡ X & X2 ➡ X
) →
+++ /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_simple.ma".
-
-(* CONTEXT-FREE REDUCIBLE TERMS *********************************************)
-
-(* reducible terms *)
-inductive trf: predicate term ≝
-| trf_abst_sn: ∀V,T. trf V → trf (ⓛV. T)
-| trf_abst_dx: ∀V,T. trf T → trf (ⓛV. T)
-| trf_appl_sn: ∀V,T. trf V → trf (ⓐV. T)
-| trf_appl_dx: ∀V,T. trf T → trf (ⓐV. T)
-| trf_abbr : ∀V,T. trf (ⓓV. T)
-| trf_cast : ∀V,T. trf (ⓝV. T)
-| trf_beta : ∀V,W,T. trf (ⓐV. ⓛW. T)
-.
-
-interpretation
- "context-free reducibility (term)"
- 'Reducible T = (trf T).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact trf_inv_atom_aux: ∀I,T. 𝐑⦃T⦄ → T = ⓪{I} → ⊥.
-#I #T * -T
-[ #V #T #_ #H destruct
-| #V #T #_ #H destruct
-| #V #T #_ #H destruct
-| #V #T #_ #H destruct
-| #V #T #H destruct
-| #V #T #H destruct
-| #V #W #T #H destruct
-]
-qed.
-
-lemma trf_inv_atom: ∀I. 𝐑⦃⓪{I}⦄ → ⊥.
-/2 width=4/ qed-.
-
-fact trf_inv_abst_aux: ∀W,U,T. 𝐑⦃T⦄ → T = ⓛW. U → 𝐑⦃W⦄ ∨ 𝐑⦃U⦄.
-#W #U #T * -T
-[ #V #T #HV #H destruct /2 width=1/
-| #V #T #HT #H destruct /2 width=1/
-| #V #T #_ #H destruct
-| #V #T #_ #H destruct
-| #V #T #H destruct
-| #V #T #H destruct
-| #V #W0 #T #H destruct
-]
-qed.
-
-lemma trf_inv_abst: ∀V,T. 𝐑⦃ⓛV.T⦄ → 𝐑⦃V⦄ ∨ 𝐑⦃T⦄.
-/2 width=3/ qed-.
-
-fact trf_inv_appl_aux: ∀W,U,T. 𝐑⦃T⦄ → T = ⓐW. U →
- ∨∨ 𝐑⦃W⦄ | 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
-#W #U #T * -T
-[ #V #T #_ #H destruct
-| #V #T #_ #H destruct
-| #V #T #HV #H destruct /2 width=1/
-| #V #T #HT #H destruct /2 width=1/
-| #V #T #H destruct
-| #V #T #H destruct
-| #V #W0 #T #H destruct
- @or3_intro2 #H elim (simple_inv_bind … H)
-]
-qed.
-
-lemma trf_inv_appl: ∀W,U. 𝐑⦃ⓐW.U⦄ → ∨∨ 𝐑⦃W⦄ | 𝐑⦃U⦄ | (𝐒⦃U⦄ → ⊥).
-/2 width=3/ 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/grammar/tshf.ma".
-include "basic_2/reducibility/tpr.ma".
-
-(* CONTEXT-FREE WEAK HEAD NORMAL TERMS **************************************)
-
-definition twhnf: predicate term ≝ NF … tpr tshf.
-
-interpretation
- "context-free weak head normality (term)"
- 'WHdNormal T = (twhnf T).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma twhnf_inv_tshf: ∀T. 𝐖𝐇𝐍⦃T⦄ → T ≈ T.
-normalize /2 width=1/
-qed-.
-
-(* Basic properties *********************************************************)
-
-lemma tpr_tshf: ∀T1,T2. T1 ➡ T2 → T1 ≈ T1 → T1 ≈ T2.
-#T1 #T2 #H elim H -T1 -T2 //
-[ #I #V1 #V2 #T1 #T2 #_ #_ #_ #IHT12 #H
- elim (tshf_inv_flat1 … H) -H #W2 #U2 #HT1U2 #HT1 #_ #H1 #H2 destruct
- lapply (IHT12 HT1U2) -IHT12 -HT1U2 #HUT2
- lapply (simple_tshf_repl_dx … HUT2 HT1) /2 width=1/
-| #a #V1 #V2 #W #T1 #T2 #_ #_ #_ #_ #H
- elim (tshf_inv_flat1 … H) -H #W2 #U2 #_ #H
- elim (simple_inv_bind … H)
-| #a #I #V1 #V2 #T1 #T #T2 #_ #_ #_ #_ #_ #H
- elim (tshf_inv_bind1 … H) -H #W2 #U2 #H1 * #H2 destruct //
-| #a #V2 #V1 #V #W1 #W2 #T1 #T2 #_ #_ #_ #_ #_ #_ #_ #H
- elim (tshf_inv_flat1 … H) -H #U1 #U2 #_ #H
- elim (simple_inv_bind … H)
-| #V #T #T1 #T2 #_ #_ #_ #H
- elim (tshf_inv_bind1 … H) -H #W2 #U2 #H1 * #H2 destruct
-| #V #T1 #T2 #_ #_ #H
- elim (tshf_inv_flat1 … H) -H #W2 #U2 #_ #_ #_ #H destruct
-]
-qed.
-
-lemma twhnf_tshf: ∀T. T ≈ T → 𝐖𝐇𝐍⦃T⦄.
-/3 width=1/ qed.
#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
qed.
+lemma ldrop_skip_lt: ∀L1,L2,I,V1,V2,d,e.
+ ⇩[d - 1, e] L1 ≡ L2 → ⇧[d - 1, e] V2 ≡ V1 → 0 < d →
+ ⇩[d, e] L1. ⓑ{I} V1 ≡ L2. ⓑ{I} V2.
+#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV21 #Hd >(plus_minus_m_m d 1) // /2 width=1/
+qed.
+
lemma ldrop_O1: ∀L,i. i < |L| → ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I}V.
#L elim L -L
[ #i #H elim (lt_zero_false … H)
]
qed-.
-lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #[L2] ≤ #[L1].
+lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #{L2} ≤ #{L1}.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize
[ /2 width=3/
| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12
qed-.
lemma ldrop_pair2_fwd_cw: ∀I,L,K,V,d,e. ⇩[d, e] L ≡ K. ⓑ{I} V →
- ∀T. #[K, V] < #[L, T].
+ ∀T. #{K, V} < #{L, T}.
#I #L #K #V #d #e #H #T
lapply (ldrop_fwd_lw … H) -H #H
@(le_to_lt_to_lt … H) -H /3 width=1/
--- /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/lenv_append.ma".
+include "basic_2/substitution/ldrop.ma".
+
+(* DROPPING *****************************************************************)
+
+(* Properties on append for local environments ******************************)
+
+lemma ldrop_append_O1_ge: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K →
+ |L2| ≤ e → ⇩[0, e - |L2|] L1 ≡ K.
+#K #L1 #L2 elim L2 -L2 normalize //
+#L2 #I #V #IHL2 #e #H #H1e
+elim (ldrop_inv_O1 … H) -H * #H2e #HL12 destruct
+[ lapply (le_n_O_to_eq … H1e) -H1e -IHL2
+ >commutative_plus normalize #H destruct
+| <minus_plus >minus_minus_comm /3 width=1/
+]
+qed.
+
+lemma ldrop_append_O1_lt: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K → e < |L2| →
+ ∃∃K2. ⇩[0, e] L2 ≡ K2 & K = L1 @@ K2.
+#K #L1 #L2 elim L2 -L2
+[ #e #_ #H elim (lt_zero_false … H)
+| #L2 #I #V #IHL2 #e normalize #HL12 #H1e
+ elim (ldrop_inv_O1 … HL12) -HL12 * #H2e #HL12 destruct
+ [ -H1e -IHL2 /3 width=3/
+ | elim (IHL2 … HL12 ?) -IHL2 -HL12 /2 width=1/ -H1e #K2 #HLK2 #H destruct /3 width=3/
+ ]
+]
+qed.
(* Basic forward lemmas *****************************************************)
-lemma tw_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → #[T1] = #[T2].
+lemma tw_lift: ∀d,e,T1,T2. ⇧[d, e] T1 ≡ T2 → #{T1} = #{T2}.
#d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
qed-.
(* Basic forward lemmas *****************************************************)
-lemma tps_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → #[T1] ≤ #[T2].
+lemma tps_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → #{T1} ≤ #{T2}.
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e normalize
/3 by monotonic_le_plus_l, le_plus/ (**) (* just /3 width=1/ is too slow *)
qed-.
(* Basic forward lemmas *****************************************************)
-lemma delift_fwd_tw: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → #[T1] ≤ #[T2].
+lemma delift_fwd_tw: ∀L,T1,T2,d,e. L ⊢ ▼*[d, e] T1 ≡ T2 → #{T1} ≤ #{T2}.
#L #T1 #T2 #d #e * #T #HT1 #HT2
>(tw_lift … HT2) -T2 /2 width=4 by tpss_fwd_tw /
qed-.
(* Basic inversion lemmas ***************************************************)
-fact at_inv_nil_aux: ∀des,i1,i2. @[i1] des ≡ i2 → des = ⟠ → i1 = i2.
+fact at_inv_nil_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → des = ⟠ → i1 = i2.
#des #i1 #i2 * -des -i1 -i2
[ //
| #des #d #e #i1 #i2 #_ #_ #H destruct
]
qed.
-lemma at_inv_nil: ∀i1,i2. @[i1] ⟠ ≡ i2 → i1 = i2.
+lemma at_inv_nil: ∀i1,i2. @⦃i1, ⟠⦄ ≡ i2 → i1 = i2.
/2 width=3/ qed-.
-fact at_inv_cons_aux: ∀des,i1,i2. @[i1] des ≡ i2 →
+fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 →
∀d,e,des0. des = {d, e} @ des0 →
- i1 < d ∧ @[i1] des0 ≡ i2 ∨
- d ≤ i1 ∧ @[i1 + e] des0 ≡ i2.
+ i1 < d ∧ @⦃i1, des0⦄ ≡ i2 ∨
+ d ≤ i1 ∧ @⦃i1 + e, des0⦄ ≡ i2.
#des #i1 #i2 * -des -i1 -i2
[ #i #d #e #des #H destruct
| #des1 #d1 #e1 #i1 #i2 #Hid1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1/
]
qed.
-lemma at_inv_cons: ∀des,d,e,i1,i2. @[i1] {d, e} @ des ≡ i2 →
- i1 < d ∧ @[i1] des ≡ i2 ∨
- d ≤ i1 ∧ @[i1 + e] des ≡ i2.
+lemma at_inv_cons: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 →
+ i1 < d ∧ @⦃i1, des⦄ ≡ i2 ∨
+ d ≤ i1 ∧ @⦃i1 + e, des⦄ ≡ i2.
/2 width=3/ qed-.
-lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @[i1] {d, e} @ des ≡ i2 →
- i1 < d → @[i1] des ≡ i2.
+lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 →
+ i1 < d → @⦃i1, des⦄ ≡ i2.
#des #d #e #i1 #e2 #H
elim (at_inv_cons … H) -H * // #Hdi1 #_ #Hi1d
lapply (le_to_lt_to_lt … Hdi1 Hi1d) -Hdi1 -Hi1d #Hd
elim (lt_refl_false … Hd)
qed-.
-lemma at_inv_cons_ge: ∀des,d,e,i1,i2. @[i1] {d, e} @ des ≡ i2 →
- d ≤ i1 → @[i1 + e] des ≡ i2.
+lemma at_inv_cons_ge: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 →
+ d ≤ i1 → @⦃i1 + e, des⦄ ≡ i2.
#des #d #e #i1 #e2 #H
elim (at_inv_cons … H) -H * // #Hi1d #_ #Hdi1
lapply (le_to_lt_to_lt … Hdi1 Hi1d) -Hdi1 -Hi1d #Hd
(* Main properties **********************************************************)
-theorem at_mono: ∀des,i,i1. @[i] des ≡ i1 → ∀i2. @[i] des ≡ i2 → i1 = i2.
+theorem at_mono: ∀des,i,i1. @⦃i, des⦄ ≡ i1 → ∀i2. @⦃i, des⦄ ≡ i2 → i1 = i2.
#des #i #i1 #H elim H -des -i -i1
[ #i #x #H <(at_inv_nil … H) -x //
| #des #d #e #i #i1 #Hid #_ #IHi1 #x #H
lemma ldrops_ldrop_trans: ∀L1,L,des. ⇩*[des] L1 ≡ L → ∀L2,i. ⇩[0, i] L ≡ L2 →
∃∃L0,des0,i0. ⇩[0, i0] L1 ≡ L0 & ⇩*[des0] L0 ≡ L2 &
- @[i] des ≡ i0 & des ▭ i ≡ des0.
+ @⦃i, des⦄ ≡ i0 & des ▭ i ≡ des0.
#L1 #L #des #H elim H -L1 -L -des
[ /2 width=7/
| #L1 #L3 #L #des3 #d #e #_ #HL3 #IHL13 #L2 #i #HL2
(* Basic_1: was: lift1_lref *)
lemma lifts_inv_lref1: ∀T2,des,i1. ⇧*[des] #i1 ≡ T2 →
- ∃∃i2. @[i1] des ≡ i2 & T2 = #i2.
+ ∃∃i2. @⦃i1, des⦄ ≡ i2 & T2 = #i2.
#T2 #des elim des -des
[ #i1 #H <(lifts_inv_nil … H) -H /2 width=3/
| #d #e #des #IH #i1 #H
qed-.
(* Basic_1: was: lift1_free (right to left) *)
-lemma lifts_lift_trans: ∀des,i,i0. @[i] des ≡ i0 →
+lemma lifts_lift_trans: ∀des,i,i0. @⦃i, des⦄ ≡ i0 →
∀des0. des + 1 ▭ i + 1 ≡ des0 + 1 →
∀T1,T0. ⇧*[des0] T1 ≡ T0 →
∀T2. ⇧[O, i0 + 1] T0 ≡ T2 →
elim (ltpss_ldrop_trans_be … HL01 … HLK1 ? ?) -HL01 -HLK1 // /2 width=2/ #X #H #HLK0
elim (ltpss_inv_tpss22 … H ?) -H /2 width=1/ #K0 #V0 #HK01 #HV01 #H destruct
lapply (tpss_fwd_tw … HV01) #H2
- lapply (transitive_le (#[K1] + #[V0]) … H1) -H1 /2 width=1/ -H2 #H
+ lapply (transitive_le (#{K1} + #{V0}) … H1) -H1 /2 width=1/ -H2 #H
lapply (tpss_trans_eq … HV01 HV12) -V1 #HV02
lapply (IH … HV02 … HK01 ? ?) -IH -HV02 -HK01
[1,3: // |2,4: skip | normalize /2 width=1/ | /2 width=6/ ]
(* Basic forward lemmas *****************************************************)
-lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → #[T1] ≤ #[T2].
+lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → #{T1} ≤ #{T2}.
#L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 //
#T #T2 #_ #HT2 #IHT1
lapply (tps_fwd_tw … HT2) -HT2 #HT2
(* star *)
inductive star (A:Type[0]) (R:relation A) (a:A): A → Prop ≝
|sstep: ∀b,c.star A R a b → R b c → star A R a c
- |refl: star A R a a.
+ |srefl: star A R a a.
lemma R_to_star: ∀A,R,a,b. R a b → star A R a b.
#A #R #a #b /2/
projects / helm.git / commitdiff