(* *)
(**************************************************************************)
+include "ground_2/notation/functions/append_2.ma".
include "basic_2/grammar/lenv_length.ma".
(* LOCAL ENVIRONMENTS *******************************************************)
interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2).
+definition l_appendable_sn: predicate (lenv→relation term) ≝ λR.
+ ∀K,T1,T2. R K T1 T2 → ∀L. R (L @@ K) T1 T2.
+
(* Basic properties *********************************************************)
lemma append_atom_sn: ∀L. ⋆ @@ L = L.
[ #L1 #L2 #_ <plus_n_Sm #H destruct
| #K2 #I2 #V2 #L1 #L2 #H1 #H2
elim (destruct_lpair_lpair … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
- elim (IH … H1 ?) -IH -H1 // -H2 /2 width=1/
+ elim (IH … H1) -IH -H1 // -H2 /2 width=1/
]
]
qed-.
elim (plus_xySz_x_false … (sym_eq … H))
| #K2 #I2 #V2 #L1 #L2 #H1 #H2
elim (destruct_lpair_lpair … H1) -H1 #H1 #H3 #H4 destruct (**) (* destruct lemma needed *)
- elim (IH … H1 ?) -IH -H1 // -H2 /2 width=1/
+ elim (IH … H1) -IH -H1 // -H2 /2 width=1/
]
]
qed-.
lemma append_inv_refl_dx: ∀L,K. L @@ K = L → K = ⋆.
#L #K #H
-elim (append_inj_dx … (⋆) … H ?) //
+elim (append_inj_dx … (⋆) … H) //
qed-.
lemma append_inv_pair_dx: ∀I,L,K,V. L @@ K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V.
#I #L #K #V #H
-elim (append_inj_dx … (⋆.ⓑ{I}V) … H ?) //
+elim (append_inj_dx … (⋆.ⓑ{I}V) … H) //
qed-.
lemma length_inv_pos_dx_append: ∀d,L. |L| = d + 1 →
∃∃I,K,V. |K| = d & L = ⋆.ⓑ{I}V @@ K.
#d @(nat_ind_plus … d) -d
-[ #L #H
+[ #L #H
elim (length_inv_pos_dx … H) -H #I #K #V #H
>(length_inv_zero_dx … H) -H #H destruct
@ex2_3_intro [4: /2 width=2/ |5: // |1,2,3: skip ] (**) (* /3/ does not work *)
(* Basic_eliminators ********************************************************)
-fact lenv_ind_dx_aux: ∀R:predicate lenv. R ⋆ →
+fact lenv_ind_dx_aux: ∀R:predicate lenv. R (⋆) →
(∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) →
∀d,L. |L| = d → R L.
#R #Hatom #Hpair #d @(nat_ind_plus … d) -d
]
qed-.
-lemma lenv_ind_dx: ∀R:predicate lenv. R ⋆ →
+lemma lenv_ind_dx: ∀R:predicate lenv. R (⋆) →
(∀I,L,V. R L → R (⋆.ⓑ{I}V @@ L)) →
∀L. R L.
/3 width=2 by lenv_ind_dx_aux/ qed-.
@(ex2_3_intro … (⋆)) // (**) (* explicit constructor *)
| #d #IHd #L #H elim (length_inv_pos_sn … H) -H #I #K #V #H1 #H2 destruct
>H1 in IHd; -H1 #IHd
- elim (IHd K ?) -IHd // #J #L #W #H1 #H2 destruct
+ elim (IHd K) -IHd // #J #L #W #H1 #H2 destruct
@(ex2_3_intro … (L.ⓑ{I}V)) // (**) (* explicit constructor *)
>append_length /2 width=1/
]