proposition: Lemma ReplaceFormulaTermSub : forall (f : fol.Formula L) (v w s2 : nat), ReplaceFormulaTerm (codeFormula (substF f v (var w))) s2 = ReplaceFormulaTerm (codeFormula f) s2.
proof: Proof. intro f; unfold ReplaceFormulaTerm; set (A := fun f0 recs s0 : nat => switchPR (car f0) (switchPR (pred (car f0)) (switchPR (pred (pred (car f0))) (switchPR (pred (pred (pred (car f0)))) (cPair (car f0) (ReplaceTermsTerm (cdr f0) s0)) (cPair 3 (cPair s0 (codeNth (f0 - S (cdr (cdr f0))) recs)))) (cPair 2 (codeNth (f0 - S (cdr f0)) recs))) (cPair 1 (cPair (codeNth (f0 - S (car (cdr f0))) recs) (codeNth (f0 - S (cdr (cdr f0))) recs)))) (cPair 0 (cPair (ReplaceTermTerm (car (cdr f0)) s0) (ReplaceTermTerm (cdr (cdr f0)) s0)))). assert (H: forall n m : nat, m < n -> extEqual 1 (evalComposeFunc 1 1 (Vector.cons _ (evalStrongRecHelp 1 A n) 0 (Vector.nil _)) (fun b : nat => codeNth (n - S m) b)) (evalStrongRec 1 A m)). { intros n m H; apply (evalStrongRecHelp2 1); assumption. } simpl in H; elim f using Formula_depth_ind2; clear f. - intros t t0 v w s2; simpl; unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList in |- *. simpl; repeat rewrite cPairProjections1. unfold A at 3 1; repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. simpl; repeat rewrite ReplaceTermTermSub. reflexivity. - intros r t v w s2; simpl; unfold evalStrongRec in |- *. unfold evalComposeFunc, evalOneParamList, evalList in |- *. repeat rewrite computeEvalStrongRecHelp. unfold compose2 in |- *. unfold evalComposeFunc, evalOneParamList, evalList in |- *. simpl in |- *. repeat rewrite cPairProjections1. unfold A at 3 1 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. simpl in |- *. rewrite ReplaceTermsTermSub. reflexivity. - intros f H0 f0 H1 v w s2; simpl in |- *. unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. simpl; repeat rewrite cPairProjections1. repeat rewrite subFormulaImp. simpl; unfold A at 3 1. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite H with (m := codeFormula (substF f v (var w))). + rewrite H with (m := codeFormula (substF f0 v (var w))). * rewrite H with (m := codeFormula f). -- rewrite H with (m := codeFormula f0). ++ simpl; rewrite H0. rewrite H1; reflexivity. ++ apply Nat.le_lt_trans with (cPair (codeFormula f) (codeFormula f0)). ** apply cPairLe2. ** apply cPairLt2. -- apply Nat.le_lt_trans with (cPair (codeFormula f) (codeFormula f0)). ++ apply cPairLe1. ++ apply cPairLt2. * apply Nat.le_lt_trans with (cPair (codeFormula (substF f v (var w))) (codeFormula (substF f0 v (var w)))). -- apply cPairLe2. -- apply cPairLt2. + apply Nat.le_lt_trans with (cPair (codeFormula (substF f v (var w))) (codeFormula (substF f0 v (var w)))). * apply cPairLe1. * apply cPairLt2. - intros f H0 v w s2; simpl. unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. simpl; repeat rewrite cPairProjections1. repeat rewrite subFormulaNot. simpl; unfold A at 3 1; repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite H with (m := codeFormula (substF f v (var w))). rewrite H with (m := codeFormula f). simpl; rewrite H0. reflexivity. apply cPairLt2. apply cPairLt2. - intros v a H0 v0 w s2; rewrite subFormulaForall. induction (eq_nat_dec v v0) as [a0 | ?]. + reflexivity. + induction (In_dec eq_nat_dec v (freeVarT (var w))) as [a0 | ?]. * simpl; unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. simpl; repeat rewrite cPairProjections1. simpl; unfold A at 3 1 in |- *. repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite H with (m := codeFormula (substF (substF a v (var (newVar (v0 :: freeVarT (L:=L) (var w) ++ freeVarF a)))) v0 (var w))). -- rewrite H with (m := codeFormula a). simpl; rewrite H0. rewrite H0. reflexivity. apply depthForall. apply eqDepth with a. symmetry in |- *. apply subFormulaDepth. apply depthForall. apply Nat.le_lt_trans with (cPair v (codeFormula a)). apply cPairLe2. apply cPairLt2. -- apply Nat.le_lt_trans with (cPair (newVar (v0 :: freeVarT (L:=L) (var w) ++ freeVarF a)) (codeFormula (substF (substF a v (var (newVar (v0 :: freeVarT (L:=L) (var w) ++ freeVarF a)))) v0 (var w)))). ++ apply cPairLe2. ++ apply cPairLt2. * simpl; unfold evalStrongRec, evalComposeFunc, evalOneParamList, evalList. repeat rewrite computeEvalStrongRecHelp. unfold compose2, evalComposeFunc, evalOneParamList, evalList. simpl; repeat rewrite cPairProjections1. simpl; unfold A at 3 1; repeat first [ rewrite cPairProjections1 | rewrite cPairProjections2 ]. rewrite H with (m := codeFormula (substF a v0 (var w))). -- rewrite H with (m := codeFormula a). ++ simpl; rewrite H0. ** reflexivity. ** apply depthForall. ++ apply Nat.le_lt_trans with (cPair v (codeFormula a)). ** apply cPairLe2. ** apply cPairLt2. -- apply Nat.le_lt_trans with (cPair v (codeFormula (substF a v0 (var w)))). ++ apply cPairLe2. ++ apply cPairLt2. Qed.
imports: Coq(Arith Vector Lia) hydras.Ackermann(primRec cPair folProp code extEqualNat codeSubTerm codeFreeVar)