103 lines
3.3 KiB
Coq
103 lines
3.3 KiB
Coq
Require Import Coq.Lists.List.
|
|
Require Import Omega.
|
|
|
|
Definition has_pair (t : nat) (is : list nat) : Prop :=
|
|
exists n1 n2 : nat, n1 <> n2 /\ In n1 is /\ In n2 is /\ n1 + n2 = t.
|
|
|
|
Fixpoint find_matching (is : list nat) (total : nat) (x : nat) : option nat :=
|
|
match is with
|
|
| nil => None
|
|
| cons y ys =>
|
|
if Nat.eqb (x + y) total
|
|
then Some y
|
|
else find_matching ys total x
|
|
end.
|
|
|
|
Fixpoint find_sum (is : list nat) (total : nat) : option (nat * nat) :=
|
|
match is with
|
|
| nil => None
|
|
| cons x xs =>
|
|
match find_matching xs total x with
|
|
| None => find_sum xs total (* Was buggy! *)
|
|
| Some y => Some (x, y)
|
|
end
|
|
end.
|
|
|
|
Lemma find_matching_correct : forall is k x y,
|
|
find_matching is k x = Some y -> x + y = k.
|
|
Proof.
|
|
intros is. induction is;
|
|
intros k x y Hev.
|
|
- simpl in Hev. inversion Hev.
|
|
- simpl in Hev. destruct (Nat.eqb (x+a) k) eqn:Heq.
|
|
+ injection Hev as H; subst.
|
|
apply EqNat.beq_nat_eq. auto.
|
|
+ apply IHis. assumption.
|
|
Qed.
|
|
|
|
Lemma find_matching_skip : forall k x y i is,
|
|
find_matching is k x = Some y -> find_matching (cons i is) k x = Some y.
|
|
Proof.
|
|
intros k x y i is Hsmall.
|
|
simpl. destruct (Nat.eqb (x+i) k) eqn:Heq.
|
|
- apply find_matching_correct in Hsmall.
|
|
symmetry in Heq. apply EqNat.beq_nat_eq in Heq.
|
|
assert (i = y). { omega. } rewrite H. reflexivity.
|
|
- assumption.
|
|
Qed.
|
|
|
|
Lemma find_matching_works : forall is k x y, In y is /\ x + y = k ->
|
|
find_matching is k x = Some y.
|
|
Proof.
|
|
intros is. induction is;
|
|
intros k x y [Hin Heq].
|
|
- inversion Hin.
|
|
- inversion Hin.
|
|
+ subst a. simpl. Search Nat.eqb.
|
|
destruct (Nat.eqb_spec (x+y) k).
|
|
* reflexivity.
|
|
* exfalso. apply n. assumption.
|
|
+ apply find_matching_skip. apply IHis.
|
|
split; assumption.
|
|
Qed.
|
|
|
|
Theorem find_sum_works :
|
|
forall k is, has_pair k is ->
|
|
exists x y, (find_sum is k = Some (x, y) /\ x + y = k).
|
|
Proof.
|
|
intros k is. generalize dependent k.
|
|
induction is; intros k [x' [y' [Hneq [Hinx [Hiny Hsum]]]]].
|
|
- (* is is empty. But x is in is! *)
|
|
inversion Hinx.
|
|
- (* is is not empty. *)
|
|
inversion Hinx.
|
|
+ (* x is the first element. *)
|
|
subst a. inversion Hiny.
|
|
* (* y is also the first element; but this is impossible! *)
|
|
exfalso. apply Hneq. apply H.
|
|
* (* y is somewhere in the rest of the list.
|
|
We've proven that we will find it! *)
|
|
exists x'. simpl.
|
|
erewrite find_matching_works.
|
|
{ exists y'. split. reflexivity. assumption. }
|
|
{ split; assumption. }
|
|
+ (* x is not the first element. *)
|
|
inversion Hiny.
|
|
* (* y is the first element,
|
|
so x is somewhere in the rest of the list.
|
|
Again, we've proven that we can find it. *)
|
|
subst a. exists y'. simpl.
|
|
erewrite find_matching_works.
|
|
{ exists x'. split. reflexivity. rewrite plus_comm. assumption. }
|
|
{ split. assumption. rewrite plus_comm. assumption. }
|
|
* (* y is not the first element, either.
|
|
Of course, there could be another matching pair
|
|
starting with a. Otherwise, the inductive hypothesis applies. *)
|
|
simpl. destruct (find_matching is k a) eqn:Hf.
|
|
{ exists a. exists n. split.
|
|
reflexivity.
|
|
apply find_matching_correct with is. assumption. }
|
|
{ apply IHis. unfold has_pair. exists x'. exists y'.
|
|
repeat split; assumption. }
|
|
Qed.
|