Require Import Measures. Require Import Recdef. Require Import List. Require Import Zwf. Let measures := (@fst nat nat) :: (@snd nat nat) :: nil. Function pairs_aux (p:nat*nat) {wf (measures_lt measures) p} :list (nat*nat):= match p with (0,_) => nil |(S i, S j) => (S i,S j)::pairs_aux (S i,j) | (S i, 0) => pairs_aux (i, i) end. constructor;auto. simpl;auto with arith. apply measures_lt_wf. Defined. Definition pairs (i:nat) := pairs_aux (i,i). Extraction "lex.ml" pairs. (* BUG coq Function pairs_aux' (p:nat*nat){wf (measures (nat*nat) ((fun p:nat*nat => fst p)::(fun p:nat*nat => snd p)::(@nil (nat*nat -> nat)))) p} :list (nat*nat):= match p with (0,_) => nil |(S i, S j) => (S i,S j)::pairs_aux' (S i,j) | (S i, 0) => pairs_aux' (i, i) end. constructor;auto. simpl. simpl;auto with arith. apply measures_lt_wf. Defined. *) (* Alternate take, without measures *) Function pairs_aux2 (p:nat*nat){wf (lex lt lt) p} :list (nat*nat):= match p with (0,_) => nil |(S i, S j) => (S i,S j)::pairs_aux2 (S i,j) | (S i, 0) => pairs_aux2 (i, i) end. constructor;auto. constructor 2;auto. apply lex_wf;apply lt_wf. Defined. (* properties of pairs *) Require Import Omega. Require Import ArithRing. Lemma pairs_length : forall n, 2 * length (pairs n) = n * S n. Proof. intro n;unfold pairs . assert (H:forall p, snd p <= fst p -> 2*length(pairs_aux p) = pred (fst p) * (fst p) + 2*snd p). (* Proof of H *) intro p;functional induction (pairs_aux p);simpl;auto. inversion 1;auto. simpl in *; intro H; assert (H0:j <= S i) by omega. apply IHl in H0; omega. simpl in *; generalize (IHl (le_n i)); intros H H0 ;clear IHl. rewrite H;destruct i;simpl;auto;ring. (* Instantiation of H *) rewrite H;simpl;destruct n;simpl;auto. ring. Qed. (* We want to prove that (pairs n) contains all pairs (i,j) where 1<=j<=i<=n Since the recursive function is pairs_aux we have to prove by induction some stronger property : pairs_aux (i,j) contains all the pairs (k,l) where 1<=l<=k and (k,l) is lexicographically less or equal than (i,j) *) (* let's first introduce this notion and a simple inversion property *) Definition lex_eq p q := lex lt lt p q \/ p = q. Lemma lex_nat_inv : forall q i j, lex lt lt q (i, S j) -> lex lt lt q (i, j) \/ q =(i,j). Proof. destruct q; inversion 1. left;left;simpl;auto. assert (H5:n0 < j \/ n0 = j) by omega. destruct H5. left;constructor 2;auto. subst n0;auto. Qed. Lemma pairs_aux_complete : forall p, snd p <= fst p -> forall q, snd q <= fst q -> lex_eq q p -> 0 < snd q -> In q (pairs_aux p). Proof. intro p;functional induction (pairs_aux p); simpl. inversion 1; destruct q; simpl. inversion 2. inversion H3. omega. omega. injection H3; omega. simpl in *;intros H q H0 H1 H2. destruct H1. destruct (lex_nat_inv _ _ _ H1). right;apply IHl;auto. omega. left;auto. right;apply IHl. omega. auto. right. auto. auto. left;symmetry;auto. intros H q H0 H1 H2. apply IHl;auto. destruct H1. destruct q. simpl in *. inversion H1. assert (H8:n = i \/ n < i) by omega. destruct H8. rewrite H8 in *. assert (H9:n0 < i \/ n0 = i) by omega. destruct H9. left; right;auto. subst n0;right;auto. left. constructor 1. simpl;auto. inversion H4. subst q;simpl in H2;inversion H2. Qed. Lemma pairs_complete : forall i j , 0 < j -> j <= i -> In (i,j) (pairs i). Proof. intros;unfold pairs. apply pairs_aux_complete;simpl;auto. case (le_lt_or_eq _ _ H0). left;constructor 2; simpl;auto. intro;subst j;right; auto. Qed.