Daily reminder that testing is for code monkeys.
Axiom array : Type -> Type.
Check array.
Axiom length : forall T : Type, array T -> nat.
Check length.
Arguments length {_} _.
Axiom nth :
forall (T : Type) (i : nat) (a : array T), i < length a -> T.
Check nth.
Arguments nth {_ _} _ _.
Axiom mk_array :
forall (T : Type) (n : nat), (forall i : nat, i < n -> T) -> array T.
Check mk_array.
Arguments mk_array {_ _} _.
Axiom mk_array_length :
forall (T : Type) (n : nat) (f : forall i : nat, i < n -> T),
length (mk_array f) = n.
Check mk_array_length.
Arguments mk_array_length {_ _} _.
Lemma trivial1 :
forall (T : Type) (n : nat) (i : nat)
(f : forall i : nat, i < n -> T),
i < n -> i < length (mk_array f).
(intros T n i f H1).
(assert (length (mk_array f) = n)).
(apply mk_array_length).
(rewrite H).
(apply H1).
Qed.
Check trivial1.
Arguments trivial1 {_ _ _} _ _.
Axiom mk_array_nth :
forall (T : Type) (n : nat) (f : forall i : nat, i < n -> T)
(i : nat) (Hi : i < n),
let Hmk : i < length (mk_array f) := trivial1 f Hi in
nth (mk_array f) Hmk = f i Hi.
Check mk_array_nth.
Definition duplicate : forall (T : Type), array T -> array T :=
fun T a => mk_array (fun i Hin => nth a Hin).
Check duplicate.
Arguments duplicate {_} _.
Theorem dup_has_same_length :
forall (T : Type) (a : array T), length (duplicate a) = length a.
(intros T a).
(unfold duplicate).
(apply mk_array_length).
Qed.
Check dup_has_same_length.
Arguments dup_has_same_length {_} _.
Lemma trivial2 :
forall (T : Type) (i : nat) (a : array T),
i < length a -> i < length (duplicate a).
(intros T i a H1).
(apply eq_ind with (x := length a)).
auto.
symmetry.
(apply dup_has_same_length).
Qed.
Check trivial2.
Arguments trivial2 {_ _} _ _.
Theorem dup_is_same :
forall (T : Type) (a : array T) (i : nat) (Ha : i < length a),
let Hda : i < length (duplicate a) := trivial2 a Ha in
nth a Ha = nth (duplicate a) Hda.