--- /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 "ground/arith/pnat_le_plus.ma".
+include "ground/arith/pnat_lt.ma".
+
+(* STRICT ORDER FOR POSITIVE INTEGERS ***************************************)
+
+(* Constructions with pplus *************************************************)
+
+lemma plt_plus_bi_dx (p) (q1) (q2): q1 < q2 → q1 + p < q2 + p.
+#p #q1 #q2 #H
+@plt_i >pplus_succ_sn /2 width=1 by ple_plus_bi_dx/
+qed.
+
+lemma plt_plus_bi_sn (p) (q1) (q2): q1 < q2 → p + q1 < p + q2.
+#p #q1 #q2 #H
+@plt_i >pplus_succ_dx /2 width=1 by ple_plus_bi_sn/
+qed.
+
+lemma plt_plus_dx_dx_refl (p) (q): p < p + q.
+/2 width=1 by ple_plus_bi_sn/ qed.
+
+lemma plt_plus_dx_sn_refl (p) (q): p < q + p.
+/2 width=1 by ple_plus_bi_dx/ qed.
+
+lemma plt_plus_dx_sn (r) (p) (q): q ≤ p → q < r + p.
+/2 width=3 by ple_plt_trans/ qed.
+
+lemma plt_plus_dx_dx (r) (p) (q): q ≤ p → q < p + r.
+/2 width=3 by ple_plt_trans/ 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 "ground/arith/pnat_lt.ma".
+
+(* WELL-FOUNDED INDUCTION ***************************************************)
+
+fact wf1_ind_plt_aux (A1) (f:A1→pnat) (Q:predicate …):
+ (∀p. (∀a1. f a1 < p → Q a1) → ∀a1. f a1 = p → Q a1) →
+ ∀p,a1. f a1 = p → Q a1.
+#A1 #f #Q #H #p @(pnat_ind_lt … p) -p /3 width=3 by/
+qed-.
+
+lemma wf1_ind_plt (A1) (f:A1→pnat) (Q:predicate …):
+ (∀p. (∀a1. f a1 < p → Q a1) → ∀a1. f a1 = p → Q a1) →
+ ∀a1. Q a1.
+#A #f #Q #H #a1 @(wf1_ind_plt_aux … H) -H //
+qed-.
[ { "well-founded induction" * } {
[ "wf1_ind_ylt" * ]
[ "wf1_ind_nlt" "wf2_ind_nlt" "wf3_ind_nlt.ma" * ]
+ [ "wf1_ind_plt" * ]
}
]
[ { "non-negative integers with infinity" * } {
}
]
[ { "positive integers" * } {
- [ "nat_lt ( ?<? )" "pnat_lt_pred" * ]
+ [ "nat_lt ( ?<? )" "pnat_lt_pred" "pnat_lt_plus" * ]
[ "pnat_le ( ?≤? )" "pnat_le_pred" "pnat_le_plus" * ]
[ "pnat_plus ( ?+? )" * ]
[ "nat_pred ( ↓? )" * ]
| LBind K I ⇒ (append L K).ⓘ[I]
].
-interpretation "append (local environment)" 'nplus L1 L2 = (append L1 L2).
+interpretation "append (local environment)" 'plus L1 L2 = (append L1 L2).
interpretation "local environment tail binding construction (generic)"
'SnItem I L = (append (LBind LAtom I) L).
(* *)
(**************************************************************************)
+include "ground/arith/nat_plus.ma".
+include "ground/arith/wf1_ind_nlt.ma".
include "static_2/syntax/lenv_length.ma".
include "static_2/syntax/append.ma".
lemma length_inv_succ_dx_ltail: ∀L,n. |L| = ↑n →
∃∃I,K. |K| = n & L = ⓘ[I].K.
#Y #n #H elim (length_inv_succ_dx … H) -H #I #L #Hn #HLK destruct
-elim (lenv_case_tail … L) [2: * #K #J ]
-#H destruct /2 width=4 by ex2_2_intro/
+elim (lenv_case_tail … L) [| * #K #J ] #H destruct
+/2 width=4 by ex2_2_intro/
+@(ex2_2_intro … (J) (K.ⓘ[I])) // (**) (* auto fails *)
+>ltail_length >length_bind //
qed-.
(* Basic_2A1: was: length_inv_pos_sn_ltail *)
lemma length_inv_succ_sn_ltail: ∀L,n. ↑n = |L| →
∃∃I,K. n = |K| & L = ⓘ[I].K.
#Y #n #H elim (length_inv_succ_sn … H) -H #I #L #Hn #HLK destruct
-elim (lenv_case_tail … L) [2: * #K #J ]
-#H destruct /2 width=4 by ex2_2_intro/
+elim (lenv_case_tail … L) [| * #K #J ] #H destruct
+/2 width=4 by ex2_2_intro/
+@(ex2_2_intro … (J) (K.ⓘ[I])) // (**) (* auto fails *)
+>ltail_length >length_bind //
qed-.
(* Inversion lemmas with length for local environments **********************)
(* Basic_2A1: was: append_inj_sn *)
lemma append_inj_length_sn: ∀K1,K2,L1,L2. L1 + K1 = L2 + K2 → |K1| = |K2| →
- L1 = L2 ∧ K1 = K2.
+ ∧∧ L1 = L2 & K1 = K2.
#K1 elim K1 -K1
[ * /2 width=1 by conj/
#K2 #I2 #L1 #L2 #_ >length_atom >length_bind
- #H destruct
+ #H elim (eq_inv_zero_nsucc … H)
| #K1 #I1 #IH *
[ #L1 #L2 #_ >length_atom >length_bind
- #H destruct
+ #H elim (eq_inv_nsucc_zero … H)
| #K2 #I2 #L1 #L2 #H1 >length_bind >length_bind #H2
+ lapply (eq_inv_nsucc_bi … H2) -H2 #H2
elim (destruct_lbind_lbind_aux … H1) -H1 #H1 #H3 destruct (**) (* destruct lemma needed *)
elim (IH … H1) -IH -H1 /3 width=4 by conj/
]
(* Note: lemma 750 *)
(* Basic_2A1: was: append_inj_dx *)
lemma append_inj_length_dx: ∀K1,K2,L1,L2. L1 + K1 = L2 + K2 → |L1| = |L2| →
- L1 = L2 ∧ K1 = K2.
+ ∧∧ L1 = L2 & K1 = K2.
#K1 elim K1 -K1
[ * /2 width=1 by conj/
#K2 #I2 #L1 #L2 >append_atom >append_bind #H destruct
- >length_bind >append_length >nplus_succ_dx
- #H elim (succ_nplus_refl_sn … H)
+ >length_bind >append_length #H
+ elim (succ_nplus_refl_sn (|L2|) (|K2|) ?) //
| #K1 #I1 #IH *
[ #L1 #L2 >append_bind >append_atom #H destruct
- >length_bind >append_length >nplus_succ_dx #H
- lapply (nplus_refl_sn … H) -H #H destruct
+ >length_bind >append_length #H
+ elim (succ_nplus_refl_sn … H)
| #K2 #I2 #L1 #L2 >append_bind >append_bind #H1 #H2
elim (destruct_lbind_lbind_aux … H1) -H1 #H1 #H3 destruct (**) (* destruct lemma needed *)
elim (IH … H1) -IH -H1 /2 width=1 by conj/
Q (⋆) → (∀I,L. Q L → Q (ⓘ[I].L)) → ∀L. Q L.
#Q #IH1 #IH2 #L @(wf1_ind_nlt … length … L) -L #x #IHx * //
#L #I -IH1 #H destruct
-elim (lenv_case_tail … L) [2: * #K #J ]
+elim (lenv_case_tail … L) [| * #K #J ]
#H destruct /3 width=1 by/
qed-.
(* WEIGHT OF A BINDER FOR LOCAL ENVIRONMENTS *******************************)
rec definition bw I ≝ match I with
-[ BUnit _ ⇒ 1
+[ BUnit _ ⇒ 𝟏
| BPair _ V ⇒ ♯❨V❩
].
-interpretation "weight (binder for local environments)" 'Weight I = (bw I).
+interpretation
+ "weight (binder for local environments)"
+ 'Weight I = (bw I).
(* Basic properties *********************************************************)
-lemma bw_pos: ∀I. 1 ≤ ♯❨I❩.
-* //
-qed.
+lemma bw_unit_unfold (I): 𝟏 = ♯❨BUnit I❩.
+// qed.
+
+lemma bw_pair_unfold (I) (V): ♯❨V❩ = ♯❨BPair I V❩.
+// qed.
(* Basic properties *********************************************************)
+lemma rfw_unfold (L) (T): ♯❨L❩ + ♯❨T❩ = ♯❨L,T❩.
+// qed.
+
(* Basic_1: was: flt_shift *)
lemma rfw_shift: ∀p,I,K,V,T. ♯❨K.ⓑ[I]V,T❩ < ♯❨K,ⓑ[p,I]V.T❩.
-normalize /2 width=1 by nle_plus_bi_sn/
-qed.
+/2 width=1 by plt_plus_bi_sn/ qed.
lemma rfw_clear: ∀p,I1,I2,K,V,T. ♯❨K.ⓤ[I1],T❩ < ♯❨K,ⓑ[p,I2]V.T❩.
-normalize /4 width=1 by nle_plus_bi_sn, nle_succ_bi/
-qed.
+/2 width=1 by plt_plus_bi_sn/ qed.
lemma rfw_tpair_sn: ∀I,L,V,T. ♯❨L,V❩ < ♯❨L,②[I]V.T❩.
-normalize in ⊢ (?→?→?→?→?%%); //
-qed.
+/2 width=1 by plt_plus_bi_sn/ qed.
lemma rfw_tpair_dx: ∀I,L,V,T. ♯❨L,T❩ < ♯❨L,②[I]V.T❩.
-normalize in ⊢ (?→?→?→?→?%%); //
-qed.
+/2 width=1 by plt_plus_bi_sn/ qed.
lemma rfw_lpair_sn: ∀I,L,V,T. ♯❨L,V❩ < ♯❨L.ⓑ[I]V,T❩.
-normalize /3 width=1 by nlt_plus_bi_dx, nle_plus_bi_sn/
-qed.
+// qed.
lemma rfw_lpair_dx: ∀I,L,V,T. ♯❨L,T❩ < ♯❨L.ⓑ[I]V,T❩.
-normalize /3 width=1 by nlt_plus_bi_dx, nle_plus_bi_sn/
-qed.
+/2 width=1 by plt_plus_bi_dx/ qed.
(* Basic_1: removed theorems 7:
flt_thead_sx flt_thead_dx flt_trans
(* Basic properties *********************************************************)
+lemma fw_unfold (G) (L) (T): ♯❨L❩ + ♯❨T❩ = ♯❨G,L,T❩.
+// qed.
+
(* Basic_1: was: flt_shift *)
lemma fw_shift: ∀p,I,G,K,V,T. ♯❨G,K.ⓑ[I]V,T❩ < ♯❨G,K,ⓑ[p,I]V.T❩.
-normalize /2 width=1 by nle_plus_bi_sn/
-qed.
+/2 width=1 by plt_plus_bi_sn/ qed.
lemma fw_clear: ∀p,I1,I2,G,K,V,T. ♯❨G,K.ⓤ[I1],T❩ < ♯❨G,K,ⓑ[p,I2]V.T❩.
-normalize /4 width=1 by nle_plus_bi_sn, nle_succ_bi/
-qed.
+/2 width=1 by plt_plus_bi_sn/ qed.
lemma fw_tpair_sn: ∀I,G,L,V,T. ♯❨G,L,V❩ < ♯❨G,L,②[I]V.T❩.
-normalize in ⊢ (?→?→?→?→?→?%%); //
-qed.
+/2 width=1 by plt_plus_bi_sn/ qed.
lemma fw_tpair_dx: ∀I,G,L,V,T. ♯❨G,L,T❩ < ♯❨G,L,②[I]V.T❩.
-normalize in ⊢ (?→?→?→?→?→?%%); //
-qed.
+/2 width=1 by plt_plus_bi_sn/ qed.
lemma fw_lpair_sn: ∀I,G,L,V,T. ♯❨G,L,V❩ < ♯❨G,L.ⓑ[I]V,T❩.
-normalize /3 width=1 by nlt_plus_bi_dx, nle_plus_bi_sn/
-qed.
+// qed.
(* Basic_1: removed theorems 7:
flt_thead_sx flt_thead_dx flt_trans
rec definition fold L T on L ≝ match L with
[ LAtom ⇒ T
| LBind L I ⇒ match I with
- [ BUnit _ ⇒ fold L (-ⓛ⋆0.T)
+ [ BUnit _ ⇒ fold L (-ⓛ⋆𝟎.T)
| BPair I V ⇒ fold L (-ⓑ[I]V.T)
]
].
-interpretation "fold (restricted closure)" 'nplus L T = (fold L T).
+interpretation "fold (restricted closure)" 'plus L T = (fold L T).
(* Basic properties *********************************************************)
lemma fold_atom: ∀T. ⋆ + T = T.
// qed.
-lemma fold_unit: ∀I,L,T. L.ⓤ[I]+T = L+(-ⓛ⋆0.T).
+lemma fold_unit: ∀I,L,T. L.ⓤ[I]+T = L+(-ⓛ⋆𝟎.T).
// qed.
lemma fold_pair: ∀I,L,V,T. (L.ⓑ[I]V)+T = L+(-ⓑ[I]V.T).
(* *)
(**************************************************************************)
+include "ground/arith/nat_succ.ma".
include "static_2/syntax/genv.ma".
(* LENGTH OF A GLOBAL ENVIRONMENT *******************************************)
rec definition glength G on G ≝ match G with
-[ GAtom ⇒ 0
+[ GAtom ⇒ 𝟎
| GPair G _ _ ⇒ ↑(glength G)
].
(* WEIGHT OF A GLOBAL ENVIRONMENT *******************************************)
rec definition gw G ≝ match G with
-[ GAtom ⇒ 0
+[ GAtom ⇒ 𝟏
| GPair G I T ⇒ gw G + ♯❨T❩
].
(* Basic properties *********************************************************)
+lemma gw_atom_unfold: 𝟏 = ♯❨⋆❩.
+// qed.
+
+lemma gw_pair_unfold (I) (G) (T): ♯❨G❩ + ♯❨T❩ = ♯❨G.ⓑ[I]T❩.
+// qed.
+
lemma gw_pair: ∀I,G,T. ♯❨G❩ < ♯❨G.ⓑ[I]T❩.
-normalize /2 width=1 by nle_plus_bi_sn/ qed.
+// qed.
(* *)
(**************************************************************************)
+include "ground/arith/nat_succ.ma".
include "static_2/syntax/lenv.ma".
(* LENGTH OF A LOCAL ENVIRONMENT ********************************************)
rec definition length L ≝ match L with
-[ LAtom ⇒ 0
+[ LAtom ⇒ 𝟎
| LBind L _ ⇒ ↑(length L)
].
(* Basic properties *********************************************************)
-lemma length_atom: |⋆| = 0.
+lemma length_atom: |⋆| = 𝟎.
// qed.
(* Basic_2A1: uses: length_pair *)
(* Basic inversion lemmas ***************************************************)
-lemma length_inv_zero_dx: ∀L. |L| = 0 → L = ⋆.
-* // #L #I >length_bind
-#H destruct
+lemma length_inv_zero_dx: ∀L. |L| = 𝟎 → L = ⋆.
+* // #L #I
+>length_bind #H
+elim (eq_inv_nsucc_zero … H)
qed-.
-lemma length_inv_zero_sn: ∀L. 0 = |L| → L = ⋆.
+lemma length_inv_zero_sn: ∀L. 𝟎 = |L| → L = ⋆.
/2 width=1 by length_inv_zero_dx/ qed-.
(* Basic_2A1: was: length_inv_pos_dx *)
lemma length_inv_succ_dx: ∀n,L. |L| = ↑n →
∃∃I,K. |K| = n & L = K. ⓘ[I].
#n *
-[ >length_atom #H destruct
-| #L #I >length_bind /3 width=4 by ex2_2_intro, eq_inv_nsucc_bi/
+[ >length_atom #H
+ elim (eq_inv_zero_nsucc … H)
+| #L #I >length_bind
+ /3 width=4 by ex2_2_intro, eq_inv_nsucc_bi/
]
qed-.
(* WEIGHT OF A LOCAL ENVIRONMENT ********************************************)
rec definition lw L ≝ match L with
-[ LAtom ⇒ 0
+[ LAtom ⇒ 𝟏
| LBind L I ⇒ lw L + ♯❨I❩
].
(* Basic properties *********************************************************)
+lemma lw_atom_unfold: 𝟏 = ♯❨⋆❩.
+// qed.
+
+lemma lw_bind_unfold (I) (L): ♯❨L❩ + ♯❨I❩ = ♯❨L.ⓘ[I]❩.
+// qed.
+
(* Basic_2A1: uses: lw_pair *)
lemma lw_bind: ∀I,L. ♯❨L❩ < ♯❨L.ⓘ[I]❩.
-normalize /2 width=1 by nle_plus_bi_sn/ qed.
+// qed.
(* Basic_1: removed theorems 4: clt_cong clt_head clt_thead clt_wf_ind *)
(* Basic_1: removed local theorems 1: clt_wf__q_ind *)
(* *)
(**************************************************************************)
+include "ground/xoa/ex_3_1.ma".
include "ground/xoa/ex_3_4.ma".
include "ground/xoa/ex_4_1.ma".
+include "ground/arith/nat_succ.ma".
include "static_2/notation/relations/voidstareq_4.ma".
include "static_2/syntax/lenv.ma".
(* EQUIVALENCE FOR LOCAL ENVIRONMENTS UP TO EXCLUSION BINDERS ***************)
inductive lveq: bi_relation nat lenv ≝
-| lveq_atom : lveq 0 (⋆) 0 (⋆)
-| lveq_bind : ∀I1,I2,K1,K2. lveq 0 K1 0 K2 →
- lveq 0 (K1.ⓘ[I1]) 0 (K2.ⓘ[I2])
-| lveq_void_sn: ∀K1,K2,n1. lveq n1 K1 0 K2 →
- lveq (↑n1) (K1.ⓧ) 0 K2
-| lveq_void_dx: ∀K1,K2,n2. lveq 0 K1 n2 K2 →
- lveq 0 K1 (↑n2) (K2.ⓧ)
+| lveq_atom : lveq 𝟎 (⋆) 𝟎 (⋆)
+| lveq_bind : ∀I1,I2,K1,K2. lveq 𝟎 K1 𝟎 K2 →
+ lveq 𝟎 (K1.ⓘ[I1]) 𝟎 (K2.ⓘ[I2])
+| lveq_void_sn: ∀K1,K2,n1. lveq n1 K1 𝟎 K2 →
+ lveq (↑n1) (K1.ⓧ) 𝟎 K2
+| lveq_void_dx: ∀K1,K2,n2. lveq 𝟎 K1 n2 K2 →
+ lveq 𝟎 K1 (↑n2) (K2.ⓧ)
.
interpretation "equivalence up to exclusion binders (local environment)"
(* Basic properties *********************************************************)
-lemma lveq_refl: ∀L. L ≋ⓧ*[0,0] L.
+lemma lveq_refl: ∀L. L ≋ⓧ*[𝟎,𝟎] L.
#L elim L -L /2 width=1 by lveq_atom, lveq_bind/
qed.
(* Basic inversion lemmas ***************************************************)
fact lveq_inv_zero_aux: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
- 0 = n1 → 0 = n2 →
+ (𝟎 = n1) → 𝟎 = n2 →
∨∨ ∧∧ ⋆ = L1 & ⋆ = L2
- | ∃∃I1,I2,K1,K2. K1 ≋ⓧ*[0,0] K2 & K1.ⓘ[I1] = L1 & K2.ⓘ[I2] = L2.
+ | ∃∃I1,I2,K1,K2. K1 ≋ⓧ*[𝟎,𝟎] K2 & K1.ⓘ[I1] = L1 & K2.ⓘ[I2] = L2.
#L1 #L2 #n1 #n2 * -L1 -L2 -n1 -n2
[1: /3 width=1 by or_introl, conj/
|2: /3 width=7 by ex3_4_intro, or_intror/
-|*: #K1 #K2 #n #_ #H1 #H2 destruct
+|*: #K1 #K2 #n #_ [ #H #_ | #_ #H ]
+ elim (eq_inv_zero_nsucc … H)
]
qed-.
-lemma lveq_inv_zero: ∀L1,L2. L1 ≋ⓧ*[0,0] L2 →
+lemma lveq_inv_zero: ∀L1,L2. L1 ≋ⓧ*[𝟎,𝟎] L2 →
∨∨ ∧∧ ⋆ = L1 & ⋆ = L2
- | ∃∃I1,I2,K1,K2. K1 ≋ⓧ*[0,0] K2 & K1.ⓘ[I1] = L1 & K2.ⓘ[I2] = L2.
+ | ∃∃I1,I2,K1,K2. K1 ≋ⓧ*[𝟎,𝟎] K2 & K1.ⓘ[I1] = L1 & K2.ⓘ[I2] = L2.
/2 width=5 by lveq_inv_zero_aux/ qed-.
fact lveq_inv_succ_sn_aux: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
∀m1. ↑m1 = n1 →
- ∃∃K1. K1 ≋ⓧ*[m1,0] L2 & K1.ⓧ = L1 & 0 = n2.
+ ∃∃K1. K1 ≋ⓧ*[m1,𝟎] L2 & K1.ⓧ = L1 & 𝟎 = n2.
#L1 #L2 #n1 #n2 * -L1 -L2 -n1 -n2
-[1: #m #H destruct
-|2: #I1 #I2 #K1 #K2 #_ #m #H destruct
-|*: #K1 #K2 #n #HK #m #H destruct /2 width=3 by ex3_intro/
+[1: #m #H elim (eq_inv_nsucc_zero … H)
+|2: #I1 #I2 #K1 #K2 #_ #m #H elim (eq_inv_nsucc_zero … H)
+|*: #K1 #K2 #n #HK #m #H
+ [ >(eq_inv_nsucc_bi … H) -m /2 width=3 by ex3_intro/
+ | elim (eq_inv_nsucc_zero … H)
+ ]
]
qed-.
lemma lveq_inv_succ_sn: ∀L1,K2,n1,n2. L1 ≋ⓧ*[↑n1,n2] K2 →
- ∃∃K1. K1 ≋ⓧ*[n1,0] K2 & K1.ⓧ = L1 & 0 = n2.
+ ∃∃K1. K1 ≋ⓧ*[n1,𝟎] K2 & K1.ⓧ = L1 & 𝟎 = n2.
/2 width=3 by lveq_inv_succ_sn_aux/ qed-.
lemma lveq_inv_succ_dx: ∀K1,L2,n1,n2. K1 ≋ⓧ*[n1,↑n2] L2 →
- ∃∃K2. K1 ≋ⓧ*[0,n2] K2 & K2.ⓧ = L2 & 0 = n1.
+ ∃∃K2. K1 ≋ⓧ*[𝟎,n2] K2 & K2.ⓧ = L2 & 𝟎 = n1.
#K1 #L2 #n1 #n2 #H
lapply (lveq_sym … H) -H #H
elim (lveq_inv_succ_sn … H) -H /3 width=3 by lveq_sym, ex3_intro/
fact lveq_inv_succ_aux: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
∀m1,m2. ↑m1 = n1 → ↑m2 = n2 → ⊥.
#L1 #L2 #n1 #n2 * -L1 -L2 -n1 -n2
-[1: #m1 #m2 #H1 #H2 destruct
-|2: #I1 #I2 #K1 #K2 #_ #m1 #m2 #H1 #H2 destruct
-|*: #K1 #K2 #n #_ #m1 #m2 #H1 #H2 destruct
+[1: #m1 #m2 #H #_ elim (eq_inv_nsucc_zero … H)
+|2: #I1 #I2 #K1 #K2 #_ #m1 #m2 #H #_ elim (eq_inv_nsucc_zero … H)
+|*: #K1 #K2 #n #_ #m1 #m2 [ #_ #H | #H #_ ]
+ elim (eq_inv_nsucc_zero … H)
]
qed-.
(* Advanced inversion lemmas ************************************************)
-lemma lveq_inv_bind_O: ∀I1,I2,K1,K2. K1.ⓘ[I1] ≋ⓧ*[0,0] K2.ⓘ[I2] → K1 ≋ⓧ*[0,0] K2.
+lemma lveq_inv_bind_O: ∀I1,I2,K1,K2. K1.ⓘ[I1] ≋ⓧ*[𝟎,𝟎] K2.ⓘ[I2] → K1 ≋ⓧ*[𝟎,𝟎] K2.
#I1 #I2 #K1 #K2 #H
elim (lveq_inv_zero … H) -H * [| #Z1 #Z2 #Y1 #Y2 #HY ] #H1 #H2 destruct //
qed-.
-lemma lveq_inv_atom_atom: ∀n1,n2. ⋆ ≋ⓧ*[n1,n2] ⋆ → ∧∧ 0 = n1 & 0 = n2.
-* [2: #n1 ] * [2,4: #n2 ] #H
+lemma lveq_inv_atom_atom: ∀n1,n2. ⋆ ≋ⓧ*[n1,n2] ⋆ → ∧∧ 𝟎 = n1 & 𝟎 = n2.
+#n1 @(nat_ind_succ … n1) -n1 [2: #n1 #_ ]
+#n2 @(nat_ind_succ … n2) -n2 [2,4: #n2 #_ ]
+#H
[ elim (lveq_inv_succ … H)
| elim (lveq_inv_succ_dx … H) -H #Y #_ #H1 #H2 destruct
| elim (lveq_inv_succ_sn … H) -H #Y #_ #H1 #H2 destruct
qed-.
lemma lveq_inv_bind_atom: ∀I1,K1,n1,n2. K1.ⓘ[I1] ≋ⓧ*[n1,n2] ⋆ →
- ∃∃m1. K1 ≋ⓧ*[m1,0] ⋆ & BUnit Void = I1 & ↑m1 = n1 & 0 = n2.
-#I1 #K1 * [2: #n1 ] * [2,4: #n2 ] #H
+ ∃∃m1. K1 ≋ⓧ*[m1,𝟎] ⋆ & BUnit Void = I1 & ↑m1 = n1 & 𝟎 = n2.
+#I1 #K1
+#n1 @(nat_ind_succ … n1) -n1 [2: #n1 #_ ]
+#n2 @(nat_ind_succ … n2) -n2 [2,4: #n2 #_ ]
+#H
[ elim (lveq_inv_succ … H)
| elim (lveq_inv_succ_dx … H) -H #Y #_ #H1 #H2 destruct
| elim (lveq_inv_succ_sn … H) -H #Y #HY #H1 #H2 destruct /2 width=3 by ex4_intro/
qed-.
lemma lveq_inv_atom_bind: ∀I2,K2,n1,n2. ⋆ ≋ⓧ*[n1,n2] K2.ⓘ[I2] →
- ∃∃m2. ⋆ ≋ⓧ*[0,m2] K2 & BUnit Void = I2 & 0 = n1 & ↑m2 = n2.
+ ∃∃m2. ⋆ ≋ⓧ*[𝟎,m2] K2 & BUnit Void = I2 & 𝟎 = n1 & ↑m2 = n2.
#I2 #K2 #n1 #n2 #H
lapply (lveq_sym … H) -H #H
elim (lveq_inv_bind_atom … H) -H
qed-.
lemma lveq_inv_pair_pair: ∀I1,I2,K1,K2,V1,V2,n1,n2. K1.ⓑ[I1]V1 ≋ⓧ*[n1,n2] K2.ⓑ[I2]V2 →
- ∧∧ K1 ≋ⓧ*[0,0] K2 & 0 = n1 & 0 = n2.
-#I1 #I2 #K1 #K2 #V1 #V2 * [2: #n1 ] * [2,4: #n2 ] #H
+ ∧∧ K1 ≋ⓧ*[𝟎,𝟎] K2 & 𝟎 = n1 & 𝟎 = n2.
+#I1 #I2 #K1 #K2 #V1 #V2
+#n1 @(nat_ind_succ … n1) -n1 [2: #n1 #_ ]
+#n2 @(nat_ind_succ … n2) -n2 [2,4: #n2 #_ ]
+#H
[ elim (lveq_inv_succ … H)
| elim (lveq_inv_succ_dx … H) -H #Y #_ #H1 #H2 destruct
| elim (lveq_inv_succ_sn … H) -H #Y #_ #H1 #H2 destruct
qed-.
lemma lveq_inv_void_succ_sn: ∀L1,L2,n1,n2. L1.ⓧ ≋ⓧ*[↑n1,n2] L2 →
- ∧∧ L1 ≋ ⓧ*[n1,0] L2 & 0 = n2.
+ ∧∧ L1 ≋ ⓧ*[n1,𝟎] L2 & 𝟎 = n2.
#L1 #L2 #n1 #n2 #H
elim (lveq_inv_succ_sn … H) -H #Y #HY #H1 #H2 destruct /2 width=1 by conj/
qed-.
lemma lveq_inv_void_succ_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,↑n2] L2.ⓧ →
- ∧∧ L1 ≋ ⓧ*[0,n2] L2 & 0 = n1.
+ ∧∧ L1 ≋ ⓧ*[𝟎,n2] L2 & 𝟎 = n1.
#L1 #L2 #n1 #n2 #H
lapply (lveq_sym … H) -H #H
elim (lveq_inv_void_succ_sn … H) -H
(* Advanced forward lemmas **************************************************)
lemma lveq_fwd_gen: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
- ∨∨ 0 = n1 | 0 = n2.
-#L1 #L2 * [2: #n1 ] * [2,4: #n2 ] #H
+ ∨∨ 𝟎 = n1 | 𝟎 = n2.
+#L1 #L2
+#n1 @(nat_ind_succ … n1) -n1 [2: #n1 #_ ]
+#n2 @(nat_ind_succ … n2) -n2 [2,4: #n2 #_ ]
+#H
[ elim (lveq_inv_succ … H) ]
/2 width=1 by or_introl, or_intror/
qed-.
-lemma lveq_fwd_pair_sn: ∀I1,K1,L2,V1,n1,n2. K1.ⓑ[I1]V1 ≋ⓧ*[n1,n2] L2 → 0 = n1.
-#I1 #K1 #L2 #V1 * [2: #n1 ] // * [2: #n2 ] #H
+lemma lveq_fwd_pair_sn:
+ ∀I1,K1,L2,V1,n1,n2. K1.ⓑ[I1]V1 ≋ⓧ*[n1,n2] L2 → 𝟎 = n1.
+#I1 #K1 #L2 #V1
+#n1 @(nat_ind_succ … n1) -n1 [2: #n1 #_ ] //
+#n2 @(nat_ind_succ … n2) -n2 [2: #n2 #_ ] #H
[ elim (lveq_inv_succ … H)
| elim (lveq_inv_succ_sn … H) -H #Y #_ #H1 #H2 destruct
]
qed-.
-lemma lveq_fwd_pair_dx: ∀I2,L1,K2,V2,n1,n2. L1 ≋ⓧ*[n1,n2] K2.ⓑ[I2]V2 → 0 = n2.
+lemma lveq_fwd_pair_dx:
+ ∀I2,L1,K2,V2,n1,n2. L1 ≋ⓧ*[n1,n2] K2.ⓑ[I2]V2 → 𝟎 = n2.
/3 width=6 by lveq_fwd_pair_sn, lveq_sym/ qed-.
(* *)
(**************************************************************************)
+include "ground/arith/nat_le_minus_plus.ma".
include "static_2/syntax/lenv_length.ma".
include "static_2/syntax/lveq.ma".
(* Properties with length for local environments ****************************)
-lemma lveq_length_eq: ∀L1,L2. |L1| = |L2| → L1 ≋ⓧ*[0,0] L2.
+lemma lveq_length_eq: ∀L1,L2. |L1| = |L2| → L1 ≋ⓧ*[𝟎,𝟎] L2.
#L1 elim L1 -L1
[ #Y2 #H >(length_inv_zero_sn … H) -Y2 /2 width=3 by lveq_atom, ex_intro/
| #K1 #I1 #IH #Y2 #H
(* Forward lemmas with length for local environments ************************)
lemma lveq_fwd_length_le_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → n1 ≤ |L1|.
-#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
/2 width=1 by nle_succ_bi/
qed-.
lemma lveq_fwd_length_le_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → n2 ≤ |L2|.
-#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
/2 width=1 by nle_succ_bi/
qed-.
lemma lveq_fwd_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
∧∧ |L1|-|L2| = n1 & |L2|-|L1| = n2.
-#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 /2 width=1 by conj/
-#K1 #K2 #n #_ * #H1 #H2 >length_bind /3 width=1 by nminus_succ_sn, conj/
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2
+[ /2 width=1 by conj/
+| #I1 #I2 #K1 #K2 #_ #IH >length_bind >length_bind //
+]
+#K1 #K2 #n #_ * #H1 #H2 destruct
+>length_bind <nminus_succ_dx <nminus_succ_sn
+/2 width=1 by nle_eq_zero_minus, conj/
qed-.
-lemma lveq_length_fwd_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L1| ≤ |L2| → 0 = n1.
+lemma lveq_length_fwd_sn: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L1| ≤ |L2| → 𝟎 = n1.
#L1 #L2 #n1 #n2 #H #HL
elim (lveq_fwd_length … H) -H
>(nle_inv_eq_zero_minus … HL) //
qed-.
-lemma lveq_length_fwd_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L2| ≤ |L1| → 0 = n2.
+lemma lveq_length_fwd_dx: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 → |L2| ≤ |L1| → 𝟎 = n2.
#L1 #L2 #n1 #n2 #H #HL
elim (lveq_fwd_length … H) -H
>(nle_inv_eq_zero_minus … HL) //
qed-.
lemma lveq_inj_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
- |L1| = |L2| → ∧∧ 0 = n1 & 0 = n2.
+ |L1| = |L2| → ∧∧ 𝟎 = n1 & 𝟎 = n2.
#L1 #L2 #n1 #n2 #H #HL
elim (lveq_fwd_length … H) -H
>HL -HL /2 width=1 by conj/
lemma lveq_fwd_length_plus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
|L1| + n2 = |L2| + n1.
-#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 normalize
-/2 width=2 by eq_inv_nplus_bi_sn/
+#L1 #L2 #n1 #n2 #H elim H -L1 -L2 -n1 -n2 //
+#k1 #K2 #n #_ #IH <nplus_succ_dx //
qed-.
-lemma lveq_fwd_length_eq: ∀L1,L2. L1 ≋ⓧ*[0,0] L2 → |L1| = |L2|.
+lemma lveq_fwd_length_eq: ∀L1,L2. L1 ≋ⓧ*[𝟎,𝟎] L2 → |L1| = |L2|.
/3 width=2 by lveq_fwd_length_plus, eq_inv_nplus_bi_dx/ qed-.
lemma lveq_fwd_length_minus: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
L1.ⓑ[I1]V1 ≋ⓧ*[n1,n2] L2.ⓘ[I2] → |L1| ≤ |L2|.
#I1 #I2 #L1 #L2 #V1 #n1 #n2 #HL
lapply (lveq_fwd_pair_sn … HL) #H destruct
-elim (lveq_fwd_length … HL) -HL >length_bind >length_bind //
+elim (lveq_fwd_length … HL) -HL >length_bind >length_bind
+<nminus_succ_bi <nminus_succ_bi //
qed-.
lemma lveq_fwd_bind_abst_length_le: ∀I1,I2,L1,L2,V2,n1,n2.
(* Inversion lemmas with length for local environments **********************)
+(**) (* state with m2 ≝ ↓n2 *)
lemma lveq_inv_void_dx_length: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2.ⓧ → |L1| ≤ |L2| →
- ∃∃m2. L1 ≋ ⓧ*[n1,m2] L2 & 0 = n1 & ↑m2 = n2.
+ ∃∃m2. L1 ≋ ⓧ*[n1,m2] L2 & 𝟎 = n1 & ↑m2 = n2.
#L1 #L2 #n1 #n2 #H #HL12
-lapply (lveq_fwd_length_plus … H) normalize >nplus_succ_dx #H0
+lapply (lveq_fwd_length_plus … H) >length_bind >nplus_succ_shift #H0
lapply (nplus_2_des_le_sn_sn … H0 HL12) -H0 -HL12 #H0
-elim (nle_inv_succ_sn … H0) -H0 #m2 #_ #H0 destruct
+elim (nle_inv_succ_sn … H0) -H0 #_ #H0 >H0 in H; -H0 #H
elim (lveq_inv_void_succ_dx … H) -H /2 width=3 by ex3_intro/
qed-.
+(**) (* state with m1 ≝ ↓n1 *)
lemma lveq_inv_void_sn_length: ∀L1,L2,n1,n2. L1.ⓧ ≋ⓧ*[n1,n2] L2 → |L2| ≤ |L1| →
- ∃∃m1. L1 ≋ ⓧ*[m1,n2] L2 & ↑m1 = n1 & 0 = n2.
+ ∃∃m1. L1 ≋ ⓧ*[m1,n2] L2 & ↑m1 = n1 & 𝟎 = n2.
#L1 #L2 #n1 #n2 #H #HL
lapply (lveq_sym … H) -H #H
elim (lveq_inv_void_dx_length … H HL) -H -HL
(* Main inversion lemmas ****************************************************)
-theorem lveq_inv_bind: ∀K1,K2. K1 ≋ⓧ*[0,0] K2 →
+theorem lveq_inv_bind: ∀K1,K2. K1 ≋ⓧ*[𝟎,𝟎] K2 →
∀I1,I2,m1,m2. K1.ⓘ[I1] ≋ⓧ*[m1,m2] K2.ⓘ[I2] →
- ∧∧ 0 = m1 & 0 = m2.
+ ∧∧ 𝟎 = m1 & 𝟎 = m2.
#K1 #K2 #HK #I1 #I2 #m1 #m2 #H
lapply (lveq_fwd_length_eq … HK) -HK #HK
-elim (lveq_inj_length … H) -H normalize /3 width=1 by conj, eq_f/
+elim (lveq_inj_length … H) -H /3 width=1 by conj/
qed-.
theorem lveq_inj: ∀L1,L2,n1,n2. L1 ≋ⓧ*[n1,n2] L2 →
theorem lveq_inj_void_sn_ge: ∀K1,K2. |K2| ≤ |K1| →
∀n1,n2. K1 ≋ⓧ*[n1,n2] K2 →
∀m1,m2. K1.ⓧ ≋ⓧ*[m1,m2] K2 →
- ∧∧ ↑n1 = m1 & 0 = m2 & 0 = n2.
+ ∧∧ ↑n1 = m1 & 𝟎 = m2 & 𝟎 = n2.
#L1 #L2 #HL #n1 #n2 #Hn #m1 #m2 #Hm
elim (lveq_fwd_length … Hn) -Hn #H1 #H2 destruct
elim (lveq_fwd_length … Hm) -Hm #H1 #H2 destruct
->length_bind >nminus_succ_dx >(nle_inv_eq_zero_minus … HL)
-/3 width=4 by nminus_plus_comm_23, and3_intro/
+>length_bind <nminus_succ_dx
+<(nminus_succ_sn … HL) <(nle_inv_eq_zero_minus … HL)
+/2 width=1 by and3_intro/
qed-.
theorem lveq_inj_void_dx_le: ∀K1,K2. |K1| ≤ |K2| →
∀n1,n2. K1 ≋ⓧ*[n1,n2] K2 →
∀m1,m2. K1 ≋ⓧ*[m1,m2] K2.ⓧ →
- ∧∧ ↑n2 = m2 & 0 = m1 & 0 = n1.
+ ∧∧ ↑n2 = m2 & 𝟎 = m1 & 𝟎 = n1.
/3 width=5 by lveq_inj_void_sn_ge, lveq_sym/ qed-. (* auto: 2x lveq_sym *)
(* SYNTACTIC EQUIVALENCE ON TERMS *******************************************)
definition teq: relation term ≝
- teqg (pr_eq …).
+ teqg (eq …).
interpretation
"context-free syntactic equivalence (term)"
(* SYNTACTIC EQUIVALENCE ****************************************************)
definition ceq: relation3 lenv term term ≝
- ceqg (pr_eq …).
+ ceqg (eq …).
definition ceq_ext: lenv → relation bind ≝
- ceqg_ext (pr_eq …).
+ ceqg_ext (eq …).
interpretation
"context-dependent syntactic equivalence (term)"
include "ground/xoa/ex_1_2.ma".
include "ground/xoa/ex_3_2.ma".
+include "ground/arith/wf1_ind_plt.ma".
include "static_2/notation/relations/tildeminus_2.ma".
include "static_2/syntax/term_weight.ma".
qed-.
lemma teqw_inv_cast_xy_y: ∀T,V. ⓝV.T ≃ T → ⊥.
-@(wf1_ind_nlt … tw) #n #IH #T #Hn #V #H destruct
+@(wf1_ind_plt … tw) #p #IH #T #Hp #V #H destruct
elim (teqw_inv_cast_sn … H) -H #X1 #X2 #_ #HX2 #H destruct -V
/2 width=4 by/
qed-.
(* TERMS ********************************************************************)
rec definition applv Vs T on Vs ≝
- match Vs with
- [ nil ⇒ T
- | cons hd pr_tl ⇒ ⓐhd. (applv pr_tl T)
- ].
+match Vs with
+[ list_nil ⇒ T
+| list_cons hd tl ⇒ ⓐhd. (applv tl T)
+].
interpretation "application to vector (term)"
'SnApplVector Vs T = (applv Vs T).
(* *)
(**************************************************************************)
+include "ground/arith/pnat_lt_plus.ma".
include "static_2/notation/functions/weight_1.ma".
include "static_2/syntax/term.ma".
(* WEIGHT OF A TERM *********************************************************)
rec definition tw T ≝ match T with
-[ TAtom _ ⇒ 1
+[ TAtom _ ⇒ 𝟏
| TPair _ V T ⇒ ↑(tw V + tw T)
].
(* Basic properties *********************************************************)
-(* Basic_1: was: tweight_lt *)
-lemma tw_pos: ∀T. 1 ≤ ♯❨T❩.
-#T elim T -T //
-qed.
+lemma tw_atom_unfold (I): 𝟏 = ♯❨⓪[I]❩.
+// qed.
+
+lemma tw_pair_unfold (I) (V) (T): ↑(♯❨V❩ + ♯❨T❩) = ♯❨②[I]V.T❩.
+// qed.
lemma tw_le_pair_dx (I): ∀V,T. ♯❨T❩ < ♯❨②[I]V.T❩.
-#I #V #T /2 width=1 by nle_succ_bi/
+/2 width=1 by plt_succ_dx_trans/
qed.
-(* Basic_1: removed theorems 11:
+(* Basic_1: removed theorems 12:
+ tweight_lt
wadd_le wadd_lt wadd_O weight_le weight_eq weight_add_O
weight_add_S tlt_trans tlt_head_sx tlt_head_dx tlt_wf_ind
*)
projects / helm.git / commitdiff