proposition: Lemma codeNthCorrect : forall (n : nat) (l : list nat), codeNth n (codeList l) = nth n l 0.
proof: Proof. unfold codeNth in |- *. set (A := fun l : list nat => match l with | nil => nil (A:=nat) | _ :: l0 => l0 end) in *. assert (H: forall l : list nat, cPairPi2 (pred (codeList l)) = codeList (A l)). { destruct l; simpl in |- *. apply (cPairProjections2 0 0). apply cPairProjections2. } assert (H0: forall (n : nat) (l : list nat), nat_rec (fun _ : nat => nat) (codeList l) (fun _ Hrecn : nat => cPairPi2 (pred Hrecn)) n = codeList (drop n l)). { simple induction n; simpl in |- *. reflexivity. intros n0 H0 l; rewrite H0, H. unfold A in |- *; clear H0; revert l. induction n0 as [| n0 Hrecn0]; simpl in |- *; intros. - reflexivity. - destruct l. + apply (Hrecn0 nil). + apply Hrecn0. } intros n l. replace (nth n l 0) with match drop n l with | nil => 0 | a :: _ => a end. rewrite H0; destruct (drop n l). + simpl in |- *; apply (cPairProjections1 0 0). + simpl in |- *; apply cPairProjections1. + revert l; induction n as [| n Hrecn]. * destruct l; reflexivity. * destruct l. -- simpl in Hrecn; destruct n; apply (Hrecn nil). -- simpl in |- *; auto. Qed.
imports: Coq(Arith Lists.List Lia) hydras(extEqualNat primRec) Extraction