(**************************************************************************)
include "basics/star.ma".
-include "basics/lists/list.ma".
-include "arithmetics/nat.ma".
+include "basics/lists/lstar.ma".
+include "arithmetics/exp.ma".
include "xoa_notation.ma".
include "xoa.ma".
+(* logic *)
+
(* Note: For some reason this cannot be in the standard library *)
interpretation "logical false" 'false = False.
non associative with precedence 90
for @{'false}.
+(* arithmetics *)
+
lemma lt_refl_false: ∀n. n < n → ⊥.
#n #H elim (lt_to_not_eq … H) -H /2 width=1/
qed-.
| #n1 #IH #n2 elim n2 -n2 // /3 width=1/
]
qed.
+
+(* lists *)
+
+(* Note: notation for nil not involving brackets *)
+notation > "◊"
+ non associative with precedence 90
+ for @{'nil}.
+
+definition map_cons: ∀A. A → list (list A) → list (list A) ≝ λA,a.
+ map … (cons … a).
+
+interpretation "map_cons" 'ho_cons a l = (map_cons ? a l).
+
+notation "hvbox(a ::: break l)"
+ right associative with precedence 47
+ for @{'ho_cons $a $l}.
+
+(* lstar *)
+
+(* Note: this cannot be in lib because of the missing xoa quantifier *)
+lemma lstar_inv_pos: ∀A,B,R,l,b1,b2. lstar A B R l b1 b2 → 0 < |l| →
+ ∃∃a,ll,b. a::ll = l & R a b1 b & lstar A B R ll b b2.
+#A #B #R #l #b1 #b2 #H @(lstar_ind_l ????????? H) -b1
+[ #H elim (lt_refl_false … H)
+| #a #ll #b1 #b #Hb1 #Hb2 #_ #_ /2 width=6/ (**) (* auto fail if we do not remove the inductive premise *)
+]
+qed-.