proposition: Lemma codeFreeVarFormulaCorrect (f : Formula) : codeFreeVarFormula (codeFormula f) = codeList (freeVarF f).
proof: Proof. set (g := fun f recs : nat => switchPR (car f) (switchPR (pred (car f)) (switchPR (pred (pred (car f))) (switchPR (pred (pred (pred (car f)))) (codeFreeVarTerms (cdr f)) (codeListRemove (car (cdr f)) (codeNth (f - S (cdr (cdr f))) recs))) (codeNth (f - S (cdr f)) recs)) (codeApp (codeNth (f - S (car (cdr f))) recs) (codeNth (f - S (cdr (cdr f))) recs))) (codeApp (codeFreeVarTerm (car (cdr f))) (codeFreeVarTerm (cdr (cdr f))))) in *. induction f as [t t0| r t| f1 Hrecf1 f0 Hrecf0| f Hrecf| n f Hrecf]. - simpl; rewrite <- codeAppCorrect; repeat rewrite <- codeFreeVarTermCorrect. generalize (codeTerm t) (codeTerm t0). clear t t0; intros n n0. unfold codeFreeVarFormula, evalStrongRec; simpl. repeat rewrite cPairProjections1 || rewrite cPairProjections2. simpl; reflexivity. - simpl; rewrite <- codeFreeVarTermsCorrect. generalize (codeTerms t). clear t. intros n; unfold codeFreeVarFormula, evalStrongRec. unfold evalStrongRecHelp, evalComposeFunc, evalOneParamList, evalPrimRecFunc. repeat rewrite cPairProjections1 || rewrite cPairProjections2. simpl; repeat rewrite cPairProjections1 || rewrite cPairProjections2. reflexivity. - simpl; rewrite <- codeAppCorrect. rewrite <- Hrecf1. rewrite <- Hrecf0. clear Hrecf0 Hrecf1. unfold codeFreeVarFormula; fold g; unfold evalStrongRec. unfold evalComposeFunc, evalOneParamList. rewrite computeEvalStrongRecHelp. simpl in |- *. repeat rewrite cPairProjections1 || rewrite cPairProjections2. unfold g at 1 in |- *. repeat rewrite cPairProjections1 || rewrite cPairProjections2. rewrite (evalStrongRecHelp1 g (cPair 1 (cPair (codeFormula f1) (codeFormula f0))) (codeFormula f1)). + rewrite (evalStrongRecHelp1 g (cPair 1 (cPair (codeFormula f1) (codeFormula f0))) (codeFormula f0)). * simpl; unfold evalStrongRec, evalComposeFunc, evalOneParamList. simpl; repeat rewrite cPairProjections1 || rewrite cPairProjections2. reflexivity. * eapply Nat.lt_le_trans. -- apply cPairLt2. -- apply cPairLe3. ++ apply le_n. ++ apply cPairLe2. + eapply Nat.lt_le_trans. * apply cPairLt2. * apply cPairLe3. -- apply le_n. -- apply cPairLe1. - simpl; rewrite <- Hrecf; clear Hrecf. generalize (codeFormula f). clear f. intros n; unfold codeFreeVarFormula at 1; fold g. unfold evalStrongRec, evalComposeFunc, evalOneParamList. rewrite computeEvalStrongRecHelp; unfold evalComposeFunc, compose2. unfold evalList, pred; repeat rewrite cPairProjections1 || rewrite cPairProjections2. unfold g at 1; repeat rewrite cPairProjections1 || rewrite cPairProjections2. rewrite (evalStrongRecHelp1 g (cPair 2 n) n). simpl; reflexivity. apply cPairLt2; simpl. - simpl; rewrite <- codeListRemoveCorrect. rewrite <- Hrecf; generalize (codeFormula f). clear Hrecf f; intros n0. unfold codeFreeVarFormula at 1; fold g; unfold evalStrongRec. unfold evalComposeFunc, evalOneParamList, evalList. rewrite computeEvalStrongRecHelp. unfold evalComposeFunc, compose2, evalList, pred. repeat rewrite cPairProjections1 || rewrite cPairProjections2. unfold g at 1; repeat rewrite cPairProjections1 || rewrite cPairProjections2. rewrite (evalStrongRecHelp1 g (cPair 3 (cPair n n0)) n0). + simpl; reflexivity. + eapply Nat.lt_le_trans. * apply cPairLt2. * apply cPairLe3. -- apply le_n. -- apply cPairLe2. Qed.
imports: hydras.Ackermann(primRec cPair) Coq(List Arith) hydras.Ackermann(ListExt) hydras(folProp code Compat815)