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}}.
#A #a1 #a2 #l1 #l2 #Heq destruct //
qed.
+(* option cons *)
+
+definition option_cons ≝ λsig.λc:option sig.λl.
+ match c with [ None ⇒ l | Some c0 ⇒ c0::l ].
+
+lemma opt_cons_tail_expand : ∀A,l.l = option_cons A (option_hd ? l) (tail ? l).
+#A * //
+qed.
+
+(* comparing lists *)
+
+lemma compare_append : ∀A,l1,l2,l3,l4. l1@l2 = l3@l4 →
+∃l:list A.(l1 = l3@l ∧ l4=l@l2) ∨ (l3 = l1@l ∧ l2=l@l4).
+#A #l1 elim l1
+ [#l2 #l3 #l4 #Heq %{l3} %2 % // @Heq
+ |#a1 #tl1 #Hind #l2 #l3 cases l3
+ [#l4 #Heq %{(a1::tl1)} %1 % // @sym_eq @Heq
+ |#a3 #tl3 #l4 normalize in ⊢ (%→?); #Heq cases (Hind l2 tl3 l4 ?)
+ [#l * * #Heq1 #Heq2 %{l}
+ [%1 % // >Heq1 >(cons_injective_l ????? Heq) //
+ |%2 % // >Heq1 >(cons_injective_l ????? Heq) //
+ ]
+ |@(cons_injective_r ????? Heq)
+ ]
+ ]
+ ]
+qed.
(**************************** iterators ******************************)
let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
#A #l elim l //
qed.
+lemma length_tail1 : ∀A,l.0 < |l| → |tail A l| < |l|.
+#A * normalize //
+qed.
+
lemma length_append: ∀A.∀l1,l2:list A.
|l1@l2| = |l1|+|l2|.
#A #l1 elim l1 // normalize /2/
#A * // #a #tl normalize #H destruct
qed.
+lemma lists_length_split :
+ ∀A.∀l1,l2:list A.(∃la,lb.(|la| = |l1| ∧ l2 = la@lb) ∨ (|la| = |l2| ∧ l1 = la@lb)).
+#A #l1 elim l1
+[ #l2 %{[ ]} %{l2} % % %
+| #hd1 #tl1 #IH *
+ [ %{[ ]} %{(hd1::tl1)} %2 % %
+ | #hd2 #tl2 cases (IH tl2) #x * #y *
+ [ * #IH1 #IH2 %{(hd2::x)} %{y} % normalize % //
+ | * #IH1 #IH2 %{(hd1::x)} %{y} %2 normalize % // ]
+ ]
+]
+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.
]
] qed.
+lemma All_append: ∀A,P,l1,l2. All A P l1 → All A P l2 → All A P (l1@l2).
+#A #P #l1 elim l1 -l1 //
+#a #l1 #IHl1 #l2 * /3 width=1/
+qed.
+
+lemma All_inv_append: ∀A,P,l1,l2. All A P (l1@l2) → All A P l1 ∧ All A P l2.
+#A #P #l1 elim l1 -l1 /2 width=1/
+#a #l1 #IHl1 #l2 * #Ha #Hl12
+elim (IHl1 … Hl12) -IHl1 -Hl12 /3 width=1/
+qed-.
+
+(**************************** Allr ******************************)
+
+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 ]
+].
+
+lemma Allr_fwd_append_sn: ∀A,R,l1,l2. Allr A R (l1@l2) → Allr A R l1.
+#A #R #l1 elim l1 -l1 // #a1 * // #a2 #l1 #IHl1 #l2 * /3 width=2/
+qed-.
+
+lemma Allr_fwd_cons: ∀A,R,a,l. Allr A R (a::l) → Allr A R l.
+#A #R #a * // #a0 #l * //
+qed-.
+
+lemma Allr_fwd_append_dx: ∀A,R,l1,l2. Allr A R (l1@l2) → Allr A R l2.
+#A #R #l1 elim l1 -l1 // #a1 #l1 #IHl1 #l2 #H
+lapply (Allr_fwd_cons … (l1@l2) H) -H /2 width=1/
+qed-.
+
(**************************** Exists *******************************)
let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝