proposition: Lemma codeListRemoveCorrect (a : nat) (l : list nat): codeListRemove a (codeList l) = codeList (List.remove eq_nat_dec a l).
proof: Proof. unfold codeListRemove; set (f := fun n Hrecs p1 : nat => switchPR n (switchPR (charFunction 2 Nat.eqb (cPairPi1 (pred n)) p1) (codeNth (n - S (cPairPi2 (pred n))) Hrecs) (S (cPair (cPairPi1 (pred n)) (codeNth (n - S (cPairPi2 (pred n))) Hrecs)))) (codeList nil)) in *. induction l as [| a0 l Hrecl]. - simpl; unfold evalStrongRec; simpl; reflexivity. - unfold evalStrongRec, evalComposeFunc, evalOneParamList. rewrite computeEvalStrongRecHelp. unfold f at 2 in |- *. unfold compose2 in |- *. set (n := codeList (a0 :: l)). set (A := n - S (cPairPi2 (pred n))). simpl; repeat rewrite cPairProjections1 || rewrite cPairProjections2. assert (H: extEqual 1 (evalComposeFunc 1 1 (Vector.cons _ (evalStrongRecHelp 1 f n) 0 (Vector.nil _)) (fun b : nat => codeNth (n - S (cPairPi2 (pred n))) b)) (evalStrongRec 1 f (cPairPi2 (pred n)))). { apply (evalStrongRecHelp2 1); simpl; unfold n. rewrite cPairProjections2. simpl; apply Compat815.le_lt_n_Sm. apply cPairLe2. } simpl in H. induction (Nat.eq_dec a0 a) as [a1 | b]. + rewrite a1, Nat.eqb_refl; simpl; unfold A. rewrite H; rewrite cPairProjections2; auto. destruct (Nat.eq_dec a a). * auto. * congruence. + rewrite nat_eqb_false; simpl. replace (codeList (List.remove eq_nat_dec a l)) with (codeNth A (evalStrongRecHelp 1 f n a)). * destruct (Nat.eq_dec a a0). -- congruence. -- simpl. f_equal. f_equal. rewrite <- Hrecl. rewrite cPairProjections2 in H. rewrite <- H. unfold A. simpl. now rewrite cPairProjections2. * unfold A; rewrite H; simpl; rewrite cPairProjections2; auto. * auto. Qed.
imports: hydras.Ackermann(primRec cPair) hydras.Ackermann(ListExt) Coq(Arith) hydras(extEqualNat Compat815)