Set Implicit Arguments.Require Import Lia.Require Import Vericertlib.From Coq Require Import Lists.List Datatypes.Import ListNotations.Local Open Scope nat_scope.RecordArray (A : Type) : Type :=
mk_array
{ arr_contents : list A
; arr_length : nat
; arr_wf : length arr_contents = arr_length
}.Definitionmake_array {A : Type} (l : list A) : Array A :=
@mk_array A l (length l) eq_refl.Fixpointlist_set {A : Type} (i : nat) (x : A) (l : list A) {structl} : list A :=
match i, l with
| _, nil => nil
| S n, h :: t => h :: list_set n x t
| O, h :: t => x :: t
end.
A:Type
forall (l : list A) (i : nat) (x : A),
i < length l -> nth_error (list_set i x l) i = Some x
A:Type
forall (l : list A) (i : nat) (x : A),
i < length l -> nth_error (list_set i x l) i = Some x
A:Type
a:A
l:list A
IHl:forall (i : nat) (x : A),
i < length l -> nth_error (list_set i x l) i = Some x
forall (l : list A) (lni : nat) (x : A),
length l = ln -> length (list_set i x l) = ln
A:Type
forall (l : list A) (lni : nat) (x : A),
length l = ln -> length (list_set i x l) = ln
A:Type
a:A
l:list A
IHl:forall (lni : nat) (x : A), length l = ln -> length (list_set i x l) = ln
ln, i:nat
x:A
H:length (a :: l) = ln
length (list_set (S i) x (a :: l)) = ln
invert H; crush; auto.Qed.Definitionarray_set {A : Type} (i : nat) (x : A) (a : Array A) :=
letl := a.(arr_contents) inletln := a.(arr_length) inletWF := a.(arr_wf) in
@mk_array A (list_set i x l) ln (@array_set_wf A l ln i x WF).
A:Type
forall (a : Array A) (i : nat) (x : A),
i < arr_length a ->
nth_error (arr_contents (array_set i x a)) i = Some x
A:Type
forall (a : Array A) (i : nat) (x : A),
i < arr_length a ->
nth_error (arr_contents (array_set i x a)) i = Some x
A:Type
a:Array A
i:nat
x:A
H:i < arr_length a
nth_error (arr_contents (array_set i x a)) i = Some x
A:Type
a:Array A
i:nat
x:A
H:i < length (arr_contents a)
nth_error (arr_contents (array_set i x a)) i = Some x
A:Type
a:Array A
i:nat
x:A
H:i < length (arr_contents a)
nth_error
(arr_contents
{|
arr_contents := list_set i x (arr_contents a);
arr_length := arr_length a;
arr_wf := array_set_wf (arr_contents a) i x
(arr_wf a) |}) i = Some x
A:Type
a:Array A
i:nat
x:A
H:i < length (arr_contents a)
nth_error (list_set i x (arr_contents a)) i = Some x
eauto with array.Qed.Hint Resolve array_set_spec1 : array.
A:Type
forall (a : Array A) (i : nat) (xd : A),
i < arr_length a ->
nth i (arr_contents (array_set i x a)) d = x
A:Type
forall (a : Array A) (i : nat) (xd : A),
i < arr_length a ->
nth i (arr_contents (array_set i x a)) d = x
A:Type
a:Array A
i:nat
x, d:A
H:i < arr_length a
nth i (arr_contents (array_set i x a)) d = x
A:Type
a:Array A
i:nat
x, d:A
H:i < length (arr_contents a)
nth i (arr_contents (array_set i x a)) d = x
A:Type
a:Array A
i:nat
x, d:A
H:i < length (arr_contents a)
nth i
(arr_contents
{|
arr_contents := list_set i x (arr_contents a);
arr_length := arr_length a;
arr_wf := array_set_wf (arr_contents a) i x
(arr_wf a) |}) d = x
A:Type
a:Array A
i:nat
x, d:A
H:i < length (arr_contents a)
nth i (list_set i x (arr_contents a)) d = x
eauto with array.Qed.Hint Resolve array_set_spec2 : array.
A:Type
forall (a : Array A) (i : nat) (x : A),
arr_length a = arr_length (array_set i x a)
A:Type
forall (a : Array A) (i : nat) (x : A),
arr_length a = arr_length (array_set i x a)
A:Type
forall (a : Array A) (i : nat) (x : A),
arr_length a =
arr_length
{|
arr_contents := list_set i x (arr_contents a);
arr_length := arr_length a;
arr_wf := array_set_wf (arr_contents a) i x
(arr_wf a) |}
crush.Qed.Definitionarray_get_error {A : Type} (i : nat) (a : Array A) : option A :=
nth_error a.(arr_contents) i.
A:Type
forall (ab : Array A) (i : nat),
arr_contents a = arr_contents b ->
array_get_error i a = array_get_error i b
A:Type
forall (ab : Array A) (i : nat),
arr_contents a = arr_contents b ->
array_get_error i a = array_get_error i b
A:Type
forall (ab : Array A) (i : nat),
arr_contents a = arr_contents b ->
nth_error (arr_contents a) i =
nth_error (arr_contents b) i
crush.Qed.
A:Type
forall (a : Array A) (i : nat),
i < arr_length a ->
existsx : A, array_get_error i a = Some x
A:Type
forall (a : Array A) (i : nat),
i < arr_length a ->
existsx : A, array_get_error i a = Some x
A:Type
a:Array A
i:nat
H:i < arr_length a
existsx : A, array_get_error i a = Some x
A:Type
a:Array A
i:nat
H:i < length (arr_contents a)
existsx : A, array_get_error i a = Some x
A:Type
a:Array A
i:nat
H:i < length (arr_contents a)
H0:~ length (arr_contents a) <= i
existsx : A, array_get_error i a = Some x
A:Type
a:Array A
i:nat
H:i < length (arr_contents a)
H0:~ length (arr_contents a) <= i
H1:nth_error (arr_contents a) i = None <->
length (arr_contents a) <= i
existsx : A, array_get_error i a = Some x
A:Type
a:Array A
i:nat
H:i < length (arr_contents a)
H0:~ length (arr_contents a) <= i
H1:nth_error (arr_contents a) i <> None <->
~ length (arr_contents a) <= i
existsx : A, array_get_error i a = Some x
A:Type
a:Array A
i:nat
H:i < length (arr_contents a)
H0:nth_error (arr_contents a) i <> None
H1:nth_error (arr_contents a) i <> None <->
~ length (arr_contents a) <= i
existsx : A, array_get_error i a = Some x
destruct (nth_error (arr_contents a) i) eqn:EQ; trycontradiction; eauto.Qed.
A:Type
forall (a : Array A) (i : nat) (x : A),
i < arr_length a ->
array_get_error i (array_set i x a) = Some x
A:Type
forall (a : Array A) (i : nat) (x : A),
i < arr_length a ->
array_get_error i (array_set i x a) = Some x
A:Type
a:Array A
i:nat
x:A
H:i < arr_length a
array_get_error i (array_set i x a) = Some x
A:Type
a:Array A
i:nat
x:A
H:i < arr_length a
nth_error (arr_contents (array_set i x a)) i = Some x
eauto with array.Qed.
A:Type
forall (a : Array A) (i1i2 : nat) (x : A),
i1 <> i2 ->
array_get_error i2 (array_set i1 x a) =
array_get_error i2 a
A:Type
forall (a : Array A) (i1i2 : nat) (x : A),
i1 <> i2 ->
array_get_error i2 (array_set i1 x a) =
array_get_error i2 a
A:Type
a:Array A
i1, i2:nat
x:A
H:i1 <> i2
array_get_error i2 (array_set i1 x a) =
array_get_error i2 a
A:Type
a:Array A
i1, i2:nat
x:A
H:i1 <> i2
nth_error (arr_contents (array_set i1 x a)) i2 =
nth_error (arr_contents a) i2
A:Type
a:Array A
i1, i2:nat
x:A
H:i1 <> i2
nth_error
(arr_contents
{|
arr_contents := list_set i1 x (arr_contents a);
arr_length := arr_length a;
arr_wf := array_set_wf (arr_contents a) i1 x
(arr_wf a) |}) i2 =
nth_error (arr_contents a) i2
A:Type
a:Array A
i1, i2:nat
x:A
H:i1 <> i2
nth_error (list_set i1 x (arr_contents a)) i2 =
nth_error (arr_contents a) i2
eauto with array.Qed.Definitionarray_get {A : Type} (i : nat) (x : A) (a : Array A) : A :=
nth i a.(arr_contents) x.
A:Type
forall (a : Array A) (i : nat) (xd : A),
i < arr_length a ->
array_get i d (array_set i x a) = x
A:Type
forall (a : Array A) (i : nat) (xd : A),
i < arr_length a ->
array_get i d (array_set i x a) = x
A:Type
a:Array A
i:nat
x, d:A
H:i < arr_length a
array_get i d (array_set i x a) = x
A:Type
a:Array A
i:nat
x, d:A
H:i < arr_length a
nth i (arr_contents (array_set i x a)) d = x
eauto with array.Qed.
A:Type
forall (a : Array A) (i : nat) (xd : A),
array_get_error i a = Some x -> array_get i d a = x
A:Type
forall (a : Array A) (i : nat) (xd : A),
array_get_error i a = Some x -> array_get i d a = x
A:Type
a:Array A
i:nat
x, d:A
H:array_get_error i a = Some x
array_get i d a = x
A:Type
a:Array A
i:nat
x, d:A
H:array_get_error i a = Some x
nth i (arr_contents a) d = x
A:Type
a:Array A
i:nat
x, d:A
H:nth_error (arr_contents a) i = Some x
nth i (arr_contents a) d = x
auto using nth_error_nth.Qed.(** Tail recursive version of standard library function. *)Fixpointlist_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A :=
match n with
| O => acc
| S n => list_repeat' (a::acc) a n
end.
A:Type
forall (a : A) (n : nat) (l : list A),
length (list_repeat' l a n) = n + length l
A:Type
forall (a : A) (n : nat) (l : list A),
length (list_repeat' l a n) = n + length l
A:Type
a:A
n:nat
IHn:foralll : list A, length (list_repeat' l a n) = n + length l
l:list A
length (list_repeat' (a :: l) a n) = S (n + length l)
A:Type
a:A
n:nat
l:list A
IHn:length (list_repeat' (a :: l) a n) = n + length (a :: l)
length (list_repeat' (a :: l) a n) = S (n + length l)
A:Type
a:A
n:nat
l:list A
IHn:length (list_repeat' (a :: l) a n) = n + length (a :: l)
n + length (a :: l) = S (n + length l)
crush.Qed.
A:Type
forall (a : A) (n : nat) (l : list A),
list_repeat' l a n = list_repeat' [] a n ++ l
A:Type
forall (a : A) (n : nat) (l : list A),
list_repeat' l a n = list_repeat' [] a n ++ l
A:Type
a:A
n:nat
IHn:foralll : list A, list_repeat' l a n = list_repeat' [] a n ++ l
l:list A
list_repeat' (a :: l) a n = list_repeat' [a] a n ++ l
A:Type
a:A
n:nat
IHn:foralll : list A, list_repeat' l a n = list_repeat' [] a n ++ l
l:list A
H:foralll : list A,
list_repeat' l a n = list_repeat' [] a n ++ l
list_repeat' (a :: l) a n = list_repeat' [a] a n ++ l
A:Type
a:A
n:nat
IHn:foralll : list A, list_repeat' l a n = list_repeat' [] a n ++ l
l:list A
H:list_repeat' (a :: l) a n =
list_repeat' [] a n ++ a :: l
list_repeat' (a :: l) a n = list_repeat' [a] a n ++ l
A:Type
a:A
n:nat
IHn:foralll : list A, list_repeat' l a n = list_repeat' [] a n ++ l
l:list A
H:list_repeat' (a :: l) a n =
list_repeat' [] a n ++ a :: l
list_repeat' [] a n ++ a :: l =
list_repeat' [a] a n ++ l
A:Type
a:A
n:nat
IHn:foralll : list A, list_repeat' l a n = list_repeat' [] a n ++ l
l:list A
list_repeat' [] a n ++ a :: l =
list_repeat' [a] a n ++ l
A:Type
a:A
n:nat
IHn:list_repeat' [a] a n = list_repeat' [] a n ++ [a]
l:list A
list_repeat' [] a n ++ a :: l =
list_repeat' [a] a n ++ l
A:Type
a:A
n:nat
IHn:list_repeat' [a] a n = list_repeat' [] a n ++ [a]
l:list A
list_repeat' [] a n ++ a :: l =
(list_repeat' [] a n ++ [a]) ++ l
A:Type
a:A
n:nat
l:list A
list_repeat' [] a n ++ a :: l =
(list_repeat' [] a n ++ [a]) ++ l
A:Type
a:A
n:nat
l, l0:list A
Heql0:l0 = list_repeat' [] a n
l0 ++ a :: l = (l0 ++ [a]) ++ l
A:Type
a:A
n:nat
l, l0:list A
Heql0:l0 = list_repeat' [] a n
l0 ++ a :: l = l0 ++ [a] ++ l
f_equal.Qed.
A:Type
forall (n : nat) (a : A),
a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
A:Type
forall (n : nat) (a : A),
a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
A:Type
n:nat
IHn:foralla : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
a :: list_repeat' [a] a n =
list_repeat' [a] a n ++ [a]
A:Type
n:nat
IHn:foralla : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
a :: list_repeat' [] a n ++ [a] =
(list_repeat' [] a n ++ [a]) ++ [a]
A:Type
n:nat
IHn:foralla : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
list_repeat' [] a n ++ [a] ++ [a] =
(list_repeat' [] a n ++ [a]) ++ [a]
A:Type
n:nat
IHn:foralla : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
list_repeat' [] a n ++ [a] ++ [a] =
a :: list_repeat' [] a n ++ [a]
A:Type
n:nat
IHn:foralla : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
list_repeat' [] a n ++ [a] ++ [a] =
a :: list_repeat' [] a n ++ [a]
A:Type
n:nat
IHn:foralla : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
list_repeat' [] a n ++ [a] ++ [a] =
(a :: list_repeat' [] a n) ++ [a]
A:Type
n:nat
IHn:foralla : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
list_repeat' [] a n ++ [a] ++ [a] =
(list_repeat' [] a n ++ [a]) ++ [a]
A:Type
n:nat
IHn:foralla : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
(list_repeat' [] a n ++ [a]) ++ [a] =
(list_repeat' [] a n ++ [a]) ++ [a]
reflexivity.
A:Type
n:nat
IHn:foralla : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
list_repeat' [] a n ++ [a] ++ [a] =
(list_repeat' [] a n ++ [a]) ++ [a]
A:Type
n:nat
IHn:foralla : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
a:A
(list_repeat' [] a n ++ [a]) ++ [a] =
(list_repeat' [] a n ++ [a]) ++ [a]
reflexivity.Qed.
A:Type
forall (a : A) (n : nat),
list_repeat' [a] a n = a :: list_repeat' [] a n
A:Type
forall (a : A) (n : nat),
list_repeat' [a] a n = a :: list_repeat' [] a n
A:Type
a:A
n:nat
list_repeat' [a] a n = a :: list_repeat' [] a n
A:Type
a:A
n:nat
list_repeat' [a] a n = list_repeat' [] a n ++ [a]
apply list_repeat'_app.Qed.Definitionlist_repeat {A : Type} : A -> nat -> list A := list_repeat' nil.
A:Type
forall (n : nat) (a : A), length (list_repeat a n) = n
A:Type
forall (n : nat) (a : A), length (list_repeat a n) = n
A:Type
n:nat
a:A
length (list_repeat a n) = n
A:Type
n:nat
a:A
length (list_repeat' [] a n) = n
A:Type
n:nat
a:A
n + length [] = n
crush.Qed.
A:Type
forall (n : nat) (aa' : A),
(forallxx' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat a n) -> a' = a
A:Type
forall (n : nat) (aa' : A),
(forallxx' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat a n) -> a' = a
A:Type
n:nat
IHn:forallaa' : A,
(forallxx' : A, {x' = x} + {x' <> x}) -> In a' (list_repeat a n) -> a' = a
a, a':A
X:forallxx' : A, {x' = x} + {x' <> x}
H:In a' (list_repeat a (S n))
a' = a
A:Type
n:nat
IHn:forallaa' : A,
(forallxx' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forallxx' : A, {x' = x} + {x' <> x}
H:In a' (list_repeat' [] a (S n))
a' = a
A:Type
n:nat
IHn:forallaa' : A,
(forallxx' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forallxx' : A, {x' = x} + {x' <> x}
H:In a' (list_repeat' [a] a n)
a' = a
A:Type
n:nat
IHn:forallaa' : A,
(forallxx' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forallxx' : A, {x' = x} + {x' <> x}
H:In a' (list_repeat' [] a n ++ [a])
a' = a
A:Type
n:nat
IHn:forallaa' : A,
(forallxx' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forallxx' : A, {x' = x} + {x' <> x}
H:In a' (list_repeat' [] a n ++ [a])
H0:{a' = a} + {a' <> a}
a' = a
A:Type
n:nat
IHn:forallaa' : A,
(forallxx' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forallxx' : A, {x' = x} + {x' <> x}
H:In a' (list_repeat' [] a n ++ [a])
n0:a' <> a
a' = a
(* This is actually a degenerate case, not an unprovable goal. *)
A:Type
n:nat
IHn:forallaa' : A,
(forallxx' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forallxx' : A, {x' = x} + {x' <> x}
H:In a' (list_repeat' [] a n ++ [a])
n0:a' <> a
H0:foralla0 : A,
In a0 (list_repeat' [] a n ++ [a]) ->
In a0 (list_repeat' [] a n) \/ In a0 [a]
a' = a
A:Type
n:nat
IHn:forallaa' : A,
(forallxx' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forallxx' : A, {x' = x} + {x' <> x}
H:In a' (list_repeat' [] a n) \/ In a' [a]
n0:a' <> a
H0:foralla0 : A,
In a0 (list_repeat' [] a n ++ [a]) ->
In a0 (list_repeat' [] a n) \/ In a0 [a]
a' = a
A:Type
n:nat
IHn:forallaa' : A,
(forallxx' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forallxx' : A, {x' = x} + {x' <> x}
n0:a' <> a
H0:foralla0 : A,
In a0 (list_repeat' [] a n ++ [a]) ->
In a0 (list_repeat' [] a n) \/ In a0 [a]
H1:In a' (list_repeat' [] a n)
a' = a
A:Type
n:nat
IHn:forallaa' : A,
(forallxx' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forallxx' : A, {x' = x} + {x' <> x}
n0:a' <> a
H0:foralla0 : A,
In a0 (list_repeat' [] a n ++ [a]) ->
In a0 (list_repeat' [] a n) \/ In a0 [a]
H1:In a' [a]
a' = a
A:Type
n:nat
IHn:forallaa' : A,
(forallxx' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forallxx' : A, {x' = x} + {x' <> x}
n0:a' <> a
H0:foralla0 : A,
In a0 (list_repeat' [] a n ++ [a]) ->
In a0 (list_repeat' [] a n) \/ In a0 [a]
H1:In a' (list_repeat' [] a n)
a' = a
eapply IHn in X; eassumption.
A:Type
n:nat
IHn:forallaa' : A,
(forallxx' : A, {x' = x} + {x' <> x}) ->
In a' (list_repeat' [] a n) -> a' = a
a, a':A
X:forallxx' : A, {x' = x} + {x' <> x}
n0:a' <> a
H0:foralla0 : A,
In a0 (list_repeat' [] a n ++ [a]) ->
In a0 (list_repeat' [] a n) \/ In a0 [a]
H1:In a' [a]
a' = a
invert H1; contradiction.Qed.
A:Type
forall (n : nat) (a : A),
a :: list_repeat a n = list_repeat a n ++ [a]
A:Type
forall (n : nat) (a : A),
a :: list_repeat a n = list_repeat a n ++ [a]
A:Type
forall (n : nat) (a : A),
a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]
apply list_repeat'_head_tail.Qed.
A:Type
forall (n : nat) (a : A),
list_repeat a (S n) = a :: list_repeat a n
A:Type
forall (n : nat) (a : A),
list_repeat a (S n) = a :: list_repeat a n
A:Type
n:nat
a:A
list_repeat a (S n) = a :: list_repeat a n
A:Type
n:nat
a:A
list_repeat' [] a (S n) = a :: list_repeat' [] a n
apply list_repeat'_cons.Qed.
A:Type
forall (ni : nat) (a : A),
i < n -> nth_error (list_repeat a n) i = Some a
A:Type
forall (ni : nat) (a : A),
i < n -> nth_error (list_repeat a n) i = Some a
A:Type
i:nat
a:A
H:i < 0
nth_error (list_repeat a 0) i = Some a
A:Type
n:nat
IHn:forall (i : nat) (a : A), i < n -> nth_error (list_repeat a n) i = Some a
i:nat
a:A
H:i < S n
nth_error (list_repeat a (S n)) i = Some a
A:Type
n:nat
IHn:forall (i : nat) (a : A), i < n -> nth_error (list_repeat a n) i = Some a
i:nat
a:A
H:i < S n
nth_error (list_repeat a (S n)) i = Some a
A:Type
n:nat
IHn:forall (i : nat) (a : A), i < n -> nth_error (list_repeat a n) i = Some a
i:nat
a:A
H:i < S n
nth_error (a :: list_repeat a n) i = Some a
A:Type
n:nat
IHn:forall (i : nat) (a : A), i < n -> nth_error (list_repeat a n) i = Some a
i:nat
a:A
H:S i < S n
nth_error (list_repeat a n) i = Some a
intuition.Qed.Definitionarr_repeat {A : Type} (a : A) (n : nat) : Array A := make_array (list_repeat a n).
A:Type
forall (n : nat) (a : A),
arr_length (arr_repeat a n) = n
A:Type
forall (n : nat) (a : A),
arr_length (arr_repeat a n) = n
A:Type
forall (n : nat) (a : A),
arr_length (arr_repeat a n) = n
A:Type
n:nat
a:A
length (list_repeat a n) = n
apply list_repeat_len.Qed.Fixpointlist_combine {ABC : Type} (f : A -> B -> C) (x : list A) (y : list B) : list C :=
match x, y with
| a :: t, b :: t' => f a b :: list_combine f t t'
| _, _ => nil
end.
A, B, C:Type
f:A -> B -> C
forall (x : list A) (y : list B),
length (list_combine f x y) =
Init.Nat.min (length x) (length y)
A, B, C:Type
f:A -> B -> C
forall (x : list A) (y : list B),
length (list_combine f x y) =
Init.Nat.min (length x) (length y)
A, B, C:Type
f:A -> B -> C
a:A
x:list A
IHx:forally : list B,
length (list_combine f x y) = Init.Nat.min (length x) (length y)
y:list B
length
match y with
| [] => []
| b :: t' => f a b :: list_combine f x t'
end =
match length y with
| 0 => 0
| S m' => S (Init.Nat.min (length x) m')
end
destruct y; crush; auto.Qed.Definitioncombine {ABC : Type} (f : A -> B -> C) (x : Array A) (y : Array B) : Array C :=
make_array (list_combine f x.(arr_contents) y.(arr_contents)).
A, B, C:Type
forall (x : Array A) (y : Array B) (f : A -> B -> C),
arr_length x = arr_length y ->
arr_length (combine f x y) = arr_length x
A, B, C:Type
forall (x : Array A) (y : Array B) (f : A -> B -> C),
arr_length x = arr_length y ->
arr_length (combine f x y) = arr_length x
A, B, C:Type
x:Array A
y:Array B
f:A -> B -> C
H:arr_length x = arr_length y
arr_length (combine f x y) = arr_length x
A, B, C:Type
x:Array A
y:Array B
f:A -> B -> C
H:arr_length x = arr_length y
arr_length
(make_array
(list_combine f (arr_contents x) (arr_contents y))) =
arr_length x
A, B, C:Type
x:Array A
y:Array B
f:A -> B -> C
H:arr_length x = arr_length y
arr_length
{|
arr_contents := list_combine f (arr_contents x)
(arr_contents y);
arr_length := length
(list_combine f (arr_contents x)
(arr_contents y));
arr_wf := eq_refl |} = arr_length x
A, B, C:Type
x:Array A
y:Array B
f:A -> B -> C
H:arr_length x = arr_length y
length
(list_combine f (arr_contents x) (arr_contents y)) =
arr_length x