right associative with precedence 47
for @{'cons $hd $tl}.
-notation "[ list0 x sep ; ]"
+notation "[ list0 term 19 x sep ; ]"
non associative with precedence 90
for ${fold right @'nil rec acc @{'cons $x $acc}}.
[ nil ⇒ 0
| cons a tl ⇒ S (length A tl)].
-notation "|M|" non associative with precedence 65 for @{'norm $M}.
-interpretation "norm" 'norm l = (length ? l).
+interpretation "list length" 'card l = (length ? l).
lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
#A #l elim l //
#A #l elim l // #a #l0 #IH >reverse_cons >length_append normalize //
qed.
+lemma lenght_to_nil: ∀A.∀l:list A.
+ |l| = 0 → l = [ ].
+#A * // #a #tl normalize #H destruct
+qed.
+
(****************** traversing two lists in parallel *****************)
lemma list_ind2 :
∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
[ nil ⇒ False
| cons hd tl ⇒ a=hd ∨ mem A a tl
].
+
+lemma mem_append: ∀A,a,l1,l2.mem A a (l1@l2) →
+ mem ? a l1 ∨ mem ? a l2.
+#A #a #l1 elim l1
+ [#l2 #mema %2 @mema
+ |#b #tl #Hind #l2 *
+ [#eqab %1 %1 @eqab
+ |#Hmema cases (Hind ? Hmema) -Hmema #Hmema [%1 %2 //|%2 //]
+ ]
+ ]
+qed.
+
+lemma mem_append_l1: ∀A,a,l1,l2.mem A a l1 → mem A a (l1@l2).
+#A #a #l1 #l2 elim l1
+ [whd in ⊢ (%→?); @False_ind
+ |#b #tl #Hind * [#eqab %1 @eqab |#Hmema %2 @Hind //]
+ ]
+qed.
+
+lemma mem_append_l2: ∀A,a,l1,l2.mem A a l2 → mem A a (l1@l2).
+#A #a #l1 #l2 elim l1 [//|#b #tl #Hind #Hmema %2 @Hind //]
+qed.
+
+lemma mem_single: ∀A,a,b. mem A a [b] → a=b.
+#A #a #b * // @False_ind
+qed.
+
+lemma mem_map: ∀A,B.∀f:A→B.∀l,b.
+ mem ? b (map … f l) → ∃a. mem ? a l ∧ f a = b.
+#A #B #f #l elim l
+ [#b normalize @False_ind
+ |#a #tl #Hind #b normalize *
+ [#eqb @(ex_intro … a) /3/
+ |#memb cases (Hind … memb) #a * #mema #eqb
+ @(ex_intro … a) /3/
+ ]
+ ]
+qed.
+
+lemma mem_map_forward: ∀A,B.∀f:A→B.∀a,l.
+ mem A a l → mem B (f a) (map ?? f l).
+ #A #B #f #a #l elim l
+ [normalize @False_ind
+ |#b #tl #Hind *
+ [#eqab <eqab normalize %1 % |#memtl normalize %2 @Hind @memtl]
+ ]
+qed.
(***************************** split *******************************)
let rec split_rev A (l:list A) acc n on n ≝
@(ex_intro … (\snd (split A l n))) % /2/
qed.
+(****************************** flatten ******************************)
+definition flatten ≝ λA.foldr (list A) (list A) (append A) [].
+
+lemma flatten_to_mem: ∀A,n,l,l1,l2.∀a:list A. 0 < n →
+ (∀x. mem ? x l → |x| = n) → |a| = n → flatten ? l = l1@a@l2 →
+ (∃q.|l1| = n*q) → mem ? a l.
+#A #n #l elim l
+ [normalize #l1 #l2 #a #posn #Hlen #Ha #Hnil @False_ind
+ cut (|a|=0) [@sym_eq @le_n_O_to_eq
+ @(transitive_le ? (|nil A|)) // >Hnil >length_append >length_append //] /2/
+ |#hd #tl #Hind #l1 #l2 #a #posn #Hlen #Ha
+ whd in match (flatten ??); #Hflat * #q cases q
+ [<times_n_O #Hl1
+ cut (a = hd) [>(lenght_to_nil… Hl1) in Hflat;
+ whd in ⊢ ((???%)→?); #Hflat @sym_eq @(append_l1_injective … Hflat)
+ >Ha >Hlen // %1 //
+ ] /2/
+ |#q1 #Hl1 lapply (split_exists … n l1 ?) //
+ * #l11 * #l12 * #Heql1 #Hlenl11 %2
+ @(Hind l12 l2 … posn ? Ha)
+ [#x #memx @Hlen %2 //
+ |@(append_l2_injective ? hd l11)
+ [>Hlenl11 @Hlen %1 %
+ |>Hflat >Heql1 >associative_append %
+ ]
+ |@(ex_intro …q1) @(injective_plus_r n)
+ <Hlenl11 in ⊢ (??%?); <length_append <Heql1 >Hl1 //
+ ]
+ ]
+ ]
+qed.
+
(****************************** nth ********************************)
let rec nth n (A:Type[0]) (l:list A) (d:A) ≝
match n with
]
] qed.
+let rec Allr (A:Type[0]) (R:relation A) (l:list A) on l : Prop ≝
+match l with
+[ nil ⇒ True
+| cons a1 l ⇒ match l with [ nil ⇒ True | cons a2 _ ⇒ R a1 a2 ∧ Allr A R l ]
+].
+
(**************************** Exists *******************************)
let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝