Library MetaCoq.Template.utils
Notation "'∑' x .. y , p" := (sigT (fun x ⇒ .. (sigT (fun y ⇒ p%type)) ..))
(at level 200, x binder, right associativity,
format "'[' '∑' '/ ' x .. y , '/ ' p ']'")
: type_scope.
Notation "( x ; y )" := (@existT _ _ x y).
Notation "( x ; y ; z )" := (x ; ( y ; z)).
Notation "( x ; y ; z ; t )" := (x ; ( y ; (z ; t))).
Notation "( x ; y ; z ; t ; u )" := (x ; ( y ; (z ; (t ; u)))).
Notation "( x ; y ; z ; t ; u ; v )" := (x ; ( y ; (z ; (t ; (u ; v))))).
Notation "x .π1" := (@projT1 _ _ x) (at level 3, format "x '.π1'").
Notation "x .π2" := (@projT2 _ _ x) (at level 3, format "x '.π2'").
Notation "p .1" := (fst p)
(at level 2, left associativity, format "p .1") : pair_scope.
Notation "p .2" := (snd p)
(at level 2, left associativity, format "p .2") : pair_scope.
Notation "x × y" := (prod x y )(at level 80, right associativity).
Notation "#| l |" := (List.length l) (at level 0, l at level 99, format "#| l |").
Tactic Notation "destruct" "?" :=
let E := fresh "E" in
match goal with
[ |- context[match ?X with _ ⇒ _ end]] ⇒ destruct X eqn:E
| [ H : context[match ?X with _ ⇒ _ end] |- _] ⇒ destruct X eqn:E
end.
Tactic Notation "destruct" "?" "in" hyp(H) :=
let e := fresh "E" in
match type of H with context [match ?x with _ ⇒ _ end] ⇒ destruct x eqn:e
end.
Notation "'eta_compose'" := (fun g f x ⇒ g (f x)).
Notation "g ∘ f" := (eta_compose g f).
Tactic Notation "destruct" "?" :=
let E := fresh "E" in
match goal with
[ |- context[match ?X with _ ⇒ _ end]] ⇒ destruct X eqn:E
| [ H : context[match ?X with _ ⇒ _ end] |- _] ⇒ destruct X eqn:E
end.
Tactic Notation "destruct" "?" "in" hyp(H) :=
let e := fresh "E" in
match type of H with context [match ?x with _ ⇒ _ end] ⇒ destruct x eqn:e
end.
Tactic Notation "apply*" constr(H) "in" hyp(H')
:= apply H in H'; [..|apply H].
Notation "'precompose'" := (fun R f x y ⇒ R (f x) (f y)) (only parsing).
Definition transport {A} (P : A → Type) {x y : A} (e : x = y) : P x → P y
:= fun u ⇒ eq_rect x P u y e.
Notation "p # x" := (transport _ p x) (right associativity, at level 65).
We cannot use ssrbool as it breaks extraction.
Coercion is_true : bool >-> Sortclass.
Definition pred (A : Type) := A → bool.
Lemma andb_and b b' : is_true (b && b') ↔ is_true b ∧ is_true b'.
Lemma andP {b b'} : is_true (b && b') → is_true b ∧ is_true b'.
Definition pred (A : Type) := A → bool.
Lemma andb_and b b' : is_true (b && b') ↔ is_true b ∧ is_true b'.
Lemma andP {b b'} : is_true (b && b') → is_true b ∧ is_true b'.
"Incoherent" notion of equivalence, that we only apply to hProps actually.
Record isEquiv (A B : Type) :=
{ equiv : A → B;
equiv_inv : B → A}.
Infix "<~>" := isEquiv (at level 90).
Record squash (A : Type) : Prop := sq { _ : A }.
Notation "∥ T ∥" := (squash T) (at level 10).
Definition on_snd {A B C} (f : B → C) (p : A × B) :=
(fst p, f (snd p)).
Definition test_snd {A B} (f : B → bool) (p : A × B) :=
f (snd p).
Definition option_get {A} (default : A) (x : option A) : A
:= match x with
| Some x ⇒ x
| None ⇒ default
end.
Definition on_some {A} (P : A → Type) (o : option A) :=
match o with
| Some t ⇒ P t
| None ⇒ False
end.
Definition option_default {A B} (f : A → B) (o : option A) (b : B) :=
match o with Some x ⇒ f x | None ⇒ b end.
Definition on_rel {A B} (R : A → A → Prop) (f : B → A) : B → B → Prop :=
fun x y ⇒ R (f x) (f y).
Definition on_Trel {A B} (R : A → A → Type) (f : B → A) : B → B → Type :=
fun x y ⇒ R (f x) (f y).
Class Fuel := fuel : nat.
{ equiv : A → B;
equiv_inv : B → A}.
Infix "<~>" := isEquiv (at level 90).
Record squash (A : Type) : Prop := sq { _ : A }.
Notation "∥ T ∥" := (squash T) (at level 10).
Definition on_snd {A B C} (f : B → C) (p : A × B) :=
(fst p, f (snd p)).
Definition test_snd {A B} (f : B → bool) (p : A × B) :=
f (snd p).
Definition option_get {A} (default : A) (x : option A) : A
:= match x with
| Some x ⇒ x
| None ⇒ default
end.
Definition on_some {A} (P : A → Type) (o : option A) :=
match o with
| Some t ⇒ P t
| None ⇒ False
end.
Definition option_default {A B} (f : A → B) (o : option A) (b : B) :=
match o with Some x ⇒ f x | None ⇒ b end.
Definition on_rel {A B} (R : A → A → Prop) (f : B → A) : B → B → Prop :=
fun x y ⇒ R (f x) (f y).
Definition on_Trel {A B} (R : A → A → Type) (f : B → A) : B → B → Type :=
fun x y ⇒ R (f x) (f y).
Class Fuel := fuel : nat.
Such a useful tactic it should be part of the stdlib.
Tactic Notation "forward" constr(H) := forward_gen H ltac:(idtac).
Tactic Notation "forward" constr(H) "by" tactic(tac) := forward_gen H tac.
Definition string_of_nat n : string :=
match n with
| 0 ⇒ "0"
| 1 ⇒ "1"
| 2 ⇒ "2"
| 3 ⇒ "3"
| 4 ⇒ "4"
| 5 ⇒ "5"
| 6 ⇒ "6"
| 7 ⇒ "7"
| 8 ⇒ "8"
| 9 ⇒ "9"
| 10 ⇒ "10"
| 11 ⇒ "11"
| 12 ⇒ "12"
| 13 ⇒ "13"
| 14 ⇒ "14"
| 15 ⇒ "15"
| 16 ⇒ "16"
| 17 ⇒ "17"
| 18 ⇒ "18"
| 19 ⇒ "19"
| 20 ⇒ "20"
| 21 ⇒ "21"
| 22 ⇒ "22"
| 23 ⇒ "23"
| 24 ⇒ "24"
| 25 ⇒ "25"
| 26 ⇒ "26"
| 27 ⇒ "27"
| 28 ⇒ "28"
| 29 ⇒ "29"
| 30 ⇒ "30"
| 31 ⇒ "31"
| 32 ⇒ "32"
| 33 ⇒ "33"
| 34 ⇒ "34"
| 35 ⇒ "35"
| 36 ⇒ "36"
| 37 ⇒ "37"
| 38 ⇒ "38"
| 39 ⇒ "39"
| 40 ⇒ "40"
| 41 ⇒ "41"
| 42 ⇒ "42"
| 43 ⇒ "43"
| 44 ⇒ "44"
| 45 ⇒ "45"
| 46 ⇒ "46"
| 47 ⇒ "47"
| 48 ⇒ "48"
| 49 ⇒ "49"
| _ ⇒ "todo string_of_nat"
end.
Fixpoint fold_left_i_aux {A B} (f : A → nat → B → A) (n0 : nat) (l : list B)
(a0 : A) {struct l} : A
:= match l with
| [] ⇒ a0
| b :: l ⇒ fold_left_i_aux f (S n0) l (f a0 n0 b)
end.
Definition fold_left_i {A B} f := @fold_left_i_aux A B f 0.
Section Forallb2.
Context {A} (f : A → A → bool).
Fixpoint forallb2 l l' :=
match l, l' with
| hd :: tl, hd' :: tl' ⇒ f hd hd' && forallb2 tl tl'
| [], [] ⇒ true
| _, _ ⇒ false
end.
End Forallb2.
Program Fixpoint safe_nth {A} (l : list A) (n : nat | n < List.length l) : A :=
match l with
| nil ⇒ !
| hd :: tl ⇒
match n with
| 0 ⇒ hd
| S n ⇒ safe_nth tl n
end
end.
Lemma nth_error_safe_nth {A} n (l : list A) (isdecl : n < Datatypes.length l) :
nth_error l n = Some (safe_nth l (exist _ n isdecl)).
Definition rev {A} (l : list A) : list A :=
let fix aux (l : list A) (acc : list A) : list A :=
match l with
| [] ⇒ acc
| x :: l ⇒ aux l (x :: acc)
end
in aux l [].
Definition rev_map {A B} (f : A → B) (l : list A) : list B :=
let fix aux (l : list A) (acc : list B) : list B :=
match l with
| [] ⇒ acc
| x :: l ⇒ aux l (f x :: acc)
end
in aux l [].
Fact rev_cons :
∀ {A} {l} {a : A},
rev (a :: l) = (rev l ++ [a])%list.
Fact rev_map_cons :
∀ {A B} {f : A → B} {l} {a : A},
rev_map f (a :: l) = (rev_map f l ++ [f a])%list.
Fact rev_length :
∀ {A} {l : list A},
List.length (rev l) = List.length l.
Fact rev_map_length :
∀ {A B} {f : A → B} {l : list A},
List.length (rev_map f l) = List.length l.
Fact rev_map_app :
∀ {A B} {f : A → B} {l1 l2},
(rev_map f (l1 ++ l2) = rev_map f l2 ++ rev_map f l1)%list.
Facts about booleans, characters and strings
Definition bool_compare (x y : bool) : comparison :=
if x then if y then Eq else Gt else if y then Lt else Eq.
Definition bool_lt (x y : bool) :=
if x then False else y = true.
Definition bool_Compare (x y : bool) : Compare bool_lt eq x y.
Lemma transitive_bool_lt : Transitive (fun b b' ⇒ bool_compare b b' = Lt).
Definition ascii_compare x y :=
let 'Ascii a b c d e f g h := x in
let 'Ascii a' b' c' d' e' f' g' h' := y in
bool_compare a a'
?? bool_compare b b'
?? bool_compare c c'
?? bool_compare d d'
?? bool_compare e e'
?? bool_compare f f'
?? bool_compare g g'
?? bool_compare h h'.
Definition ascii_lt x y := ascii_compare x y = Lt.
Lemma ascii_Compare_eq : ∀ x y, ascii_compare x y = Eq ↔ x = y.
Lemma ascii_compare_Lt x y : ascii_compare x y = Gt ↔ ascii_compare y x = Lt.
Definition ascii_Compare (x y : ascii) : Compare ascii_lt eq x y.
Lemma transitive_ascii_lt : Transitive ascii_lt.
Fixpoint string_compare x y :=
match x, y with
| EmptyString, EmptyString ⇒ Eq
| String a s, String b s' ⇒
match ascii_compare a b with
| Eq ⇒ string_compare s s'
| Lt ⇒ Lt
| Gt ⇒ Gt
end
| EmptyString, String _ _ ⇒ Lt
| String _ _, EmptyString ⇒ Gt
end.
Definition string_lt x y : Prop := string_compare x y = Lt.
Lemma string_compare_eq : ∀ x y : string, string_compare x y = Eq ↔ eq x y.
Lemma string_compare_lt : ∀ x y : string, string_compare x y = Lt ↔ string_compare y x = Gt.
Definition string_Compare (x y : string) : Compare string_lt eq x y.
Lemma transitive_string_lt : Transitive string_lt.
Lemma CompareSpec_Proper : Proper (iff ==> iff ==> iff ==> Logic.eq ==> iff) CompareSpec.
Lemma CompareSpec_string s s'
: CompareSpec (s = s') (string_lt s s') (string_lt s' s) (string_compare s s').
Combinators
Forall combinators in Type to allow building them by recursion
Inductive All (A : Type) (P : A → Type) : list A → Type :=
All_nil : All A P []
| All_cons : ∀ (x : A) (l : list A),
P x → All A P l → All A P (x :: l).
Inductive Alli {A} (P : nat → A → Type) (n : nat) : list A → Type :=
| Alli_nil : Alli P n []
| Alli_cons hd tl : P n hd → Alli P (S n) tl → Alli P n (hd :: tl).
Inductive All2 {A B : Type} (R : A → B → Type) : list A → list B → Type :=
All2_nil : All2 R [] []
| All2_cons : ∀ (x : A) (y : B) (l : list A) (l' : list B),
R x y → All2 R l l' → All2 R (x :: l) (y :: l').
Inductive OnOne2 {A : Type} (P : A → A → Type) : list A → list A → Type :=
| OnOne2_hd hd hd' tl : P hd hd' → OnOne2 P (hd :: tl) (hd' :: tl)
| OnOne2_tl hd tl tl' : OnOne2 P tl tl' → OnOne2 P (hd :: tl) (hd :: tl').
Fixpoint mapi_rec {A B} (f : nat → A → B) (l : list A) (n : nat) : list B :=
match l with
| [] ⇒ []
| hd :: tl ⇒ f n hd :: mapi_rec f tl (S n)
end.
Definition mapi {A B} (f : nat → A → B) (l : list A) := mapi_rec f l 0.
Lemma on_snd_on_snd {A B C D} (f : C → D) (g : B → C) (d : A × B) :
on_snd f (on_snd g d) = on_snd (fun x ⇒ f (g x)) d.
Lemma snd_on_snd {A B C} (f : B → C) (p : A × B) : snd (on_snd f p) = f (snd p).
Lemma compose_on_snd {A B C D} (f : C → D) (g : B → C) :
compose (A:=A × B) (on_snd f) (on_snd g) = on_snd (compose f g).
Lemma map_map_compose :
∀ (A B C : Type) (f : A → B) (g : B → C) (l : list A),
map g (map f l) = map (compose g f) l.
Lemma map_id_f {A} (l : list A) (f : A → A) :
(∀ x, f x = x) →
map f l = l.
Lemma forall_map_spec {A B} {l} {f g : A → B} :
Forall (fun x ⇒ f x = g x) l ↔
map f l = map g l.
Lemma forall_map_id_spec {A} {P : A → Prop} {l} {f : A → A} :
Forall (fun x ⇒ f x = x) l ↔ map f l = l.
Lemma on_snd_eq_spec {A B C} (f g : B → C) (x : A × B) :
f (snd x) = g (snd x) ↔
on_snd f x = on_snd g x.
Section Reverse_Induction.
Context {A : Type}.
Lemma rev_list_ind :
∀ P:list A→ Type,
P [] →
(∀ (a:A) (l:list A), P (List.rev l) → P (List.rev (a :: l))) →
∀ l:list A, P (List.rev l).
Theorem rev_ind :
∀ P:list A → Type,
P [] →
(∀ (x:A) (l:list A), P l → P (l ++ [x])) → ∀ l:list A, P l.
End Reverse_Induction.
Lemma forallb_Forall {A} (p : pred A) l
: Forall (is_true ∘ p) l ↔ is_true (forallb p l).
Lemma skipn_nil :
∀ {A} n, @skipn A n [] = [].
Lemma skipn_S {A} a (l : list A) n : skipn (S n) (a :: l) = skipn n l.
All_nil : All A P []
| All_cons : ∀ (x : A) (l : list A),
P x → All A P l → All A P (x :: l).
Inductive Alli {A} (P : nat → A → Type) (n : nat) : list A → Type :=
| Alli_nil : Alli P n []
| Alli_cons hd tl : P n hd → Alli P (S n) tl → Alli P n (hd :: tl).
Inductive All2 {A B : Type} (R : A → B → Type) : list A → list B → Type :=
All2_nil : All2 R [] []
| All2_cons : ∀ (x : A) (y : B) (l : list A) (l' : list B),
R x y → All2 R l l' → All2 R (x :: l) (y :: l').
Inductive OnOne2 {A : Type} (P : A → A → Type) : list A → list A → Type :=
| OnOne2_hd hd hd' tl : P hd hd' → OnOne2 P (hd :: tl) (hd' :: tl)
| OnOne2_tl hd tl tl' : OnOne2 P tl tl' → OnOne2 P (hd :: tl) (hd :: tl').
Fixpoint mapi_rec {A B} (f : nat → A → B) (l : list A) (n : nat) : list B :=
match l with
| [] ⇒ []
| hd :: tl ⇒ f n hd :: mapi_rec f tl (S n)
end.
Definition mapi {A B} (f : nat → A → B) (l : list A) := mapi_rec f l 0.
Lemma on_snd_on_snd {A B C D} (f : C → D) (g : B → C) (d : A × B) :
on_snd f (on_snd g d) = on_snd (fun x ⇒ f (g x)) d.
Lemma snd_on_snd {A B C} (f : B → C) (p : A × B) : snd (on_snd f p) = f (snd p).
Lemma compose_on_snd {A B C D} (f : C → D) (g : B → C) :
compose (A:=A × B) (on_snd f) (on_snd g) = on_snd (compose f g).
Lemma map_map_compose :
∀ (A B C : Type) (f : A → B) (g : B → C) (l : list A),
map g (map f l) = map (compose g f) l.
Lemma map_id_f {A} (l : list A) (f : A → A) :
(∀ x, f x = x) →
map f l = l.
Lemma forall_map_spec {A B} {l} {f g : A → B} :
Forall (fun x ⇒ f x = g x) l ↔
map f l = map g l.
Lemma forall_map_id_spec {A} {P : A → Prop} {l} {f : A → A} :
Forall (fun x ⇒ f x = x) l ↔ map f l = l.
Lemma on_snd_eq_spec {A B C} (f g : B → C) (x : A × B) :
f (snd x) = g (snd x) ↔
on_snd f x = on_snd g x.
Section Reverse_Induction.
Context {A : Type}.
Lemma rev_list_ind :
∀ P:list A→ Type,
P [] →
(∀ (a:A) (l:list A), P (List.rev l) → P (List.rev (a :: l))) →
∀ l:list A, P (List.rev l).
Theorem rev_ind :
∀ P:list A → Type,
P [] →
(∀ (x:A) (l:list A), P l → P (l ++ [x])) → ∀ l:list A, P l.
End Reverse_Induction.
Lemma forallb_Forall {A} (p : pred A) l
: Forall (is_true ∘ p) l ↔ is_true (forallb p l).
Lemma skipn_nil :
∀ {A} n, @skipn A n [] = [].
Lemma skipn_S {A} a (l : list A) n : skipn (S n) (a :: l) = skipn n l.
Generic strategy for dealing with Forall/forall, etc:
1) Move all boolean foralls into All/All2 (in the goal and the context).
2) Merge all context Foralls into one
3) Apply Forall implication
4) optionally simplify and call eauto.
Lemma Forall_mix {A} (P Q : A → Prop) : ∀ l, Forall P l → Forall Q l → Forall (fun x ⇒ P x ∧ Q x) l.
Lemma Forall_skipn {A} (P : A → Prop) n l : Forall P l → Forall P (skipn n l).
Lemma Forall_firstn {A} (P : A → Prop) n l : Forall P l → Forall P (firstn n l).
Lemma forallb2_All2 {A : Type} {p : A → A → bool}
{l l' : list A} :
is_true (forallb2 p l l') → All2 (fun x y ⇒ is_true (p x y)) l l'.
Lemma All2_forallb2 {A : Type} {p : A → A → bool}
{l l' : list A} :
All2 (fun x y ⇒ is_true (p x y)) l l' → is_true (forallb2 p l l').
Lemma forallb2_app {A} (p : A → A → bool) l l' q q' :
is_true (forallb2 p l l' && forallb2 p q q')
→ is_true (forallb2 p (l ++ q) (l' ++ q')).
Lemma All2_map {A B C D} (R : C → D → Type) (f : A → C) (g : B → D) l l' :
All2 (fun x y ⇒ R (f x) (g y)) l l' → All2 R (map f l) (map g l').
Lemma All2_map_inv {A B C D} (R : C → D → Type) (f : A → C) (g : B → D) l l' :
All2 R (map f l) (map g l') → All2 (fun x y ⇒ R (f x) (g y)) l l'.
Lemma All2_All_mix_left {A B} {P : A → Type} {Q : A → B → Type}
{l : list A} {l' : list B} :
All P l → All2 Q l l' → All2 (fun x y ⇒ (P x × Q x y)%type) l l'.
Lemma All2_All_mix_right {A B} {P : B → Type} {Q : A → B → Type}
{l : list A} {l' : list B} :
All P l' → All2 Q l l' → All2 (fun x y ⇒ (Q x y × P y)%type) l l'.
Lemma Forall_All {A : Type} (P : A → Prop) l :
Forall P l → All P l.
Lemma All_Forall {A : Type} (P : A → Prop) l :
All P l → Forall P l.
Lemma forallb_All {A} (p : pred A) l : is_true (forallb p l) → All (is_true ∘ p) l.
Lemma All_forallb {A} (p : pred A) l : All (is_true ∘ p) l → is_true (forallb p l).
Lemma OnOne2_All_mix_left {A} {P : A → A → Type} {Q : A → Type} {l l'} :
All Q l → OnOne2 P l l' → OnOne2 (fun x y ⇒ (P x y × Q x)%type) l l'.
Lemma OnOne2_app {A} (P : A → A → Type) l tl tl' : OnOne2 P tl tl' → OnOne2 P (l ++ tl) (l ++ tl').
Lemma OnOne2_length {A} {P} {l l' : list A} : OnOne2 P l l' → #|l| = #|l'|.
Lemma OnOne2_mapP {A B} {P} {l l' : list A} (f : A → B) :
OnOne2 (on_rel P f) l l' → OnOne2 P (map f l) (map f l').
Lemma OnOne2_map {A B} {P : B → B → Type} {l l' : list A} (f : A → B) :
OnOne2 (on_Trel P f) l l' → OnOne2 P (map f l) (map f l').
Lemma OnOne2_sym {A} (P : A → A → Type) l l' : OnOne2 (fun x y ⇒ P y x) l' l → OnOne2 P l l'.
Lemma OnOne2_exist {A} (P : A → A → Type) (Q : A → A → Type) l l' :
OnOne2 P l l' →
(∀ x y, P x y → ∑ z, Q x z × Q y z) →
∑ r, (OnOne2 Q l r × OnOne2 Q l' r).
Lemma All_firstn {A} {P : A → Type} {l} {n} : All P l → All P (firstn n l).
Lemma All_skipn {A} {P : A → Type} {l} {n} : All P l → All P (skipn n l).
Lemma All_app {A} {P : A → Type} {l l'} : All P (l ++ l') → All P l × All P l'.
Lemma All_app_inv {A} (P : A → Type) l l' : All P l → All P l' → All P (l ++ l').
Lemma All_mix {A} {P : A → Type} {Q : A → Type} {l} :
All P l → All Q l → All (fun x ⇒ (P x × Q x)%type) l.
Lemma All2_All_left {A B} {P : A → B → Type} {Q : A → Type} {l l'} :
All2 P l l' →
(∀ x y, P x y → Q x) →
All Q l.
Lemma All2_All_right {A B} {P : A → B → Type} {Q : B → Type} {l l'} :
All2 P l l' →
(∀ x y, P x y → Q y) →
All Q l'.
Lemma All2_right {A B} {P : B → Type} {l : list A} {l'} :
All2 (fun x y ⇒ P y) l l' → All P l'.
Lemma All_rev_map {A B} (P : A → Type) f (l : list B) : All (compose P f) l → All P (rev_map f l).
Lemma All_rev (A : Type) (P : A → Type) (l : list A) : All P l → All P (List.rev l).
Lemma All_rev_inv {A} (P : A → Type) (l : list A) : All P (List.rev l) → All P l.
Lemma All_impl {A} {P Q} {l : list A} : All P l → (∀ x, P x → Q x) → All Q l.
Lemma Alli_impl {A} {P Q} (l : list A) {n} : Alli P n l → (∀ n x, P n x → Q n x) → Alli Q n l.
Lemma All_map {A B} {P : B → Type} {f : A → B} {l : list A} :
All (compose P f) l → All P (map f l).
Lemma All_map_inv {A B} (P : B → Prop) (f : A → B) l : All P (map f l) → All (compose P f) l.
Lemma All_nth_error :
∀ A P l i x,
@All A P l →
nth_error l i = Some x →
P x.
Lemma Alli_mix {A} {P : nat → A → Type} {Q : nat → A → Type} {n l} :
Alli P n l → Alli Q n l → Alli (fun n x ⇒ (P n x × Q n x)%type) n l.
Lemma Alli_All {A} {P : nat → A → Type} {Q : A → Type} {l n} :
Alli P n l →
(∀ n x, P n x → Q x) →
All Q l.
Lemma Alli_app {A} (P : nat → A → Type) n l l' : Alli P n (l ++ l') → Alli P n l × Alli P (length l + n) l'.
Lemma Alli_nth_error :
∀ A P k l i x,
@Alli A P k l →
nth_error l i = Some x →
P (k + i) x.
Lemma map_eq_inj {A B} (f g : A → B) l: map f l = map g l →
All (fun x ⇒ f x = g x) l.
Lemma mapi_ext_size {A B} (f g : nat → A → B) l k :
(∀ k' x, k' < k + #|l| → f k' x = g k' x) →
mapi_rec f l k = mapi_rec g l k.
Lemma map_ext_size {A B} (f g : nat → A → B) l :
(∀ k x, k < #|l| → f k x = g k x) →
mapi f l = mapi g l.
Lemma forall_nth_error_All :
∀ {A} (P : A → Type) l,
(∀ i x, nth_error l i = Some x → P x) →
All P l.
Lemma forall_nth_error_Alli :
∀ {A} (P : nat → A → Type) k l,
(∀ i x, nth_error l i = Some x → P (k + i) x) →
Alli P k l.
Lemma Alli_mapi {A B} {P : nat → B → Type} (f : nat → A → B) k l :
Alli (fun n a ⇒ P n (f n a)) k l <~>
Alli P k (mapi_rec f l k).
Lemma Alli_shift {A} {P : nat → A → Type} k l :
Alli (fun x ⇒ P (S x)) k l →
Alli P (S k) l.
Lemma Alli_rev {A} {P : nat → A → Type} k l :
Alli P k l →
Alli (fun k' ⇒ P (Nat.pred #|l| - k' + k)) 0 (List.rev l).
Lemma Alli_All_mix {A} {P : nat → A → Type} (Q : A → Type) k l :
Alli P k l → All Q l → Alli (fun k x ⇒ (P k x) × Q x)%type k l.
Lemma OnOne2_impl {A} {P Q} {l l' : list A} :
OnOne2 P l l' →
(∀ x y, P x y → Q x y) →
OnOne2 Q l l'.
Lemma All_map_eq {A B} {l} {f g : A → B} :
All (fun x ⇒ f x = g x) l →
map f l = map g l.
Lemma All_map_id {A} {l} {f : A → A} :
All (fun x ⇒ f x = x) l →
map f l = l.
Lemma forall_forallb_map_spec {A B : Type} {P : A → Prop} {p : A → bool}
{l : list A} {f g : A → B} :
Forall P l → is_true (forallb p l) →
(∀ x : A, P x → is_true (p x) → f x = g x) → map f l = map g l.
Lemma forall_forallb_forallb_spec {A : Type} {P : A → Prop} {p : A → bool}
{l : list A} {f : A → bool} :
Forall P l → is_true (forallb p l) →
(∀ x : A, P x → is_true (p x) → is_true (f x)) → is_true (forallb f l).
Lemma on_snd_test_spec {A B C} (P : B → Type) (p : B → bool) (f g : B → C) (x : A × B) :
P (snd x) → (∀ x, P x → is_true (p x) → f x = g x) →
is_true (test_snd p x) →
on_snd f x = on_snd g x.
Lemma Forall_map {A B} (P : B → Prop) (f : A → B) l : Forall (Program.Basics.compose P f) l → Forall P (map f l).
Lemma Forall_map_inv {A B} (P : B → Prop) (f : A → B) l : Forall P (map f l) → Forall (compose P f) l.
Lemma Forall_impl {A} {P Q : A → Prop} {l} :
Forall P l → (∀ x, P x → Q x) → Forall Q l.
Lemma All2_impl {A B} {P Q : A → B → Type} {l l'} :
All2 P l l' →
(∀ x y, P x y → Q x y) →
All2 Q l l'.
Lemma Forall_app {A} (P : A → Prop) l l' : Forall P (l ++ l') → Forall P l ∧ Forall P l'.
Lemma firstn_map {A B} n (f : A → B) l : firstn n (map f l) = map f (firstn n l).
Lemma All_safe_nth {A} {P : A → Type} {Γ n} (isdecl : n < length Γ) : All P Γ →
P (safe_nth Γ (exist _ n isdecl)).
Definition size := nat.
Section All_size.
Context {A} (P : A → Type) (fn : ∀ x1, P x1 → size).
Fixpoint all_size {l1 : list A} (f : All P l1) : size :=
match f with
| All_nil ⇒ 0
| All_cons x l px pl ⇒ fn _ px + all_size pl
end.
End All_size.
Section Alli_size.
Context {A} (P : nat → A → Type) (fn : ∀ n x1, P n x1 → size).
Fixpoint alli_size {l1 : list A} {n} (f : Alli P n l1) : size :=
match f with
| Alli_nil ⇒ 0
| Alli_cons x l px pl ⇒ fn _ _ px + alli_size pl
end.
End Alli_size.
Section All2_size.
Context {A} (P : A → A → Type) (fn : ∀ x1 x2, P x1 x2 → size).
Fixpoint all2_size {l1 l2 : list A} (f : All2 P l1 l2) : size :=
match f with
| All2_nil ⇒ 0
| All2_cons x y l l' rxy rll' ⇒ fn _ _ rxy + all2_size rll'
end.
End All2_size.
Lemma All2_non_nil {A B} (P : A → B → Type) (l : list A) (l' : list B) :
All2 P l l' → l ≠ nil → l' ≠ nil.
Lemma map_ext {A B : Type} (f g : A → B) (l : list A) :
(∀ x, f x = g x) →
map f l = map g l.
Lemma map_skipn {A B} (f : A → B) (l : list A) (n : nat) : map f (skipn n l) = skipn n (map f l).
Lemma nth_error_map {A B} (f : A → B) n l : nth_error (map f l) n = option_map f (nth_error l n).
Lemma map_nil {A B} (f : A → B) (l : list A) : l ≠ [] → map f l ≠ [].
Inductive BoolSpecSet (P Q : Prop) : bool → Set :=
BoolSpecT : P → BoolSpecSet P Q true | BoolSpecF : Q → BoolSpecSet P Q false.
Lemma leb_spec_Set : ∀ x y : nat, BoolSpecSet (x ≤ y) (y < x) (x <=? y).
Lemma some_inj {A} {x y : A} : Some x = Some y → x = y.
Inductive nth_error_Spec {A} (l : list A) (n : nat) : option A → Type :=
| nth_error_Spec_Some x : nth_error l n = Some x → n < length l → nth_error_Spec l n (Some x)
| nth_error_Spec_None : length l ≤ n → nth_error_Spec l n None.
Lemma mapi_rec_eqn {A B} (f : nat → A → B) (l : list A) a n :
mapi_rec f (a :: l) n = f n a :: mapi_rec f l (S n).
Lemma nth_error_mapi_rec {A B} (f : nat → A → B) n k l :
nth_error (mapi_rec f l k) n = option_map (f (n + k)) (nth_error l n).
Lemma nth_error_mapi {A B} (f : nat → A → B) n l :
nth_error (mapi f l) n = option_map (f n) (nth_error l n).
Lemma nth_error_Some_length {A} {l : list A} {n t} : nth_error l n = Some t → n < length l.
Lemma nth_error_Some_non_nil {A} (l : list A) (n : nat) (x : A) : nth_error l n = Some x → l ≠ [].
Lemma nth_error_spec {A} (l : list A) (n : nat) : nth_error_Spec l n (nth_error l n).
Lemma nth_error_app_left {A} (l l' : list A) n t : nth_error l n = Some t → nth_error (l ++ l') n = Some t.
Lemma nth_error_nil {A} n : nth_error (@nil A) n = None.
Lemma nth_error_forall {A} {P : A → Prop} {l : list A} {n x} :
nth_error l n = Some x → Forall P l → P x.
Lemma nth_error_all {A} {P : A → Type} {l : list A} {n x} :
nth_error l n = Some x → All P l → P x.
Lemma nth_error_alli {A} {P : nat → A → Type} {l : list A} {n x} {k} :
nth_error l n = Some x → Alli P k l → P (k + n) x.
Fixpoint chop {A} (n : nat) (l : list A) :=
match n with
| 0 ⇒ ([], l)
| S n ⇒
match l with
| hd :: tl ⇒
let '(l, r) := chop n tl in
(hd :: l, r)
| [] ⇒ ([], [])
end
end.
Lemma nth_map {A} (f : A → A) n l d :
(d = f d) →
nth n (map f l) d = f (nth n l d).
Definition on_pi2 {A B C} (f : B → B) (p : A × B × C) : A × B × C :=
(fst (fst p), f (snd (fst p)), snd p).
Lemma All_map_id' {A} {P : A → Type} {l} {f} :
All P l →
(∀ x, P x → f x = x) →
map f l = l.
Lemma Alli_mapi_spec {A B} {P : nat → A → Type} {l} {f g : nat → A → B} {n} :
Alli P n l → (∀ n x, P n x → f n x = g n x) →
mapi_rec f l n = mapi_rec g l n.
Lemma Alli_mapi_id {A} {P : nat → A → Type} {l} {f} {n} :
Alli P n l →
(∀ n x, P n x → f n x = x) →
mapi_rec f l n = l.
Lemma Alli_map_id {A} {P : nat → A → Type} {l} {f} {n} :
Alli P n l →
(∀ n x, P n x → f x = x) →
map f l = l.
Lemma nlt_map {A B} (l : list A) (f : A → B) (n : {n | n < length l }) : `n < length (map f l).
Lemma map_def_safe_nth {A B} (l : list A) (n : {n | n < length l}) (f : A → B) :
f (safe_nth l n) = safe_nth (map f l) (exist _ (`n) (nlt_map l f n)).
Lemma mapi_map {A B C} (f : nat → B → C) (l : list A) (g : A → B) :
mapi f (map g l) = mapi (fun i x ⇒ f i (g x)) l.
Lemma map_mapi {A B C} (f : nat → A → B) (l : list A) (g : B → C) :
map g (mapi f l) = mapi (fun i x ⇒ g (f i x)) l.
Lemma chop_map {A B} (f : A → B) n l l' l'' :
chop n l = (l', l'') → chop n (map f l) = (map f l', map f l'').
Lemma chop_n_app {A} {l l' : list A} {n} : n = length l → chop n (l ++ l') = (l, l').
Lemma mapi_mapi {A B C} (g : nat → A → B) (f : nat → B → C) (l : list A) :
mapi f (mapi g l) = mapi (fun n x ⇒ f n (g n x)) l.
Lemma mapi_rec_ext {A B} (f g : nat → A → B) (l : list A) n :
(∀ k x, n ≤ k → k < length l + n → f k x = g k x) →
mapi_rec f l n = mapi_rec g l n.
Lemma mapi_ext {A B} (f g : nat → A → B) (l : list A) :
(∀ n x, f n x = g n x) →
mapi f l = mapi g l.
Lemma mapi_rec_app {A B} (f : nat → A → B) (l l' : list A) n :
(mapi_rec f (l ++ l') n = mapi_rec f l n ++ mapi_rec f l' (length l + n))%list.
Lemma mapi_app {A B} (f : nat → A → B) (l l' : list A) :
(mapi f (l ++ l') = mapi f l ++ mapi (fun n x ⇒ f (length l + n) x) l')%list.
Lemma mapi_rec_Sk {A B} (f : nat → A → B) (l : list A) k :
mapi_rec f l (S k) = mapi_rec (fun n x ⇒ f (S n) x) l k.
Lemma rev_mapi_rec {A B} (f : nat → A → B) (l : list A) n k : k ≤ n →
List.rev (mapi_rec f l (n - k)) = mapi_rec (fun k x ⇒ f (Nat.pred (length l) + n - k) x) (List.rev l) k.
Lemma rev_mapi {A B} (f : nat → A → B) (l : list A) :
List.rev (mapi f l) = mapi (fun k x ⇒ f (Nat.pred (length l) - k) x) (List.rev l).
Lemma mapi_rec_rev {A B} (f : nat → A → B) (l : list A) n :
mapi_rec f (List.rev l) n = List.rev (mapi (fun k x ⇒ f (length l + n - S k) x) l).
Lemma mapi_rev {A B} (f : nat → A → B) (l : list A) :
mapi f (List.rev l) = List.rev (mapi (fun k x ⇒ f (length l - S k) x) l).
Lemma mapi_rec_length {A B} (f : nat → A → B) (l : list A) n :
length (mapi_rec f l n) = length l.
Lemma mapi_length {A B} (f : nat → A → B) (l : list A) :
length (mapi f l) = length l.
Lemma skipn_length {A} n (l : list A) : n ≤ length l → length (skipn n l) = length l - n.
Lemma forallb_map {A B} (f : A → B) (l : list A) p :
forallb p (map f l) = forallb (compose p f) l.
Lemma All_forallb' {A} P (l : list A) (p : pred A) :
All P l →
(∀ x, P x → is_true (p x)) →
is_true (forallb p l).
Lemma forallb_Forall' {A} (P : A → Prop) (l : list A) p :
is_true (forallb p l) →
(∀ x, is_true (p x) → P x) →
Forall P l.
Lemma forallb_skipn {A} (p : A → bool) n l :
is_true (forallb p l) →
is_true (forallb p (skipn n l)).
Lemma forallb_rev {A} (p : A → bool) l :
forallb p (List.rev l) = forallb p l.
Lemma Forall_forallb_eq_forallb {A} (P : A → Prop) (p q : A → bool) l :
Forall P l →
(∀ x, P x → p x = q x) →
forallb p l = forallb q l.
Lemma forallb2_length {A} (p : A → A → bool) l l' : is_true (forallb2 p l l') → length l = length l'.
Fixpoint map_option_out {A} (l : list (option A)) : option (list A) :=
match l with
| nil ⇒ Some nil
| hd :: tl ⇒ match hd, map_option_out tl with
| Some hd, Some tl ⇒ Some (hd :: tl)
| _, _ ⇒ None
end
end.
Lemma map_option_out_map_option_map {A} (l : list (option A)) (f : A → A) :
map_option_out (map (option_map f) l) =
option_map (map f) (map_option_out l).
Lemma Alli_map_option_out_mapi_Some_spec {A B} (f g : nat → A → option B) l t P :
Alli P 0 l →
(∀ i x t, P i x → f i x = Some t → g i x = Some t) →
map_option_out (mapi f l) = Some t →
map_option_out (mapi g l) = Some t.
Lemma combine_map_id {A B} (l : list (A × B)) :
l = combine (map fst l) (map snd l).
Lemma Forall_forallb {A} P (l : list A) (p : pred A) :
Forall P l →
(∀ x, P x → is_true (p x)) →
is_true (forallb p l).
Lemma Forall2_right {A B} (P : B → Prop) (l : list A) (l' : list B) :
Forall2 (fun x y ⇒ P y) l l' → List.Forall (fun x ⇒ P x) l'.
Lemma Forall2_non_nil {A B} (P : A → B → Prop) (l : list A) (l' : list B) :
Forall2 P l l' → l ≠ nil → l' ≠ nil.
Lemma Forall2_length {A B} {P : A → B → Prop} {l l'} : Forall2 P l l' → #|l| = #|l'|.
Lemma Forall2_app_r {A} (P : A → A → Prop) l l' r r' : Forall2 P (l ++ [r]) (l' ++ [r']) →
(Forall2 P l l') ∧ (P r r').
Lemma Forall2_map_inv :
∀ {A B A' B'} (R : A' → B' → Prop) (f : A → A')
(g : B → B') (l : list A) (l' : list B),
Forall2 R (map f l) (map g l') →
Forall2 (fun x ⇒ R (f x) ∘ g) l l'.
Lemma All2_app_inv : ∀ (A B : Type) (R : A → B → Type),
∀ l l1 l2, All2 R (l1 ++ l2) l → { '(l1',l2') : _ & (l = l1' ++ l2')%list × (All2 R l1 l1') × (All2 R l2 l2')}%type.
Lemma All2_ind_rev : ∀ (A B : Type) (R : A → B → Type) (P : ∀ (l : list A) (l0 : list B), Prop),
P [] [] →
(∀ (x : A) (y : B) (l : list A) (l' : list B) (r : R x y) (a : All2 R l l'),
P l l' → P (l ++ [x])%list (l' ++ [y]))%list →
∀ (l : list A) (l0 : list B) (a : All2 R l l0), P l l0.
Lemma last_inv A (l1 l2 : list A) x y :
(l1 ++ [x] = l2 ++ [y] → l1 = l2 ∧ x = y)%list.
Lemma All2_app :
∀ (A B : Type) (R : A → B → Type),
∀ l1 l2 l1' l2',
All2 R l1 l1' →
All2 R l2 l2' →
All2 R (l1 ++ l2) (l1' ++ l2').
Lemma All2_impl_In {A B} {P Q : A → B → Type} {l l'} :
All2 P l l' →
(∀ x y, In x l → In y l' → P x y → Q x y) →
All2 Q l l'.
Lemma Forall2_skipn A B (P : A → B → Prop) l l' n:
Forall2 P l l' → Forall2 P (skipn n l) (skipn n l').
Lemma All2_Forall2 {A B} {P : A → B → Prop} {l l'} :
All2 P l l' → Forall2 P l l'.
Lemma Forall2_nth_error_Some {A B} {P : A → B → Prop} {l l'} n t :
Forall2 P l l' →
nth_error l n = Some t →
∃ t' : B, (nth_error l' n = Some t') ∧ P t t'.
Lemma Forall2_impl {A B} {P Q : A → B → Prop} {l l'} :
Forall2 P l l' →
(∀ x y, P x y → Q x y) →
Forall2 Q l l'.
Lemma skipn_all2 :
∀ {A n} (l : list A),
#|l| ≤ n →
skipn n l = [].
Lemma nat_rev_ind (max : nat) :
∀ (P : nat → Prop),
(∀ n, n ≥ max → P n) →
(∀ n, n < max → P (S n) → P n) →
∀ n, P n.
Lemma strong_nat_ind :
∀ (P : nat → Prop),
(∀ n, (∀ m, m < n → P m) → P n) →
∀ n, P n.
Lemma app_Forall :
∀ A P (l1 l2 : list A),
Forall P l1 →
Forall P l2 →
Forall P (l1 ++ l2).
Lemma rev_Forall :
∀ A P l,
Forall P l →
Forall P (@List.rev A l).
Lemma Forall2_impl' {A B} {P Q : A → B → Prop} {l l'} :
Forall2 P l l' →
Forall (fun x ⇒ ∀ y, P x y → Q x y) l →
Forall2 Q l l'.
Lemma Forall2_Forall {A R l} : @Forall2 A A R l l → Forall (fun x ⇒ R x x) l.
Lemma All2_All {A R l} : @All2 A A R l l → All (fun x ⇒ R x x) l.
Lemma Forall_Forall2 {A R l} : Forall (fun x ⇒ R x x) l → @Forall2 A A R l l.
Lemma Forall_True {A} {P : A → Prop} l : (∀ x, P x) → Forall P l.
Lemma Forall2_True {A B} {R : A → B → Prop} l l'
: (∀ x y, R x y) → #|l| = #|l'| → Forall2 R l l'.
Lemma Forall2_map {A B A' B'} (R : A' → B' → Prop) (f : A → A') (g : B → B') l l'
: Forall2 (fun x y ⇒ R (f x) (g y)) l l' → Forall2 R (map f l) (map g l').
Lemma Forall2_and {A B} (R R' : A → B → Prop) l l'
: Forall2 R l l' → Forall2 R' l l' → Forall2 (fun x y ⇒ R x y ∧ R' x y) l l'.
Lemma Forall_Forall2_and {A B} {R : A → B → Prop} {P l l'}
: Forall2 R l l' → Forall P l → Forall2 (fun x y ⇒ P x ∧ R x y) l l'.
Lemma Forall_Forall2_and' {A B} {R : A → B → Prop} {P l l'}
: Forall2 R l l' → Forall P l' → Forall2 (fun x y ⇒ R x y ∧ P y) l l'.
Class ComparableType A := { compare : A → A → comparison }.
Fixpoint insert {A} `{ComparableType A} (x : A) (l : list A) :=
match l with
| [] ⇒ [x]
| y :: l' ⇒ match compare x y with
| Eq ⇒ l
| Lt ⇒ x :: l
| Gt ⇒ y :: (insert x l')
end
end.
Definition list_union {A} `{ComparableType A} (l l' : list A) : list A
:= fold_left (fun l' x ⇒ insert x l') l l'.
Definition compare_bool b1 b2 :=
match b1, b2 with
| false, true ⇒ Lt
| true, false ⇒ Gt
| _, _ ⇒ Eq
end.
Definition bool_lt' b1 b2 := match compare_bool b1 b2 with Lt ⇒ true | _ ⇒ false end.
Lemma Forall2_nth :
∀ A B P l l' n (d : A) (d' : B),
Forall2 P l l' →
P d d' →
P (nth n l d) (nth n l' d').
Lemma Forall2_nth_error_Some_l :
∀ A B (P : A → B → Prop) l l' n t,
nth_error l n = Some t →
Forall2 P l l' →
∃ t',
nth_error l' n = Some t' ∧
P t t'.
Lemma Forall2_nth_error_None_l :
∀ A B (P : A → B → Prop) l l' n,
nth_error l n = None →
Forall2 P l l' →
nth_error l' n = None.
Lemma Forall2_trans :
∀ A (P : A → A → Prop),
Transitive P →
Transitive (Forall2 P).
Lemma Forall2_rev :
∀ A B R l l',
@Forall2 A B R l l' →
Forall2 R (List.rev l) (List.rev l').
Lemma Forall2_mapi :
∀ A B A' B' (R : A' → B' → Prop) (f : nat → A → A') (g : nat → B → B') l l',
Forall2 (fun x y ⇒ ∀ i, R (f i x) (g i y)) l l' →
Forall2 R (mapi f l) (mapi g l').
Lemma All2_nth :
∀ A B P l l' n (d : A) (d' : B),
All2 P l l' →
P d d' →
P (nth n l d) (nth n l' d').
Lemma OnOne2_ind_l :
∀ A (R : list A → A → A → Type)
(P : ∀ L l l', OnOne2 (R L) l l' → Type),
(∀ L x y l (r : R L x y), P L (x :: l) (y :: l) (OnOne2_hd _ _ _ l r)) →
(∀ L x l l' (h : OnOne2 (R L) l l'),
P L l l' h →
P L (x :: l) (x :: l') (OnOne2_tl _ x _ _ h)
) →
∀ l l' h, P l l l' h.
Lemma All2_mapi :
∀ A B A' B' (R : A' → B' → Type) (f : nat → A → A') (g : nat → B → B') l l',
All2 (fun x y ⇒ ∀ i, R (f i x) (g i y)) l l' →
All2 R (mapi f l) (mapi g l').
Lemma OnOne2_impl_exist_and_All :
∀ A (l1 l2 l3 : list A) R1 R2 R3,
OnOne2 R1 l1 l2 →
All2 R2 l3 l2 →
(∀ x x' y, R1 x y → R2 x' y → ∑ z : A, R3 x z × R2 x' z) →
∑ l4, OnOne2 R3 l1 l4 × All2 R2 l3 l4.
Lemma OnOne2_impl_exist_and_All_r :
∀ A (l1 l2 l3 : list A) R1 R2 R3,
OnOne2 R1 l1 l2 →
All2 R2 l2 l3 →
(∀ x x' y, R1 x y → R2 y x' → ∑ z : A, R3 x z × R2 z x') →
∑ l4, ( OnOne2 R3 l1 l4 × All2 R2 l4 l3 ).
Lemma All2_skipn :
∀ A B R l l' n,
@All2 A B R l l' →
@All2 A B R (skipn n l) (skipn n l').
Lemma All2_rev (A : Type) (P : A → A → Type) (l l' : list A) :
All2 P l l' →
All2 P (List.rev l) (List.rev l').
Module NEL.
Inductive t (A : Set) :=
| sing : A → t A
| cons : A → t A → t A.
Infix "::" := cons : nel_scope.
Notation "[ x ]" := (sing x) : nel_scope.
Fixpoint length {A} (l : t A) : nat :=
match l with
| [ _ ] ⇒ 1
| _ :: l' ⇒ S (length l')
end.
Notation "[ x ; y ; .. ; z ; e ]" :=
(cons x (cons y .. (cons z (sing e)) ..)) : nel_scope.
Fixpoint to_list {A} (l : t A) : list A :=
match l with
| [x] ⇒ [x]
| x :: l ⇒ x :: (to_list l)
end.
Fixpoint map {A B : Set} (f : A → B) (l : t A) : t B :=
match l with
| [x] ⇒ [f x]
| x :: l ⇒ f x :: map f l
end.
Fixpoint app {A} (l l' : t A) : t A :=
match l with
| [x] ⇒ x :: l'
| x :: l ⇒ x :: (app l l')
end.
Infix "++" := app : nel_scope.
Fixpoint app_r {A : Set} (l : list A) (l' : t A) : t A :=
match l with
| [] ⇒ l'
| (x :: l)%list ⇒ x :: app_r l l'
end.
Fixpoint cons' {A : Set} (x : A) (l : list A) : t A :=
match l with
| [] ⇒ [x]
| (y :: l)%list ⇒ x :: cons' y l
end.
Lemma cons'_spec {A : Set} (x : A) l
: to_list (cons' x l) = (x :: l)%list.
Fixpoint fold_left {A} {B : Set} (f : A → B → A) (l : t B) (a0 : A) : A :=
match l with
| [b] ⇒ f a0 b
| b :: l ⇒ fold_left f l (f a0 b)
end.
Fixpoint forallb {A : Set} (f : A → bool) (l : t A) :=
match l with
| [x] ⇒ f x
| hd :: tl ⇒ f hd && forallb f tl
end.
Fixpoint forallb2 {A : Set} (f : A → A → bool) (l l' : t A) :=
match l, l' with
| [x], [x'] ⇒ f x x'
| hd :: tl, hd' :: tl' ⇒ f hd hd' && forallb2 f tl tl'
| _, _ ⇒ false
end.
Lemma map_to_list {A B : Set} (f : A → B) (l : t A)
: to_list (map f l) = List.map f (to_list l).
Lemma map_app {A B : Set} (f : A → B) l l' :
map f (l ++ l') = map f l ++ map f l'.
Lemma map_map {A B C : Set} (f : A → B) (g : B → C) l :
map g (map f l) = map (fun x ⇒ g (f x)) l.
Lemma map_ext {A B : Set} (f g : A → B) l :
(∀ x, f x = g x) → map f l = map g l.
End NEL.
Definition non_empty_list := NEL.t.
Lemma iff_forall {A} B C (H : ∀ x : A, B x ↔ C x)
: (∀ x, B x) ↔ (∀ x, C x).
Lemma iff_ex {A} B C (H : ∀ x : A, B x ↔ C x)
: (ex B) ↔ (ex C).
Lemma if_true_false (b : bool) : (if b then true else false) = b.
Lemma not_empty_map {A B} (f : A → B) l : l ≠ [] → map f l ≠ [].
Lemma Z_of_pos_alt p : Z.of_nat (Pos.to_nat p) = Z.pos p.
Lemma All2_right_triv {A B} {l : list A} {l' : list B} P :
All P l' → #|l| = #|l'| → All2 (fun _ b ⇒ P b) l l'.
Lemma All_repeat {A} {n P} x :
P x → @All A P (repeat x n).
Lemma All2_map_left {A B C} (P : A → C → Type) l l' (f : B → A) :
All2 (fun x y ⇒ P (f x) y) l l' → All2 P (map f l) l'.
Lemma All2_map_right {A B C} (P : A → C → Type) l l' (f : B → C) :
All2 (fun x y ⇒ P x (f y)) l l' → All2 P l (map f l').
Lemma Forall2_Forall_right {A B} {P : A → B → Prop} {Q : B → Prop} {l l'} :
Forall2 P l l' →
(∀ x y, P x y → Q y) →
Forall Q l'.
Lemma All2_from_nth_error A B L1 L2 (P : A → B → Type) :
#|L1| = #|L2| →
(∀ n x1 x2, n < #|L1| → nth_error L1 n = Some x1
→ nth_error L2 n = Some x2
→ P x1 x2) →
All2 P L1 L2.
Lemma All2_nth_error {A B} {P : A → B → Type} {l l'} n t t' :
All2 P l l' →
nth_error l n = Some t →
nth_error l' n = Some t' →
P t t'.
Lemma All_In X (P : X → Type) (l : list X) x : All P l → In x l → squash (P x).
Lemma nth_error_skipn_add A l m n (a : A) :
nth_error l (m + n) = Some a →
nth_error (skipn m l) n = Some a.
Lemma All2_swap :
∀ A B R l l',
@All2 A B R l l' →
All2 (fun x y ⇒ R y x) l' l.
Lemma All2_firstn :
∀ A B R l l' n,
@All2 A B R l l' →
@All2 A B R (firstn n l) (firstn n l').
Lemma skipn_all_app :
∀ A (l1 l2 : list A),
skipn #|l1| (l1 ++ l2) = l2.
Lemma All2_app_inv_r :
∀ A B R l r1 r2,
@All2 A B R l (r1 ++ r2) →
∑ l1 l2,
(l = l1 ++ l2)%list ×
All2 R l1 r1 ×
All2 R l2 r2.
Lemma rev_app :
∀ A (l l' : list A),
(rev (l ++ l') = rev l' ++ rev l)%list.
Lemma rev_invol :
∀ A (l : list A),
rev (rev l) = l.
Lemma list_ind_rev :
∀ A (P : list A → Prop),
P nil →
(∀ a l, P l → P (l ++ [a])%list) →
∀ l, P l.
Lemma list_rect_rev :
∀ A (P : list A → Type),
P nil →
(∀ a l, P l → P (l ++ [a])%list) →
∀ l, P l.
Lemma last_app {A} (l l' : list A) d : l' ≠ [] → last (l ++ l') d = last l' d.
Lemma last_nonempty_eq {A} {l : list A} {d d'} : l ≠ [] → last l d = last l d'.
Lemma nth_error_removelast {A} (args : list A) n :
n < Nat.pred #|args| → nth_error args n = nth_error (removelast args) n.
Lemma nth_error_skipn {A} n (l : list A) i : nth_error (skipn n l) i = nth_error l (n + i).
Lemma skipn_skipn {A} n m (l : list A) : skipn n (skipn m l) = skipn (m + n) l.
Lemma skipn_nth_error {A} (l : list A) i :
match nth_error l i with
| Some a ⇒ skipn i l = a :: skipn (S i) l
| None ⇒ skipn i l = []
end.
Lemma nth_error_app_ge {A} (l l' : list A) (v : nat) :
length l ≤ v →
nth_error (l ++ l') v = nth_error l' (v - length l).
Lemma nth_error_app_lt {A} (l l' : list A) (v : nat) :
v < length l →
nth_error (l ++ l') v = nth_error l v.
Lemma nth_error_rev {A} (l : list A) i : i < #|l| →
nth_error l i = nth_error (List.rev l) (#|l| - S i).
Axiom todo : string → ∀ {A}, A.
Extract Constant todo ⇒ "fun s -> failwith (String.concat """" (List.map (String.make 1) s))".
Lemma All2_trans {A} (P : A → A → Type) :
CRelationClasses.Transitive P →
CRelationClasses.Transitive (All2 P).
Lemma All2_impl' {A B} {P Q : A → B → Type} {l : list A} {l' : list B}
: All2 P l l' → All (fun x ⇒ ∀ y, P x y → Q x y) l → All2 Q l l'.
Lemma All_All2 {A} {P : A → A → Type} {Q} {l : list A} :
All Q l →
(∀ x, Q x → P x x) →
All2 P l l.
Lemma All2_nth_error_Some {A B} {P : A → B → Type} {l l'} n t :
All2 P l l' →
nth_error l n = Some t →
{ t' : B & (nth_error l' n = Some t') × P t t'}%type.
Lemma All2_nth_error_Some_r {A B} {P : A → B → Type} {l l'} n t' :
All2 P l l' →
nth_error l' n = Some t' →
∑ t, nth_error l n = Some t × P t t'.
Lemma All2_nth_error_None {A B} {P : A → B → Type} {l l'} n :
All2 P l l' →
nth_error l n = None →
nth_error l' n = None.
Lemma All2_length {A B} {P : A → B → Type} l l' : All2 P l l' → #|l| = #|l'|.
Lemma All2_same {A} (P : A → A → Type) l : (∀ x, P x x) → All2 P l l.
Notation Trel_conj R S :=
(fun x y ⇒ R x y × S x y)%type.
Lemma All2_prod {A} P Q (l l' : list A) : All2 P l l' → All2 Q l l' → All2 (Trel_conj P Q) l l'.
Lemma All2_prod_inv :
∀ A (P : A → A → Type) Q l l',
All2 (Trel_conj P Q) l l' →
All2 P l l' × All2 Q l l'.
Lemma All2_sym {A} (P : A → A → Type) l l' :
All2 P l l' → All2 (fun x y ⇒ P y x) l' l.
Lemma All2_symP {A} (P : A → A → Type) :
CRelationClasses.Symmetric P →
CRelationClasses.Symmetric (All2 P).
Lemma All_All2_All2_mix {A B} (P : B → B → Type) (Q R : A → B → Type) l l' l'' :
All (fun x ⇒ ∀ y z, Q x y → R x z → ∑ v, P y v × P z v) l → All2 Q l l' → All2 R l l'' →
∑ l''', All2 P l' l''' × All2 P l'' l'''.
Lemma All_forallb_map_spec {A B : Type} {P : A → Type} {p : A → bool}
{l : list A} {f g : A → B} :
All P l → forallb p l →
(∀ x : A, P x → p x → f x = g x) → map f l = map g l.
Lemma All_forallb_forallb_spec {A : Type} {P : A → Type} {p : A → bool}
{l : list A} {f : A → bool} :
All P l → forallb p l →
(∀ x : A, P x → p x → f x) → forallb f l.
Lemma forallb_nth {A} (l : list A) (n : nat) P d :
forallb P l → n < #|l| → ∃ x, (nth n l d = x) ∧ P x.
Lemma forallb_nth' {A} {l : list A} {P} n d :
forallb P l → {∃ x, (nth n l d = x) ∧ P x} + {nth n l d = d}.
Lemma forallb_impl {A} (p q : pred A) l :
(∀ x, In x l → p x → q x) → forallb p l → forallb q l.
Lemma forallb_iff {A} (p q : pred A) l :
(∀ x, In x l → p x ↔ q x) → forallb p l = forallb q l.
Lemma map_inj :
∀ A B (f : A → B) l l',
(∀ x y, f x = f y → x = y) →
map f l = map f l' →
l = l'.
Lemma All2_eq :
∀ A (l l' : list A),
All2 eq l l' →
l = l'.
Lemma All_prod_inv :
∀ A P Q l,
All (fun x : A ⇒ P x × Q x) l →
All P l × All Q l.
Lemma All_prod :
∀ A P Q l,
All P l →
All Q l →
All (fun x : A ⇒ P x × Q x) l.
Inductive t (A : Set) :=
| sing : A → t A
| cons : A → t A → t A.
Infix "::" := cons : nel_scope.
Notation "[ x ]" := (sing x) : nel_scope.
Fixpoint length {A} (l : t A) : nat :=
match l with
| [ _ ] ⇒ 1
| _ :: l' ⇒ S (length l')
end.
Notation "[ x ; y ; .. ; z ; e ]" :=
(cons x (cons y .. (cons z (sing e)) ..)) : nel_scope.
Fixpoint to_list {A} (l : t A) : list A :=
match l with
| [x] ⇒ [x]
| x :: l ⇒ x :: (to_list l)
end.
Fixpoint map {A B : Set} (f : A → B) (l : t A) : t B :=
match l with
| [x] ⇒ [f x]
| x :: l ⇒ f x :: map f l
end.
Fixpoint app {A} (l l' : t A) : t A :=
match l with
| [x] ⇒ x :: l'
| x :: l ⇒ x :: (app l l')
end.
Infix "++" := app : nel_scope.
Fixpoint app_r {A : Set} (l : list A) (l' : t A) : t A :=
match l with
| [] ⇒ l'
| (x :: l)%list ⇒ x :: app_r l l'
end.
Fixpoint cons' {A : Set} (x : A) (l : list A) : t A :=
match l with
| [] ⇒ [x]
| (y :: l)%list ⇒ x :: cons' y l
end.
Lemma cons'_spec {A : Set} (x : A) l
: to_list (cons' x l) = (x :: l)%list.
Fixpoint fold_left {A} {B : Set} (f : A → B → A) (l : t B) (a0 : A) : A :=
match l with
| [b] ⇒ f a0 b
| b :: l ⇒ fold_left f l (f a0 b)
end.
Fixpoint forallb {A : Set} (f : A → bool) (l : t A) :=
match l with
| [x] ⇒ f x
| hd :: tl ⇒ f hd && forallb f tl
end.
Fixpoint forallb2 {A : Set} (f : A → A → bool) (l l' : t A) :=
match l, l' with
| [x], [x'] ⇒ f x x'
| hd :: tl, hd' :: tl' ⇒ f hd hd' && forallb2 f tl tl'
| _, _ ⇒ false
end.
Lemma map_to_list {A B : Set} (f : A → B) (l : t A)
: to_list (map f l) = List.map f (to_list l).
Lemma map_app {A B : Set} (f : A → B) l l' :
map f (l ++ l') = map f l ++ map f l'.
Lemma map_map {A B C : Set} (f : A → B) (g : B → C) l :
map g (map f l) = map (fun x ⇒ g (f x)) l.
Lemma map_ext {A B : Set} (f g : A → B) l :
(∀ x, f x = g x) → map f l = map g l.
End NEL.
Definition non_empty_list := NEL.t.
Lemma iff_forall {A} B C (H : ∀ x : A, B x ↔ C x)
: (∀ x, B x) ↔ (∀ x, C x).
Lemma iff_ex {A} B C (H : ∀ x : A, B x ↔ C x)
: (ex B) ↔ (ex C).
Lemma if_true_false (b : bool) : (if b then true else false) = b.
Lemma not_empty_map {A B} (f : A → B) l : l ≠ [] → map f l ≠ [].
Lemma Z_of_pos_alt p : Z.of_nat (Pos.to_nat p) = Z.pos p.
Lemma All2_right_triv {A B} {l : list A} {l' : list B} P :
All P l' → #|l| = #|l'| → All2 (fun _ b ⇒ P b) l l'.
Lemma All_repeat {A} {n P} x :
P x → @All A P (repeat x n).
Lemma All2_map_left {A B C} (P : A → C → Type) l l' (f : B → A) :
All2 (fun x y ⇒ P (f x) y) l l' → All2 P (map f l) l'.
Lemma All2_map_right {A B C} (P : A → C → Type) l l' (f : B → C) :
All2 (fun x y ⇒ P x (f y)) l l' → All2 P l (map f l').
Lemma Forall2_Forall_right {A B} {P : A → B → Prop} {Q : B → Prop} {l l'} :
Forall2 P l l' →
(∀ x y, P x y → Q y) →
Forall Q l'.
Lemma All2_from_nth_error A B L1 L2 (P : A → B → Type) :
#|L1| = #|L2| →
(∀ n x1 x2, n < #|L1| → nth_error L1 n = Some x1
→ nth_error L2 n = Some x2
→ P x1 x2) →
All2 P L1 L2.
Lemma All2_nth_error {A B} {P : A → B → Type} {l l'} n t t' :
All2 P l l' →
nth_error l n = Some t →
nth_error l' n = Some t' →
P t t'.
Lemma All_In X (P : X → Type) (l : list X) x : All P l → In x l → squash (P x).
Lemma nth_error_skipn_add A l m n (a : A) :
nth_error l (m + n) = Some a →
nth_error (skipn m l) n = Some a.
Lemma All2_swap :
∀ A B R l l',
@All2 A B R l l' →
All2 (fun x y ⇒ R y x) l' l.
Lemma All2_firstn :
∀ A B R l l' n,
@All2 A B R l l' →
@All2 A B R (firstn n l) (firstn n l').
Lemma skipn_all_app :
∀ A (l1 l2 : list A),
skipn #|l1| (l1 ++ l2) = l2.
Lemma All2_app_inv_r :
∀ A B R l r1 r2,
@All2 A B R l (r1 ++ r2) →
∑ l1 l2,
(l = l1 ++ l2)%list ×
All2 R l1 r1 ×
All2 R l2 r2.
Lemma rev_app :
∀ A (l l' : list A),
(rev (l ++ l') = rev l' ++ rev l)%list.
Lemma rev_invol :
∀ A (l : list A),
rev (rev l) = l.
Lemma list_ind_rev :
∀ A (P : list A → Prop),
P nil →
(∀ a l, P l → P (l ++ [a])%list) →
∀ l, P l.
Lemma list_rect_rev :
∀ A (P : list A → Type),
P nil →
(∀ a l, P l → P (l ++ [a])%list) →
∀ l, P l.
Lemma last_app {A} (l l' : list A) d : l' ≠ [] → last (l ++ l') d = last l' d.
Lemma last_nonempty_eq {A} {l : list A} {d d'} : l ≠ [] → last l d = last l d'.
Lemma nth_error_removelast {A} (args : list A) n :
n < Nat.pred #|args| → nth_error args n = nth_error (removelast args) n.
Lemma nth_error_skipn {A} n (l : list A) i : nth_error (skipn n l) i = nth_error l (n + i).
Lemma skipn_skipn {A} n m (l : list A) : skipn n (skipn m l) = skipn (m + n) l.
Lemma skipn_nth_error {A} (l : list A) i :
match nth_error l i with
| Some a ⇒ skipn i l = a :: skipn (S i) l
| None ⇒ skipn i l = []
end.
Lemma nth_error_app_ge {A} (l l' : list A) (v : nat) :
length l ≤ v →
nth_error (l ++ l') v = nth_error l' (v - length l).
Lemma nth_error_app_lt {A} (l l' : list A) (v : nat) :
v < length l →
nth_error (l ++ l') v = nth_error l v.
Lemma nth_error_rev {A} (l : list A) i : i < #|l| →
nth_error l i = nth_error (List.rev l) (#|l| - S i).
Axiom todo : string → ∀ {A}, A.
Extract Constant todo ⇒ "fun s -> failwith (String.concat """" (List.map (String.make 1) s))".
Lemma All2_trans {A} (P : A → A → Type) :
CRelationClasses.Transitive P →
CRelationClasses.Transitive (All2 P).
Lemma All2_impl' {A B} {P Q : A → B → Type} {l : list A} {l' : list B}
: All2 P l l' → All (fun x ⇒ ∀ y, P x y → Q x y) l → All2 Q l l'.
Lemma All_All2 {A} {P : A → A → Type} {Q} {l : list A} :
All Q l →
(∀ x, Q x → P x x) →
All2 P l l.
Lemma All2_nth_error_Some {A B} {P : A → B → Type} {l l'} n t :
All2 P l l' →
nth_error l n = Some t →
{ t' : B & (nth_error l' n = Some t') × P t t'}%type.
Lemma All2_nth_error_Some_r {A B} {P : A → B → Type} {l l'} n t' :
All2 P l l' →
nth_error l' n = Some t' →
∑ t, nth_error l n = Some t × P t t'.
Lemma All2_nth_error_None {A B} {P : A → B → Type} {l l'} n :
All2 P l l' →
nth_error l n = None →
nth_error l' n = None.
Lemma All2_length {A B} {P : A → B → Type} l l' : All2 P l l' → #|l| = #|l'|.
Lemma All2_same {A} (P : A → A → Type) l : (∀ x, P x x) → All2 P l l.
Notation Trel_conj R S :=
(fun x y ⇒ R x y × S x y)%type.
Lemma All2_prod {A} P Q (l l' : list A) : All2 P l l' → All2 Q l l' → All2 (Trel_conj P Q) l l'.
Lemma All2_prod_inv :
∀ A (P : A → A → Type) Q l l',
All2 (Trel_conj P Q) l l' →
All2 P l l' × All2 Q l l'.
Lemma All2_sym {A} (P : A → A → Type) l l' :
All2 P l l' → All2 (fun x y ⇒ P y x) l' l.
Lemma All2_symP {A} (P : A → A → Type) :
CRelationClasses.Symmetric P →
CRelationClasses.Symmetric (All2 P).
Lemma All_All2_All2_mix {A B} (P : B → B → Type) (Q R : A → B → Type) l l' l'' :
All (fun x ⇒ ∀ y z, Q x y → R x z → ∑ v, P y v × P z v) l → All2 Q l l' → All2 R l l'' →
∑ l''', All2 P l' l''' × All2 P l'' l'''.
Lemma All_forallb_map_spec {A B : Type} {P : A → Type} {p : A → bool}
{l : list A} {f g : A → B} :
All P l → forallb p l →
(∀ x : A, P x → p x → f x = g x) → map f l = map g l.
Lemma All_forallb_forallb_spec {A : Type} {P : A → Type} {p : A → bool}
{l : list A} {f : A → bool} :
All P l → forallb p l →
(∀ x : A, P x → p x → f x) → forallb f l.
Lemma forallb_nth {A} (l : list A) (n : nat) P d :
forallb P l → n < #|l| → ∃ x, (nth n l d = x) ∧ P x.
Lemma forallb_nth' {A} {l : list A} {P} n d :
forallb P l → {∃ x, (nth n l d = x) ∧ P x} + {nth n l d = d}.
Lemma forallb_impl {A} (p q : pred A) l :
(∀ x, In x l → p x → q x) → forallb p l → forallb q l.
Lemma forallb_iff {A} (p q : pred A) l :
(∀ x, In x l → p x ↔ q x) → forallb p l = forallb q l.
Lemma map_inj :
∀ A B (f : A → B) l l',
(∀ x y, f x = f y → x = y) →
map f l = map f l' →
l = l'.
Lemma All2_eq :
∀ A (l l' : list A),
All2 eq l l' →
l = l'.
Lemma All_prod_inv :
∀ A P Q l,
All (fun x : A ⇒ P x × Q x) l →
All P l × All Q l.
Lemma All_prod :
∀ A P Q l,
All P l →
All Q l →
All (fun x : A ⇒ P x × Q x) l.