API tools faq
paste
Advertisement
Guest User

Problem at line 4299

a guest
Oct 8th, 2022
57
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 299.95 KB | None | 0 0
raw download clone embed print report
  1. From Coq Require Import Arith.
  2. From hydras.Ackermann Require Import extEqualNat.
  3. From hydras.Ackermann Require Import subAll.
  4. From hydras.Ackermann Require Import folProp.
  5. From hydras.Ackermann Require Import subProp.
  6. From hydras.Ackermann Require Import folReplace.
  7. From hydras.Ackermann Require Import folLogic3.
  8. From hydras.Ackermann Require Import NN.
  9. From hydras.Ackermann Require Import NNtheory.
  10. From hydras.Ackermann Require Import primRec.
  11. From Coqprime Require Import ChineseRem.
  12. From hydras.Ackermann Require Import expressible.
  13. From Coq Require Import List.
  14. From Coq Require Vector.
  15. From hydras.Ackermann Require Import ListExt.
  16. From hydras.Ackermann Require Import cPair.
  17. From Coq Require Import Decidable.
  18. From Coq Require Import Lia.
  19.  
  20. Section Primitive_Recursive_Representable.
  21.  
  22. Definition Representable := Representable NN.
  23. Definition RepresentableAlternate := RepresentableAlternate NN closedNN1.
  24. Definition RepresentableHelp := RepresentableHelp NN.
  25. Definition Representable_ext := Representable_ext NN.
  26.  
  27. Definition beta (a z : nat) : nat :=
  28. snd
  29. (proj1_sig
  30. (div_eucl (coPrimeBeta z (cPairPi1 a)) (gtBeta z (cPairPi1 a))
  31. (cPairPi2 a))).
  32.  
  33. Definition betaFormula : Formula :=
  34. existH 3
  35. (andH (LT (var 3) (Succ (var 2)))
  36. (existH 4
  37. (andH (LT (var 4) (Succ (var 2)))
  38. (andH
  39. (equal
  40. (Plus
  41. (Times (Plus (var 3) (var 4))
  42. (Succ (Plus (var 3) (var 4))))
  43. (Times (natToTerm 2) (var 3)))
  44. (Times (natToTerm 2) (var 2)))
  45. (andH (LT (var 0) (Succ (Times (var 3) (Succ (var 1)))))
  46. (existH 5
  47. (andH (LT (var 5) (Succ (var 4)))
  48. (equal
  49. (Plus (var 0)
  50. (Times (var 5)
  51. (Succ (Times (var 3) (Succ (var 1))))))
  52. (var 4))))))))).
  53.  
  54. Lemma betaRepresentable : Representable 2 beta betaFormula.
  55. Proof.
  56. assert
  57. (cPairLemma1 :
  58. forall a b : nat, (a + b) * S (a + b) + 2 * a = 2 * cPair a b).
  59. { intros a b. unfold cPair in |- *.
  60. assert (2 * sumToN (a + b) = (a + b) * S (a + b)) by ( induction (a + b); simpl in |- *; lia ).
  61. lia. }
  62. unfold Representable in |- *. split.
  63. + intros v H. simpl in H. lia.
  64. + simpl in |- *. intros a a0. unfold betaFormula in |- *.
  65. assert
  66. (forall (A : Formula) (v x a : nat),
  67. v <> x ->
  68. substituteFormula LNN (existH v A) x (natToTerm a) =
  69. existH v (substituteFormula LNN A x (natToTerm a))).
  70. { intros A v x a1 H. rewrite (subFormulaExist LNN).
  71. destruct (eq_nat_dec v x) as [H0 | H0]; try congruence.
  72. destruct (In_dec eq_nat_dec v (freeVarTerm LNN (natToTerm a1))) as [i | i]; try reflexivity.
  73. elim (closedNatToTerm _ _ i). }
  74. assert
  75. (forall (t1 t2 : Term) (v a : nat),
  76. substituteFormula LNN (LT t1 t2) v (natToTerm a) =
  77. LT (substituteTerm LNN t1 v (natToTerm a))
  78. (substituteTerm LNN t2 v (natToTerm a))).
  79. { intros. unfold LT at 1 in |- *. rewrite (subFormulaRelation LNN). reflexivity. }
  80. repeat first
  81. [ rewrite H; [| discriminate ]
  82. | rewrite H0
  83. | rewrite (subFormulaAnd LNN)
  84. | rewrite (subFormulaEqual LNN) ].
  85. simpl in |- *. repeat rewrite (subTermNil LNN).
  86. - assert
  87. (SysPrf NN
  88. (iffH
  89. (existH 3
  90. (andH (LT (var 3) (natToTerm (S a)))
  91. (existH 4
  92. (andH (LT (var 4) (natToTerm (S a)))
  93. (andH
  94. (equal
  95. (Plus
  96. (Times (Plus (var 3) (var 4))
  97. (Succ (Plus (var 3) (var 4))))
  98. (Times (natToTerm 2) (var 3)))
  99. (Times (natToTerm 2) (natToTerm a)))
  100. (andH
  101. (LT (var 0)
  102. (Succ (Times (var 3) (Succ (natToTerm a0)))))
  103. (existH 5
  104. (andH (LT (var 5) (Succ (var 4)))
  105. (equal
  106. (Plus (var 0)
  107. (Times (var 5)
  108. (Succ
  109. (Times (var 3)
  110. (Succ (natToTerm a0))))))
  111. (var 4))))))))))
  112. (equal (var 0) (natToTerm (beta a a0))))); auto.
  113. apply iffI.
  114. * apply impI. apply existSys.
  115. ++ apply closedNN.
  116. ++ intros [H1 | H1]; try lia. simpl in H1. elim (closedNatToTerm _ _ H1).
  117. ++ apply impE with (LT (var 3) (natToTerm (S a))).
  118. -- apply
  119. impE
  120. with
  121. (existH 4
  122. (andH (LT (var 4) (natToTerm (S a)))
  123. (andH
  124. (equal
  125. (Plus
  126. (Times (Plus (var 3) (var 4))
  127. (Succ (Plus (var 3) (var 4))))
  128. (Times (natToTerm 2) (var 3)))
  129. (Times (natToTerm 2) (natToTerm a)))
  130. (andH (LT (var 0) (Succ (Times (var 3) (Succ (natToTerm a0)))))
  131. (existH 5
  132. (andH (LT (var 5) (Succ (var 4)))
  133. (equal
  134. (Plus (var 0)
  135. (Times (var 5)
  136. (Succ (Times (var 3) (Succ (natToTerm a0))))))
  137. (var 4)))))))).
  138. ** apply sysWeaken. apply impI. apply existSys.
  139. +++ apply closedNN.
  140. +++ replace
  141. (freeVarFormula LNN
  142. (impH (LT (var 3) (natToTerm (S a)))
  143. (equal (var 0) (natToTerm (beta a a0))))) with
  144. ((freeVarTerm LNN (var 3) ++ freeVarTerm LNN (natToTerm (S a))) ++
  145. freeVarFormula LNN (equal (var 0) (natToTerm (beta a a0))))
  146. by (rewrite <- freeVarLT; reflexivity).
  147. intros [H1 | H1]; try lia.
  148. destruct (in_app_or _ _ _ H1) as [H2 | H2].
  149. --- elim (closedNatToTerm _ _ H2).
  150. --- destruct H2 as [H2| H2]; try lia. elim (closedNatToTerm _ _ H2).
  151. +++ apply
  152. impTrans
  153. with
  154. (andH (equal (var 3) (natToTerm (cPairPi1 a)))
  155. (equal (var 4) (natToTerm (cPairPi2 a)))).
  156. --- apply impI.
  157. apply
  158. impE
  159. with
  160. (equal
  161. (Plus (Times (Plus (var 3) (var 4)) (Succ (Plus (var 3) (var 4))))
  162. (Times (natToTerm 2) (var 3))) (Times (natToTerm 2) (natToTerm a))).
  163. *** apply impE with (LT (var 4) (natToTerm (S a))).
  164. ++++ apply impE with (LT (var 3) (natToTerm (S a))).
  165. ---- do 2 apply sysWeaken.
  166. apply boundedLT. intros n H1.
  167. rewrite (subFormulaImp LNN).
  168. unfold LT at 1 in |- *.
  169. rewrite (subFormulaRelation LNN).
  170. simpl in |- *.
  171. rewrite subTermNil.
  172. **** fold (var 4) in |- *.
  173. replace (apply LNN Languages.Succ (Tcons LNN 0 (natToTerm a) (Tnil LNN)))
  174. with (natToTerm (S a)); [| reflexivity ].
  175. fold (LT (var 4) (natToTerm (S a))) in |- *.
  176. apply boundedLT. intros n0 H2.
  177. repeat rewrite (subFormulaImp LNN).
  178. repeat rewrite (subFormulaAnd LNN).
  179. repeat rewrite (subFormulaEqual LNN).
  180. assert
  181. ((substituteTerm LNN
  182. (substituteTerm LNN
  183. (Plus (Times (Plus (var 3) (var 4)) (Succ (Plus (var 3) (var 4))))
  184. (Times (Succ (Succ Zero)) (var 3))) 3 (natToTerm n)) 4
  185. (natToTerm n0)) =
  186. (Plus
  187. (Times (Plus (natToTerm n) (natToTerm n0))
  188. (Succ (Plus (natToTerm n) (natToTerm n0))))
  189. (Times (Succ (Succ Zero)) (natToTerm n)))) as H3.
  190. { simpl in |- *.
  191. repeat (rewrite (subTermNil LNN (natToTerm n))); [| apply closedNatToTerm].
  192. reflexivity. }
  193. rewrite H3; clear H3.
  194. assert
  195. ((substituteTerm LNN
  196. (substituteTerm LNN (Times (Succ (Succ Zero)) (natToTerm a)) 3
  197. (natToTerm n)) 4 (natToTerm n0)) =
  198. (Times (natToTerm 2) (natToTerm a))).
  199. { simpl in |- *.
  200. repeat (rewrite (subTermNil LNN (natToTerm a)); [| apply closedNatToTerm ]).
  201. reflexivity. }
  202. simpl in |- *.
  203. assert
  204. (forall (a b : nat) (s : Term),
  205. substituteTerm LNN (natToTerm a) b s = natToTerm a).
  206. { intros. apply (subTermNil LNN). apply closedNatToTerm. }
  207. repeat rewrite H4.
  208. apply
  209. impTrans
  210. with
  211. (equal (natToTerm ((n + n0) * S (n + n0) + 2 * n)) (natToTerm (2 * a))).
  212. { apply impI. eapply eqTrans.
  213. + apply sysWeaken; apply eqSym; apply natPlus.
  214. + eapply eqTrans.
  215. - apply eqPlus. eapply eqTrans.
  216. * apply sysWeaken; apply eqSym; apply natTimes.
  217. * eapply eqTrans.
  218. ++ apply eqTimes.
  219. -- apply sysWeaken; apply eqSym. apply natPlus.
  220. -- eapply eqTrans.
  221. ** apply sysWeaken; apply eqSym.
  222. simpl in |- *. apply eqSucc. apply natPlus.
  223. ** apply eqRefl.
  224. ++ apply eqRefl.
  225. * apply sysWeaken; apply eqSym. apply natTimes.
  226. - eapply eqTrans.
  227. * apply Axm; right; constructor.
  228. * apply sysWeaken.
  229. (* I broke smth and replacing (Succ (Succ (Zero))) with (natToTerm 2) doesn't work anymore. *)
  230. replace
  231. (apply LNN Languages.Succ
  232. (Tcons LNN 0
  233. (apply LNN Languages.Succ
  234. (Tcons LNN 0
  235. (apply LNN Languages.Zero
  236. (Tnil LNN))
  237. (Tnil LNN)))
  238. (Tnil LNN)))
  239. with (natToTerm 2) by reflexivity.
  240. apply natTimes. }
  241. { rewrite cPairLemma1.
  242. destruct (eq_nat_dec a (cPair n n0)) as [e | e].
  243. + rewrite e, cPairProjections1, cPairProjections2.
  244. apply impI. apply andI; apply eqRefl.
  245. + apply impI.
  246. apply contradiction with (equal (natToTerm (2 * cPair n n0)) (natToTerm (2 * a))).
  247. - apply Axm; right; constructor.
  248. - apply sysWeaken. apply natNE. lia. }
  249. **** apply closedNatToTerm.
  250. ---- apply Axm; right; constructor.
  251. ++++ eapply andE1. apply Axm; left; right; constructor.
  252. *** eapply andE1. eapply andE2.
  253. apply Axm; left; right; constructor.
  254. --- repeat apply impI.
  255. apply
  256. impE
  257. with
  258. (existH 5
  259. (andH (LT (var 5) (Succ (var 4)))
  260. (equal
  261. (Plus (var 0)
  262. (Times (var 5) (Succ (Times (var 3) (Succ (natToTerm a0))))))
  263. (var 4)))).
  264. *** apply impE with (LT (var 0) (Succ (Times (var 3) (Succ (natToTerm a0))))).
  265. ++++ rewrite <-
  266. (subFormulaId LNN
  267. (impH (LT (var 0) (Succ (Times (var 3) (Succ (natToTerm a0)))))
  268. (impH
  269. (existH 5
  270. (andH (LT (var 5) (Succ (var 4)))
  271. (equal
  272. (Plus (var 0)
  273. (Times (var 5)
  274. (Succ (Times (var 3) (Succ (natToTerm a0))))))
  275. (var 4)))) (equal (var 0) (natToTerm (beta a a0))))) 3).
  276. apply
  277. impE
  278. with
  279. (substituteFormula LNN
  280. (impH (LT (var 0) (Succ (Times (var 3) (Succ (natToTerm a0)))))
  281. (impH
  282. (existH 5
  283. (andH (LT (var 5) (Succ (var 4)))
  284. (equal
  285. (Plus (var 0)
  286. (Times (var 5)
  287. (Succ (Times (var 3) (Succ (natToTerm a0))))))
  288. (var 4)))) (equal (var 0) (natToTerm (beta a a0))))) 3
  289. (natToTerm (cPairPi1 a))).
  290. ---- apply (subWithEquals LNN). apply eqSym. eapply andE1.
  291. apply Axm; right; constructor.
  292. ---- rewrite <-
  293. (subFormulaId LNN
  294. (substituteFormula LNN
  295. (impH (LT (var 0) (Succ (Times (var 3) (Succ (natToTerm a0)))))
  296. (impH
  297. (existH 5
  298. (andH (LT (var 5) (Succ (var 4)))
  299. (equal
  300. (Plus (var 0)
  301. (Times (var 5)
  302. (Succ (Times (var 3) (Succ (natToTerm a0))))))
  303. (var 4)))) (equal (var 0) (natToTerm (beta a a0))))) 3
  304. (natToTerm (cPairPi1 a))) 4).
  305. apply
  306. impE
  307. with
  308. (substituteFormula LNN
  309. (substituteFormula LNN
  310. (impH (LT (var 0) (Succ (Times (var 3) (Succ (natToTerm a0)))))
  311. (impH
  312. (existH 5
  313. (andH (LT (var 5) (Succ (var 4)))
  314. (equal
  315. (Plus (var 0)
  316. (Times (var 5)
  317. (Succ (Times (var 3) (Succ (natToTerm a0))))))
  318. (var 4)))) (equal (var 0) (natToTerm (beta a a0)))))
  319. 3 (natToTerm (cPairPi1 a))) 4 (natToTerm (cPairPi2 a))).
  320. ***** apply (subWithEquals LNN). apply eqSym. eapply andE2.
  321. apply Axm; right; constructor.
  322. ***** do 2 apply sysWeaken.
  323. repeat first
  324. [ rewrite H; [| discriminate ]
  325. | rewrite H0
  326. | rewrite (subFormulaImp LNN)
  327. | rewrite (subFormulaAnd LNN)
  328. | rewrite (subFormulaEqual LNN) ].
  329. simpl in |- *.
  330. repeat (rewrite (subTermNil LNN); [| apply closedNatToTerm ]).
  331. repeat (rewrite (subTermNil LNN (natToTerm a0)); [| apply closedNatToTerm ]).
  332. repeat (rewrite (subTermNil LNN (natToTerm (beta a a0))); [| apply closedNatToTerm ]).
  333. apply impTrans with (LT (var 0) (natToTerm (S (cPairPi1 a * S a0)))).
  334. { apply impI.
  335. apply
  336. impE
  337. with
  338. (substituteFormula LNN (LT (var 0) (var 1)) 1
  339. (natToTerm (S (cPairPi1 a * S a0)))).
  340. + unfold LT at 2 in |- *.
  341. rewrite (subFormulaRelation LNN).
  342. apply impRefl.
  343. + apply
  344. impE
  345. with
  346. (substituteFormula LNN (LT (var 0) (var 1)) 1
  347. (Succ (Times (natToTerm (cPairPi1 a)) (Succ (natToTerm a0))))).
  348. - apply (subWithEquals LNN). apply sysWeaken. simpl in |- *.
  349. apply eqSucc.
  350. replace (Succ (natToTerm a0)) with (natToTerm (S a0)) by reflexivity.
  351. apply natTimes.
  352. - unfold LT at 2 in |- *.
  353. rewrite (subFormulaRelation LNN).
  354. apply Axm; right; constructor. }
  355. { apply boundedLT. intros n H1.
  356. repeat first
  357. [ rewrite H; [| discriminate ]
  358. | rewrite H0
  359. | rewrite (subFormulaImp LNN)
  360. | rewrite (subFormulaAnd LNN)
  361. | rewrite (subFormulaEqual LNN) ].
  362. simpl in |- *.
  363. repeat (rewrite (subTermNil LNN); [| apply closedNatToTerm ]).
  364. apply impI. apply existSys.
  365. + apply closedNN.
  366. + simpl in |- *. intro H2.
  367. destruct (in_app_or _ _ _ H2) as [H3 | H3]; elim (closedNatToTerm _ _ H3).
  368. + apply
  369. impE
  370. with
  371. (fol.equal LNN
  372. (apply LNN Languages.Plus
  373. (Tcons LNN 1 (natToTerm n)
  374. (Tcons LNN 0
  375. (apply LNN Languages.Times
  376. (Tcons LNN 1 (fol.var LNN 5)
  377. (Tcons LNN 0
  378. (apply LNN Languages.Succ
  379. (Tcons LNN 0
  380. (apply LNN Languages.Times
  381. (Tcons LNN 1 (natToTerm (cPairPi1 a))
  382. (Tcons LNN 0
  383. (apply LNN Languages.Succ
  384. (Tcons LNN 0
  385. (natToTerm a0)
  386. (Tnil LNN)))
  387. (Tnil LNN))))
  388. (Tnil LNN))) (Tnil LNN))))
  389. (Tnil LNN)))) (natToTerm (cPairPi2 a))).
  390. - apply impE with (LT (var 5) (natToTerm (S (cPairPi2 a)))).
  391. apply sysWeaken.
  392. * apply boundedLT. intros n0 H2.
  393. repeat first
  394. [ rewrite H; [| discriminate ]
  395. | rewrite H0
  396. | rewrite (subFormulaImp LNN)
  397. | rewrite (subFormulaAnd LNN)
  398. | rewrite (subFormulaEqual LNN) ].
  399. simpl in |- *.
  400. repeat (rewrite (subTermNil LNN); [| apply closedNatToTerm ]).
  401. apply impI. destruct (eq_nat_dec n (beta a a0)) as [e | e].
  402. ++ rewrite <- e. apply eqRefl.
  403. ++ apply
  404. contradiction
  405. with
  406. (equal (natToTerm (n + n0 * S (cPairPi1 a * S a0)))
  407. (natToTerm (cPairPi2 a))).
  408. -- eapply eqTrans; [| apply Axm; right; constructor ].
  409. apply sysWeaken. eapply eqTrans.
  410. ** apply eqSym. apply natPlus.
  411. ** replace
  412. (apply LNN Languages.Plus
  413. (Tcons LNN 1 (natToTerm n)
  414. (Tcons LNN 0
  415. (apply LNN Languages.Times
  416. (Tcons LNN 1 (natToTerm n0)
  417. (Tcons LNN 0
  418. (apply LNN Languages.Succ
  419. (Tcons LNN 0
  420. (apply LNN Languages.Times
  421. (Tcons LNN 1 (natToTerm (cPairPi1 a))
  422. (Tcons LNN 0
  423. (apply LNN Languages.Succ
  424. (Tcons LNN 0 (natToTerm a0) (Tnil LNN)))
  425. (Tnil LNN)))) (Tnil LNN)))
  426. (Tnil LNN)))) (Tnil LNN)))) with
  427. (Plus (natToTerm n)
  428. (Times (natToTerm n0)
  429. (Succ (Times (natToTerm (cPairPi1 a)) (Succ (natToTerm a0))))))
  430. by reflexivity.
  431. apply eqPlus.
  432. +++ apply eqRefl.
  433. +++ eapply eqTrans.
  434. --- apply eqSym. apply natTimes.
  435. --- apply eqTimes. apply eqRefl.
  436. simpl in |- *. apply eqSucc.
  437. replace (Succ (natToTerm a0)) with (natToTerm (S a0)) by reflexivity.
  438. apply eqSym. apply natTimes.
  439. -- apply sysWeaken. apply natNE.
  440. intro; elim e. unfold beta in |- *.
  441. destruct
  442. (div_eucl (coPrimeBeta a0 (cPairPi1 a)) (gtBeta a0 (cPairPi1 a)) (cPairPi2 a)) as [[a1 b0] H4].
  443. simpl in H4. simpl in |- *.
  444. destruct H4 as (H4, H5).
  445. unfold coPrimeBeta in H4.
  446. rewrite Nat.add_comm in H3.
  447. eapply uniqueRem.
  448. ** apply Nat.lt_0_succ.
  449. ** exists n0; split; [symmetry |]; eauto.
  450. ** exists a1; split; eauto.
  451. * eapply andE1. apply Axm; right; constructor.
  452. - eapply andE2. apply Axm; right; constructor. }
  453. ++++ eapply andE1. eapply andE2. eapply andE2. apply Axm; left; right; constructor.
  454. *** eapply andE2. eapply andE2. eapply andE2. apply Axm; left; right; constructor.
  455. ** eapply andE2. apply Axm; right; constructor.
  456. -- eapply andE1. apply Axm; right; constructor.
  457. * apply impI. unfold beta in |- *.
  458. destruct (div_eucl (coPrimeBeta a0 (cPairPi1 a)) (gtBeta a0 (cPairPi1 a)) (cPairPi2 a)) as [x H1].
  459. induction x as (a1, b). simpl in |- *. simpl in H1. destruct H1 as (H1, H2).
  460. apply existI with (natToTerm (cPairPi1 a)). rewrite (subFormulaAnd LNN). apply andI.
  461. ++ apply sysWeaken. rewrite H0. simpl in |- *. rewrite subTermNil.
  462. -- replace (apply LNN Languages.Succ (Tcons LNN 0 (natToTerm a) (Tnil LNN))) with (natToTerm (S a)) by reflexivity.
  463. apply natLT. apply Nat.lt_succ_r. apply Nat.le_trans with (cPair (cPairPi1 a) (cPairPi2 a)).
  464. apply cPairLe1. rewrite cPairProjections. apply le_n.
  465. -- apply closedNatToTerm.
  466. ++ rewrite H; try lia.
  467. -- apply existI with (natToTerm (cPairPi2 a)). repeat rewrite (subFormulaAnd LNN). apply andI.
  468. ** apply sysWeaken. repeat rewrite H0. simpl in |- *.
  469. repeat rewrite (subTermNil LNN (natToTerm a)).
  470. +++ replace (apply LNN Languages.Succ (Tcons LNN 0 (natToTerm a) (Tnil LNN))) with (natToTerm (S a)) by reflexivity.
  471. apply natLT. apply Nat.lt_succ_r. apply Nat.le_trans with (cPair (cPairPi1 a) (cPairPi2 a)).
  472. --- apply cPairLe2.
  473. --- rewrite cPairProjections. apply le_n.
  474. +++ apply closedNatToTerm.
  475. +++ apply closedNatToTerm.
  476. ** apply andI.
  477. +++ repeat rewrite (subFormulaEqual LNN). simpl in |- *.
  478. repeat
  479. (rewrite (subTermNil LNN (natToTerm (cPairPi1 a)));
  480. [| apply closedNatToTerm ]).
  481. repeat
  482. (rewrite (subTermNil LNN (natToTerm a)); [| apply closedNatToTerm ]).
  483. replace
  484. (fol.equal LNN
  485. (apply LNN Languages.Plus
  486. (Tcons LNN 1
  487. (apply LNN Languages.Times
  488. (Tcons LNN 1
  489. (apply LNN Languages.Plus
  490. (Tcons LNN 1 (natToTerm (cPairPi1 a))
  491. (Tcons LNN 0 (natToTerm (cPairPi2 a)) (Tnil LNN))))
  492. (Tcons LNN 0
  493. (apply LNN Languages.Succ
  494. (Tcons LNN 0
  495. (apply LNN Languages.Plus
  496. (Tcons LNN 1 (natToTerm (cPairPi1 a))
  497. (Tcons LNN 0 (natToTerm (cPairPi2 a))
  498. (Tnil LNN)))) (Tnil LNN)))
  499. (Tnil LNN))))
  500. (Tcons LNN 0
  501. (apply LNN Languages.Times
  502. (Tcons LNN 1
  503. (apply LNN Languages.Succ
  504. (Tcons LNN 0
  505. (apply LNN Languages.Succ
  506. (Tcons LNN 0
  507. (apply LNN Languages.Zero (Tnil LNN))
  508. (Tnil LNN))) (Tnil LNN)))
  509. (Tcons LNN 0 (natToTerm (cPairPi1 a)) (Tnil LNN))))
  510. (Tnil LNN))))
  511. (apply LNN Languages.Times
  512. (Tcons LNN 1
  513. (apply LNN Languages.Succ
  514. (Tcons LNN 0
  515. (apply LNN Languages.Succ
  516. (Tcons LNN 0 (apply LNN Languages.Zero (Tnil LNN))
  517. (Tnil LNN))) (Tnil LNN)))
  518. (Tcons LNN 0 (natToTerm a) (Tnil LNN))))) with
  519. (equal
  520. (Plus
  521. (Times (Plus (natToTerm (cPairPi1 a)) (natToTerm (cPairPi2 a)))
  522. (Succ (Plus (natToTerm (cPairPi1 a)) (natToTerm (cPairPi2 a)))))
  523. (Times (natToTerm 2) (natToTerm (cPairPi1 a))))
  524. (Times (natToTerm 2) (natToTerm a))) by reflexivity.
  525. apply
  526. eqTrans
  527. with
  528. (natToTerm
  529. ((cPairPi1 a + cPairPi2 a) * S (cPairPi1 a + cPairPi2 a) +
  530. 2 * cPairPi1 a)).
  531. --- apply sysWeaken. apply eqSym. eapply eqTrans.
  532. *** apply eqSym. apply natPlus.
  533. *** apply eqPlus.
  534. ++++ eapply eqTrans.
  535. ---- apply eqSym. apply natTimes.
  536. ---- apply eqTimes.
  537. **** apply eqSym. apply natPlus.
  538. **** simpl in |- *. apply eqSucc. apply eqSym. apply natPlus.
  539. ++++ apply eqSym. apply natTimes.
  540. --- rewrite cPairLemma1. apply eqSym. rewrite cPairProjections. apply sysWeaken. apply natTimes.
  541. +++ apply andI.
  542. --- rewrite <-
  543. (subFormulaId LNN
  544. (substituteFormula LNN
  545. (substituteFormula LNN
  546. (LT (var 0) (Succ (Times (var 3) (Succ (natToTerm a0))))) 3
  547. (natToTerm (cPairPi1 a))) 4 (natToTerm (cPairPi2 a))) 0).
  548. apply
  549. impE
  550. with
  551. (substituteFormula LNN
  552. (substituteFormula LNN
  553. (substituteFormula LNN
  554. (LT (var 0) (Succ (Times (var 3) (Succ (natToTerm a0))))) 3
  555. (natToTerm (cPairPi1 a))) 4 (natToTerm (cPairPi2 a))) 0
  556. (natToTerm b)).
  557. *** apply (subWithEquals LNN). apply eqSym. apply Axm; right; constructor.
  558. *** apply sysWeaken. repeat rewrite H0. simpl in |- *.
  559. repeat
  560. (rewrite (subTermNil LNN (natToTerm (cPairPi1 a)));
  561. [| apply closedNatToTerm ]).
  562. repeat
  563. (rewrite (subTermNil LNN (natToTerm a0)); [| apply closedNatToTerm ]).
  564. apply
  565. impE
  566. with
  567. (substituteFormula LNN (LT (natToTerm b) (var 0)) 0
  568. (Succ (Times (natToTerm (cPairPi1 a)) (Succ (natToTerm a0))))).
  569. ++++ unfold LT at 1 in |- *. rewrite (subFormulaRelation LNN).
  570. simpl in |- *.
  571. repeat
  572. (rewrite (subTermNil LNN (natToTerm b)); [| apply closedNatToTerm ]).
  573. apply impRefl.
  574. ++++ apply
  575. impE
  576. with
  577. (substituteFormula LNN (LT (natToTerm b) (var 0)) 0
  578. (natToTerm (S (cPairPi1 a * S a0)))).
  579. ---- apply (subWithEquals LNN). simpl in |- *. apply eqSucc.
  580. replace (Succ (natToTerm a0)) with (natToTerm (S a0)) by reflexivity.
  581. apply eqSym. apply natTimes.
  582. ---- rewrite H0.
  583. repeat (rewrite (subTermNil LNN (natToTerm b)); [| apply closedNatToTerm ]).
  584. rewrite (subTermVar1 LNN). apply natLT. apply H2.
  585. --- repeat (rewrite H; [| discriminate ]).
  586. apply existI with (natToTerm a1).
  587. rewrite <-
  588. (subFormulaId LNN
  589. (substituteFormula LNN
  590. (substituteFormula LNN
  591. (substituteFormula LNN
  592. (andH (LT (var 5) (Succ (var 4)))
  593. (equal
  594. (Plus (var 0)
  595. (Times (var 5)
  596. (Succ (Times (var 3) (Succ (natToTerm a0))))))
  597. (var 4))) 3 (natToTerm (cPairPi1 a))) 4
  598. (natToTerm (cPairPi2 a))) 5 (natToTerm a1)) 0).
  599. apply
  600. impE
  601. with
  602. (substituteFormula LNN
  603. (substituteFormula LNN
  604. (substituteFormula LNN
  605. (substituteFormula LNN
  606. (andH (LT (var 5) (Succ (var 4)))
  607. (equal
  608. (Plus (var 0)
  609. (Times (var 5)
  610. (Succ (Times (var 3) (Succ (natToTerm a0))))))
  611. (var 4))) 3 (natToTerm (cPairPi1 a))) 4
  612. (natToTerm (cPairPi2 a))) 5 (natToTerm a1)) 0
  613. (natToTerm b)).
  614. *** apply (subWithEquals LNN). apply eqSym. apply Axm; right; constructor.
  615. *** apply sysWeaken.
  616. repeat first
  617. [ rewrite H; [| discriminate ]
  618. | rewrite H0
  619. | rewrite (subFormulaImp LNN)
  620. | rewrite (subFormulaAnd LNN)
  621. | rewrite (subFormulaEqual LNN) ].
  622. simpl in |- *.
  623. repeat
  624. (rewrite (subTermNil LNN (natToTerm (cPairPi1 a)));
  625. [| apply closedNatToTerm ]).
  626. repeat
  627. (rewrite (subTermNil LNN (natToTerm a0)); [| apply closedNatToTerm ]).
  628. repeat
  629. (rewrite (subTermNil LNN (natToTerm (cPairPi2 a)));
  630. [| apply closedNatToTerm ]).
  631. repeat
  632. (rewrite (subTermNil LNN (natToTerm a1)); [| apply closedNatToTerm ]).
  633. apply andI.
  634. ++++ replace (apply LNN Languages.Succ (Tcons LNN 0 (natToTerm (cPairPi2 a)) (Tnil LNN))) with (natToTerm (S (cPairPi2 a))) by reflexivity.
  635. apply natLT. unfold coPrimeBeta in *. lia.
  636. ++++ replace
  637. (apply LNN Languages.Plus
  638. (Tcons LNN 1 (natToTerm b)
  639. (Tcons LNN 0
  640. (apply LNN Languages.Times
  641. (Tcons LNN 1 (natToTerm a1)
  642. (Tcons LNN 0
  643. (apply LNN Languages.Succ
  644. (Tcons LNN 0
  645. (apply LNN Languages.Times
  646. (Tcons LNN 1 (natToTerm (cPairPi1 a))
  647. (Tcons LNN 0
  648. (apply LNN Languages.Succ
  649. (Tcons LNN 0 (natToTerm a0) (Tnil LNN)))
  650. (Tnil LNN)))) (Tnil LNN)))
  651. (Tnil LNN)))) (Tnil LNN)))) with
  652. (Plus (natToTerm b)
  653. (Times (natToTerm a1)
  654. (Succ (Times (natToTerm (cPairPi1 a)) (Succ (natToTerm a0)))))) by reflexivity.
  655. apply eqTrans with (natToTerm (a1 * coPrimeBeta a0 (cPairPi1 a) + b)).
  656. ---- rewrite Nat.add_comm. apply eqSym. eapply eqTrans.
  657. **** apply eqSym. apply natPlus.
  658. **** apply eqPlus.
  659. +++++ apply eqRefl.
  660. +++++ eapply eqTrans.
  661. ----- apply eqSym. apply natTimes.
  662. ----- apply eqTimes.
  663. ***** apply eqRefl.
  664. ***** unfold coPrimeBeta in |- *. simpl in |- *.
  665. apply eqSucc.
  666. replace (Succ (natToTerm a0)) with (natToTerm (S a0)) by reflexivity.
  667. apply eqSym. apply natTimes.
  668. ---- rewrite <- H1. apply eqRefl.
  669. - apply closedNatToTerm.
  670. Qed.
  671.  
  672. Fixpoint addExists (m n : nat) (f : Formula) {struct n} : Formula :=
  673. match n with
  674. | O => f
  675. | S n' => existH (n' + m) (addExists m n' f)
  676. end.
  677.  
  678. Lemma freeVarAddExists1 :
  679. forall (n m v : nat) (A : Formula),
  680. In v (freeVarFormula LNN (addExists m n A)) -> In v (freeVarFormula LNN A).
  681. Proof.
  682. intros n m v A H. induction n as [| n Hrecn].
  683. + simpl in H. exact H.
  684. + simpl in H. apply Hrecn. eapply In_list_remove1. exact H.
  685. Qed.
  686.  
  687. Lemma freeVarAddExists2 :
  688. forall (n m v : nat) (A : Formula),
  689. In v (freeVarFormula LNN (addExists m n A)) -> n + m <= v \/ v < m.
  690. Proof.
  691. intros n m v A H. induction n as [| n Hrecn]; try lia.
  692. simpl in H. simpl in |- *.
  693. assert (In v (freeVarFormula LNN (addExists m n A))) as H1.
  694. { eapply In_list_remove1. exact H. }
  695. pose proof (In_list_remove2 _ _ _ _ _ H).
  696. pose proof (Hrecn H1). lia.
  697. Qed.
  698.  
  699. Lemma reduceAddExistsOneWay :
  700. forall (n m : nat) (A B : Formula),
  701. SysPrf NN (impH A B) -> SysPrf NN (impH (addExists m n A) (addExists m n B)).
  702. Proof.
  703. intros n m A B H. apply impI. induction n as [| n Hrecn].
  704. + apply impE with A.
  705. - apply sysWeaken. apply H.
  706. - apply Axm; right; constructor.
  707. + simpl in |- *. apply existSys.
  708. - apply closedNN.
  709. - simpl in |- *; intro H0.
  710. pose proof (In_list_remove2 _ _ _ _ _ H0). congruence.
  711. - apply existSimp. exact Hrecn.
  712. Qed.
  713.  
  714. Lemma reduceAddExists :
  715. forall (n m : nat) (A B : Formula),
  716. SysPrf NN (iffH A B) -> SysPrf NN (iffH (addExists m n A) (addExists m n B)).
  717. Proof.
  718. intros n m A B H. induction n as [| n Hrecn]; simpl in |- *; auto.
  719. apply (reduceExist LNN); auto. apply closedNN.
  720. Qed.
  721.  
  722. Lemma subAddExistsNice :
  723. forall (n m : nat) (A : Formula) (v : nat) (s : Term),
  724. n + m <= v \/ v < m ->
  725. (forall v : nat, In v (freeVarTerm LNN s) -> n + m <= v \/ v < m) ->
  726. substituteFormula LNN (addExists m n A) v s =
  727. addExists m n (substituteFormula LNN A v s).
  728. Proof.
  729. intros n m A v s H H0. induction n as [| n Hrecn]; simpl in |- *; auto.
  730. rewrite (subFormulaExist LNN).
  731. destruct (eq_nat_dec (n + m) v) as [e | e]; try lia.
  732. destruct (in_dec Nat.eq_dec (n + m) (freeVarTerm LNN s)) as [e0 | e0].
  733. + pose proof (H0 _ e0). lia.
  734. + rewrite Hrecn.
  735. - reflexivity.
  736. - lia.
  737. - intros v0 H1. pose proof (H0 _ H1). lia.
  738. Qed.
  739.  
  740. Fixpoint addForalls (m n : nat) (f : Formula) {struct n} : Formula :=
  741. match n with
  742. | O => f
  743. | S n' => forallH (n' + m) (addForalls m n' f)
  744. end.
  745.  
  746. Lemma freeVarAddForalls1 :
  747. forall (n m v : nat) (A : Formula),
  748. In v (freeVarFormula LNN (addForalls m n A)) -> In v (freeVarFormula LNN A).
  749. Proof.
  750. intros n m v A H. induction n as [| n Hrecn]; simpl in H; auto.
  751. apply Hrecn. eapply In_list_remove1. exact H.
  752. Qed.
  753.  
  754. Lemma freeVarAddForalls2 :
  755. forall (n m v : nat) (A : Formula),
  756. In v (freeVarFormula LNN (addForalls m n A)) -> n + m <= v \/ v < m.
  757. Proof.
  758. intros n m v A H. induction n as [| n Hrecn]; try lia.
  759. simpl in H. simpl in |- *.
  760. assert (In v (freeVarFormula LNN (addForalls m n A))).
  761. { eapply In_list_remove1. exact H. }
  762. pose proof (Hrecn H0). pose proof (In_list_remove2 _ _ _ _ _ H). lia.
  763. Qed.
  764.  
  765. Lemma reduceAddForalls :
  766. forall (n m : nat) (A B : Formula),
  767. SysPrf NN (iffH A B) ->
  768. SysPrf NN (iffH (addForalls m n A) (addForalls m n B)).
  769. Proof.
  770. intros n m A B H. induction n as [| n Hrecn]; simpl in |- *; auto.
  771. apply (reduceForall LNN). apply closedNN. auto.
  772. Qed.
  773.  
  774. Lemma subAddForallsNice :
  775. forall (n m : nat) (A : Formula) (v : nat) (s : Term),
  776. n + m <= v \/ v < m ->
  777. (forall v : nat, In v (freeVarTerm LNN s) -> n + m <= v \/ v < m) ->
  778. substituteFormula LNN (addForalls m n A) v s =
  779. addForalls m n (substituteFormula LNN A v s).
  780. Proof.
  781. intros n m A v s H H0. induction n as [| n Hrecn]; simpl in |- *; auto.
  782. rewrite (subFormulaForall LNN). destruct (eq_nat_dec (n + m) v) as [e | e]; try lia.
  783. destruct (in_dec Nat.eq_dec (n + m) (freeVarTerm LNN s)) as [e0 | e0].
  784. + pose proof (H0 _ e0). lia.
  785. + rewrite Hrecn.
  786. - reflexivity.
  787. - lia.
  788. - intros v0 H1. pose proof (H0 _ H1). lia.
  789. Qed.
  790.  
  791. Fixpoint FormulasToFormula (n w m : nat)
  792. (vs : Vector.t (Formula * naryFunc n) m) {struct vs} : Formula :=
  793. match vs with
  794. | Vector.nil => equal (var 0) (var 0)
  795. | Vector.cons v m' vs' =>
  796. andH (substituteFormula LNN (fst v) 0 (var (S m' + w)))
  797. (FormulasToFormula n w m' vs')
  798. end.
  799.  
  800. Fixpoint FormulasToFuncs (n m : nat) (vs : Vector.t (Formula * naryFunc n) m)
  801. {struct vs} : Vector.t (naryFunc n) m :=
  802. match vs in (Vector.t _ m) return (Vector.t (naryFunc n) m) with
  803. | Vector.nil => Vector.nil _
  804. | Vector.cons v m' vs' => Vector.cons _ (snd v) m' (FormulasToFuncs n m' vs')
  805. end.
  806.  
  807. Fixpoint RepresentablesHelp (n m : nat)
  808. (vs : Vector.t (Formula * naryFunc n) m) {struct vs} : Prop :=
  809. match vs with
  810. | Vector.nil => True
  811. | Vector.cons a m' vs' =>
  812. RepresentableHelp _ (snd a) (fst a) /\ RepresentablesHelp n m' vs'
  813. end.
  814.  
  815. Definition succFormula : Formula := equal (var 0) (Succ (var 1)).
  816.  
  817. Remark succRepresentable : Representable 1 S succFormula.
  818. Proof.
  819. unfold Representable in |- *. split.
  820. + simpl. lia.
  821. + intros a. unfold succFormula in |- *.
  822. rewrite (subFormulaEqual LNN). apply iffRefl.
  823. Qed.
  824.  
  825. Definition zeroFormula : Formula := equal (var 0) Zero.
  826.  
  827. Remark zeroRepresentable : Representable 0 0 zeroFormula.
  828. Proof.
  829. unfold Representable in |- *. split.
  830. + simpl. lia.
  831. + apply iffRefl.
  832. Qed.
  833.  
  834. Definition projFormula (m : nat) : Formula := equal (var 0) (var (S m)).
  835.  
  836.  
  837. Remark projRepresentable :
  838. forall (n m : nat) (pr : m < n),
  839. Representable n (evalProjFunc n m pr) (projFormula m).
  840. Proof.
  841. intros n m pr; unfold Representable in |- *. split.
  842. + simpl. lia.
  843. + induction n as [| n Hrecn]; try lia.
  844. simpl in |- *. intros a. destruct (Nat.eq_dec m n) as [e | e].
  845. - rewrite e. clear e Hrecn pr m. induction n as [| n Hrecn].
  846. * simpl in |- *. unfold projFormula in |- *.
  847. rewrite (subFormulaEqual LNN). apply iffRefl.
  848. * simpl in |- *. intros a0. unfold projFormula in |- *.
  849. repeat rewrite (subFormulaEqual LNN). simpl in |- *.
  850. destruct (Nat.eq_dec n n); try lia.
  851. replace
  852. (fol.equal LNN (fol.var LNN 0)
  853. (substituteTerm LNN (natToTerm a) (S n)
  854. (natToTerm a0)))
  855. with
  856. (substituteFormula LNN (equal (var 0)
  857. (var (S n))) (S n)
  858. (natToTerm a)).
  859. ++ auto.
  860. ++ rewrite (subFormulaEqual LNN); simpl in |- *.
  861. destruct (Nat.eq_dec n n); try lia.
  862. rewrite subTermNil; try reflexivity.
  863. apply closedNatToTerm.
  864. - apply RepresentableAlternate with (equal (var 0) (var (S m))).
  865. * apply iffSym. apply (subFormulaNil LNN). simpl in |- *. lia.
  866. * auto.
  867. Qed.
  868.  
  869.  
  870. Definition composeSigmaFormula (n w m : nat) (A : Vector.t (Formula * naryFunc n) m)
  871. (B : Formula) : Formula :=
  872. addExists (S w) m
  873. (andH (FormulasToFormula n w m A)
  874. (subAllFormula LNN B
  875. (fun x : nat =>
  876. match x with
  877. | O => var 0
  878. | S x' => var (S x' + w)
  879. end))).
  880.  
  881. Remark composeSigmaRepresentable :
  882. forall n w m : nat,
  883. n <= w ->
  884. forall (A : Vector.t (Formula * naryFunc n) m) (B : Formula) (g : naryFunc m),
  885. RepresentablesHelp n m A ->
  886. Vector.t_rect (Formula * naryFunc n) (fun _ _ => Prop) True
  887. (fun (pair : Formula * naryFunc n) (m : nat) (v : Vector.t _ m) (rec : Prop) =>
  888. (forall v : nat, In v (freeVarFormula LNN (fst pair)) -> v <= n) /\ rec)
  889. m A ->
  890. Representable m g B ->
  891. Representable n (evalComposeFunc n m (FormulasToFuncs n m A) g)
  892. (composeSigmaFormula n w m A B).
  893. Proof.
  894. assert
  895. (forall n w m : nat,
  896. n <= w ->
  897. forall (A : Vector.t (Formula * naryFunc n) m) (B : Formula) (g : naryFunc m),
  898. RepresentablesHelp n m A ->
  899. Vector.t_rect (Formula * naryFunc n) (fun _ _ => Prop) True
  900. (fun (pair : Formula * naryFunc n) (m : nat) (v : Vector.t _ m)
  901. (rec : Prop) =>
  902. (forall v : nat, In v (freeVarFormula LNN (fst pair)) -> v <= n) /\ rec)
  903. m A ->
  904. Representable m g B ->
  905. RepresentableHelp n (evalComposeFunc n m (FormulasToFuncs n m A) g)
  906. (composeSigmaFormula n w m A B)).
  907. { intro. induction n as [| n Hrecn]; simpl in |- *.
  908. + intros w m H v.
  909. induction v as [| a n v Hrecv]; simpl in |- *; intros B g H0 H1 H2.
  910. - unfold composeSigmaFormula in |- *. simpl in |- *.
  911. replace
  912. (subAllFormula LNN B
  913. (fun x : nat => match x with
  914. | O => var 0
  915. | S x' => var (S (x' + w))
  916. end)) with (subAllFormula LNN B (fun x : nat => var x)).
  917. * apply iffTrans with B.
  918. ++ apply iffTrans with (subAllFormula LNN B (fun x : nat => var x)).
  919. -- apply iffI; apply impI.
  920. ** eapply andE2. apply Axm; right; constructor.
  921. ** apply andI.
  922. +++ apply eqRefl.
  923. +++ apply Axm; right; constructor.
  924. -- apply (subAllFormulaId LNN).
  925. ++ induction H2 as (H2, H3). auto.
  926. * apply subAllFormula_ext. intros m H3. destruct m as [| n]; auto.
  927. destruct H2 as (H2, H4). apply H2 in H3. lia.
  928. - destruct H0 as (H0, H3). destruct H1 as (H1, H4). destruct H2 as (H2, H5).
  929. assert
  930. (forall a : nat,
  931. SysPrf NN
  932. (iffH
  933. (composeSigmaFormula 0 w n v
  934. (substituteFormula LNN B (S n) (natToTerm a)))
  935. (equal (var 0) (natToTerm (evalList n (FormulasToFuncs 0 n v) (g a)))))).
  936. { intros a0. apply Hrecv; auto. split.
  937. + intros v0 H6. destruct (freeVarSubFormula3 _ _ _ _ _ H6).
  938. - assert (In v0 (freeVarFormula LNN B)).
  939. { eapply In_list_remove1. exact H7. }
  940. pose proof (In_list_remove2 _ _ _ _ _ H7).
  941. pose proof (H2 _ H8). lia.
  942. - elim (closedNatToTerm _ _ H7).
  943. + apply H5. }
  944. clear Hrecv. unfold composeSigmaFormula in |- *.
  945. unfold composeSigmaFormula in H6. simpl in |- *.
  946. apply
  947. iffTrans
  948. with
  949. (addExists (S w) n
  950. (andH (FormulasToFormula 0 w n v)
  951. (subAllFormula LNN
  952. (substituteFormula LNN B (S n) (natToTerm (snd a)))
  953. (fun x : nat =>
  954. match x with
  955. | O => var 0
  956. | S x' => var (S (x' + w))
  957. end)))); [| apply H6 ].
  958. clear H6.
  959. apply
  960. iffTrans
  961. with
  962. (existH (n + S w)
  963. (addExists (S w) n
  964. (andH
  965. (andH
  966. (substituteFormula LNN (equal (var 0) (natToTerm (snd a))) 0
  967. (var (S (n + w)))) (FormulasToFormula 0 w n v))
  968. (subAllFormula LNN B
  969. (fun x : nat =>
  970. match x with
  971. | O => var 0
  972. | S x' => var (S (x' + w))
  973. end))))).
  974. * apply (reduceExist LNN).
  975. ++ apply closedNN.
  976. ++ apply reduceAddExists.
  977. repeat apply (reduceAnd LNN); try apply iffRefl.
  978. apply (reduceSub LNN); auto.
  979. apply closedNN.
  980. * rewrite (subFormulaEqual LNN). rewrite (subTermVar1 LNN).
  981. rewrite (subTermNil LNN).
  982. apply
  983. iffTrans
  984. with
  985. (existH (n + S w)
  986. (andH (fol.equal LNN (var (S (n + w))) (natToTerm (snd a)))
  987. (addExists (S w) n
  988. (andH (FormulasToFormula 0 w n v)
  989. (subAllFormula LNN B
  990. (fun x : nat =>
  991. match x with
  992. | O => var 0
  993. | S x' => var (S (x' + w))
  994. end)))))).
  995. ++ apply (reduceExist LNN).
  996. -- apply closedNN.
  997. -- apply iffI.
  998. ** apply impI. apply andI.
  999. cut
  1000. (SysPrf
  1001. (Ensembles.Add (fol.Formula LNN) NN
  1002. (andH
  1003. (andH (fol.equal LNN (var (S (n + w))) (natToTerm (snd a)))
  1004. (FormulasToFormula 0 w n v))
  1005. (subAllFormula LNN B
  1006. (fun x : nat =>
  1007. match x with
  1008. | O => var 0
  1009. | S x' => var (S (x' + w))
  1010. end)))) (fol.equal LNN (var (S (n + w))) (natToTerm (snd a)))).
  1011. +++ generalize
  1012. (andH
  1013. (andH (fol.equal LNN (var (S (n + w))) (natToTerm (snd a)))
  1014. (FormulasToFormula 0 w n v))
  1015. (subAllFormula LNN B
  1016. (fun x : nat =>
  1017. match x with
  1018. | O => var 0
  1019. | S x' => var (S (x' + w))
  1020. end))).
  1021. cut (n + w < S (n + w)); try lia.
  1022. --- generalize (S (n + w)).
  1023. intros n0 H6 f H7.
  1024. clear H5 H2 H4 H1 H3 H0 g B v.
  1025. induction n as [| n Hrecn].
  1026. *** simpl in |- *. auto.
  1027. *** simpl in |- *. apply existSys.
  1028. ++++ apply closedNN.
  1029. ++++ simpl in |- *; intro.
  1030. destruct H0 as [H0 | H0]; try lia.
  1031. elim (closedNatToTerm _ _ H0).
  1032. ++++ apply Hrecn. lia.
  1033. +++ eapply andE1. eapply andE1. apply Axm; right; constructor.
  1034. +++ apply
  1035. impE
  1036. with
  1037. (addExists (S w) n
  1038. (andH
  1039. (andH (fol.equal LNN (var (S (n + w))) (natToTerm (snd a)))
  1040. (FormulasToFormula 0 w n v))
  1041. (subAllFormula LNN B
  1042. (fun x : nat =>
  1043. match x with
  1044. | O => var 0
  1045. | S x' => var (S (x' + w))
  1046. end)))).
  1047. --- apply sysWeaken.
  1048. apply reduceAddExistsOneWay.
  1049. apply impI. apply andI.
  1050. *** eapply andE2. eapply andE1.
  1051. apply Axm; right; constructor.
  1052. *** eapply andE2.
  1053. apply Axm; right; constructor.
  1054. --- apply Axm; right; constructor.
  1055. ** apply impI.
  1056. apply
  1057. impE
  1058. with
  1059. (addExists (S w) n
  1060. (andH (FormulasToFormula 0 w n v)
  1061. (subAllFormula LNN B
  1062. (fun x : nat =>
  1063. match x with
  1064. | O => var 0
  1065. | S x' => var (S (x' + w))
  1066. end)))).
  1067. +++ apply impE with (fol.equal LNN (var (S (n + w))) (natToTerm (snd a))).
  1068. --- apply sysWeaken. apply impI.
  1069. cut
  1070. (SysPrf
  1071. (Ensembles.Add (fol.Formula LNN) NN
  1072. (fol.equal LNN (var (S (n + w))) (natToTerm (snd a))))
  1073. (impH
  1074. (andH (FormulasToFormula 0 w n v)
  1075. (subAllFormula LNN B
  1076. (fun x : nat =>
  1077. match x with
  1078. | O => var 0
  1079. | S x' => var (S (x' + w))
  1080. end)))
  1081. (andH
  1082. (andH (fol.equal LNN (var (S (n + w))) (natToTerm (snd a)))
  1083. (FormulasToFormula 0 w n v))
  1084. (subAllFormula LNN B
  1085. (fun x : nat =>
  1086. match x with
  1087. | O => var 0
  1088. | S x' => var (S (x' + w))
  1089. end))))).
  1090. *** generalize
  1091. (andH (FormulasToFormula 0 w n v)
  1092. (subAllFormula LNN B
  1093. (fun x : nat =>
  1094. match x with
  1095. | O => var 0
  1096. | S x' => var (S (x' + w))
  1097. end)))
  1098. (andH
  1099. (andH (fol.equal LNN (var (S (n + w))) (natToTerm (snd a)))
  1100. (FormulasToFormula 0 w n v))
  1101. (subAllFormula LNN B
  1102. (fun x : nat =>
  1103. match x with
  1104. | O => var 0
  1105. | S x' => var (S (x' + w))
  1106. end))).
  1107. cut (n + w < S (n + w)); try lia.
  1108. generalize (S (n + w)).
  1109. clear H5 H2 H4 H1 H3 H0 g B v.
  1110. induction n as [| n Hrecn]; auto.
  1111. simpl in |- *. intros n0 H0 f f0 H1.
  1112. apply impI. apply existSys.
  1113. ++++ intro. destruct H2 as (x, H2).
  1114. destruct H2 as (H2, H3).
  1115. destruct H3 as [x H3 | x H3].
  1116. ---- elim (closedNN (n + S w)).
  1117. exists x. auto.
  1118. ---- destruct H3. simpl in H2.
  1119. destruct H2 as [H2 | H2]; try lia.
  1120. elim (closedNatToTerm _ _ H2).
  1121. ++++ simpl in |- *. intro H2.
  1122. elim (In_list_remove2 _ _ _ _ _ H2). auto.
  1123. ++++ apply existSimp. apply impE with (addExists (S w) n f).
  1124. ---- apply sysWeaken. apply Hrecn; auto. lia.
  1125. ---- apply Axm; right; constructor.
  1126. *** apply impI. repeat apply andI.
  1127. ++++ apply Axm; left; right; constructor.
  1128. ++++ eapply andE1. apply Axm; right; constructor.
  1129. ++++ eapply andE2. apply Axm; right; constructor.
  1130. --- eapply andE1. apply Axm; right; constructor.
  1131. +++ eapply andE2. apply Axm; right; constructor.
  1132. ++ apply
  1133. iffTrans
  1134. with
  1135. (substituteFormula LNN
  1136. (addExists (S w) n
  1137. (andH (FormulasToFormula 0 w n v)
  1138. (subAllFormula LNN B
  1139. (fun x : nat =>
  1140. match x with
  1141. | O => var 0
  1142. | S x' => var (S (x' + w))
  1143. end)))) (S n + w) (natToTerm (snd a))).
  1144. -- apply iffI.
  1145. ** apply impI. apply existSys.
  1146. +++ apply closedNN.
  1147. +++ intro H6. destruct (freeVarSubFormula3 _ _ _ _ _ H6).
  1148. ---- elim (In_list_remove2 _ _ _ _ _ H7). lia.
  1149. ---- elim (closedNatToTerm _ _ H7).
  1150. +++ apply
  1151. impE
  1152. with
  1153. (substituteFormula LNN
  1154. (addExists (S w) n
  1155. (andH (FormulasToFormula 0 w n v)
  1156. (subAllFormula LNN B
  1157. (fun x : nat =>
  1158. match x with
  1159. | O => var 0
  1160. | S x' => var (S (x' + w))
  1161. end)))) (S n + w) (var (S n + w))).
  1162. --- apply (subWithEquals LNN). eapply andE1.
  1163. apply Axm; right; constructor.
  1164. --- rewrite (subFormulaId LNN). eapply andE2.
  1165. apply Axm; right; constructor.
  1166. ** apply impI. apply existI with (natToTerm (snd a)).
  1167. rewrite (subFormulaAnd LNN). rewrite <- plus_Snm_nSm.
  1168. apply andI.
  1169. +++ rewrite subFormulaEqual. rewrite (subTermVar1 LNN).
  1170. rewrite (subTermNil LNN).
  1171. --- apply eqRefl.
  1172. --- apply closedNatToTerm.
  1173. +++ apply Axm; right; constructor.
  1174. -- rewrite subAddExistsNice.
  1175. ** apply reduceAddExists. rewrite (subFormulaAnd LNN).
  1176. apply (reduceAnd LNN).
  1177. +++ apply (subFormulaNil LNN).
  1178. cut (n + w < S n + w); try lia.
  1179. generalize (S n + w). clear H5 H3 g H2.
  1180. induction v as [| a0 n v Hrecv]; unfold not in |- *; intros n0 H2 H3.
  1181. --- simpl in H3. lia.
  1182. --- simpl in H3. destruct (in_app_or _ _ _ H3) as [H5 | H5].
  1183. *** simpl in H4.
  1184. induction (freeVarSubFormula3 _ _ _ _ _ H5) as [H6 | H6].
  1185. elim (le_not_lt n0 0).
  1186. ++++ decompose record H4. apply H7.
  1187. eapply In_list_remove1. apply H6.
  1188. ++++ lia.
  1189. ++++ destruct H6 as [H6 | H6].
  1190. ---- lia.
  1191. ---- elim H6.
  1192. *** lazymatch goal with _ : In ?n _ |- _ => elim Hrecv with n end.
  1193. ++++ simpl in H4. tauto.
  1194. ++++ lia.
  1195. ++++ auto.
  1196. +++ eapply iffTrans. apply (subSubAllFormula LNN).
  1197. apply iffSym. eapply iffTrans.
  1198. --- apply (subAllSubFormula LNN).
  1199. --- replace
  1200. (subAllFormula LNN B
  1201. (fun n1 : nat =>
  1202. substituteTerm LNN
  1203. match n1 with
  1204. | O => var 0
  1205. | S x' => var (S (x' + w))
  1206. end (S n + w) (natToTerm (snd a)))) with
  1207. (subAllFormula LNN B
  1208. (fun x : nat =>
  1209. match eq_nat_dec (S n) x with
  1210. | left _ =>
  1211. subAllTerm LNN (natToTerm (snd a))
  1212. (fun x0 : nat =>
  1213. match x0 with
  1214. | O => var 0
  1215. | S x' => var (S (x' + w))
  1216. end)
  1217. | right _ =>
  1218. (fun x0 : nat =>
  1219. match x0 with
  1220. | O => var 0
  1221. | S x' => var (S (x' + w))
  1222. end) x
  1223. end)).
  1224. *** apply iffRefl.
  1225. *** apply subAllFormula_ext. intros m H6.
  1226. destruct (eq_nat_dec (S n) m) as [e | e].
  1227. ++++ rewrite <- e. rewrite (subTermVar1 LNN).
  1228. clear H0. induction (snd a).
  1229. ---- simpl in |- *. reflexivity.
  1230. ---- simpl in |- *. rewrite IHn0. reflexivity.
  1231. ++++ destruct m as [| n0].
  1232. ---- simpl in |- *. reflexivity.
  1233. ---- rewrite (subTermVar2 LNN).
  1234. **** reflexivity.
  1235. **** lia.
  1236. ** lia.
  1237. ** intros v0 H6. elim (closedNatToTerm _ _ H6).
  1238. ++ apply closedNatToTerm.
  1239. + intros.
  1240. set
  1241. (v' :=
  1242. Vector.t_rec (Formula * (nat -> naryFunc n))
  1243. (fun (m : nat) (v : Vector.t _ m) => Vector.t (Formula * naryFunc n) m)
  1244. (Vector.nil _)
  1245. (fun (pair : Formula * (nat -> naryFunc n)) (m : nat)
  1246. (v : Vector.t _ m) (rec : Vector.t (Formula * naryFunc n) m) =>
  1247. Vector.cons _
  1248. (substituteFormula LNN (fst pair) (S n) (natToTerm a), snd pair a) m
  1249. rec) _ A) in *.
  1250. assert
  1251. (RepresentableHelp n (evalComposeFunc n m (FormulasToFuncs n m v') g)
  1252. (addExists (S w) m
  1253. (andH (FormulasToFormula n w m v')
  1254. (subAllFormula LNN B
  1255. (fun x : nat =>
  1256. match x with
  1257. | O => var 0
  1258. | S x' => var (S (x' + w))
  1259. end))))).
  1260. - unfold composeSigmaFormula in Hrecn.
  1261. simpl in Hrecn. apply Hrecn.
  1262. * lia.
  1263. * clear B g H2.
  1264. induction A as [| a0 n0 A HrecA]; simpl in (value of v'); simpl in |- *; auto.
  1265. split.
  1266. ++ simpl in H0. destruct H0 as (H0, H2). apply H0.
  1267. ++ apply HrecA.
  1268. -- destruct H0 as (H0, H2). auto.
  1269. -- simpl in H1. destruct H1 as (H1, H2). auto.
  1270. * simpl in H1. clear H2 H0 g B. induction A as [| a0 n0 A HrecA].
  1271. ++ simpl in |- *. auto.
  1272. ++ simpl in |- *. split.
  1273. -- simpl in H1. destruct H1 as (H0, H1). intros v H2.
  1274. destruct (freeVarSubFormula3 _ _ _ _ _ H2).
  1275. ** assert (v <= S n).
  1276. { apply H0. eapply In_list_remove1. exact H3. }
  1277. destruct (le_lt_or_eq _ _ H4).
  1278. +++ lia.
  1279. +++ elim (In_list_remove2 _ _ _ _ _ H3). auto.
  1280. ** elim (closedNatToTerm _ _ H3).
  1281. -- apply HrecA. destruct H1 as (H0, H1). auto.
  1282. * auto.
  1283. - unfold composeSigmaFormula in |- *. clear Hrecn.
  1284. apply
  1285. RepresentableAlternate
  1286. with
  1287. (addExists (S w) m
  1288. (andH (FormulasToFormula n w m v')
  1289. (subAllFormula LNN B
  1290. (fun x : nat =>
  1291. match x with
  1292. | O => var 0
  1293. | S x' => var (S (x' + w))
  1294. end)))).
  1295. * rewrite subAddExistsNice.
  1296. ++ apply reduceAddExists. rewrite (subFormulaAnd LNN).
  1297. apply (reduceAnd LNN).
  1298. -- clear H3 H2 H1 H0 g B. induction A as [| a0 n0 A HrecA].
  1299. ** simpl in |- *. apply iffSym. apply (subFormulaNil LNN). simpl in |- *. lia.
  1300. ** simpl in |- *. rewrite (subFormulaAnd LNN).
  1301. apply (reduceAnd LNN); [| apply HrecA ].
  1302. apply (subFormulaExch LNN); try lia.
  1303. +++ apply closedNatToTerm.
  1304. +++ unfold not in |- *; intros. destruct H0 as [H0 | H0].
  1305. --- lia.
  1306. --- apply H0.
  1307. -- apply iffSym. apply (subFormulaNil LNN).
  1308. intro H4. decompose record (freeVarSubAllFormula1 _ _ _ _ H4).
  1309. destruct x as [| n0].
  1310. ** destruct H7 as [H5 | H5]; try lia. elim H5.
  1311. ** destruct H7 as [H5| H5].
  1312. +++ lia.
  1313. +++ elim H5.
  1314. ++ lia.
  1315. ++ intros. elim (closedNatToTerm _ _ H4).
  1316. * apply Representable_ext with (evalComposeFunc n m (FormulasToFuncs n m v') g).
  1317. clear H3 H2 H1 H0 B.
  1318. ++ apply extEqualCompose.
  1319. -- unfold extEqualVector in |- *. clear g.
  1320. induction A as [| a0 n0 A HrecA]; simpl in |- *; auto.
  1321. split.
  1322. ** apply extEqualRefl.
  1323. ** apply HrecA.
  1324. -- apply extEqualRefl.
  1325. ++ apply H3. }
  1326. intros n w m H0 A B g H1 H2 H3. split.
  1327. + intros v H4. unfold composeSigmaFormula in H4.
  1328. assert
  1329. (In v
  1330. (freeVarFormula LNN
  1331. (andH (FormulasToFormula n w m A)
  1332. (subAllFormula LNN B
  1333. (fun x : nat =>
  1334. match x with
  1335. | O => var 0
  1336. | S x' => var (S x' + w)
  1337. end))))).
  1338. { eapply freeVarAddExists1. apply H4. }
  1339. simpl in H5. destruct (in_app_or _ _ _ H5).
  1340. - assert (m + S w <= v \/ v < S w).
  1341. { eapply freeVarAddExists2. apply H4. }
  1342. clear H5 H4 H3 H1 g B.
  1343. induction A as [| a n0 A HrecA].
  1344. * simpl in H6. lia.
  1345. * simpl in H6. destruct (in_app_or _ _ _ H6).
  1346. ++ simpl in H2. destruct H2 as (H2, H3).
  1347. destruct (freeVarSubFormula3 _ _ _ _ _ H1) as [H4 | H4].
  1348. -- apply H2. eapply In_list_remove1. exact H4.
  1349. -- destruct H4 as [H4 | H4].
  1350. ** lia.
  1351. ** elim H4.
  1352. ++ apply HrecA; auto.
  1353. -- simpl in H2. tauto.
  1354. -- lia.
  1355. - decompose record (freeVarSubAllFormula1 _ _ _ _ H6).
  1356. destruct x as [| n0].
  1357. * destruct H9 as [H7 | H7]; try lia. elim H7.
  1358. * induction H9 as [H7 | H7].
  1359. ++ rewrite <- H7. destruct H3 as (H3, H9).
  1360. assert (S n0 <= m). { apply H3. auto. }
  1361. destruct (freeVarAddExists2 _ _ _ _ H4) as [H11 | H11].
  1362. -- lia.
  1363. -- lia.
  1364. ++ elim H7.
  1365. + apply H; auto.
  1366. Qed.
  1367.  
  1368. (*
  1369. Local composePiFormula [n,w,m:nat][A:(vector Formula*(naryFunc n) m)][B:Formula] : Formula :=
  1370. (addForalls (S w) m (impH (FormulasToFormula n w m A)
  1371. (subAllFormula LNN B [x:nat]
  1372. (Cases x of O => (var O) | (S x')=>(var (plus (S x') w))end)))).
  1373.  
  1374. Remark composePiRepresentable : (n,w,m:nat)(le n w)->(A:(vector Formula*(naryFunc n) m))
  1375. (B:Formula)(g:(naryFunc m))
  1376. (RepresentablesHelp n m A)->
  1377. (vector_rect Formula*(naryFunc n) [_][_]Prop
  1378. True
  1379. [pair:(Formula*(naryFunc n))][m:nat][v:(vector ? m)][rec:Prop]
  1380. ((v:nat)(In v (freeVarFormula LNN (Fst pair)))->(le v n))/\rec
  1381. m A)->
  1382. (Representable m g B)->
  1383. (Representable n (evalComposeFunc n m (FormulasToFuncs n m A) g)
  1384. (composePiFormula n w m A B)).
  1385. Proof.
  1386. Assert (n,w,m:nat)(le n w)->(A:(vector Formula*(naryFunc n) m))
  1387. (B:Formula)(g:(naryFunc m))
  1388. (RepresentablesHelp n m A)->
  1389. (vector_rect Formula*(naryFunc n) [_][_]Prop
  1390. True
  1391. [pair:(Formula*(naryFunc n))][m:nat][v:(vector ? m)][rec:Prop]
  1392. ((v:nat)(In v (freeVarFormula LNN (Fst pair)))->(le v n))/\rec
  1393. m A)->
  1394. (Representable m g B)->
  1395. (RepresentableHelp n (evalComposeFunc n m (FormulasToFuncs n m A) g)
  1396. (composePiFormula n w m A B)).
  1397. Intro.
  1398. Induction n; Simpl.
  1399. Intros w m H v.
  1400. Induction v; Simpl; Intros.
  1401. Unfold composePiFormula.
  1402. Simpl.
  1403. Replace (subAllFormula LNN B
  1404. [x:nat]
  1405. Cases x of
  1406. 0 => (var (0))
  1407. | (S x') => (var (S (plus x' w)))
  1408. end)
  1409. with (subAllFormula LNN B [x:nat](var x)).
  1410. Apply iffTrans with B.
  1411. Apply iffTrans with (subAllFormula LNN B [x:nat](var x)).
  1412. Apply iffI;
  1413. Apply impI.
  1414. Apply impE with (equal (var (0)) (var (0))).
  1415. Apply Axm; Right; Constructor.
  1416. Apply eqRefl.
  1417. Apply impI.
  1418. Apply Axm; Left; Right; Constructor.
  1419. Apply (subAllFormulaId LNN).
  1420. Induction H2.
  1421. Auto.
  1422. Apply subAllFormula_ext.
  1423. Intros.
  1424. NewDestruct m.
  1425. Auto.
  1426. Elim (le_Sn_O n).
  1427. Induction H2.
  1428. Apply H2.
  1429. Auto.
  1430. Induction H0.
  1431. Induction H1.
  1432. Induction H2.
  1433. Assert (a:nat)(SysPrf NN
  1434. (iffH (composePiFormula (0) w n v (substituteFormula LNN B (S n) (natToTerm a)))
  1435. (equal (var (0))
  1436. (natToTerm
  1437. (evalList n (FormulasToFuncs (0) n v) (g a)))))).
  1438. Intros.
  1439. Apply Hrecv.
  1440. Auto.
  1441. Auto.
  1442. Split.
  1443. Intros.
  1444. NewInduction (freeVarSubFormula3 ? ? ? ? ? H6).
  1445. Assert (In v0 (freeVarFormula LNN B)).
  1446. EApply In_list_remove1.
  1447. Apply H7.
  1448. NewInduction (le_lt_or_eq ? ? (H2 ? H8)).
  1449. Apply lt_n_Sm_le.
  1450. Auto.
  1451. Elim (In_list_remove2 ? ? ? ? ? H7).
  1452. Auto.
  1453. Elim (closedNatToTerm ? ? H7).
  1454. Apply H5.
  1455. Clear Hrecv.
  1456. Unfold composePiFormula.
  1457. Unfold composePiFormula in H6.
  1458. Simpl.
  1459. Apply iffTrans with (addForalls (S w) n
  1460. (impH (FormulasToFormula (0) w n v)
  1461. (subAllFormula LNN
  1462. (substituteFormula LNN B (S n) (natToTerm (Snd a)))
  1463. [x:nat]
  1464. Cases x of
  1465. 0 => (var (0))
  1466. | (S x') => (var (S (plus x' w)))
  1467. end)));
  1468. [Idtac | Apply H6].
  1469. Clear H6.
  1470. Apply iffTrans with (forallH (plus n (S w))
  1471. (addForalls (S w) n
  1472. (impH
  1473. (andH
  1474. (substituteFormula LNN (equal (var (0)) (natToTerm (Snd a))) (0) (var (S (plus n w))))
  1475. (FormulasToFormula (0) w n v))
  1476. (subAllFormula LNN B
  1477. [x:nat]
  1478. Cases x of
  1479. 0 => (var (0))
  1480. | (S x') => (var (S (plus x' w)))
  1481. end)))).
  1482. Apply (reduceForall LNN).
  1483. Apply closedNN.
  1484. Apply reduceAddForalls.
  1485. Apply (reduceImp LNN); Try Apply iffRefl.
  1486. Apply (reduceAnd LNN); Try Apply iffRefl.
  1487. Apply (reduceSub LNN).
  1488. Apply closedNN.
  1489. Auto.
  1490. Rewrite (subFormulaEqual LNN).
  1491. Rewrite (subTermVar1 LNN).
  1492. Rewrite (subTermNil LNN).
  1493. Apply iffTrans with (forallH (plus n (S w))
  1494. (impH (fol.equal LNN (var (S (plus n w))) (natToTerm (Snd a)))
  1495. (addForalls (S w) n
  1496. (impH
  1497. (FormulasToFormula (0) w n v)
  1498. (subAllFormula LNN B
  1499. [x:nat]
  1500. Cases x of
  1501. 0 => (var (0))
  1502. | (S x') => (var (S (plus x' w)))
  1503. end))))).
  1504. Apply (reduceForall LNN).
  1505. Apply closedNN.
  1506. Apply iffI.
  1507. Repeat Apply impI.
  1508. Cut (SysPrf
  1509. (Ensembles.Add (fol.Formula LNN)
  1510. (Ensembles.Add (fol.Formula LNN) NN
  1511. (impH
  1512. (andH
  1513. (fol.equal LNN (var (S (plus n w))) (natToTerm (Snd a)))
  1514. (FormulasToFormula (0) w n v))
  1515. (subAllFormula LNN B
  1516. [x:nat]
  1517. Cases x of
  1518. 0 => (var (0))
  1519. | (S x') => (var (S (plus x' w)))
  1520. end)))
  1521. (fol.equal LNN (var (S (plus n w))) (natToTerm (Snd a))))
  1522. (impH (FormulasToFormula (0) w n v)
  1523. (subAllFormula LNN B
  1524. [x:nat]
  1525. Cases x of
  1526. 0 => (var (0))
  1527. | (S x') => (var (S (plus x' w)))
  1528. end))).
  1529. Generalize (impH
  1530. (andH
  1531. (fol.equal LNN (var (S (plus n w))) (natToTerm (Snd a)))
  1532. (FormulasToFormula (0) w n v))
  1533. (subAllFormula LNN B
  1534. [x:nat]
  1535. Cases x of
  1536. 0 => (var (0))
  1537. | (S x') => (var (S (plus x' w)))
  1538. end)) (impH (FormulasToFormula (0) w n v)
  1539. (subAllFormula LNN B
  1540. [x:nat]
  1541. Cases x of
  1542. 0 => (var (0))
  1543. | (S x') => (var (S (plus x' w)))
  1544. end)).
  1545. Cut (lt (plus n w) (S (plus n w))).
  1546. Generalize (S (plus n w)).
  1547. Intros.
  1548. Clear H5 H2 H4 H1 H3 H0 g B v.
  1549. Induction n.
  1550. Simpl.
  1551. Auto.
  1552. Simpl.
  1553. Apply forallI.
  1554. Simpl; Unfold not; Intros.
  1555. Induction H0; Induction H0.
  1556. Induction H1.
  1557. Induction H1.
  1558. Elim closedNN with (plus n (S w)).
  1559. Exists x; Auto.
  1560. Induction H1.
  1561. Simpl in H0.
  1562. Elim (In_list_remove2 ? ? ? ? ? H0).
  1563. Auto.
  1564. Induction H1.
  1565. Induction H0.
  1566. Rewrite <- plus_Snm_nSm in H0.
  1567. Rewrite H0 in H6.
  1568. Elim (lt_n_n ? H6).
  1569. Simpl in H0.
  1570. Elim (closedNatToTerm ? ? H0).
  1571. Apply impE with (fol.equal LNN (var n0) (natToTerm (Snd a))).
  1572. Apply impE with (addForalls (S w) n f).
  1573. Repeat Apply sysWeaken.
  1574. Repeat Apply impI.
  1575. Apply Hrecn.
  1576. EApply lt_trans.
  1577. Apply lt_n_Sn.
  1578. Auto.
  1579. Apply forallSimp with (plus n (S w)).
  1580. Apply Axm; Left; Right; Constructor.
  1581. Apply Axm; Right; Constructor.
  1582. Apply lt_n_Sn.
  1583. Apply impI.
  1584. Apply impE with (andH
  1585. (fol.equal LNN (var (S (plus n w))) (natToTerm (Snd a)))
  1586. (FormulasToFormula (0) w n v)).
  1587. Apply Axm; Left; Left; Right; Constructor.
  1588. Apply andI.
  1589. Apply Axm; Left; Right; Constructor.
  1590. Apply Axm; Right; Constructor.
  1591. Apply impI.
  1592. Cut (SysPrf
  1593. (Ensembles.Add (fol.Formula LNN) NN
  1594. (impH (fol.equal LNN (var (S (plus n w))) (natToTerm (Snd a)))
  1595. (impH (FormulasToFormula (0) w n v)
  1596. (subAllFormula LNN B
  1597. [x:nat]
  1598. Cases x of
  1599. 0 => (var (0))
  1600. | (S x') => (var (S (plus x' w)))
  1601. end))))
  1602. (impH
  1603. (andH (fol.equal LNN (var (S (plus n w))) (natToTerm (Snd a)))
  1604. (FormulasToFormula (0) w n v))
  1605. (subAllFormula LNN B
  1606. [x:nat]
  1607. Cases x of
  1608. 0 => (var (0))
  1609. | (S x') => (var (S (plus x' w)))
  1610. end))).
  1611. Generalize (impH (FormulasToFormula (0) w n v)
  1612. (subAllFormula LNN B
  1613. [x:nat]
  1614. Cases x of
  1615. 0 => (var (0))
  1616. | (S x') => (var (S (plus x' w)))
  1617. end))
  1618. (impH
  1619. (andH
  1620. (fol.equal LNN (var (S (plus n w))) (natToTerm (Snd a)))
  1621. (FormulasToFormula (0) w n v))
  1622. (subAllFormula LNN B
  1623. [x:nat]
  1624. Cases x of
  1625. 0 => (var (0))
  1626. | (S x') => (var (S (plus x' w)))
  1627. end)).
  1628. Cut (lt (plus n w) (S (plus n w))).
  1629. Generalize (S (plus n w)).
  1630. Intros.
  1631. Clear H5 H2 H4 H1 H3 H0 g B v.
  1632. Induction n.
  1633. Auto.
  1634. Simpl.
  1635. Apply forallI.
  1636. Unfold not; Intros.
  1637. Induction H0; Induction H0.
  1638. Induction H1.
  1639. Elim closedNN with (plus n (S w)).
  1640. Exists x; Auto.
  1641. Induction H1.
  1642. Simpl in H0.
  1643. Induction H0.
  1644. Rewrite <- plus_Snm_nSm in H0.
  1645. Rewrite <- H0 in H6.
  1646. Elim (lt_n_n ? H6).
  1647. NewInduction (in_app_or H0).
  1648. Elim (closedNatToTerm ? ? H1).
  1649. Elim (In_list_remove2 ? ? ? ? ? H1).
  1650. Auto.
  1651. Apply impE with (impH (fol.equal LNN (var n0) (natToTerm (Snd a)))
  1652. (addForalls (S w) n f)).
  1653. Apply sysWeaken.
  1654. Apply impI.
  1655. Apply Hrecn.
  1656. EApply lt_trans.
  1657. Apply lt_n_Sn.
  1658. Apply H6.
  1659. Apply impI.
  1660. EApply forallSimp.
  1661. Apply impE with (fol.equal LNN (var n0) (natToTerm (Snd a))).
  1662. Apply Axm; Left; Right; Constructor.
  1663. Apply Axm; Right; Constructor.
  1664. Apply lt_n_Sn.
  1665. Apply impI.
  1666. Apply impE with (FormulasToFormula (0) w n v).
  1667. Apply impE with (fol.equal LNN (var (S (plus n w))) (natToTerm (Snd a))).
  1668. Apply Axm; Left; Right; Constructor.
  1669. EApply andE1.
  1670. Apply Axm; Right; Constructor.
  1671. EApply andE2.
  1672. Apply Axm; Right; Constructor.
  1673. Apply iffTrans with (substituteFormula LNN (addForalls (S w) n
  1674. (impH (FormulasToFormula (0) w n v)
  1675. (subAllFormula LNN B
  1676. [x:nat]
  1677. Cases x of
  1678. 0 => (var (0))
  1679. | (S x') => (var (S (plus x' w)))
  1680. end))) (plus (S n) w) (natToTerm (Snd a))).
  1681. Rewrite <- plus_Snm_nSm.
  1682. Apply iffI.
  1683. Apply impI.
  1684. Apply impE with (substituteFormula LNN
  1685. (fol.equal LNN (var (S (plus n w))) (natToTerm (Snd a)))
  1686. (S (plus n w)) (natToTerm (Snd a))).
  1687. Rewrite <- (subFormulaImp LNN).
  1688. Apply forallE.
  1689. Apply Axm; Right; Constructor.
  1690. Rewrite subFormulaEqual.
  1691. Rewrite (subTermVar1 LNN).
  1692. Rewrite (subTermNil LNN).
  1693. Apply eqRefl.
  1694. Apply closedNatToTerm.
  1695. Apply impI.
  1696. Apply forallI.
  1697. Unfold not; Intros.
  1698. Induction H6; Induction H6.
  1699. Induction H7.
  1700. Elim closedNN with (plus (S n) w).
  1701. Exists x; Auto.
  1702. Induction H7.
  1703. Simpl in H6.
  1704. NewInduction (freeVarSubFormula3 ? ? ? ? ? H6).
  1705. Elim (In_list_remove2 ? ? ? ? ? H7).
  1706. Auto.
  1707. Elim (closedNatToTerm ? ? H7).
  1708. Apply impI.
  1709. Rewrite <- (subFormulaId LNN (addForalls (S w) n
  1710. (impH (FormulasToFormula (0) w n v)
  1711. (subAllFormula LNN B
  1712. [x:nat]
  1713. Cases x of
  1714. 0 => (var (0))
  1715. | (S x') => (var (S (plus x' w)))
  1716. end))) (S (plus n w))).
  1717. Apply impE with (substituteFormula LNN
  1718. (addForalls (S w) n
  1719. (impH (FormulasToFormula (0) w n v)
  1720. (subAllFormula LNN B
  1721. [x:nat]
  1722. Cases x of
  1723. 0 => (var (0))
  1724. | (S x') => (var (S (plus x' w)))
  1725. end))) (S (plus n w)) (natToTerm (Snd a))).
  1726. Apply (subWithEquals LNN).
  1727. Apply eqSym.
  1728. Apply Axm; Right; Constructor.
  1729. Rewrite subFormulaId.
  1730. Apply Axm; Left; Right; Constructor.
  1731. Rewrite subAddForallsNice.
  1732. Apply reduceAddForalls.
  1733. Rewrite (subFormulaImp LNN).
  1734. Apply (reduceImp LNN).
  1735. Apply (subFormulaNil LNN).
  1736. Cut (lt (plus n w) (plus (S n) w)).
  1737. Generalize (plus (S n) w).
  1738. Clear H5 H3 g H2.
  1739. Induction v; Unfold not; Intros.
  1740. Simpl in H3.
  1741. Decompose Sum H3.
  1742. Rewrite <- H5 in H2.
  1743. Elim (lt_n_O ? H2).
  1744. Rewrite <- H6 in H2.
  1745. Elim (lt_n_O ? H2).
  1746. Simpl in H3.
  1747. NewInduction (in_app_or H3).
  1748. Simpl in H4.
  1749. NewInduction (freeVarSubFormula3 ? ? ? ? ? H5).
  1750. Elim (le_not_lt n0 O).
  1751. Decompose Record H4.
  1752. Apply H7.
  1753. EApply In_list_remove1.
  1754. Apply H6.
  1755. Apply lt_trans with (plus (S n) w).
  1756. Simpl; Apply lt_O_Sn.
  1757. Auto.
  1758. Induction H6.
  1759. Rewrite <- H6 in H2.
  1760. Elim (lt_n_n ? H2).
  1761. Elim H6.
  1762. Elim Hrecv with n0:=n0.
  1763. Simpl in H4.
  1764. Tauto.
  1765. EApply lt_trans.
  1766. Apply lt_n_Sn.
  1767. Auto.
  1768. Auto.
  1769. Simpl.
  1770. Apply lt_n_Sn.
  1771. EApply iffTrans.
  1772. Apply (subSubAllFormula LNN).
  1773. Apply iffSym.
  1774. EApply iffTrans.
  1775. Apply (subAllSubFormula LNN).
  1776. Replace (subAllFormula LNN B
  1777. [n1:nat]
  1778. (substituteTerm LNN
  1779. Cases n1 of
  1780. 0 => (var (0))
  1781. | (S x') => (var (S (plus x' w)))
  1782. end (plus (S n) w) (natToTerm (Snd a))))
  1783. with (subAllFormula LNN B
  1784. [x:nat]
  1785. Cases (eq_nat_dec (S n) x) of
  1786. (left _) =>
  1787. (subAllTerm LNN (natToTerm (Snd a))
  1788. [x0:nat]
  1789. Cases x0 of
  1790. 0 => (var (0))
  1791. | (S x') => (var (S (plus x' w)))
  1792. end)
  1793. | (right _) =>
  1794. ([x0:nat]
  1795. Cases x0 of
  1796. 0 => (var (0))
  1797. | (S x') => (var (S (plus x' w)))
  1798. end x)
  1799. end).
  1800. Apply iffRefl.
  1801. Apply subAllFormula_ext.
  1802. Intros.
  1803. NewInduction (eq_nat_dec (S n) m).
  1804. Rewrite <- a0.
  1805. Rewrite (subTermVar1 LNN).
  1806. Clear H0.
  1807. NewInduction (Snd a).
  1808. Simpl.
  1809. Reflexivity.
  1810. Simpl.
  1811. Rewrite IHn0.
  1812. Reflexivity.
  1813. NewDestruct m.
  1814. Simpl.
  1815. Reflexivity.
  1816. Rewrite (subTermVar2 LNN).
  1817. Reflexivity.
  1818. Unfold not; Intros; Elim b.
  1819. Apply simpl_plus_l with w.
  1820. Repeat Rewrite (plus_sym w).
  1821. Apply H7.
  1822. Left.
  1823. Rewrite <- (plus_Snm_nSm).
  1824. Apply le_n.
  1825. Intros.
  1826. Elim (closedNatToTerm ? ? H6).
  1827. Apply closedNatToTerm.
  1828. Intros.
  1829. DefinitionTac v' := (vector_rec Formula*(nat->(naryFunc n)) [m:nat][v:(vector ? m)](vector Formula*(naryFunc n) m)
  1830. (Vnil ?)
  1831. [pair:Formula*(nat->(naryFunc n))][m:nat][v:(vector ? m)][rec:(vector Formula*(naryFunc n) m)]
  1832. (Vcons ? ((substituteFormula LNN (Fst pair) (S n) (natToTerm a)),
  1833. (Snd pair a)) m rec)
  1834. ? A).
  1835. Assert (RepresentableHelp n
  1836. (evalComposeFunc n m (FormulasToFuncs n m v') g)
  1837. (addForalls (S w) m
  1838. (impH (FormulasToFormula n w m v')
  1839. (subAllFormula LNN B
  1840. [x:nat]
  1841. Cases x of
  1842. 0 => (var (0))
  1843. | (S x') => (var (S (plus x' w)))
  1844. end)))).
  1845. Unfold composePiFormula in Hrecn.
  1846. Simpl in Hrecn.
  1847. Apply Hrecn.
  1848. EApply le_trans.
  1849. Apply le_n_Sn.
  1850. Auto.
  1851. Clear B g H2.
  1852. Induction A;
  1853. Simpl in v';
  1854. Simpl.
  1855. Auto.
  1856. Split.
  1857. Simpl in H0.
  1858. Induction H0.
  1859. Apply H0.
  1860. Apply HrecA.
  1861. Induction H0.
  1862. Auto.
  1863. Simpl in H1.
  1864. Induction H1.
  1865. Auto.
  1866. Simpl in H1.
  1867. Clear H2 H0 g B.
  1868. Induction A.
  1869. Simpl.
  1870. Auto.
  1871. Simpl.
  1872. Split.
  1873. Simpl in H1.
  1874. Induction H1.
  1875. Intros.
  1876. NewInduction (freeVarSubFormula3 ? ? ? ? ? H2).
  1877. Assert (le v (S n)).
  1878. Apply H0.
  1879. EApply In_list_remove1.
  1880. Apply H3.
  1881. NewInduction (le_lt_or_eq ? ? H4).
  1882. Apply lt_n_Sm_le.
  1883. Auto.
  1884. Elim (In_list_remove2 ? ? ? ? ? H3).
  1885. Auto.
  1886. Elim (closedNatToTerm ? ? H3).
  1887. Apply HrecA.
  1888. Induction H1.
  1889. Auto.
  1890. Auto.
  1891. Unfold composePiFormula.
  1892. Clear Hrecn.
  1893. Apply RepresentableAlternate with (addForalls (S w) m
  1894. (impH (FormulasToFormula n w m v')
  1895. (subAllFormula LNN B
  1896. [x:nat]
  1897. Cases x of
  1898. 0 => (var (0))
  1899. | (S x') => (var (S (plus x' w)))
  1900. end))).
  1901. Rewrite subAddForallsNice.
  1902. Apply reduceAddForalls.
  1903. Rewrite (subFormulaImp LNN).
  1904. Apply (reduceImp LNN).
  1905. Clear H3 H2 H1 H0 g B.
  1906. Induction A.
  1907. Simpl.
  1908. Apply iffSym.
  1909. Apply (subFormulaNil LNN).
  1910. Simpl.
  1911. Unfold not; Intros.
  1912. Decompose Sum H0.
  1913. Discriminate H1.
  1914. Discriminate H2.
  1915. Simpl.
  1916. Rewrite (subFormulaAnd LNN).
  1917. Apply (reduceAnd LNN); [Idtac | Apply HrecA].
  1918. Apply (subFormulaExch LNN).
  1919. Discriminate.
  1920. Apply closedNatToTerm.
  1921. Unfold not; Intros.
  1922. Induction H0.
  1923. Rewrite <- H0 in H.
  1924. Elim (le_not_lt ? ? H).
  1925. Apply le_lt_n_Sm.
  1926. Apply le_plus_r.
  1927. Apply H0.
  1928. Apply iffSym.
  1929. Apply (subFormulaNil LNN).
  1930. Unfold not; Intros.
  1931. Decompose Record (freeVarSubAllFormula1 ? ? ? ? H4).
  1932. NewDestruct x.
  1933. Induction H7.
  1934. Discriminate H5.
  1935. Elim H5.
  1936. Induction H7.
  1937. Rewrite <- H5 in H.
  1938. Elim (le_not_lt ? ? H).
  1939. Apply le_lt_n_Sm.
  1940. Apply le_plus_r.
  1941. Apply H5.
  1942. Right.
  1943. Apply le_lt_n_Sm.
  1944. Auto.
  1945. Intros.
  1946. Elim (closedNatToTerm ? ? H4).
  1947. Apply Representable_ext with (evalComposeFunc n m (FormulasToFuncs n m v') g).
  1948. Clear H3 H2 H1 H0 B.
  1949. Apply extEqualCompose.
  1950. Unfold extEqualVector.
  1951. Clear g.
  1952. Induction A; Simpl.
  1953. Auto.
  1954. Split.
  1955. Apply extEqualRefl.
  1956. Apply HrecA.
  1957. Apply extEqualRefl.
  1958. Apply H3.
  1959. Intros.
  1960. Split.
  1961. Intros.
  1962. Unfold composePiFormula in H4.
  1963. Assert (In v (freeVarFormula LNN
  1964. (impH (FormulasToFormula n w m A)
  1965. (subAllFormula LNN B
  1966. [x:nat]
  1967. Cases x of
  1968. 0 => (var (0))
  1969. | (S x') => (var (plus (S x') w))
  1970. end)))).
  1971. EApply freeVarAddForalls1.
  1972. Apply H4.
  1973. Simpl in H5.
  1974. NewInduction (in_app_or H5).
  1975. Assert (le (plus m (S w)) v)\/(lt v (S w)).
  1976. EApply freeVarAddForalls2.
  1977. Apply H4.
  1978. Clear H5 H4 H3 H1 g B.
  1979. Induction A.
  1980. Simpl in H6.
  1981. Decompose Sum H6.
  1982. Rewrite <- H1.
  1983. Apply le_O_n.
  1984. Rewrite <- H3.
  1985. Apply le_O_n.
  1986. Simpl in H6.
  1987. NewInduction (in_app_or H6).
  1988. Simpl in H2.
  1989. Induction H2.
  1990. NewInduction (freeVarSubFormula3 ? ? ? ? ? H1).
  1991. Apply H2.
  1992. EApply In_list_remove1.
  1993. Apply H4.
  1994. Induction H4.
  1995. Rewrite <- H4 in H7.
  1996. Induction H7.
  1997. Rewrite <- plus_Snm_nSm in H5.
  1998. Simpl in H5.
  1999. Elim (le_Sn_n ? H5).
  2000. Elim (lt_not_le ? ? H5).
  2001. Apply le_n_S.
  2002. Apply le_plus_r.
  2003. Elim H4.
  2004. Apply HrecA; Auto.
  2005. Simpl in H2.
  2006. Tauto.
  2007. Induction H7.
  2008. Left.
  2009. Simpl in H3.
  2010. EApply le_trans.
  2011. Apply le_n_Sn.
  2012. Apply H3.
  2013. Auto.
  2014. Decompose Record (freeVarSubAllFormula1 ? ? ? ? H6).
  2015. NewDestruct x.
  2016. Induction H9.
  2017. Rewrite <- H7.
  2018. Apply le_O_n.
  2019. Elim H7.
  2020. Induction H9.
  2021. Rewrite <- H7.
  2022. Induction H3.
  2023. Assert (le (S n0) m).
  2024. Apply H3.
  2025. Auto.
  2026. NewInduction (freeVarAddForalls2 ? ? ? ? H4).
  2027. Rewrite <- H7 in H11.
  2028. Rewrite <- plus_Snm_nSm in H11.
  2029. Simpl in H11.
  2030. Elim (le_not_lt m n0).
  2031. Apply simpl_le_plus_l with w.
  2032. Repeat Rewrite (plus_sym w).
  2033. Apply le_S_n.
  2034. Auto.
  2035. Apply lt_S_n.
  2036. Apply le_lt_n_Sm.
  2037. Auto.
  2038. Rewrite <- H7 in H11.
  2039. Elim (lt_not_le ? ? H11).
  2040. Apply le_n_S.
  2041. Apply le_plus_r.
  2042. Elim H7.
  2043. Apply H; Auto.
  2044. Qed.
  2045. *)
  2046.  
  2047. Remark boundedCheck :
  2048. forall P : nat -> Prop,
  2049. (forall x : nat, decidable (P x)) ->
  2050. forall c : nat,
  2051. (forall d : nat, d < c -> ~ P d) \/ (exists d : nat, d < c /\ P d).
  2052. Proof.
  2053. intros P H c. induction c as [| c Hrecc].
  2054. + left; intros d H0. lia.
  2055. + destruct (H c) as [e | e].
  2056. - right. exists c. split; auto.
  2057. - destruct Hrecc as [H0 | H0].
  2058. * left. intros d H1. assert (d < c \/ d = c) as H2 by lia. destruct H2.
  2059. ++ eauto.
  2060. ++ congruence.
  2061. * destruct H0 as (x, H0). right. exists x. split; try lia. tauto.
  2062. Qed.
  2063.  
  2064. Remark smallestExists :
  2065. forall P : nat -> Prop,
  2066. (forall x : nat, decidable (P x)) ->
  2067. forall c : nat,
  2068. P c -> exists a : nat, P a /\ (forall b : nat, b < a -> ~ P b).
  2069. Proof.
  2070. assert
  2071. (forall P : nat -> Prop,
  2072. (forall x : nat, decidable (P x)) ->
  2073. forall d c : nat,
  2074. c < d -> P c -> exists a : nat, P a /\ (forall b : nat, b < a -> ~ P b)).
  2075. { intros P H d. induction d as [| d Hrecd].
  2076. + intros c H0 H1. lia.
  2077. + intros c H0 H1. assert (c < d \/ c = d) as H2 by lia. destruct H2.
  2078. - eauto.
  2079. - destruct (boundedCheck P H c).
  2080. * exists c. tauto.
  2081. * destruct H3 as (x, H3). apply (Hrecd x).
  2082. ++ lia.
  2083. ++ tauto. }
  2084. intros P H0 c H1. eapply H.
  2085. + exact H0.
  2086. + exact (lt_n_Sn c).
  2087. + exact H1.
  2088. Qed.
  2089.  
  2090. Definition minimize (A B : Formula) (v x : nat) : Formula :=
  2091. andH A
  2092. (forallH x
  2093. (impH (LT (var x) (var v)) (notH (substituteFormula LNN B v (var x))))).
  2094.  
  2095. Remark minimize1 :
  2096. forall (A B : Formula) (v x : nat),
  2097. v <> x ->
  2098. ~ In x (freeVarFormula LNN B) ->
  2099. forall a : nat,
  2100. SysPrf NN (substituteFormula LNN A v (natToTerm a)) ->
  2101. SysPrf NN (substituteFormula LNN B v (natToTerm a)) ->
  2102. (forall b : nat,
  2103. b < a -> SysPrf NN (notH (substituteFormula LNN A v (natToTerm b)))) ->
  2104. (forall b : nat,
  2105. b < a -> SysPrf NN (notH (substituteFormula LNN B v (natToTerm b)))) ->
  2106. SysPrf NN (iffH (minimize A B v x) (equal (var v) (natToTerm a))).
  2107. Proof.
  2108. intros A B v x H H0 a H1 H2 H3 H4. apply iffI.
  2109. unfold minimize in |- *. apply impI.
  2110. apply
  2111. impE
  2112. with
  2113. (substituteFormula LNN
  2114. (impH (LT (var x) (var v)) (notH (substituteFormula LNN B v (var x))))
  2115. x (natToTerm a)).
  2116. + rewrite (subFormulaImp LNN). rewrite (subFormulaNot LNN).
  2117. apply
  2118. impTrans
  2119. with
  2120. (impH (LT (natToTerm a) (var v))
  2121. (notH (substituteFormula LNN B v (natToTerm a)))).
  2122. - apply iffE1. apply (reduceImp LNN).
  2123. * unfold LT at 2 in |- *. rewrite (subFormulaRelation LNN).
  2124. simpl in |- *. destruct (eq_nat_dec x x) as [e | e]; try lia.
  2125. destruct (eq_nat_dec x v).
  2126. ++ elim H. auto.
  2127. ++ apply iffRefl.
  2128. * apply (reduceNot LNN). apply (subFormulaTrans LNN).
  2129. intro H5. elim H0. eapply In_list_remove1. exact H5.
  2130. - apply impTrans with (notH (LT (natToTerm a) (var v))).
  2131. * apply impI. apply impE with (notH (notH (substituteFormula LNN B v (natToTerm a)))).
  2132. apply cp2.
  2133. ++ apply Axm; right; constructor.
  2134. ++ apply nnI. do 2 apply sysWeaken. exact H2.
  2135. * apply impE with (notH (LT (var v) (natToTerm a))).
  2136. apply
  2137. orE
  2138. with
  2139. (LT (var v) (natToTerm a))
  2140. (orH (equal (var v) (natToTerm a)) (LT (natToTerm a) (var v))).
  2141. ++ apply sysWeaken. apply nn9.
  2142. ++ repeat apply impI.
  2143. apply contradiction with (LT (var v) (natToTerm a)).
  2144. -- apply Axm; left; left; right; constructor.
  2145. -- apply Axm; left; right; constructor.
  2146. ++ apply impI. apply orSys; repeat apply impI.
  2147. -- apply Axm; left; left; right; constructor.
  2148. -- apply contradiction with (LT (natToTerm a) (var v)).
  2149. ** apply Axm; left; left; right; constructor.
  2150. ** apply Axm; right; constructor.
  2151. ++ apply impE with (notH (notH A)). apply cp2.
  2152. -- apply sysWeaken. apply boundedLT. intros n H5.
  2153. rewrite (subFormulaNot LNN). auto.
  2154. -- apply nnI. eapply andE1. apply Axm; right; constructor.
  2155. + apply forallE. eapply andE2. apply Axm; right; constructor.
  2156. + apply impI. unfold minimize in |- *.
  2157. rewrite <-
  2158. (subFormulaId LNN
  2159. (andH A
  2160. (forallH x
  2161. (impH (LT (var x) (var v))
  2162. (notH (substituteFormula LNN B v (var x)))))) v).
  2163. apply
  2164. impE
  2165. with
  2166. (substituteFormula LNN
  2167. (andH A
  2168. (forallH x
  2169. (impH (LT (var x) (var v))
  2170. (notH (substituteFormula LNN B v (var x)))))) v
  2171. (natToTerm a)).
  2172. - apply (subWithEquals LNN). apply eqSym. apply Axm; right; constructor.
  2173. - apply sysWeaken. rewrite (subFormulaAnd LNN). apply andI.
  2174. * auto.
  2175. * rewrite (subFormulaForall LNN). destruct (eq_nat_dec x v) as [e | e]; try congruence.
  2176. destruct (In_dec eq_nat_dec x (freeVarTerm LNN (natToTerm a))) as [e0 | e0].
  2177. ++ elim (closedNatToTerm _ _ e0).
  2178. ++ apply forallI. apply closedNN. rewrite (subFormulaImp LNN).
  2179. unfold LT in |- *. rewrite (subFormulaRelation LNN).
  2180. simpl in |- *. destruct (eq_nat_dec v v) as [e1 | e1]; try congruence.
  2181. -- induction (eq_nat_dec v x) as [e2 | e2]; try congruence.
  2182. apply impI. apply forallE. apply forallI. intro H5.
  2183. destruct H5 as (x0, H5); destruct H5 as (H5, H6).
  2184. destruct H6 as [x0 H6 | x0 H6].
  2185. ** elim closedNN with v. exists x0; auto.
  2186. ** destruct H6. destruct H5 as [H5 | H5]; try congruence.
  2187. fold (freeVarTerm LNN (natToTerm a)) in H5. simpl in H5.
  2188. rewrite <- app_nil_end in H5. elim (closedNatToTerm _ _ H5).
  2189. ** apply impE with (LT (var x) (natToTerm a)).
  2190. +++ apply sysWeaken. apply boundedLT. intros n H5.
  2191. rewrite (subFormulaNot LNN).
  2192. apply impE with (notH (substituteFormula LNN B v (natToTerm n))).
  2193. --- apply cp2. apply iffE1. apply (subFormulaTrans LNN).
  2194. intro H6. elim H0. eapply In_list_remove1. exact H6.
  2195. --- apply H4; auto.
  2196. +++ apply Axm; right; constructor.
  2197. Qed.
  2198.  
  2199. Lemma subFormulaMinimize :
  2200. forall (A B : Formula) (v x z : nat) (s : Term),
  2201. ~ In x (freeVarTerm LNN s) ->
  2202. ~ In v (freeVarTerm LNN s) ->
  2203. x <> z ->
  2204. v <> z ->
  2205. SysPrf NN
  2206. (iffH (substituteFormula LNN (minimize A B v x) z s)
  2207. (minimize (substituteFormula LNN A z s) (substituteFormula LNN B z s) v
  2208. x)).
  2209. Proof.
  2210. intros A B v x z s H H0 H1 H2. unfold minimize in |- *.
  2211. rewrite (subFormulaAnd LNN). rewrite (subFormulaForall LNN).
  2212. destruct (eq_nat_dec x z) as [e | e]; try congruence.
  2213. destruct (In_dec eq_nat_dec x (freeVarTerm LNN s)) as [e0 | e0]; try tauto.
  2214. rewrite (subFormulaImp LNN). unfold LT at 1 in |- *.
  2215. rewrite (subFormulaRelation LNN). simpl in |- *.
  2216. destruct (eq_nat_dec z x); try congruence.
  2217. destruct (eq_nat_dec z v); try congruence.
  2218. rewrite (subFormulaNot LNN).
  2219. repeat first
  2220. [ apply iffRefl
  2221. | apply (reduceAnd LNN)
  2222. | apply (reduceImp LNN)
  2223. | apply (reduceNot LNN)
  2224. | apply (reduceForall LNN); [ apply closedNN |] ].
  2225. apply (subFormulaExch LNN).
  2226. + congruence.
  2227. + simpl in |- *. intro H3. tauto.
  2228. + auto.
  2229. Qed.
  2230.  
  2231. Definition primRecSigmaFormulaHelp (n : nat) (SigA SigB : Formula) : Formula :=
  2232. andH
  2233. (existH 0
  2234. (andH SigA
  2235. (substituteFormula LNN (substituteFormula LNN betaFormula 1 Zero) 2
  2236. (var (S (S n))))))
  2237. (forallH (S (S (S n)))
  2238. (impH (LT (var (S (S (S n)))) (var (S n)))
  2239. (existH 0
  2240. (existH (S n)
  2241. (andH
  2242. (substituteFormula LNN
  2243. (substituteFormula LNN
  2244. (substituteFormula LNN betaFormula 1
  2245. (var (S (S (S n))))) 2
  2246. (var (S (S n)))) 0 (var (S n)))
  2247. (andH
  2248. (substituteFormula LNN SigB (S (S n))
  2249. (var (S (S (S n)))))
  2250. (substituteFormula LNN
  2251. (substituteFormula LNN betaFormula 1
  2252. (Succ (var (S (S (S n)))))) 2
  2253. (var (S (S n)))))))))).
  2254.  
  2255. Definition primRecPiFormulaHelp (n : nat) (SigA SigB : Formula) : Formula :=
  2256. andH
  2257. (forallH 0
  2258. (impH SigA
  2259. (substituteFormula LNN (substituteFormula LNN betaFormula 1 Zero) 2
  2260. (var (S (S n))))))
  2261. (forallH (S (S (S n)))
  2262. (impH (LT (var (S (S (S n)))) (var (S n)))
  2263. (forallH 0
  2264. (forallH (S n)
  2265. (impH
  2266. (substituteFormula LNN
  2267. (substituteFormula LNN
  2268. (substituteFormula LNN betaFormula 1
  2269. (var (S (S (S n))))) 2
  2270. (var (S (S n)))) 0 (var (S n)))
  2271. (impH
  2272. (substituteFormula LNN SigB (S (S n))
  2273. (var (S (S (S n)))))
  2274. (substituteFormula LNN
  2275. (substituteFormula LNN betaFormula 1
  2276. (Succ (var (S (S (S n)))))) 2
  2277. (var (S (S n)))))))))).
  2278.  
  2279. Lemma freeVarPrimRecSigmaFormulaHelp1 :
  2280. forall (n : nat) (A B : Formula) (v : nat),
  2281. In v (freeVarFormula LNN (primRecSigmaFormulaHelp n A B)) ->
  2282. In v (freeVarFormula LNN A) \/
  2283. In v (freeVarFormula LNN B) \/ v = S (S n) \/ v = S n.
  2284. Proof.
  2285. intros n A B v H. unfold primRecSigmaFormulaHelp in H.
  2286. assert
  2287. (forall v : nat,
  2288. In v (freeVarFormula LNN betaFormula) -> v = 0 \/ v = 1 \/ v = 2).
  2289. { intros v0 H0. assert (Representable 2 beta betaFormula).
  2290. apply betaRepresentable. destruct H1 as (H1, H2).
  2291. apply H1 in H0. lia. }
  2292. repeat
  2293. match goal with
  2294. | H:(In v (freeVarFormula LNN (existH ?X1 ?X2))) |- _ =>
  2295. assert (In v (freeVarFormula LNN X2));
  2296. [ eapply In_list_remove1; apply H
  2297. | assert (v <> X1); [ eapply In_list_remove2; apply H | clear H ] ]
  2298. | H:(In v (freeVarFormula LNN (forallH ?X1 ?X2))) |- _ =>
  2299. assert (In v (freeVarFormula LNN X2));
  2300. [ eapply In_list_remove1; apply H
  2301. | assert (v <> X1); [ eapply In_list_remove2; apply H | clear H ] ]
  2302. | H:(In v (list_remove nat eq_nat_dec ?X1 (freeVarFormula LNN ?X2))) |- _ =>
  2303. assert (In v (freeVarFormula LNN X2));
  2304. [ eapply In_list_remove1; apply H
  2305. | assert (v <> X1); [ eapply In_list_remove2; apply H | clear H ] ]
  2306. | H:(In v (freeVarFormula LNN (andH ?X1 ?X2))) |- _ =>
  2307. assert (In v (freeVarFormula LNN X1 ++ freeVarFormula LNN X2));
  2308. [ apply H | clear H ]
  2309. | H:(In v (freeVarFormula LNN (impH ?X1 ?X2))) |- _ =>
  2310. assert (In v (freeVarFormula LNN X1 ++ freeVarFormula LNN X2));
  2311. [ apply H | clear H ]
  2312. | H:(In v (_ ++ _)) |- _ =>
  2313. destruct (in_app_or _ _ _ H); clear H
  2314. | H:(In v (freeVarFormula LNN (substituteFormula LNN ?X1 ?X2 ?X3))) |- _ =>
  2315. induction (freeVarSubFormula3 _ _ _ _ _ H); clear H
  2316. | H:(In v (freeVarFormula LNN (LT ?X1 ?X2))) |- _ =>
  2317. rewrite freeVarLT in H
  2318. | H:(In v (freeVarFormula LNN betaFormula)) |- _ =>
  2319. decompose sum (H0 v H); clear H
  2320. end; try tauto;
  2321. match goal with
  2322. | H:(In v _) |- _ => simpl in H; decompose sum H; clear H
  2323. end; auto;
  2324. try match goal with
  2325. | H:(?X1 = ?X2),H2:(?X2 <> ?X1) |- _ => elim H2; auto
  2326. end; simpl in |- *; try tauto.
  2327. Qed.
  2328.  
  2329. Lemma freeVarPrimRecPiFormulaHelp1 :
  2330. forall (n : nat) (A B : Formula) (v : nat),
  2331. In v (freeVarFormula LNN (primRecPiFormulaHelp n A B)) ->
  2332. In v (freeVarFormula LNN A) \/
  2333. In v (freeVarFormula LNN B) \/ v = S (S n) \/ v = S n.
  2334. Proof.
  2335. intros n A B v H. unfold primRecPiFormulaHelp in H.
  2336. assert
  2337. (forall v : nat,
  2338. In v (freeVarFormula LNN betaFormula) -> v = 0 \/ v = 1 \/ v = 2).
  2339. { intros v0 H0. assert (Representable 2 beta betaFormula).
  2340. apply betaRepresentable.
  2341. destruct H1 as (H1, H2). apply H1 in H0. lia. }
  2342. repeat
  2343. match goal with
  2344. | H:(In v (freeVarFormula LNN (existH ?X1 ?X2))) |- _ =>
  2345. assert (In v (freeVarFormula LNN X2));
  2346. [ eapply In_list_remove1; apply H
  2347. | assert (v <> X1); [ eapply In_list_remove2; apply H | clear H ] ]
  2348. | H:(In v (freeVarFormula LNN (forallH ?X1 ?X2))) |- _ =>
  2349. assert (In v (freeVarFormula LNN X2));
  2350. [ eapply In_list_remove1; apply H
  2351. | assert (v <> X1); [ eapply In_list_remove2; apply H | clear H ] ]
  2352. | H:(In v (list_remove nat eq_nat_dec ?X1 (freeVarFormula LNN ?X2))) |- _ =>
  2353. assert (In v (freeVarFormula LNN X2));
  2354. [ eapply In_list_remove1; apply H
  2355. | assert (v <> X1); [ eapply In_list_remove2; apply H | clear H ] ]
  2356. | H:(In v (freeVarFormula LNN (andH ?X1 ?X2))) |- _ =>
  2357. assert (In v (freeVarFormula LNN X1 ++ freeVarFormula LNN X2));
  2358. [ apply H | clear H ]
  2359. | H:(In v (freeVarFormula LNN (impH ?X1 ?X2))) |- _ =>
  2360. assert (In v (freeVarFormula LNN X1 ++ freeVarFormula LNN X2));
  2361. [ apply H | clear H ]
  2362. | H:(In v (_ ++ _)) |- _ =>
  2363. induction (in_app_or _ _ _ H); clear H
  2364. | H:(In v (freeVarFormula LNN (substituteFormula LNN ?X1 ?X2 ?X3))) |- _ =>
  2365. induction (freeVarSubFormula3 _ _ _ _ _ H); clear H
  2366. | H:(In v (freeVarFormula LNN (LT ?X1 ?X2))) |- _ =>
  2367. rewrite freeVarLT in H
  2368. | H:(In v (freeVarFormula LNN betaFormula)) |- _ =>
  2369. decompose sum (H0 v H); clear H
  2370. end; try tauto;
  2371. match goal with
  2372. | H:(In v _) |- _ => simpl in H; decompose sum H; clear H
  2373. end; auto;
  2374. try match goal with
  2375. | H:(?X1 = ?X2),H2:(?X2 <> ?X1) |- _ => elim H2; auto
  2376. end; simpl in |- *; try tauto.
  2377. Qed.
  2378.  
  2379. Definition primRecSigmaFormula (n : nat) (SigA SigB : Formula) : Formula :=
  2380. existH (S (S n))
  2381. (andH
  2382. (minimize (primRecSigmaFormulaHelp n SigA SigB)
  2383. (primRecPiFormulaHelp n SigA SigB) (S (S n))
  2384. (S (S (S (S n)))))
  2385. (substituteFormula LNN
  2386. (substituteFormula LNN betaFormula 2 (var (S (S n)))) 1
  2387. (var (S n)))).
  2388.  
  2389. Remark notBoundedForall :
  2390. forall (P : nat -> Prop) (b : nat),
  2391. (forall x : nat, decidable (P x)) ->
  2392. ~ (forall n : nat, n < b -> P n) -> exists n : nat, n < b /\ ~ P n.
  2393. Proof.
  2394. intros P b H H0. induction b as [| b Hrecb].
  2395. + elim H0. lia.
  2396. + destruct (H b) as [e | e].
  2397. - assert (~ (forall n : nat, n < b -> P n)).
  2398. { intro H1. elim H0. intros n H2.
  2399. assert (n < b \/ n = b) as H3 by lia. destruct H3.
  2400. + auto.
  2401. + rewrite H3; auto. }
  2402. decompose record (Hrecb H1).
  2403. exists x. split; auto; lia.
  2404. - exists b. split; auto; lia.
  2405. Qed.
  2406.  
  2407.  
  2408. Lemma succ_plus_discr : forall n m : nat, n <> S (m + n).
  2409. Proof.
  2410. lia.
  2411. Qed.
  2412.  
  2413. Remark In_betaFormula_subst_1_2_0 :
  2414. forall (a b c : Term) (v : nat),
  2415. In v
  2416. (freeVarFormula LNN
  2417. (substituteFormula LNN
  2418. (substituteFormula LNN (substituteFormula LNN betaFormula 1 a) 2 b)
  2419. 0 c)) ->
  2420. In v (freeVarTerm LNN a) \/
  2421. In v (freeVarTerm LNN b) \/ In v (freeVarTerm LNN c).
  2422. Proof.
  2423. intros a b c v H. destruct (freeVarSubFormula3 _ _ _ _ _ H) as [H0 | H0].
  2424. + assert
  2425. (In v
  2426. (freeVarFormula LNN
  2427. (substituteFormula LNN (substituteFormula LNN betaFormula 1 a) 2 b))).
  2428. { eapply In_list_remove1; apply H0. }
  2429. destruct (freeVarSubFormula3 _ _ _ _ _ H1) as [H2 | H2].
  2430. - assert (In v (freeVarFormula LNN (substituteFormula LNN betaFormula 1 a))).
  2431. { eapply In_list_remove1; apply H2. }
  2432. destruct (freeVarSubFormula3 _ _ _ _ _ H3) as [H4 | H4].
  2433. * destruct v as [| n].
  2434. ++ elim (In_list_remove2 _ _ _ _ _ H0). reflexivity.
  2435. ++ destruct n as [| n].
  2436. -- elim (In_list_remove2 _ _ _ _ _ H4); reflexivity.
  2437. -- destruct n as [| n].
  2438. ** elim (In_list_remove2 _ _ _ _ _ H2). reflexivity.
  2439. ** elim (le_not_lt (S (S (S n))) 2).
  2440. +++ assert (Representable 2 beta betaFormula).
  2441. { apply betaRepresentable. }
  2442. destruct H5 as (H5, H6). apply H5.
  2443. eapply In_list_remove1. exact H4.
  2444. +++ lia.
  2445. * tauto.
  2446. - tauto.
  2447. + tauto.
  2448. Qed.
  2449.  
  2450. Remark In_betaFormula_subst_1_2 :
  2451. forall (a b : Term) (v : nat),
  2452. In v
  2453. (freeVarFormula LNN
  2454. (substituteFormula LNN (substituteFormula LNN betaFormula 1 a) 2 b)) ->
  2455. In v (freeVarTerm LNN a) \/
  2456. In v (freeVarTerm LNN b) \/ In v (freeVarTerm LNN (var 0)).
  2457. Proof.
  2458. intros a b v H. apply In_betaFormula_subst_1_2_0.
  2459. rewrite (subFormulaId LNN). exact H.
  2460. Qed.
  2461.  
  2462. Remark In_betaFormula_subst_1 :
  2463. forall (a : Term) (v : nat),
  2464. In v (freeVarFormula LNN (substituteFormula LNN betaFormula 1 a)) ->
  2465. In v (freeVarTerm LNN a) \/
  2466. In v (freeVarTerm LNN (var 2)) \/ In v (freeVarTerm LNN (var 0)).
  2467. Proof.
  2468. intros a v H. apply In_betaFormula_subst_1_2.
  2469. rewrite (subFormulaId LNN). exact H.
  2470. Qed.
  2471.  
  2472. Remark In_betaFormula :
  2473. forall v : nat,
  2474. In v (freeVarFormula LNN betaFormula) ->
  2475. In v (freeVarTerm LNN (var 1)) \/
  2476. In v (freeVarTerm LNN (var 2)) \/ In v (freeVarTerm LNN (var 0)).
  2477. Proof.
  2478. intros v H. apply In_betaFormula_subst_1.
  2479. rewrite (subFormulaId LNN). exact H.
  2480. Qed.
  2481.  
  2482. Remark In_betaFormula_subst_2 :
  2483. forall (a : Term) (v : nat),
  2484. In v (freeVarFormula LNN (substituteFormula LNN betaFormula 2 a)) ->
  2485. In v (freeVarTerm LNN a) \/
  2486. In v (freeVarTerm LNN (var 1)) \/ In v (freeVarTerm LNN (var 0)).
  2487. Proof.
  2488. intros a v H. rewrite <- (subFormulaId LNN betaFormula 1) in H.
  2489. decompose sum (In_betaFormula_subst_1_2 _ _ _ H); tauto.
  2490. Qed.
  2491.  
  2492. Remark In_betaFormula_subst_2_1 :
  2493. forall (a b : Term) (v : nat),
  2494. In v
  2495. (freeVarFormula LNN
  2496. (substituteFormula LNN (substituteFormula LNN betaFormula 2 a) 1 b)) ->
  2497. In v (freeVarTerm LNN a) \/
  2498. In v (freeVarTerm LNN b) \/ In v (freeVarTerm LNN (var 0)).
  2499. Proof.
  2500. intros a b v H. destruct (freeVarSubFormula3 _ _ _ _ _ H) as [H0 | H0].
  2501. + assert (In v (freeVarFormula LNN (substituteFormula LNN betaFormula 2 a))).
  2502. { eapply In_list_remove1. apply H0. }
  2503. decompose sum (In_betaFormula_subst_2 _ _ H1); try tauto.
  2504. destruct H3 as [H2 | H2].
  2505. elim (In_list_remove2 _ _ _ _ _ H0).
  2506. symmetry in |- *; assumption.
  2507. elim H2.
  2508. + tauto.
  2509. Qed.
  2510.  
  2511. Ltac PRsolveFV A B n :=
  2512. unfold existH, forallH, not in |- *; intros;
  2513. repeat
  2514. match goal with
  2515. | H:(_ = _) |- _ => discriminate H
  2516. | H:(?X1 <> ?X1) |- _ => elim H; reflexivity
  2517. | H:(?X1 = S ?X1) |- _ => elim (n_Sn _ H)
  2518. | H:(S ?X1 = ?X1) |- _ =>
  2519. elim (n_Sn X1); symmetry in |- *; apply H
  2520. | H:(?X1 = S (S ?X1)) |- _ => elim (n_SSn _ H)
  2521. | H:(S (S ?X1) = ?X1) |- _ =>
  2522. elim (n_SSn X1); symmetry in |- *; apply H
  2523. | H:(?X1 = S (S (S ?X1))) |- _ =>
  2524. elim (n_SSSn _ H)
  2525. | H:(S (S (S ?X1)) = ?X1) |- _ =>
  2526. elim (n_SSSn X1); symmetry in |- *; apply H
  2527. | H:(In ?X3
  2528. (freeVarFormula LNN
  2529. (substituteFormula LNN
  2530. (substituteFormula LNN
  2531. (substituteFormula LNN betaFormula 1 _) 2 _) 0 _))) |- _
  2532. =>
  2533. decompose sum (In_betaFormula_subst_1_2_0 _ _ _ _ H); clear H
  2534. | H:(In ?X3
  2535. (freeVarFormula LNN
  2536. (substituteFormula LNN (substituteFormula LNN betaFormula 1 _)
  2537. 2 _))) |- _ =>
  2538. decompose sum (In_betaFormula_subst_1_2 _ _ _ H); clear H
  2539. | H:(In ?X3 (freeVarFormula LNN (substituteFormula LNN betaFormula 1 _)))
  2540. |- _ =>
  2541. decompose sum (In_betaFormula_subst_1 _ _ H); clear H
  2542. | H:(In ?X3 (freeVarFormula LNN betaFormula)) |- _ =>
  2543. decompose sum (In_betaFormula _ H); clear H
  2544. | H:(In ?X3
  2545. (freeVarFormula LNN
  2546. (substituteFormula LNN (substituteFormula LNN betaFormula 2 _)
  2547. 1 _))) |- _ =>
  2548. decompose sum (In_betaFormula_subst_2_1 _ _ _ H); clear H
  2549. | H:(In ?X3 (freeVarFormula LNN (substituteFormula LNN betaFormula 2 _)))
  2550. |- _ =>
  2551. decompose sum (In_betaFormula_subst_2 _ _ H);
  2552. clear H
  2553. (*
  2554. Match Context With
  2555. *)
  2556. | H:(In ?X3 (freeVarFormula LNN (fol.existH LNN ?X1 ?X2))) |- _ =>
  2557. assert
  2558. (In X3 (list_remove nat eq_nat_dec X1 (freeVarFormula LNN X2)));
  2559. [ apply H | clear H ]
  2560. | H:(In ?X3 (freeVarFormula LNN (fol.forallH LNN ?X1 ?X2))) |- _ =>
  2561. assert
  2562. (In X3 (list_remove nat eq_nat_dec X1 (freeVarFormula LNN X2)));
  2563. [ apply H | clear H ]
  2564. |
  2565. (*
  2566. .
  2567. *)
  2568. H:(In ?X3 (list_remove nat eq_nat_dec ?X1 (freeVarFormula LNN ?X2))) |- _
  2569. =>
  2570. assert (In X3 (freeVarFormula LNN X2));
  2571. [ eapply In_list_remove1; apply H
  2572. | assert (X3 <> X1); [ eapply In_list_remove2; apply H | clear H ] ]
  2573. | H:(In ?X3 (freeVarFormula LNN (fol.andH LNN ?X1 ?X2))) |- _ =>
  2574. assert (In X3 (freeVarFormula LNN X1 ++ freeVarFormula LNN X2));
  2575. [ apply H | clear H ]
  2576. | H:(In ?X3 (freeVarFormula LNN (fol.impH LNN ?X1 ?X2))) |- _ =>
  2577. assert (In X3 (freeVarFormula LNN X1 ++ freeVarFormula LNN X2));
  2578. [ apply H | clear H ]
  2579. | H:(In ?X3 (freeVarFormula LNN (fol.notH LNN ?X1))) |- _ =>
  2580. assert (In X3 (freeVarFormula LNN X1)); [ apply H | clear H ]
  2581. | H:(In _ (freeVarFormula LNN (primRecPiFormulaHelp _ _ _))) |- _ =>
  2582. decompose sum (freeVarPrimRecPiFormulaHelp1 _ _ _ _ H); clear H
  2583. | J:(In ?X3 (freeVarFormula LNN A)),H:(forall v : nat,
  2584. In v (freeVarFormula LNN A) ->
  2585. v <= S n) |- _ =>
  2586. elim (le_not_lt X3 (S n));
  2587. [ apply H; apply J | clear J; repeat apply lt_n_Sn || apply lt_S ]
  2588. | H:(In ?X3 (freeVarFormula LNN B)),H0:(forall v : nat,
  2589. In v (freeVarFormula LNN B) ->
  2590. v <= S (S (S n))) |- _ =>
  2591. elim (le_not_lt X3 (S (S (S n))));
  2592. [ apply H0; apply H | clear H; repeat apply lt_n_Sn || apply lt_S ]
  2593. | H:(In _ (_ ++ _)) |- _ =>
  2594. induction (in_app_or _ _ _ H); clear H
  2595. | H:(In _ (freeVarFormula LNN (substituteFormula LNN ?X1 ?X2 ?X3))) |- _
  2596. =>
  2597. induction (freeVarSubFormula3 _ _ _ _ _ H); clear H
  2598. | H:(In _ (freeVarFormula LNN (LT ?X1 ?X2))) |- _ =>
  2599. rewrite freeVarLT in H
  2600. | H:(In _ (freeVarTerm LNN (natToTerm _))) |- _ =>
  2601. elim (closedNatToTerm _ _ H)
  2602. | H:(In _ (freeVarTerm LNN Zero)) |- _ =>
  2603. elim H
  2604. | H:(In _ (freeVarTerm LNN (Succ _))) |- _ =>
  2605. rewrite freeVarSucc in H
  2606. | H:(In _ (freeVarTerm LNN (var _))) |- _ =>
  2607. simpl in H; decompose sum H; clear H
  2608. | H:(In _ (freeVarTerm LNN (fol.var LNN _))) |- _ =>
  2609. simpl in H; decompose sum H; clear H
  2610. end.
  2611.  
  2612. (* start *)
  2613. Remark primRecSigmaRepresentable :
  2614. forall (n : nat) (A : Formula) (g : naryFunc n),
  2615. Representable n g A ->
  2616. forall (B : Formula) (h : naryFunc (S (S n))),
  2617. Representable (S (S n)) h B ->
  2618. Representable (S n) (evalPrimRecFunc n g h) (primRecSigmaFormula n A B).
  2619. Proof.
  2620. assert
  2621. (forall (n : nat) (A : Formula) (g : naryFunc n),
  2622. Representable n g A ->
  2623. forall (B : Formula) (h : naryFunc (S (S n))),
  2624. Representable (S (S n)) h B ->
  2625. RepresentableHelp (S n) (evalPrimRecFunc n g h) (primRecSigmaFormula n A B)).
  2626. { intros n A g H B h H0. induction n as [| n Hrecn].
  2627. + simpl; intros a. unfold primRecSigmaFormula. rewrite (subFormulaExist LNN).
  2628. induction (In_dec eq_nat_dec 2 (freeVarTerm LNN (natToTerm a))) as [a0 | b].
  2629. - elim (closedNatToTerm _ _ a0).
  2630. - simpl. clear b. assert (repBeta : Representable 2 beta betaFormula).
  2631. { apply betaRepresentable. }
  2632. rewrite (subFormulaAnd LNN). repeat rewrite (subFormulaId LNN).
  2633. apply
  2634. iffTrans
  2635. with
  2636. (fol.existH LNN 2
  2637. (fol.andH LNN
  2638. (minimize
  2639. (substituteFormula LNN (primRecSigmaFormulaHelp 0 A B) 1
  2640. (natToTerm a))
  2641. (substituteFormula LNN (primRecPiFormulaHelp 0 A B) 1
  2642. (natToTerm a)) 2 4)
  2643. (substituteFormula LNN betaFormula 1 (natToTerm a)))).
  2644. * apply (reduceExist LNN).
  2645. ++ apply closedNN.
  2646. ++ apply (reduceAnd LNN).
  2647. -- apply subFormulaMinimize; first [ discriminate | apply closedNatToTerm ].
  2648. -- apply iffRefl.
  2649. * set (f := evalPrimRecFunc 0 g h) in *. destruct (betaTheorem1 (S a) f) as [x p]. destruct x as (a0, b). simpl in p.
  2650. set (P := fun c : nat => forall z : nat, z < S a -> f z = beta c z) in *.
  2651. assert (forall c : nat, decidable (P c)).
  2652. { intros c. unfold decidable, P. set (Q := fun z : nat => f z <> beta c z) in *.
  2653. assert (forall z : nat, decidable (Q z)).
  2654. { intros. unfold decidable, Q. destruct (eq_nat_dec (f z) (beta c z)); auto. }
  2655. destruct (boundedCheck Q H1 (S a)) as [H2 | H2].
  2656. + left. unfold Q in H2. intros z H3. destruct (eq_nat_dec (f z) (beta c z)).
  2657. - auto.
  2658. - elim (H2 z); auto.
  2659. + right. intro H3. destruct H2 as (x, H2). destruct H2 as (H2, H4). elim H4. apply H3; auto. }
  2660. induction (smallestExists P H1 (cPair b a0)).
  2661. ++ destruct H2 as (H2, H3). clear H1 p b a0.
  2662. apply
  2663. iffTrans
  2664. with
  2665. (fol.existH LNN 2
  2666. (fol.andH LNN (equal (var 2) (natToTerm x))
  2667. (substituteFormula LNN betaFormula 1 (natToTerm a)))).
  2668. -- apply (reduceExist LNN).
  2669. ** apply closedNN.
  2670. ** apply (reduceAnd LNN).
  2671. +++ assert
  2672. (subExistSpecial :
  2673. forall (F : Formula) (a b c : nat),
  2674. b <> c ->
  2675. substituteFormula LNN (existH b F) c (natToTerm a) =
  2676. existH b (substituteFormula LNN F c (natToTerm a))).
  2677. { intros F a0 b c H1. rewrite (subFormulaExist LNN). destruct (eq_nat_dec b c) as [e | e].
  2678. + elim H1. auto.
  2679. + destruct (In_dec eq_nat_dec b (freeVarTerm LNN (natToTerm a0))) as [H4 | H4].
  2680. - elim (closedNatToTerm _ _ H4).
  2681. - reflexivity. }
  2682. assert
  2683. (subForallSpecial :
  2684. forall (F : Formula) (a b c : nat),
  2685. b <> c ->
  2686. substituteFormula LNN (forallH b F) c (natToTerm a) =
  2687. forallH b (substituteFormula LNN F c (natToTerm a))).
  2688. { intros F a0 b c H1. rewrite (subFormulaForall LNN). destruct (eq_nat_dec b c) as [e | e].
  2689. + elim H1. auto.
  2690. + destruct (In_dec eq_nat_dec b (freeVarTerm LNN (natToTerm a0))) as [e0 | e0].
  2691. - elim (closedNatToTerm _ _ e0).
  2692. - reflexivity. }
  2693. apply minimize1.
  2694. --- discriminate.
  2695. --- intro H1. destruct (freeVarSubFormula3 _ _ _ _ _ H1) as [H4 | H4].
  2696. *** assert (In 4 (freeVarFormula LNN (primRecPiFormulaHelp 0 A B))).
  2697. { eapply In_list_remove1. apply H4. }
  2698. decompose sum (freeVarPrimRecPiFormulaHelp1 _ _ _ _ H5).
  2699. ++++ destruct H as (H, H7). elim (le_not_lt 4 0).
  2700. ---- apply H. apply H6.
  2701. ---- repeat constructor.
  2702. ++++ destruct H0 as (H0, H6). elim (le_not_lt 4 2).
  2703. ---- apply H0. apply H7.
  2704. ---- repeat constructor.
  2705. ++++ discriminate H6.
  2706. ++++ discriminate H6.
  2707. *** elim (closedNatToTerm _ _ H4).
  2708. --- unfold primRecSigmaFormulaHelp.
  2709. repeat first
  2710. [ rewrite subExistSpecial; [| discriminate ]
  2711. | rewrite subForallSpecial; [| discriminate ]
  2712. | rewrite (subFormulaAnd LNN)
  2713. | rewrite (subFormulaImp LNN) ].
  2714. rewrite (subFormulaExist LNN). simpl.
  2715. repeat first
  2716. [ rewrite subExistSpecial; [| discriminate ]
  2717. | rewrite subForallSpecial; [| discriminate ]
  2718. | rewrite (subFormulaAnd LNN)
  2719. | rewrite (subFormulaImp LNN) ].
  2720. apply andI.
  2721. *** apply existI with (natToTerm (f 0)). rewrite (subFormulaAnd LNN). apply andI.
  2722. ++++ unfold f, evalPrimRecFunc. destruct H as (H, H1). simpl in H1.
  2723. apply impE with (substituteFormula LNN A 0 (natToTerm g)).
  2724. ---- apply iffE2. apply (reduceSub LNN).
  2725. **** apply closedNN.
  2726. **** apply iffTrans with (substituteFormula LNN A 2 (natToTerm x)).
  2727. apply (reduceSub LNN).
  2728. { apply closedNN. }
  2729. { apply (subFormulaNil LNN). intro H4. elim (le_not_lt 1 0).
  2730. + apply H; auto.
  2731. + auto. }
  2732. { apply (subFormulaNil LNN). intro H4. elim (le_not_lt 2 0).
  2733. + apply H; auto.
  2734. + auto. }
  2735. ---- apply
  2736. impE
  2737. with (substituteFormula LNN (equal (var 0) (natToTerm g)) 0 (natToTerm g)).
  2738. **** apply iffE2. apply (reduceSub LNN).
  2739. { apply closedNN. }
  2740. { auto. }
  2741. **** rewrite (subFormulaEqual LNN). simpl. rewrite (subTermNil LNN).
  2742. { apply eqRefl. }
  2743. { apply closedNatToTerm. }
  2744. ++++ destruct repBeta as (H1, H4). simpl in H4. rewrite (subFormulaId LNN).
  2745. apply
  2746. impE
  2747. with
  2748. (substituteFormula LNN
  2749. (substituteFormula LNN (substituteFormula LNN betaFormula 1 Zero) 2
  2750. (natToTerm x)) 0 (natToTerm (f 0))).
  2751. ---- apply iffE2. apply (reduceSub LNN).
  2752. **** apply closedNN.
  2753. **** apply (reduceSub LNN).
  2754. { apply closedNN. }
  2755. { apply (subFormulaNil LNN). intro H5.
  2756. destruct (freeVarSubFormula3 _ _ _ _ _ H5) as [H6 | H6].
  2757. + elim (In_list_remove2 _ _ _ _ _ H6). reflexivity.
  2758. + elim H6. }
  2759. ---- apply
  2760. impE
  2761. with
  2762. (substituteFormula LNN (equal (var 0) (natToTerm (beta x 0))) 0
  2763. (natToTerm (f 0))).
  2764. **** apply iffE2. apply (reduceSub LNN).
  2765. { apply closedNN. }
  2766. { apply
  2767. iffTrans
  2768. with
  2769. (substituteFormula LNN
  2770. (substituteFormula LNN betaFormula 2 (natToTerm x)) 1
  2771. (natToTerm 0)).
  2772. + apply (subFormulaExch LNN).
  2773. - discriminate.
  2774. - apply closedNatToTerm.
  2775. - apply closedNatToTerm.
  2776. + apply H4. }
  2777. **** rewrite (subFormulaEqual LNN). simpl. rewrite (subTermNil LNN).
  2778. { rewrite H2. apply eqRefl. apply lt_O_Sn. }
  2779. { apply closedNatToTerm. }
  2780. *** apply forallI.
  2781. ++++ apply closedNN.
  2782. ++++ apply impTrans with (LT (var 3) (natToTerm a)).
  2783. ---- unfold LT at 1. repeat rewrite (subFormulaRelation LNN). simpl.
  2784. rewrite (subTermNil LNN).
  2785. **** apply impRefl.
  2786. **** apply closedNatToTerm.
  2787. ---- apply boundedLT. intros n H1. repeat rewrite (subFormulaId LNN).
  2788. repeat first
  2789. [ rewrite subExistSpecial; [| discriminate ]
  2790. | rewrite subForallSpecial; [| discriminate ]
  2791. | rewrite (subFormulaAnd LNN)
  2792. | rewrite (subFormulaImp LNN) ].
  2793. apply existI with (natToTerm (f (S n))).
  2794. repeat first
  2795. [ rewrite subExistSpecial; [| discriminate ]
  2796. | rewrite subForallSpecial; [| discriminate ]
  2797. | rewrite (subFormulaAnd LNN)
  2798. | rewrite (subFormulaImp LNN) ].
  2799. apply existI with (natToTerm (f n)).
  2800. repeat first
  2801. [ rewrite subExistSpecial; [| discriminate ]
  2802. | rewrite subForallSpecial; [| discriminate ]
  2803. | rewrite (subFormulaAnd LNN)
  2804. | rewrite (subFormulaImp LNN) ].
  2805. apply andI.
  2806. **** destruct repBeta as (H4, H5). simpl in H5.
  2807. apply
  2808. impE
  2809. with
  2810. (substituteFormula LNN
  2811. (substituteFormula LNN
  2812. (substituteFormula LNN
  2813. (substituteFormula LNN
  2814. (substituteFormula LNN
  2815. (substituteFormula LNN betaFormula 1 (var 3)) 2
  2816. (natToTerm x)) 0 (var 1)) 3 (natToTerm n)) 0
  2817. (natToTerm (f (S n)))) 1 (natToTerm (f n))).
  2818. { apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  2819. apply (subFormulaExch LNN).
  2820. + discriminate.
  2821. + apply closedNatToTerm.
  2822. + intro H6. induction H6 as [H6 | H6].
  2823. - discriminate H6.
  2824. - elim H6. }
  2825. { apply
  2826. impE
  2827. with
  2828. (substituteFormula LNN
  2829. (substituteFormula LNN
  2830. (substituteFormula LNN
  2831. (substituteFormula LNN
  2832. (substituteFormula LNN
  2833. (substituteFormula LNN betaFormula 1 (var 3)) 2
  2834. (natToTerm x)) 3 (natToTerm n)) 0
  2835. (var 1)) 0 (natToTerm (f (S n)))) 1 (natToTerm (f n))).
  2836. + apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  2837. apply (subFormulaExch LNN).
  2838. - discriminate.
  2839. - apply closedNatToTerm.
  2840. - intro H6. destruct H6 as [H6 | H6].
  2841. * discriminate H6.
  2842. * elim H6.
  2843. + apply
  2844. impE
  2845. with
  2846. (substituteFormula LNN
  2847. (substituteFormula LNN
  2848. (substituteFormula LNN
  2849. (substituteFormula LNN
  2850. (substituteFormula LNN betaFormula 1 (var 3)) 2
  2851. (natToTerm x)) 3 (natToTerm n)) 0 (var 1)) 1
  2852. (natToTerm (f n))).
  2853. - apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  2854. apply (subFormulaNil LNN). intro H6.
  2855. destruct (freeVarSubFormula3 _ _ _ _ _ H6) as [H7 | H7].
  2856. * elim (In_list_remove2 _ _ _ _ _ H7). reflexivity.
  2857. * destruct H7 as [H7 | H7].
  2858. ++ discriminate H7.
  2859. ++ elim H7.
  2860. - apply
  2861. impE
  2862. with
  2863. (substituteFormula LNN
  2864. (substituteFormula LNN
  2865. (substituteFormula LNN
  2866. (substituteFormula LNN
  2867. (substituteFormula LNN betaFormula 2 (natToTerm x)) 1
  2868. (var 3)) 3 (natToTerm n)) 0 (var 1)) 1
  2869. (natToTerm (f n))).
  2870. * apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  2871. apply (subFormulaExch LNN).
  2872. ++ discriminate.
  2873. ++ intro H6. destruct H6 as [H6 | H6].
  2874. -- discriminate H6.
  2875. -- elim H6.
  2876. ++ apply closedNatToTerm.
  2877. * apply
  2878. impE
  2879. with
  2880. (substituteFormula LNN
  2881. (substituteFormula LNN
  2882. (substituteFormula LNN
  2883. (substituteFormula LNN betaFormula 2 (natToTerm x)) 1
  2884. (natToTerm n)) 0 (var 1)) 1 (natToTerm (f n))).
  2885. ++ apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  2886. apply (subFormulaTrans LNN). intro H6.
  2887. assert
  2888. (In 3
  2889. (freeVarFormula LNN (substituteFormula LNN betaFormula 2 (natToTerm x)))).
  2890. { eapply In_list_remove1. apply H6. }
  2891. destruct (freeVarSubFormula3 _ _ _ _ _ H7) as [H8 | H8].
  2892. -- elim (le_not_lt 3 2).
  2893. ** apply H4. eapply In_list_remove1. apply H8.
  2894. ** repeat constructor.
  2895. -- elim (closedNatToTerm _ _ H8).
  2896. ++ apply
  2897. impE
  2898. with
  2899. (substituteFormula LNN
  2900. (substituteFormula LNN (equal (var 0) (natToTerm (beta x n))) 0
  2901. (var 1)) 1 (natToTerm (f n))).
  2902. -- apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  2903. apply H5.
  2904. -- repeat rewrite (subFormulaEqual LNN). simpl.
  2905. repeat rewrite (subTermNil LNN (natToTerm (beta x n))).
  2906. ** rewrite H2. apply eqRefl. apply lt_S. apply H1.
  2907. ** apply closedNatToTerm.
  2908. ** apply closedNatToTerm. }
  2909. **** apply andI.
  2910. { destruct H0 as (H0, H4). simpl in H4.
  2911. apply
  2912. impE
  2913. with
  2914. (substituteFormula LNN
  2915. (substituteFormula LNN
  2916. (substituteFormula LNN (substituteFormula LNN B 2 (var 3)) 3
  2917. (natToTerm n)) 0 (natToTerm (f (S n)))) 1
  2918. (natToTerm (f n))).
  2919. + apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  2920. apply (subFormulaNil LNN). intro H5.
  2921. destruct (freeVarSubFormula3 _ _ _ _ _ H5) as [H6 | [H6 | H6]].
  2922. - elim (In_list_remove2 _ _ _ _ _ H6). reflexivity.
  2923. - discriminate H6.
  2924. - elim H6.
  2925. + apply
  2926. impE
  2927. with
  2928. (substituteFormula LNN
  2929. (substituteFormula LNN (substituteFormula LNN B 2 (natToTerm n)) 0
  2930. (natToTerm (f (S n)))) 1 (natToTerm (f n))).
  2931. - apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  2932. apply (subFormulaTrans LNN). intro H5. elim (le_not_lt 3 2).
  2933. * apply H0. eapply In_list_remove1. apply H5.
  2934. * repeat constructor.
  2935. - apply
  2936. impE
  2937. with
  2938. (substituteFormula LNN
  2939. (substituteFormula LNN (substituteFormula LNN B 2 (natToTerm n)) 1
  2940. (natToTerm (f n))) 0 (natToTerm (f (S n)))).
  2941. * apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  2942. apply (subFormulaExch LNN).
  2943. ++ discriminate.
  2944. ++ apply closedNatToTerm.
  2945. ++ apply closedNatToTerm.
  2946. * apply
  2947. impE
  2948. with
  2949. (substituteFormula LNN (equal (var 0) (natToTerm (h n (f n)))) 0
  2950. (natToTerm (f (S n)))).
  2951. ++ apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  2952. apply H4.
  2953. ++ rewrite (subFormulaEqual LNN). simpl. rewrite (subTermNil LNN).
  2954. -- unfold f. simpl. apply eqRefl.
  2955. -- apply closedNatToTerm. }
  2956. { apply
  2957. impE
  2958. with
  2959. (substituteFormula LNN
  2960. (substituteFormula LNN
  2961. (substituteFormula LNN
  2962. (substituteFormula LNN
  2963. (substituteFormula LNN betaFormula 2 (natToTerm x)) 1
  2964. (Succ (var 3))) 3 (natToTerm n)) 0
  2965. (natToTerm (f (S n)))) 1 (natToTerm (f n))).
  2966. + apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  2967. apply (subFormulaExch LNN).
  2968. - discriminate.
  2969. - simpl. intro H4. lia.
  2970. - apply closedNatToTerm.
  2971. + apply
  2972. impE
  2973. with
  2974. (substituteFormula LNN
  2975. (substituteFormula LNN
  2976. (substituteFormula LNN
  2977. (substituteFormula LNN
  2978. (substituteFormula LNN betaFormula 2 (natToTerm x)) 3
  2979. (natToTerm n)) 1 (natToTerm (S n))) 0
  2980. (natToTerm (f (S n)))) 1 (natToTerm (f n))).
  2981. - apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  2982. replace (natToTerm (S n)) with
  2983. (substituteTerm LNN (Succ (var 3)) 3 (natToTerm n)).
  2984. * apply (subSubFormula LNN).
  2985. ++ discriminate.
  2986. ++ apply closedNatToTerm.
  2987. * simpl. reflexivity.
  2988. - destruct repBeta as (H4, H5).
  2989. apply
  2990. impE
  2991. with
  2992. (substituteFormula LNN
  2993. (substituteFormula LNN
  2994. (substituteFormula LNN
  2995. (substituteFormula LNN betaFormula 2 (natToTerm x)) 1
  2996. (natToTerm (S n))) 0 (natToTerm (f (S n)))) 1
  2997. (natToTerm (f n))).
  2998. * apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  2999. apply (subFormulaNil LNN). intro H6.
  3000. destruct (freeVarSubFormula3 _ _ _ _ _ H6) as [H7 | H7].
  3001. ++ elim (le_not_lt 3 2).
  3002. -- apply H4. eapply In_list_remove1. apply H7.
  3003. -- repeat constructor.
  3004. ++ elim (closedNatToTerm _ _ H7).
  3005. * simpl in H5.
  3006. apply
  3007. impE
  3008. with
  3009. (substituteFormula LNN
  3010. (substituteFormula LNN (equal (var 0) (natToTerm (beta x (S n)))) 0
  3011. (natToTerm (f (S n)))) 1 (natToTerm (f n))).
  3012. ++ apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3013. apply H5.
  3014. ++ repeat rewrite (subFormulaEqual LNN). simpl.
  3015. repeat
  3016. (rewrite (subTermNil LNN (natToTerm (beta x (S n))));
  3017. [| apply closedNatToTerm ]).
  3018. rewrite (subTermNil LNN).
  3019. -- rewrite H2.
  3020. ** apply eqRefl.
  3021. ** apply lt_n_S. apply H1.
  3022. -- apply closedNatToTerm. }
  3023. --- unfold primRecPiFormulaHelp.
  3024. repeat first
  3025. [ rewrite subExistSpecial; [| discriminate ]
  3026. | rewrite subForallSpecial; [| discriminate ]
  3027. | rewrite (subFormulaAnd LNN)
  3028. | rewrite (subFormulaImp LNN) ].
  3029. rewrite (subFormulaForall LNN). simpl.
  3030. repeat first
  3031. [ rewrite subExistSpecial; [| discriminate ]
  3032. | rewrite subForallSpecial; [| discriminate ]
  3033. | rewrite (subFormulaAnd LNN)
  3034. | rewrite (subFormulaImp LNN) ].
  3035. apply andI.
  3036. *** apply forallI.
  3037. ++++ apply closedNN.
  3038. ++++ destruct H as (H, H1). simpl in H1.
  3039. apply
  3040. impTrans
  3041. with
  3042. (substituteFormula LNN
  3043. (substituteFormula LNN (equal (var 0) (natToTerm g)) 1 (natToTerm a))
  3044. 2 (natToTerm x)).
  3045. ---- apply iffE1. apply (reduceSub LNN).
  3046. **** apply closedNN.
  3047. **** apply (reduceSub LNN).
  3048. { apply closedNN. }
  3049. { apply H1. }
  3050. ---- repeat rewrite (subFormulaEqual LNN). simpl.
  3051. repeat
  3052. (rewrite (subTermNil LNN (natToTerm g)); [| apply closedNatToTerm ]).
  3053. apply impI.
  3054. rewrite <-
  3055. (subFormulaId LNN
  3056. (substituteFormula LNN
  3057. (substituteFormula LNN
  3058. (substituteFormula LNN (substituteFormula LNN betaFormula 1 Zero) 2
  3059. (var 2)) 1 (natToTerm a)) 2 (natToTerm x)) 0).
  3060. apply
  3061. impE
  3062. with
  3063. (substituteFormula LNN
  3064. (substituteFormula LNN
  3065. (substituteFormula LNN
  3066. (substituteFormula LNN
  3067. (substituteFormula LNN betaFormula 1 Zero) 2
  3068. (var 2)) 1 (natToTerm a)) 2 (natToTerm x)) 0
  3069. (natToTerm g)).
  3070. **** apply (subWithEquals LNN). apply eqSym. apply Axm; right; constructor.
  3071. **** apply sysWeaken. clear H1. destruct repBeta as (H1, H4). simpl in H4.
  3072. rewrite (subFormulaId LNN).
  3073. apply
  3074. impE
  3075. with
  3076. (substituteFormula LNN
  3077. (substituteFormula LNN (substituteFormula LNN betaFormula 1 Zero) 2
  3078. (natToTerm x)) 0 (natToTerm (f 0))).
  3079. { apply iffE2. apply (reduceSub LNN).
  3080. + apply closedNN.
  3081. + apply (reduceSub LNN). apply closedNN. apply (subFormulaNil LNN).
  3082. intro H5. destruct (freeVarSubFormula3 _ _ _ _ _ H5) as [H6 | H6].
  3083. - elim (In_list_remove2 _ _ _ _ _ H6). reflexivity.
  3084. - elim H6. }
  3085. { apply
  3086. impE
  3087. with
  3088. (substituteFormula LNN (equal (var 0) (natToTerm (beta x 0))) 0
  3089. (natToTerm (f 0))).
  3090. + apply iffE2. apply (reduceSub LNN).
  3091. - apply closedNN.
  3092. - apply
  3093. iffTrans
  3094. with
  3095. (substituteFormula LNN
  3096. (substituteFormula LNN betaFormula 2 (natToTerm x)) 1
  3097. (natToTerm 0)).
  3098. * apply (subFormulaExch LNN).
  3099. ++ discriminate.
  3100. ++ apply closedNatToTerm.
  3101. ++ apply closedNatToTerm.
  3102. * apply H4.
  3103. + rewrite (subFormulaEqual LNN). simpl. rewrite (subTermNil LNN).
  3104. - rewrite H2. apply eqRefl. apply lt_O_Sn.
  3105. - apply closedNatToTerm. }
  3106. *** apply forallI.
  3107. ++++ apply closedNN.
  3108. ++++ apply impTrans with (LT (var 3) (natToTerm a)).
  3109. ---- unfold LT at 1. repeat rewrite (subFormulaRelation LNN). simpl.
  3110. rewrite (subTermNil LNN).
  3111. **** apply impRefl.
  3112. **** apply closedNatToTerm.
  3113. ---- apply boundedLT. intros n H1. repeat rewrite (subFormulaId LNN).
  3114. repeat first
  3115. [ rewrite subExistSpecial; [| discriminate ]
  3116. | rewrite subForallSpecial; [| discriminate ]
  3117. | rewrite (subFormulaAnd LNN)
  3118. | rewrite (subFormulaImp LNN) ].
  3119. apply forallI.
  3120. **** apply closedNN.
  3121. **** apply forallI.
  3122. { apply closedNN. }
  3123. { apply impTrans with (equal (var 1) (natToTerm (f n))).
  3124. + destruct repBeta as (H4, H5). simpl in H5.
  3125. apply
  3126. impTrans
  3127. with
  3128. (substituteFormula LNN
  3129. (substituteFormula LNN
  3130. (substituteFormula LNN
  3131. (substituteFormula LNN betaFormula 1 (var 3)) 2
  3132. (natToTerm x)) 0 (var 1)) 3 (natToTerm n)).
  3133. apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3134. - apply (subFormulaExch LNN).
  3135. * discriminate.
  3136. * intro H6. destruct H6 as [H6 | H6].
  3137. ++ discriminate H6.
  3138. ++ elim H6.
  3139. * apply closedNatToTerm.
  3140. - apply
  3141. impTrans
  3142. with
  3143. (substituteFormula LNN
  3144. (substituteFormula LNN
  3145. (substituteFormula LNN
  3146. (substituteFormula LNN betaFormula 1 (var 3)) 2
  3147. (natToTerm x)) 3 (natToTerm n)) 0 (var 1)).
  3148. * apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3149. apply (subFormulaExch LNN).
  3150. ++ discriminate.
  3151. ++ intro H6. destruct H6 as [H6 | H6].
  3152. -- discriminate H6.
  3153. -- elim H6.
  3154. ++ apply closedNatToTerm.
  3155. * apply
  3156. impTrans
  3157. with
  3158. (substituteFormula LNN
  3159. (substituteFormula LNN
  3160. (substituteFormula LNN
  3161. (substituteFormula LNN betaFormula 2 (natToTerm x)) 1
  3162. (var 3)) 3 (natToTerm n)) 0 (var 1)).
  3163. ++ apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3164. apply (subFormulaExch LNN).
  3165. -- discriminate.
  3166. -- apply closedNatToTerm.
  3167. -- intro H6. destruct H6 as [H6 | H6].
  3168. ** discriminate H6.
  3169. ** elim H6.
  3170. ++ apply
  3171. impTrans
  3172. with
  3173. (substituteFormula LNN
  3174. (substituteFormula LNN
  3175. (substituteFormula LNN betaFormula 2 (natToTerm x)) 1
  3176. (natToTerm n)) 0 (var 1)).
  3177. -- apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3178. apply (subFormulaTrans LNN). intro H6.
  3179. assert
  3180. (In 3
  3181. (freeVarFormula LNN (substituteFormula LNN betaFormula 2 (natToTerm x)))).
  3182. { eapply In_list_remove1. apply H6. }
  3183. destruct (freeVarSubFormula3 _ _ _ _ _ H7) as [H8 | H8].
  3184. ** elim (le_not_lt 3 2). apply H4. eapply In_list_remove1.
  3185. +++ apply H8.
  3186. +++ repeat constructor.
  3187. ** elim (closedNatToTerm _ _ H8).
  3188. -- apply
  3189. impTrans
  3190. with
  3191. (substituteFormula LNN (equal (var 0) (natToTerm (beta x n))) 0 (var 1)).
  3192. ** apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3193. apply H5.
  3194. ** repeat rewrite (subFormulaEqual LNN). simpl.
  3195. repeat rewrite (subTermNil LNN (natToTerm (beta x n))).
  3196. ++++ rewrite H2.
  3197. ---- apply impRefl.
  3198. ---- apply lt_S. apply H1.
  3199. ++++ apply closedNatToTerm.
  3200. + rewrite <-
  3201. (subFormulaId LNN
  3202. (fol.impH LNN
  3203. (substituteFormula LNN
  3204. (substituteFormula LNN (substituteFormula LNN B 2 (var 3)) 2
  3205. (natToTerm x)) 3 (natToTerm n))
  3206. (substituteFormula LNN
  3207. (substituteFormula LNN
  3208. (substituteFormula LNN betaFormula 1 (Succ (var 3))) 2
  3209. (natToTerm x)) 3 (natToTerm n))) 1).
  3210. apply impI.
  3211. apply
  3212. impE
  3213. with
  3214. (substituteFormula LNN
  3215. (fol.impH LNN
  3216. (substituteFormula LNN
  3217. (substituteFormula LNN (substituteFormula LNN B 2 (var 3)) 2
  3218. (natToTerm x)) 3 (natToTerm n))
  3219. (substituteFormula LNN
  3220. (substituteFormula LNN
  3221. (substituteFormula LNN betaFormula 1 (Succ (var 3))) 2
  3222. (natToTerm x)) 3 (natToTerm n))) 1
  3223. (natToTerm (f n))).
  3224. - apply (subWithEquals LNN). apply eqSym. apply Axm; right; constructor.
  3225. - apply sysWeaken. rewrite (subFormulaImp LNN).
  3226. apply impTrans with (equal (var 0) (natToTerm (f (S n)))).
  3227. * destruct H0 as (H0, H4). simpl in H4.
  3228. apply
  3229. impTrans
  3230. with
  3231. (substituteFormula LNN
  3232. (substituteFormula LNN (substituteFormula LNN B 2 (var 3)) 3
  3233. (natToTerm n)) 1 (natToTerm (f n))).
  3234. ++ apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3235. apply (subFormulaNil LNN). intro H5.
  3236. destruct (freeVarSubFormula3 _ _ _ _ _ H5) as [H6 | [H6 | H6]].
  3237. -- elim (In_list_remove2 _ _ _ _ _ H6). reflexivity.
  3238. -- discriminate H6.
  3239. -- elim H6.
  3240. ++ apply
  3241. impTrans
  3242. with
  3243. (substituteFormula LNN (substituteFormula LNN B 2 (natToTerm n)) 1
  3244. (natToTerm (f n))).
  3245. -- apply iffE1. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3246. apply (subFormulaTrans LNN). intro H5. elim (le_not_lt 3 2).
  3247. ** apply H0. eapply In_list_remove1. apply H5.
  3248. ** repeat constructor.
  3249. -- unfold f. simpl. apply iffE1. apply H4.
  3250. * rewrite <-
  3251. (subFormulaId LNN
  3252. (substituteFormula LNN
  3253. (substituteFormula LNN
  3254. (substituteFormula LNN
  3255. (substituteFormula LNN betaFormula 1 (Succ (var 3))) 2
  3256. (natToTerm x)) 3 (natToTerm n)) 1 (natToTerm (f n))) 0).
  3257. apply impI.
  3258. apply
  3259. impE
  3260. with
  3261. (substituteFormula LNN
  3262. (substituteFormula LNN
  3263. (substituteFormula LNN
  3264. (substituteFormula LNN
  3265. (substituteFormula LNN betaFormula 1 (Succ (var 3))) 2
  3266. (natToTerm x)) 3 (natToTerm n)) 1 (natToTerm (f n))) 0
  3267. (natToTerm (f (S n)))).
  3268. ++ apply (subWithEquals LNN). apply eqSym. apply Axm; right; constructor.
  3269. ++ apply sysWeaken.
  3270. apply
  3271. impE
  3272. with
  3273. (substituteFormula LNN
  3274. (substituteFormula LNN
  3275. (substituteFormula LNN
  3276. (substituteFormula LNN
  3277. (substituteFormula LNN betaFormula 2 (natToTerm x)) 1
  3278. (Succ (var 3))) 3 (natToTerm n)) 1
  3279. (natToTerm (f n))) 0 (natToTerm (f (S n)))).
  3280. -- apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3281. apply (subFormulaExch LNN).
  3282. ** discriminate.
  3283. ** simpl. lia.
  3284. ** apply closedNatToTerm.
  3285. -- apply
  3286. impE
  3287. with
  3288. (substituteFormula LNN
  3289. (substituteFormula LNN
  3290. (substituteFormula LNN
  3291. (substituteFormula LNN
  3292. (substituteFormula LNN betaFormula 2 (natToTerm x)) 3
  3293. (natToTerm n)) 1 (natToTerm (S n))) 1
  3294. (natToTerm (f n))) 0 (natToTerm (f (S n)))).
  3295. ** apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3296. replace (natToTerm (S n)) with
  3297. (substituteTerm LNN (Succ (var 3)) 3 (natToTerm n)).
  3298. +++ apply (subSubFormula LNN).
  3299. --- discriminate.
  3300. --- apply closedNatToTerm.
  3301. +++ simpl. reflexivity.
  3302. ** destruct repBeta as (H4, H5).
  3303. apply
  3304. impE
  3305. with
  3306. (substituteFormula LNN
  3307. (substituteFormula LNN
  3308. (substituteFormula LNN
  3309. (substituteFormula LNN betaFormula 2 (natToTerm x)) 1
  3310. (natToTerm (S n))) 1 (natToTerm (f n))) 0
  3311. (natToTerm (f (S n)))).
  3312. +++ apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3313. apply (subFormulaNil LNN). intro H6.
  3314. destruct (freeVarSubFormula3 _ _ _ _ _ H6) as [H7 | H7].
  3315. --- elim (le_not_lt 3 2).
  3316. *** apply H4. eapply In_list_remove1. apply H7.
  3317. *** repeat constructor.
  3318. --- elim (closedNatToTerm _ _ H7).
  3319. +++ simpl in H5.
  3320. apply
  3321. impE
  3322. with
  3323. (substituteFormula LNN
  3324. (substituteFormula LNN (equal (var 0) (natToTerm (beta x (S n)))) 1
  3325. (natToTerm (f n))) 0 (natToTerm (f (S n)))).
  3326. --- apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3327. apply H5.
  3328. --- repeat rewrite (subFormulaEqual LNN). simpl.
  3329. repeat
  3330. (rewrite (subTermNil LNN (natToTerm (beta x (S n))));
  3331. [| apply closedNatToTerm ]).
  3332. rewrite H2.
  3333. *** apply eqRefl.
  3334. *** apply lt_n_S. apply H1. }
  3335. --- intros b H1. assert (forall z : nat, decidable (f z = beta b z)).
  3336. { unfold decidable. intros z. destruct (eq_nat_dec (f z) (beta b z)); auto. }
  3337. decompose record
  3338. (notBoundedForall (fun z : nat => f z = beta b z) (S a) H4 (H3 b H1)).
  3339. apply impE with (notH (equal (natToTerm (f x0)) (natToTerm (beta b x0)))).
  3340. *** apply cp2. unfold primRecSigmaFormulaHelp.
  3341. repeat first
  3342. [ rewrite subExistSpecial; [| discriminate ]
  3343. | rewrite subForallSpecial; [| discriminate ]
  3344. | rewrite (subFormulaAnd LNN)
  3345. | rewrite (subFormulaImp LNN) ].
  3346. rewrite (subFormulaExist LNN). simpl.
  3347. repeat first
  3348. [ rewrite subExistSpecial; [| discriminate ]
  3349. | rewrite subForallSpecial; [| discriminate ]
  3350. | rewrite (subFormulaAnd LNN)
  3351. | rewrite (subFormulaImp LNN) ].
  3352. apply impI. clear H4 H1 H3 H2 x P H7.
  3353. induction x0 as [| x0 Hrecx0].
  3354. ++++ apply
  3355. impE
  3356. with
  3357. (existH 0
  3358. (fol.andH LNN
  3359. (substituteFormula LNN (substituteFormula LNN A 1 (natToTerm a)) 2
  3360. (natToTerm b))
  3361. (substituteFormula LNN
  3362. (substituteFormula LNN
  3363. (substituteFormula LNN
  3364. (substituteFormula LNN betaFormula 1 Zero) 2
  3365. (var 2)) 1 (natToTerm a)) 2 (natToTerm b)))).
  3366. ---- apply sysWeaken. apply impI. apply existSys.
  3367. **** apply closedNN.
  3368. **** intro H1. destruct (in_app_or _ _ _ H1) as [H2 | H2].
  3369. { elim (closedNatToTerm _ _ H2). }
  3370. { elim (closedNatToTerm _ _ H2). }
  3371. **** apply eqTrans with (var 0).
  3372. { destruct H as (H, H1). simpl in H1. apply eqSym. unfold f; simpl.
  3373. apply impE with A.
  3374. + apply sysWeaken. apply iffE1. assumption.
  3375. + apply
  3376. impE
  3377. with
  3378. (substituteFormula LNN (substituteFormula LNN A 1 (natToTerm a)) 2
  3379. (natToTerm b)).
  3380. - apply sysWeaken. apply iffE1.
  3381. apply iffTrans with (substituteFormula LNN A 2 (natToTerm b)).
  3382. * repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3383. apply (subFormulaNil LNN). intro H2. elim (le_not_lt 1 0); auto.
  3384. * apply (subFormulaNil LNN). intro H2. elim (le_not_lt 2 0); auto.
  3385. - eapply andE1. apply Axm; right; constructor. }
  3386. { destruct repBeta as (H1, H2). simpl in H2.
  3387. apply
  3388. impE
  3389. with
  3390. (substituteFormula LNN
  3391. (substituteFormula LNN
  3392. (substituteFormula LNN (substituteFormula LNN betaFormula 1 Zero) 2
  3393. (var 2)) 1 (natToTerm a)) 2 (natToTerm b)).
  3394. + apply sysWeaken. apply iffE1.
  3395. apply
  3396. iffTrans
  3397. with
  3398. (substituteFormula LNN
  3399. (substituteFormula LNN betaFormula 2 (natToTerm b)) 1
  3400. (natToTerm 0)).
  3401. - rewrite (subFormulaId LNN).
  3402. apply
  3403. iffTrans
  3404. with
  3405. (substituteFormula LNN (substituteFormula LNN betaFormula 1 Zero) 2
  3406. (natToTerm b)).
  3407. * repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3408. apply (subFormulaNil LNN). intro H3.
  3409. destruct (freeVarSubFormula3 _ _ _ _ _ H3) as [H4 | H4].
  3410. ++ elim (In_list_remove2 _ _ _ _ _ H4); reflexivity.
  3411. ++ apply H4.
  3412. * apply (subFormulaExch LNN).
  3413. ++ discriminate.
  3414. ++ apply closedNatToTerm.
  3415. ++ apply closedNatToTerm.
  3416. - apply H2.
  3417. + eapply andE2. apply Axm; right; constructor. }
  3418. ---- eapply andE1. apply Axm; right; constructor.
  3419. ++++ apply impE with (equal (natToTerm (f x0)) (natToTerm (beta b x0))); [| apply Hrecx0 ].
  3420. ---- clear Hrecx0.
  3421. apply
  3422. impE
  3423. with
  3424. (forallH 3
  3425. (fol.impH LNN
  3426. (substituteFormula LNN
  3427. (substituteFormula LNN (LT (var 3) (var 1)) 1 (natToTerm a)) 2
  3428. (natToTerm b))
  3429. (existH 0
  3430. (existH 1
  3431. (fol.andH LNN
  3432. (substituteFormula LNN
  3433. (substituteFormula LNN
  3434. (substituteFormula LNN
  3435. (substituteFormula LNN betaFormula 1 (var 3)) 2
  3436. (var 2)) 0 (var 1)) 2 (natToTerm b))
  3437. (fol.andH LNN
  3438. (substituteFormula LNN
  3439. (substituteFormula LNN B 2 (var 3)) 2
  3440. (natToTerm b))
  3441. (substituteFormula LNN
  3442. (substituteFormula LNN
  3443. (substituteFormula LNN betaFormula 1
  3444. (Succ (var 3))) 2 (var 2)) 2
  3445. (natToTerm b))))))));
  3446. [| eapply andE2; apply Axm; right; constructor ].
  3447. apply sysWeaken.
  3448. apply
  3449. impTrans
  3450. with
  3451. (substituteFormula LNN
  3452. (fol.impH LNN
  3453. (substituteFormula LNN
  3454. (substituteFormula LNN (LT (var 3) (var 1)) 1 (natToTerm a)) 2
  3455. (natToTerm b))
  3456. (existH 0
  3457. (existH 1
  3458. (fol.andH LNN
  3459. (substituteFormula LNN
  3460. (substituteFormula LNN
  3461. (substituteFormula LNN
  3462. (substituteFormula LNN betaFormula 1 (var 3)) 2
  3463. (var 2)) 0 (var 1)) 2 (natToTerm b))
  3464. (fol.andH LNN
  3465. (substituteFormula LNN
  3466. (substituteFormula LNN B 2 (var 3)) 2
  3467. (natToTerm b))
  3468. (substituteFormula LNN
  3469. (substituteFormula LNN
  3470. (substituteFormula LNN betaFormula 1
  3471. (Succ (var 3))) 2 (var 2)) 2
  3472. (natToTerm b))))))) 3 (natToTerm x0)).
  3473. **** apply impI. apply forallE. apply Axm; right; constructor.
  3474. **** repeat first
  3475. [ rewrite subExistSpecial; [| discriminate ]
  3476. | rewrite subForallSpecial; [| discriminate ]
  3477. | rewrite (subFormulaAnd LNN)
  3478. | rewrite (subFormulaImp LNN) ].
  3479. apply
  3480. impTrans
  3481. with
  3482. (existH 0
  3483. (existH 1
  3484. (fol.andH LNN
  3485. (substituteFormula LNN
  3486. (substituteFormula LNN
  3487. (substituteFormula LNN
  3488. (substituteFormula LNN
  3489. (substituteFormula LNN betaFormula 1 (var 3)) 2
  3490. (var 2)) 0 (var 1)) 2 (natToTerm b)) 3
  3491. (natToTerm x0))
  3492. (fol.andH LNN
  3493. (substituteFormula LNN
  3494. (substituteFormula LNN (substituteFormula LNN B 2 (var 3))
  3495. 2 (natToTerm b)) 3 (natToTerm x0))
  3496. (substituteFormula LNN
  3497. (substituteFormula LNN
  3498. (substituteFormula LNN
  3499. (substituteFormula LNN betaFormula 1 (Succ (var 3)))
  3500. 2 (var 2)) 2 (natToTerm b)) 3
  3501. (natToTerm x0)))))).
  3502. { apply impI.
  3503. apply
  3504. impE
  3505. with
  3506. (substituteFormula LNN
  3507. (substituteFormula LNN
  3508. (substituteFormula LNN (LT (var 3) (var 1)) 1 (natToTerm a)) 2
  3509. (natToTerm b)) 3 (natToTerm x0)).
  3510. + apply Axm; right; constructor.
  3511. + apply sysWeaken. unfold LT. repeat rewrite (subFormulaRelation LNN). simpl.
  3512. repeat (rewrite (subTermNil LNN (natToTerm a)); [| apply closedNatToTerm ]).
  3513. fold (LT (natToTerm x0) (natToTerm a)). apply natLT. apply lt_S_n. auto. }
  3514. { apply impI.
  3515. assert
  3516. (forall n : nat,
  3517. ~
  3518. In n
  3519. (freeVarFormula LNN
  3520. (impH (equal (natToTerm (f x0)) (natToTerm (beta b x0)))
  3521. (equal (natToTerm (f (S x0))) (natToTerm (beta b (S x0))))))).
  3522. { simpl. intros n H1.
  3523. destruct (in_app_or _ _ _ H1) as [H2 | H2]; induction (in_app_or _ _ _ H2) as [H3 | H3];
  3524. elim (closedNatToTerm _ _ H3). }
  3525. apply existSys.
  3526. + apply closedNN.
  3527. + apply H1.
  3528. + apply existSys.
  3529. - apply closedNN.
  3530. - apply H1.
  3531. - unfold f at 2; simpl. fold (f x0) in |- *.
  3532. apply impE with (equal (var 1) (natToTerm (beta b x0))).
  3533. * apply impI. apply impE with (equal (var 0) (natToTerm (h x0 (beta b x0)))).
  3534. ++ repeat apply impI. apply eqTrans with (var 0).
  3535. -- apply eqTrans with (natToTerm (h x0 (beta b x0))).
  3536. ** destruct (eq_nat_dec (f x0) (beta b x0)) as [a0 | b0].
  3537. +++ rewrite a0. apply eqRefl.
  3538. +++ apply contradiction with (equal (natToTerm (f x0)) (natToTerm (beta b x0))).
  3539. --- apply Axm; right; constructor.
  3540. --- do 4 apply sysWeaken. apply natNE. auto.
  3541. ** apply eqSym. apply Axm; left; right; constructor.
  3542. -- apply
  3543. impE
  3544. with
  3545. (substituteFormula LNN
  3546. (substituteFormula LNN
  3547. (substituteFormula LNN
  3548. (substituteFormula LNN betaFormula 1 (Succ (var 3))) 2
  3549. (var 2)) 2 (natToTerm b)) 3 (natToTerm x0)).
  3550. ** do 4 apply sysWeaken. apply iffE1. destruct repBeta as (H2, H3).
  3551. simpl in H3.
  3552. apply
  3553. iffTrans
  3554. with
  3555. (substituteFormula LNN
  3556. (substituteFormula LNN betaFormula 2 (natToTerm b)) 1
  3557. (natToTerm (S x0))).
  3558. +++ rewrite (subFormulaId LNN).
  3559. apply
  3560. iffTrans
  3561. with
  3562. (substituteFormula LNN
  3563. (substituteFormula LNN
  3564. (substituteFormula LNN betaFormula 2 (natToTerm b)) 1
  3565. (Succ (var 3))) 3 (natToTerm x0)).
  3566. --- repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3567. apply (subFormulaExch LNN).
  3568. *** discriminate.
  3569. *** simpl; lia.
  3570. *** apply closedNatToTerm.
  3571. --- apply
  3572. iffTrans
  3573. with
  3574. (substituteFormula LNN
  3575. (substituteFormula LNN
  3576. (substituteFormula LNN betaFormula 2 (natToTerm b)) 3
  3577. (natToTerm x0)) 1
  3578. (substituteTerm LNN (Succ (var 3)) 3 (natToTerm x0))).
  3579. *** apply (subSubFormula LNN).
  3580. ++++ discriminate.
  3581. ++++ apply closedNatToTerm.
  3582. *** simpl.
  3583. apply
  3584. iffTrans
  3585. with
  3586. (substituteFormula LNN
  3587. (substituteFormula LNN betaFormula 2 (natToTerm b)) 1
  3588. (substituteTerm LNN (Succ (var 3)) 3 (natToTerm x0))).
  3589. ++++ repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3590. apply (subFormulaNil LNN).
  3591. intro H4. destruct (freeVarSubFormula3 _ _ _ _ _ H4) as [H5 | H5].
  3592. ---- elim (le_not_lt 3 2).
  3593. **** apply H2. eapply In_list_remove1. apply H5.
  3594. **** repeat constructor.
  3595. ---- elim (closedNatToTerm _ _ H5).
  3596. ++++ apply iffRefl.
  3597. +++ apply H3.
  3598. ** eapply andE2. eapply andE2. apply Axm; do 3 left; right; constructor.
  3599. ++ apply
  3600. impE
  3601. with
  3602. (substituteFormula LNN
  3603. (substituteFormula LNN
  3604. (substituteFormula LNN (substituteFormula LNN B 2 (var 3)) 2
  3605. (natToTerm b)) 3 (natToTerm x0)) 1 (natToTerm (beta b x0))).
  3606. -- do 2 apply sysWeaken. destruct H0 as (H0, H2). simpl in H2. apply iffE1.
  3607. apply
  3608. iffTrans
  3609. with
  3610. (substituteFormula LNN (substituteFormula LNN B 2 (natToTerm x0)) 1
  3611. (natToTerm (beta b x0))).
  3612. ** apply
  3613. iffTrans
  3614. with
  3615. (substituteFormula LNN
  3616. (substituteFormula LNN (substituteFormula LNN B 2 (var 3)) 3
  3617. (natToTerm x0)) 1 (natToTerm (beta b x0))).
  3618. +++ repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3619. apply (subFormulaNil LNN). intro H3.
  3620. destruct (freeVarSubFormula3 _ _ _ _ _ H3) as [H4 | H4].
  3621. --- elim (In_list_remove2 _ _ _ _ _ H4). reflexivity.
  3622. --- destruct H4 as [H4 | H4].
  3623. *** discriminate H4.
  3624. *** apply H4.
  3625. +++ repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3626. apply (subFormulaTrans LNN). intro H3. elim (le_not_lt 3 2).
  3627. --- apply H0. eapply In_list_remove1. apply H3.
  3628. --- repeat constructor.
  3629. ** apply H2.
  3630. -- apply
  3631. impE
  3632. with
  3633. (substituteFormula LNN
  3634. (substituteFormula LNN
  3635. (substituteFormula LNN (substituteFormula LNN B 2 (var 3)) 2
  3636. (natToTerm b)) 3 (natToTerm x0)) 1 (var 1)).
  3637. ** apply (subWithEquals LNN). apply Axm; right; constructor.
  3638. ** repeat rewrite (subFormulaId LNN). eapply andE1. eapply andE2.
  3639. apply Axm; left; right; constructor.
  3640. * apply
  3641. impE
  3642. with
  3643. (substituteFormula LNN
  3644. (substituteFormula LNN
  3645. (substituteFormula LNN
  3646. (substituteFormula LNN
  3647. (substituteFormula LNN betaFormula 1 (var 3)) 2
  3648. (var 2)) 0 (var 1)) 2 (natToTerm b)) 3
  3649. (natToTerm x0)).
  3650. ++ apply sysWeaken. apply iffE1. destruct repBeta as (H2, H3). simpl in H3.
  3651. apply
  3652. iffTrans
  3653. with
  3654. (substituteFormula LNN (equal (var 0) (natToTerm (beta b x0))) 0 (var 1)).
  3655. -- rewrite (subFormulaId LNN).
  3656. apply
  3657. iffTrans
  3658. with
  3659. (substituteFormula LNN
  3660. (substituteFormula LNN
  3661. (substituteFormula LNN
  3662. (substituteFormula LNN betaFormula 1 (var 3)) 2
  3663. (natToTerm b)) 0 (var 1)) 3 (natToTerm x0)).
  3664. ** repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3665. apply (subFormulaExch LNN).
  3666. +++ discriminate.
  3667. +++ intros [H4 | H4].
  3668. --- discriminate H4.
  3669. --- apply H4.
  3670. +++ apply closedNatToTerm.
  3671. ** apply
  3672. iffTrans
  3673. with
  3674. (substituteFormula LNN
  3675. (substituteFormula LNN
  3676. (substituteFormula LNN
  3677. (substituteFormula LNN betaFormula 1 (var 3)) 2
  3678. (natToTerm b)) 3 (natToTerm x0)) 0 (var 1)).
  3679. +++ repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3680. apply (subFormulaExch LNN).
  3681. --- discriminate.
  3682. --- intros [H4 | H4].
  3683. *** discriminate H4.
  3684. *** apply H4.
  3685. --- apply closedNatToTerm.
  3686. +++ apply (reduceSub LNN).
  3687. --- apply closedNN.
  3688. --- apply
  3689. iffTrans
  3690. with
  3691. (substituteFormula LNN
  3692. (substituteFormula LNN
  3693. (substituteFormula LNN betaFormula 2 (natToTerm b)) 1
  3694. (var 3)) 3 (natToTerm x0)).
  3695. *** repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3696. apply (subFormulaExch LNN).
  3697. ++++ discriminate.
  3698. ++++ intros [H4 | H4].
  3699. ---- discriminate H4.
  3700. ---- apply H4.
  3701. ++++ apply closedNatToTerm.
  3702. *** apply
  3703. iffTrans
  3704. with
  3705. (substituteFormula LNN
  3706. (substituteFormula LNN betaFormula 2 (natToTerm b)) 1
  3707. (natToTerm x0)).
  3708. ++++ repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3709. apply (subFormulaTrans LNN). intro H4.
  3710. assert
  3711. (In 3
  3712. (freeVarFormula LNN (substituteFormula LNN betaFormula 2 (natToTerm b)))).
  3713. { eapply In_list_remove1. apply H4. }
  3714. destruct (freeVarSubFormula3 _ _ _ _ _ H5) as [H7 | H7].
  3715. ---- elim (le_not_lt 3 2).
  3716. **** apply H2. eapply In_list_remove1. apply H7.
  3717. **** repeat constructor.
  3718. ---- elim (closedNatToTerm _ _ H7).
  3719. ++++ apply H3.
  3720. -- rewrite (subFormulaEqual LNN). simpl. rewrite subTermNil.
  3721. ** apply iffRefl.
  3722. ** apply closedNatToTerm.
  3723. ++ eapply andE1. apply Axm; right; constructor. }
  3724. ---- apply lt_S. apply lt_S_n. assumption.
  3725. *** apply natNE. auto.
  3726. --- intros b H1. assert (forall z : nat, decidable (f z = beta b z)).
  3727. { unfold decidable. intros z. destruct (eq_nat_dec (f z) (beta b z)); auto. }
  3728. decompose record
  3729. (notBoundedForall (fun z : nat => f z = beta b z) (S a) H4 (H3 b H1)).
  3730. apply impE with (notH (equal (natToTerm (f x0)) (natToTerm (beta b x0)))).
  3731. *** apply cp2. unfold primRecPiFormulaHelp.
  3732. repeat first
  3733. [ rewrite subExistSpecial; [| discriminate ]
  3734. | rewrite subForallSpecial; [| discriminate ]
  3735. | rewrite (subFormulaAnd LNN)
  3736. | rewrite (subFormulaImp LNN) ].
  3737. rewrite (subFormulaForall LNN). simpl.
  3738. repeat first
  3739. [ rewrite subExistSpecial; [| discriminate ]
  3740. | rewrite subForallSpecial; [| discriminate ]
  3741. | rewrite (subFormulaAnd LNN)
  3742. | rewrite (subFormulaImp LNN) ].
  3743. apply impI. clear H4 H1 H3 H2 x P H7. induction x0 as [| x0 Hrecx0].
  3744. ++++ apply
  3745. impE
  3746. with
  3747. (forallH 0
  3748. (fol.impH LNN
  3749. (substituteFormula LNN (substituteFormula LNN A 1 (natToTerm a)) 2
  3750. (natToTerm b))
  3751. (substituteFormula LNN
  3752. (substituteFormula LNN
  3753. (substituteFormula LNN
  3754. (substituteFormula LNN betaFormula 1 Zero) 2
  3755. (var 2)) 1 (natToTerm a)) 2 (natToTerm b)))).
  3756. ---- apply sysWeaken.
  3757. apply
  3758. impTrans
  3759. with
  3760. (substituteFormula LNN
  3761. (fol.impH LNN
  3762. (substituteFormula LNN (substituteFormula LNN A 1 (natToTerm a)) 2
  3763. (natToTerm b))
  3764. (substituteFormula LNN
  3765. (substituteFormula LNN
  3766. (substituteFormula LNN
  3767. (substituteFormula LNN betaFormula 1 Zero) 2
  3768. (var 2)) 1 (natToTerm a)) 2 (natToTerm b))) 0
  3769. (natToTerm (f 0))).
  3770. **** apply impI. apply forallE. apply Axm; right; constructor.
  3771. **** apply impI. rewrite (subFormulaImp LNN).
  3772. apply
  3773. impE
  3774. with
  3775. (substituteFormula LNN
  3776. (substituteFormula LNN
  3777. (substituteFormula LNN
  3778. (substituteFormula LNN
  3779. (substituteFormula LNN betaFormula 1 Zero) 2
  3780. (var 2)) 1 (natToTerm a)) 2 (natToTerm b)) 0
  3781. (natToTerm (f 0))).
  3782. { apply sysWeaken.
  3783. apply
  3784. impTrans
  3785. with
  3786. (substituteFormula LNN (equal (var 0) (natToTerm (beta b 0))) 0
  3787. (natToTerm (f 0))).
  3788. + apply iffE1. apply (reduceSub LNN).
  3789. - apply closedNN.
  3790. - rewrite (subFormulaId LNN). destruct repBeta as (H1, H2). simpl in H2.
  3791. apply
  3792. iffTrans
  3793. with
  3794. (substituteFormula LNN
  3795. (substituteFormula LNN betaFormula 2 (natToTerm b)) 1
  3796. (natToTerm 0)).
  3797. * apply
  3798. iffTrans
  3799. with
  3800. (substituteFormula LNN (substituteFormula LNN betaFormula 1 Zero) 2
  3801. (natToTerm b)).
  3802. ++ repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3803. apply (subFormulaNil LNN). intro H3.
  3804. destruct (freeVarSubFormula3 _ _ _ _ _ H3) as [H4 | H4].
  3805. -- elim (In_list_remove2 _ _ _ _ _ H4); reflexivity.
  3806. -- apply H4.
  3807. ++ apply (subFormulaExch LNN).
  3808. -- discriminate.
  3809. -- apply closedNatToTerm.
  3810. -- apply closedNatToTerm.
  3811. * apply H2.
  3812. + rewrite (subFormulaEqual LNN). simpl. rewrite (subTermNil LNN).
  3813. - apply impRefl.
  3814. - apply closedNatToTerm. }
  3815. { apply
  3816. impE
  3817. with
  3818. (substituteFormula LNN
  3819. (substituteFormula LNN (substituteFormula LNN A 1 (natToTerm a)) 2
  3820. (natToTerm b)) 0 (natToTerm (f 0))).
  3821. + apply Axm; right; constructor.
  3822. + apply sysWeaken.
  3823. apply
  3824. impE
  3825. with
  3826. (substituteFormula LNN (equal (var 0) (natToTerm (f 0))) 0
  3827. (natToTerm (f 0))).
  3828. - apply iffE2. apply (reduceSub LNN); [ apply closedNN |].
  3829. destruct H as (H, H1). simpl in H1. unfold f; simpl.
  3830. apply iffTrans with A; [| assumption ].
  3831. apply iffTrans with (substituteFormula LNN A 2 (natToTerm b)).
  3832. * repeat (apply (reduceSub LNN); [ apply closedNN |]).
  3833. apply (subFormulaNil LNN). intro H2. elim (le_not_lt 1 0); auto.
  3834. * apply (subFormulaNil LNN). intro H2. elim (le_not_lt 2 0); auto.
  3835. - rewrite (subFormulaEqual LNN). simpl. rewrite (subTermNil LNN).
  3836. * apply eqRefl.
  3837. * apply closedNatToTerm. }
  3838. ---- eapply andE1. apply Axm; right; constructor.
  3839. ++++ apply impE with (equal (natToTerm (f x0)) (natToTerm (beta b x0))); [| apply Hrecx0 ].
  3840. ---- clear Hrecx0.
  3841. apply
  3842. impE
  3843. with
  3844. (forallH 3
  3845. (fol.impH LNN
  3846. (substituteFormula LNN
  3847. (substituteFormula LNN (LT (var 3) (var 1)) 1 (natToTerm a)) 2
  3848. (natToTerm b))
  3849. (forallH 0
  3850. (forallH 1
  3851. (fol.impH LNN
  3852. (substituteFormula LNN
  3853. (substituteFormula LNN
  3854. (substituteFormula LNN
  3855. (substituteFormula LNN betaFormula 1 (var 3)) 2
  3856. (var 2)) 0 (var 1)) 2 (natToTerm b))
  3857. (fol.impH LNN
  3858. (substituteFormula LNN
  3859. (substituteFormula LNN B 2 (var 3)) 2
  3860. (natToTerm b))
  3861. (substituteFormula LNN
  3862. (substituteFormula LNN
  3863. (substituteFormula LNN betaFormula 1
  3864. (Succ (var 3))) 2 (var 2)) 2
  3865. (natToTerm b))))))));
  3866. [| eapply andE2; apply Axm; right; constructor ].
  3867. apply sysWeaken.
  3868. apply
  3869. impTrans
  3870. with
  3871. (substituteFormula LNN
  3872. (fol.impH LNN
  3873. (substituteFormula LNN
  3874. (substituteFormula LNN (LT (var 3) (var 1)) 1 (natToTerm a)) 2
  3875. (natToTerm b))
  3876. (forallH 0
  3877. (forallH 1
  3878. (fol.impH LNN
  3879. (substituteFormula LNN
  3880. (substituteFormula LNN
  3881. (substituteFormula LNN
  3882. (substituteFormula LNN betaFormula 1 (var 3)) 2
  3883. (var 2)) 0 (var 1)) 2 (natToTerm b))
  3884. (fol.impH LNN
  3885. (substituteFormula LNN
  3886. (substituteFormula LNN B 2 (var 3)) 2
  3887. (natToTerm b))
  3888. (substituteFormula LNN
  3889. (substituteFormula LNN
  3890. (substituteFormula LNN betaFormula 1
  3891. (Succ (var 3))) 2 (var 2)) 2
  3892. (natToTerm b))))))) 3 (natToTerm x0)).
  3893. **** apply impI. apply forallE. apply Axm; right; constructor.
  3894. **** repeat first
  3895. [ rewrite subExistSpecial; [| discriminate ]
  3896. | rewrite subForallSpecial; [| discriminate ]
  3897. | rewrite (subFormulaAnd LNN)
  3898. | rewrite (subFormulaImp LNN) ].
  3899. apply
  3900. impTrans
  3901. with
  3902. (forallH 0
  3903. (forallH 1
  3904. (fol.impH LNN
  3905. (substituteFormula LNN
  3906. (substituteFormula LNN
  3907. (substituteFormula LNN
  3908. (substituteFormula LNN
  3909. (substituteFormula LNN betaFormula 1 (var 3)) 2
  3910. (var 2)) 0 (var 1)) 2 (natToTerm b)) 3
  3911. (natToTerm x0))
  3912. (fol.impH LNN
  3913. (substituteFormula LNN
  3914. (substituteFormula LNN (substituteFormula LNN B 2 (var 3))
  3915. 2 (natToTerm b)) 3 (natToTerm x0))
  3916. (substituteFormula LNN
  3917. (substituteFormula LNN
  3918. (substituteFormula LNN
  3919. (substituteFormula LNN betaFormula 1 (Succ (var 3)))
  3920. 2 (var 2)) 2 (natToTerm b)) 3
  3921. (natToTerm x0)))))).
  3922. { apply impI.
  3923. apply
  3924. impE
  3925. with
  3926. (substituteFormula LNN
  3927. (substituteFormula LNN
  3928. (substituteFormula LNN (LT (var 3) (var 1)) 1 (natToTerm a)) 2
  3929. (natToTerm b)) 3 (natToTerm x0)).
  3930. + apply Axm; right; constructor.
  3931. + apply sysWeaken. unfold LT. repeat rewrite (subFormulaRelation LNN). simpl.
  3932. repeat (rewrite (subTermNil LNN (natToTerm a)); [| apply closedNatToTerm ]).
  3933. fold (LT (natToTerm x0) (natToTerm a)). apply natLT. apply lt_S_n. auto. }
  3934. { apply
  3935. impTrans
  3936. with
  3937. (substituteFormula LNN
  3938. (forallH 1
  3939. (fol.impH LNN
  3940. (substituteFormula LNN
  3941. (substituteFormula LNN
  3942. (substituteFormula LNN
  3943. (substituteFormula LNN
  3944. (substituteFormula LNN betaFormula 1 (var 3)) 2
  3945. (var 2)) 0 (var 1)) 2 (natToTerm b)) 3
  3946. (natToTerm x0))
  3947. (fol.impH LNN
  3948. (substituteFormula LNN
  3949. (substituteFormula LNN (substituteFormula LNN B 2 (var 3))
  3950. 2 (natToTerm b)) 3 (natToTerm x0))
  3951. (substituteFormula LNN
  3952. (substituteFormula LNN
  3953. (substituteFormula LNN
  3954. (substituteFormula LNN betaFormula 1 (Succ (var 3)))
  3955. 2 (var 2)) 2 (natToTerm b)) 3
  3956. (natToTerm x0))))) 0 (natToTerm (f (S x0)))).
  3957. + apply impI. apply forallE. apply Axm; right; constructor.
  3958. + repeat first
  3959. [ rewrite subExistSpecial; [| discriminate ]
  3960. | rewrite subForallSpecial; [| discriminate ]
  3961. | rewrite (subFormulaAnd LNN)
  3962. | rewrite (subFormulaImp LNN) ].
  3963. apply
  3964. impTrans
  3965. with
  3966. (substituteFormula LNN
  3967. (fol.impH LNN
  3968. (substituteFormula LNN
  3969. (substituteFormula LNN
  3970. (substituteFormula LNN
  3971. (substituteFormula LNN
  3972. (substituteFormula LNN
  3973. (substituteFormula LNN betaFormula 1 (var 3)) 2
  3974. (var 2)) 0 (var 1)) 2 (natToTerm b)) 3
  3975. (natToTerm x0)) 0 (natToTerm (f (S x0))))
  3976. (fol.impH LNN
  3977. (substituteFormula LNN
  3978. (substituteFormula LNN
  3979. (substituteFormula LNN (substituteFormula LNN B 2 (var 3))
  3980. 2 (natToTerm b)) 3 (natToTerm x0)) 0
  3981. (natToTerm (f (S x0))))
  3982. (substituteFormula LNN
  3983. (substituteFormula LNN
  3984. (substituteFormula LNN
  3985. (substituteFormula LNN
  3986. (substituteFormula LNN betaFormula 1 (Succ (var 3)))
  3987. 2 (var 2)) 2 (natToTerm b)) 3
  3988. (natToTerm x0)) 0 (natToTerm (f (S x0)))))) 1
  3989. (natToTerm (beta b x0))).
  3990. - apply impI. apply forallE. apply Axm; right; constructor.
  3991. - repeat first
  3992. [ rewrite subExistSpecial; [| discriminate ]
  3993. | rewrite subForallSpecial; [| discriminate ]
  3994. | rewrite (subFormulaAnd LNN)
  3995. | rewrite (subFormulaImp LNN) ].
  3996. repeat apply impI.
  3997. apply
  3998. impE
  3999. with
  4000. (substituteFormula LNN (equal (var 0) (natToTerm (beta b (S x0)))) 0
  4001. (natToTerm (f (S x0)))).
  4002. * rewrite (subFormulaEqual LNN). simpl. rewrite (subTermNil LNN).
  4003. ++ apply impRefl.
  4004. ++ apply closedNatToTerm.
  4005. * apply
  4006. impE
  4007. with
  4008. (substituteFormula LNN
  4009. (substituteFormula LNN
  4010. (substituteFormula LNN
  4011. (substituteFormula LNN
  4012. (substituteFormula LNN
  4013. (substituteFormula LNN betaFormula 1 (Succ (var 3))) 2
  4014. (var 2)) 2 (natToTerm b)) 3 (natToTerm x0)) 0
  4015. (natToTerm (f (S x0)))) 1 (natToTerm (beta b x0))).
  4016. ++ do 2 apply sysWeaken. apply iffE1.
  4017. apply
  4018. iffTrans
  4019. with
  4020. (substituteFormula LNN
  4021. (substituteFormula LNN
  4022. (substituteFormula LNN
  4023. (substituteFormula LNN
  4024. (substituteFormula LNN
  4025. (substituteFormula LNN betaFormula 1 (Succ (var 3))) 2
  4026. (var 2)) 2 (natToTerm b)) 3 (natToTerm x0)) 1
  4027. (natToTerm (beta b x0))) 0 (natToTerm (f (S x0)))).
  4028. -- apply (subFormulaExch LNN).
  4029. ** discriminate.
  4030. ** apply closedNatToTerm.
  4031. ** apply closedNatToTerm.
  4032. -- apply (reduceSub LNN).
  4033. ** apply closedNN.
  4034. ** destruct H0 as (H0, H1). destruct repBeta as (H2, H3). simpl in H3.
  4035. apply
  4036. iffTrans
  4037. with
  4038. (substituteFormula LNN
  4039. (substituteFormula LNN betaFormula 2 (natToTerm b)) 1
  4040. (natToTerm (S x0))).
  4041. +++ rewrite (subFormulaId LNN).
  4042. apply
  4043. iffTrans
  4044. with
  4045. (substituteFormula LNN
  4046. (substituteFormula LNN
  4047. (substituteFormula LNN
  4048. (substituteFormula LNN betaFormula 2 (natToTerm b)) 1
  4049. (Succ (var 3))) 3 (natToTerm x0)) 1 (natToTerm (beta b x0))).
  4050. --- repeat (apply (reduceSub LNN); [ apply closedNN |]).
  4051. apply (subFormulaExch LNN).
  4052. *** discriminate.
  4053. *** intros [H4 | H4].
  4054. ++++ discriminate H4.
  4055. ++++ apply H4.
  4056. *** apply closedNatToTerm.
  4057. --- apply
  4058. iffTrans
  4059. with
  4060. (substituteFormula LNN
  4061. (substituteFormula LNN
  4062. (substituteFormula LNN
  4063. (substituteFormula LNN betaFormula 2 (natToTerm b)) 3
  4064. (natToTerm x0)) 1
  4065. (substituteTerm LNN (Succ (var 3)) 3 (natToTerm x0))) 1
  4066. (natToTerm (beta b x0))).
  4067. *** repeat (apply (reduceSub LNN); [ apply closedNN |]).
  4068. apply (subSubFormula LNN).
  4069. ++++ discriminate.
  4070. ++++ apply closedNatToTerm.
  4071. *** simpl.
  4072. apply
  4073. iffTrans
  4074. with
  4075. (substituteFormula LNN
  4076. (substituteFormula LNN
  4077. (substituteFormula LNN betaFormula 2 (natToTerm b)) 1
  4078. (substituteTerm LNN (Succ (var 3)) 3 (natToTerm x0))) 1
  4079. (natToTerm (beta b x0))).
  4080. ++++ repeat (apply (reduceSub LNN); [ apply closedNN |]).
  4081. apply (subFormulaNil LNN). intro H4.
  4082. destruct (freeVarSubFormula3 _ _ _ _ _ H4) as [H5 | H5].
  4083. { elim (le_not_lt 3 2).
  4084. + apply H2. eapply In_list_remove1. apply H5.
  4085. + repeat constructor. }
  4086. { elim (closedNatToTerm _ _ H5). }
  4087. ++++ apply (subFormulaNil LNN). intro H4.
  4088. destruct (freeVarSubFormula3 _ _ _ _ _ H4) as [H5 | H5].
  4089. { elim (In_list_remove2 _ _ _ _ _ H5). reflexivity. }
  4090. { rewrite freeVarSucc in H5. elim (closedNatToTerm _ _ H5). }
  4091. +++ apply H3.
  4092. ++ eapply impE.
  4093. -- eapply impE.
  4094. ** apply Axm; left; right; constructor.
  4095. ** do 2 apply sysWeaken.
  4096. apply
  4097. impE
  4098. with
  4099. (substituteFormula LNN
  4100. (substituteFormula LNN (equal (var 1) (natToTerm (beta b x0))) 0
  4101. (natToTerm (f (S x0)))) 1 (natToTerm (beta b x0))).
  4102. +++ apply iffE2. repeat (apply (reduceSub LNN); [ apply closedNN |]).
  4103. destruct H0 as (H0, H1). destruct repBeta as (H2, H3). simpl in H3.
  4104. apply
  4105. iffTrans
  4106. with
  4107. (substituteFormula LNN (equal (var 0) (natToTerm (beta b x0))) 0 (var 1)).
  4108. --- rewrite (subFormulaId LNN).
  4109. apply
  4110. iffTrans
  4111. with
  4112. (substituteFormula LNN
  4113. (substituteFormula LNN
  4114. (substituteFormula LNN
  4115. (substituteFormula LNN betaFormula 1 (var 3)) 2
  4116. (natToTerm b)) 0 (var 1)) 3 (natToTerm x0)).
  4117. *** repeat (apply (reduceSub LNN); [ apply closedNN |]).
  4118. apply (subFormulaExch LNN).
  4119. ++++ discriminate.
  4120. ++++ intros [H4 | H4].
  4121. ---- discriminate H4.
  4122. ---- apply H4.
  4123. ++++ apply closedNatToTerm.
  4124. *** apply
  4125. iffTrans
  4126. with
  4127. (substituteFormula LNN
  4128. (substituteFormula LNN
  4129. (substituteFormula LNN
  4130. (substituteFormula LNN betaFormula 1 (var 3)) 2
  4131. (natToTerm b)) 3 (natToTerm x0)) 0 (var 1)).
  4132. ++++ repeat (apply (reduceSub LNN); [ apply closedNN |]).
  4133. apply (subFormulaExch LNN).
  4134. ---- discriminate.
  4135. ---- simpl. lia.
  4136. ---- apply closedNatToTerm.
  4137. ++++ apply (reduceSub LNN).
  4138. ---- apply closedNN.
  4139. ---- apply
  4140. iffTrans
  4141. with
  4142. (substituteFormula LNN
  4143. (substituteFormula LNN
  4144. (substituteFormula LNN betaFormula 2 (natToTerm b)) 1
  4145. (var 3)) 3 (natToTerm x0)).
  4146. **** repeat (apply (reduceSub LNN); [ apply closedNN |]).
  4147. apply (subFormulaExch LNN).
  4148. { discriminate. }
  4149. { simpl. lia. }
  4150. { apply closedNatToTerm. }
  4151. **** apply
  4152. iffTrans
  4153. with
  4154. (substituteFormula LNN
  4155. (substituteFormula LNN betaFormula 2 (natToTerm b)) 1
  4156. (natToTerm x0)).
  4157. { repeat (apply (reduceSub LNN); [ apply closedNN |]).
  4158. apply (subFormulaTrans LNN). intro H4.
  4159. assert
  4160. (In 3
  4161. (freeVarFormula LNN (substituteFormula LNN betaFormula 2 (natToTerm b)))).
  4162. { eapply In_list_remove1. apply H4. }
  4163. destruct (freeVarSubFormula3 _ _ _ _ _ H5) as [H7 | H7].
  4164. + elim (le_not_lt 3 2).
  4165. - apply H2. eapply In_list_remove1. apply H7.
  4166. - repeat constructor.
  4167. + elim (closedNatToTerm _ _ H7). }
  4168. { apply H3. }
  4169. --- rewrite (subFormulaEqual LNN). simpl. rewrite subTermNil.
  4170. **** apply iffRefl.
  4171. **** apply closedNatToTerm.
  4172. +++ repeat rewrite (subFormulaEqual LNN). simpl.
  4173. repeat rewrite (subTermNil LNN (natToTerm (beta b x0)));
  4174. try apply closedNatToTerm.
  4175. apply eqRefl.
  4176. -- apply
  4177. impE
  4178. with
  4179. (substituteFormula LNN
  4180. (substituteFormula LNN
  4181. (substituteFormula LNN
  4182. (substituteFormula LNN (substituteFormula LNN B 2 (var 3)) 2
  4183. (natToTerm b)) 3 (natToTerm x0)) 0
  4184. (natToTerm (f (S x0)))) 1 (natToTerm (f x0))).
  4185. ** apply (subWithEquals LNN). apply Axm; right; constructor.
  4186. ** do 2 apply sysWeaken.
  4187. apply
  4188. impE
  4189. with
  4190. (substituteFormula LNN
  4191. (substituteFormula LNN
  4192. (substituteFormula LNN
  4193. (substituteFormula LNN (substituteFormula LNN B 2 (var 3)) 2
  4194. (natToTerm b)) 3 (natToTerm x0)) 1
  4195. (natToTerm (f x0))) 0 (natToTerm (f (S x0)))).
  4196. +++ apply iffE1. apply (subFormulaExch LNN).
  4197. --- discriminate.
  4198. --- apply closedNatToTerm.
  4199. --- apply closedNatToTerm.
  4200. +++ apply
  4201. impE
  4202. with
  4203. (substituteFormula LNN (equal (var 0) (natToTerm (f (S x0)))) 0
  4204. (natToTerm (f (S x0)))).
  4205. --- apply iffE2. apply (reduceSub LNN).
  4206. *** apply closedNN.
  4207. *** destruct H0 as (H0, H1). simpl in H1.
  4208. apply
  4209. iffTrans
  4210. with
  4211. (substituteFormula LNN (substituteFormula LNN B 2 (natToTerm x0)) 1
  4212. (natToTerm (f x0))).
  4213. ++++ apply
  4214. iffTrans
  4215. with
  4216. (substituteFormula LNN
  4217. (substituteFormula LNN (substituteFormula LNN B 2 (var 3)) 3
  4218. (natToTerm x0)) 1 (natToTerm (f x0))).
  4219. ---- repeat (apply (reduceSub LNN); [ apply closedNN |]).
  4220. apply (subFormulaNil LNN). intro H2.
  4221. destruct (freeVarSubFormula3 _ _ _ _ _ H2) as [H3 | H3].
  4222. **** elim (In_list_remove2 _ _ _ _ _ H3). reflexivity.
  4223. **** destruct H3 as [H3 | H3].
  4224. { discriminate H3. }
  4225. { apply H3. }
  4226. ---- repeat (apply (reduceSub LNN); [ apply closedNN |]).
  4227. apply (subFormulaTrans LNN). intro H2.
  4228. elim (le_not_lt 3 2).
  4229. **** apply H0. eapply In_list_remove1. apply H2.
  4230. **** repeat constructor.
  4231. ++++ unfold f. simpl. apply H1.
  4232. --- rewrite (subFormulaEqual LNN). simpl.
  4233. rewrite (subTermNil LNN).
  4234. *** apply eqRefl.
  4235. *** apply closedNatToTerm. }
  4236. ---- apply lt_S. apply lt_S_n. assumption.
  4237. *** apply natNE. auto.
  4238. +++ apply iffRefl.
  4239. -- apply
  4240. iffTrans
  4241. with
  4242. (substituteFormula LNN
  4243. (substituteFormula LNN betaFormula 1 (natToTerm a)) 2
  4244. (natToTerm x)).
  4245. ** apply iffI.
  4246. +++ apply impI. apply existSys.
  4247. --- apply closedNN.
  4248. --- intro H1. destruct (freeVarSubFormula3 _ _ _ _ _ H1) as [H4 | H4].
  4249. *** elim (In_list_remove2 _ _ _ _ _ H4). reflexivity.
  4250. *** elim (closedNatToTerm _ _ H4).
  4251. --- apply
  4252. impE
  4253. with
  4254. (substituteFormula LNN
  4255. (substituteFormula LNN betaFormula 1 (natToTerm a)) 2
  4256. (var 2)).
  4257. *** apply (subWithEquals LNN). eapply andE1. apply Axm; right; constructor.
  4258. *** rewrite (subFormulaId LNN). eapply andE2. apply Axm; right; constructor.
  4259. +++ apply impI. apply existI with (natToTerm x). rewrite (subFormulaAnd LNN). apply andI.
  4260. --- rewrite (subFormulaEqual LNN). simpl. rewrite subTermNil.
  4261. *** apply eqRefl.
  4262. *** apply closedNatToTerm.
  4263. --- apply Axm; right; constructor.
  4264. ** apply
  4265. iffTrans
  4266. with
  4267. (substituteFormula LNN
  4268. (substituteFormula LNN betaFormula 2 (natToTerm x)) 1
  4269. (natToTerm a)).
  4270. +++ apply (subFormulaExch LNN).
  4271. --- discriminate.
  4272. --- apply closedNatToTerm.
  4273. --- apply closedNatToTerm.
  4274. +++ rewrite H2.
  4275. --- destruct repBeta as (H1, H4). apply H4.
  4276. --- apply lt_n_Sn.
  4277. ++ unfold P. intros z H2. unfold beta. repeat rewrite cPairProjections1. repeat rewrite cPairProjections2.
  4278. apply (p z). assumption.
  4279. + simpl. intros.
  4280. apply
  4281. Representable_ext
  4282. with (evalPrimRecFunc n (g a0) (fun x y : nat => h x y a0) a).
  4283. - induction a as [| a Hreca].
  4284. * simpl. apply extEqualRefl.
  4285. * simpl. apply extEqualCompose2.
  4286. ++ apply Hreca.
  4287. ++ apply extEqualRefl.
  4288. - induction H as (H, H1). induction H0 as (H0, H2). simpl in H1. simpl in H2.
  4289. assert
  4290. (RepresentableHelp n
  4291. (evalPrimRecFunc n (g a0) (fun x y : nat => h x y a0) a)
  4292. (substituteFormula LNN
  4293. (primRecSigmaFormula n (substituteFormula LNN A (S n) (natToTerm a0))
  4294. (substituteFormula LNN
  4295. (substituteFormula LNN
  4296. (substituteFormula LNN B (S n) (natToTerm a0))
  4297. (S (S n)) (var (S n))) (S (S (S n)))
  4298. (var (S (S n))))) (S n) (natToTerm a))).
  4299. { apply Hrecn.
  4300.  
  4301. split.
  4302. intros.
  4303. induction (freeVarSubFormula3 _ _ _ _ _ H3).
  4304. assert (v <= S n).
  4305. apply H.
  4306. eapply In_list_remove1.
  4307. apply H4.
  4308. induction (le_lt_or_eq _ _ H5).
  4309. apply lt_n_Sm_le.
  4310. auto.
  4311. elim (In_list_remove2 _ _ _ _ _ H4).
  4312. auto.
  4313. elim (closedNatToTerm _ _ H4).
  4314. apply H1.
  4315. split.
  4316. intros.
  4317. repeat
  4318. match goal with
  4319. | H:(In v (list_remove nat eq_nat_dec ?X1 (freeVarFormula LNN ?X2))) |- _ =>
  4320. assert (In v (freeVarFormula LNN X2));
  4321. [ eapply In_list_remove1; apply H
  4322. | assert (v <> X1); [ eapply In_list_remove2; apply H | clear H ] ]
  4323. | H:(In v (freeVarFormula LNN (substituteFormula LNN ?X1 ?X2 ?X3))) |- _ =>
  4324. induction (freeVarSubFormula3 _ _ _ _ _ H); clear H
  4325. end.
  4326. assert (v <= S (S (S n))).
  4327. apply H0.
  4328. auto.
  4329. induction (le_lt_or_eq _ _ H4).
  4330. apply lt_n_Sm_le.
  4331. auto.
  4332. elim H5; auto.
  4333. elim (closedNatToTerm _ _ H4).
  4334. induction H4 as [H3| H3].
  4335. rewrite <- H3.
  4336. apply le_n_Sn.
  4337. elim H3.
  4338. induction H4 as [H3| H3].
  4339. rewrite <- H3.
  4340. apply le_n.
  4341. elim H3.
  4342. simpl in |- *.
  4343. intros.
  4344. apply
  4345. RepresentableAlternate
  4346. with
  4347. (substituteFormula LNN
  4348. (substituteFormula LNN
  4349. (substituteFormula LNN B (S (S (S n))) (natToTerm a1))
  4350. (S (S n)) (natToTerm a2)) (S n) (natToTerm a0)).
  4351. apply iffSym.
  4352. apply
  4353. iffTrans
  4354. with
  4355. (substituteFormula LNN
  4356. (substituteFormula LNN
  4357. (substituteFormula LNN
  4358. (substituteFormula LNN B (S n) (natToTerm a0))
  4359. (S (S n)) (var (S n))) (S (S (S n))) (natToTerm a1))
  4360. (S n) (natToTerm a2)).
  4361. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4362. apply (subFormulaTrans LNN).
  4363. unfold not in |- *; intros.
  4364. repeat
  4365. match goal with
  4366. | H:(In ?X1 (list_remove nat eq_nat_dec ?X1 (freeVarFormula LNN ?X2))) |- _
  4367. =>
  4368. elim (In_list_remove2 _ _ _ _ _ H); reflexivity
  4369. | H:(In ?X3 (list_remove nat eq_nat_dec ?X1 (freeVarFormula LNN ?X2))) |- _
  4370. =>
  4371. assert (In X3 (freeVarFormula LNN X2));
  4372. [ eapply In_list_remove1; apply H
  4373. | assert (X3 <> X1); [ eapply In_list_remove2; apply H | clear H ] ]
  4374. | H:(In ?X4 (freeVarFormula LNN (substituteFormula LNN ?X1 ?X2 ?X3))) |- _
  4375. =>
  4376. induction (freeVarSubFormula3 _ _ _ _ _ H); clear H
  4377. | H:(In ?X4 (freeVarTerm LNN (var ?X1))) |- _ =>
  4378. induction H as [H3| H3]; [ idtac | contradiction ]
  4379. end.
  4380. elim (le_not_lt (S (S n)) (S n)).
  4381. rewrite <- H3.
  4382. apply le_n.
  4383. apply lt_n_Sn.
  4384. apply
  4385. iffTrans
  4386. with
  4387. (substituteFormula LNN
  4388. (substituteFormula LNN
  4389. (substituteFormula LNN
  4390. (substituteFormula LNN B (S n) (natToTerm a0))
  4391. (S (S (S n))) (natToTerm a1)) (S (S n))
  4392. (var (S n))) (S n) (natToTerm a2)).
  4393. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4394. apply (subFormulaExch LNN).
  4395. unfold not in |- *; intros.
  4396. elim (le_not_lt (S (S (S n))) (S (S n))).
  4397. rewrite <- H3.
  4398. apply le_n.
  4399. apply lt_n_Sn.
  4400. unfold not in |- *; intros.
  4401. simpl in H3.
  4402. decompose sum H3.
  4403. elim (le_not_lt (S (S (S n))) (S n)).
  4404. rewrite <- H4.
  4405. apply le_n.
  4406. apply lt_S.
  4407. apply lt_n_Sn.
  4408. apply closedNatToTerm.
  4409. apply
  4410. iffTrans
  4411. with
  4412. (substituteFormula LNN
  4413. (substituteFormula LNN (substituteFormula LNN B (S n) (natToTerm a0))
  4414. (S (S (S n))) (natToTerm a1)) (S (S n)) (natToTerm a2)).
  4415. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4416. apply (subFormulaTrans LNN).
  4417. unfold not in |- *; intros.
  4418. repeat
  4419. match goal with
  4420. | H:(In ?X1 (list_remove nat eq_nat_dec ?X1 (freeVarFormula LNN ?X2))) |- _
  4421. =>
  4422. elim (In_list_remove2 _ _ _ _ _ H); reflexivity
  4423. | H:(In ?X3 (list_remove nat eq_nat_dec ?X1 (freeVarFormula LNN ?X2))) |- _
  4424. =>
  4425. assert (In X3 (freeVarFormula LNN X2));
  4426. [ eapply In_list_remove1; apply H
  4427. | assert (X3 <> X1); [ eapply In_list_remove2; apply H | clear H ] ]
  4428. | H:(In ?X4 (freeVarFormula LNN (substituteFormula LNN ?X1 ?X2 ?X3))) |- _
  4429. =>
  4430. induction (freeVarSubFormula3 _ _ _ _ _ H); clear H
  4431. | H:(In ?X4 (freeVarTerm LNN (var ?X1))) |- _ =>
  4432. simple induction H; [ idtac | contradiction ]
  4433. end.
  4434. elim (closedNatToTerm _ _ H3).
  4435. elim (closedNatToTerm _ _ H3).
  4436. apply
  4437. iffTrans
  4438. with
  4439. (substituteFormula LNN
  4440. (substituteFormula LNN
  4441. (substituteFormula LNN B (S (S (S n))) (natToTerm a1))
  4442. (S n) (natToTerm a0)) (S (S n)) (natToTerm a2)).
  4443. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4444. apply (subFormulaExch LNN).
  4445. unfold not in |- *; intros.
  4446. elim (le_not_lt (S (S (S n))) (S n)).
  4447. rewrite <- H3.
  4448. apply le_n.
  4449. apply lt_S.
  4450. apply lt_n_Sn.
  4451. apply closedNatToTerm.
  4452. apply closedNatToTerm.
  4453. apply (subFormulaExch LNN).
  4454. unfold not in |- *; intros.
  4455. elim (le_not_lt (S (S n)) (S n)).
  4456. rewrite <- H3.
  4457. apply le_n.
  4458. apply lt_n_Sn.
  4459. apply closedNatToTerm.
  4460. apply closedNatToTerm.
  4461. apply H2.
  4462. apply
  4463. RepresentableAlternate
  4464. with
  4465. (substituteFormula LNN
  4466. (primRecSigmaFormula n (substituteFormula LNN A (S n) (natToTerm a0))
  4467. (substituteFormula LNN
  4468. (substituteFormula LNN
  4469. (substituteFormula LNN B (S n) (natToTerm a0))
  4470. (S (S n)) (var (S n))) (S (S (S n)))
  4471. (var (S (S n))))) (S n) (natToTerm a)).
  4472. clear H3 Hrecn.
  4473. apply iffSym.
  4474. apply
  4475. iffTrans
  4476. with
  4477. (substituteFormula LNN
  4478. (substituteFormula LNN (primRecSigmaFormula (S n) A B)
  4479. (S n) (natToTerm a0)) (S (S n)) (natToTerm a)).
  4480. apply (subFormulaExch LNN).
  4481. unfold not in |- *; intros.
  4482. elim (le_not_lt (S (S n)) (S n)).
  4483. rewrite H3.
  4484. apply le_n.
  4485. apply lt_n_Sn.
  4486. apply closedNatToTerm.
  4487. apply closedNatToTerm.
  4488. apply
  4489. iffTrans
  4490. with
  4491. (substituteFormula LNN
  4492. (substituteFormula LNN
  4493. (substituteFormula LNN (primRecSigmaFormula (S n) A B)
  4494. (S n) (natToTerm a0)) (S (S n)) (var (S n)))
  4495. (S n) (natToTerm a)).
  4496. apply iffSym.
  4497. apply (subFormulaTrans LNN).
  4498. unfold not in |- *; intros.
  4499. assert
  4500. (In (S n)
  4501. (freeVarFormula LNN
  4502. (substituteFormula LNN (primRecSigmaFormula (S n) A B)
  4503. (S n) (natToTerm a0)))).
  4504. eapply In_list_remove1.
  4505. apply H3.
  4506. induction (freeVarSubFormula3 _ _ _ _ _ H4).
  4507. elim (In_list_remove2 _ _ _ _ _ H5).
  4508. reflexivity.
  4509. elim (closedNatToTerm _ _ H5).
  4510. apply (reduceSub LNN).
  4511. apply closedNN.
  4512. unfold primRecSigmaFormula in |- *.
  4513. assert (H3 := I). (* For hyps numbering compatibility *)
  4514. assert (H4 := I). (* For hyps numbering compatibility *)
  4515. assert
  4516. (subExistSpecial :
  4517. forall (F : Formula) (a b c : nat),
  4518. b <> c ->
  4519. substituteFormula LNN (existH b F) c (natToTerm a) =
  4520. existH b (substituteFormula LNN F c (natToTerm a))).
  4521. intros.
  4522. rewrite (subFormulaExist LNN).
  4523. induction (eq_nat_dec b c).
  4524. elim H5.
  4525. auto.
  4526. induction (In_dec eq_nat_dec b (freeVarTerm LNN (natToTerm a1))).
  4527. elim (closedNatToTerm _ _ a2).
  4528. reflexivity.
  4529. assert
  4530. (subForallSpecial :
  4531. forall (F : Formula) (a b c : nat),
  4532. b <> c ->
  4533. substituteFormula LNN (forallH b F) c (natToTerm a) =
  4534. forallH b (substituteFormula LNN F c (natToTerm a))).
  4535. intros.
  4536. rewrite (subFormulaForall LNN).
  4537. induction (eq_nat_dec b c).
  4538. elim H5.
  4539. auto.
  4540. induction (In_dec eq_nat_dec b (freeVarTerm LNN (natToTerm a1))).
  4541. elim (closedNatToTerm _ _ a2).
  4542. reflexivity.
  4543. assert (forall a b : nat, a <> b -> b <> a).
  4544. auto.
  4545. assert
  4546. (subExistSpecial2 :
  4547. forall (F : Formula) (a b c : nat),
  4548. b <> c ->
  4549. b <> a ->
  4550. substituteFormula LNN (existH b F) c (var a) =
  4551. existH b (substituteFormula LNN F c (var a))).
  4552. intros.
  4553. rewrite (subFormulaExist LNN).
  4554. induction (eq_nat_dec b c).
  4555. elim H6.
  4556. auto.
  4557. induction (In_dec eq_nat_dec b (freeVarTerm LNN (var a1))).
  4558. induction a2 as [H8| H8].
  4559. elim H7; auto.
  4560. elim H8.
  4561. reflexivity.
  4562. assert
  4563. (subForallSpecial2 :
  4564. forall (F : Formula) (a b c : nat),
  4565. b <> c ->
  4566. b <> a ->
  4567. substituteFormula LNN (forallH b F) c (var a) =
  4568. forallH b (substituteFormula LNN F c (var a))).
  4569. intros.
  4570. rewrite (subFormulaForall LNN).
  4571. induction (eq_nat_dec b c).
  4572. elim H6.
  4573. auto.
  4574. induction (In_dec eq_nat_dec b (freeVarTerm LNN (var a1))).
  4575. induction a2 as [H8| H8].
  4576. elim H7; auto.
  4577. elim H8.
  4578. reflexivity.
  4579. assert (H6 := I). (* For hyps numbering compatibility *)
  4580. assert (H7 := I). (* For hyps numbering compatibility *)
  4581. assert
  4582. (forall (a b : Term) (v : nat) (s : Term),
  4583. substituteFormula LNN (LT a b) v s =
  4584. LT (substituteTerm LNN a v s) (substituteTerm LNN b v s)).
  4585. intros.
  4586. unfold LT in |- *.
  4587. rewrite (subFormulaRelation LNN).
  4588. reflexivity.
  4589. assert
  4590. (forall (f : Formula) (a : nat) (s : Term),
  4591. substituteFormula LNN (existH a f) a s = existH a f).
  4592. intros.
  4593. rewrite (subFormulaExist LNN).
  4594. induction (eq_nat_dec a1 a1).
  4595. reflexivity.
  4596. elim b; auto.
  4597. assert
  4598. (forall (f : Formula) (a : nat) (s : Term),
  4599. substituteFormula LNN (forallH a f) a s = forallH a f).
  4600. intros.
  4601. rewrite (subFormulaForall LNN).
  4602. induction (eq_nat_dec a1 a1).
  4603. reflexivity.
  4604. elim b; auto.
  4605. assert (H11 := I). (* For hyps numbering compatibility *)
  4606. assert (H12 := I). (* For hyps numbering compatibility *)
  4607. assert (H13 := I). (* For hyps numbering compatibility *)
  4608. assert (H14 := I). (* For hyps numbering compatibility *)
  4609. assert (H15 := I). (* For hyps numbering compatibility *)
  4610. assert (H16 := I). (* For hyps numbering compatibility *)
  4611.  
  4612. Opaque substituteFormula.
  4613.  
  4614.  
  4615. unfold minimize, primRecSigmaFormulaHelp, primRecPiFormulaHelp, andH, impH,
  4616. notH in |- *;
  4617. repeat first
  4618. [ discriminate
  4619. | simple apply iffRefl
  4620. | simple apply (reduceExist LNN); [ apply closedNN | idtac ]
  4621. | simple apply (reduceForall LNN); [ apply closedNN | idtac ]
  4622. | simple apply (reduceAnd LNN)
  4623. | simple apply (reduceImp LNN)
  4624. | simple apply (reduceNot LNN)
  4625. | match goal with
  4626. | |-
  4627. (folProof.SysPrf LNN NN
  4628. (fol.iffH LNN
  4629. (substituteFormula LNN
  4630. (substituteFormula LNN (existH (S (S n)) ?X1) ?X2
  4631. (var (S (S n)))) ?X3 ?X4) _)) =>
  4632. apply
  4633. iffTrans
  4634. with
  4635. (substituteFormula LNN
  4636. (substituteFormula LNN
  4637. (existH (S n)
  4638. (substituteFormula LNN X1 (S (S n)) (var (S n)))) X2
  4639. (var (S (S n)))) X3 X4);
  4640. [ repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]);
  4641. apply (rebindExist LNN)
  4642. | idtac ]
  4643. | |-
  4644. (folProof.SysPrf LNN NN
  4645. (fol.iffH LNN
  4646. (substituteFormula LNN
  4647. (substituteFormula LNN
  4648. (substituteFormula LNN (forallH (S (S n)) ?X1) ?X2
  4649. (var (S (S n)))) ?X3 ?X4) ?X5 ?X6) _)) =>
  4650. apply
  4651. iffTrans
  4652. with
  4653. (substituteFormula LNN
  4654. (substituteFormula LNN
  4655. (substituteFormula LNN
  4656. (forallH (S n)
  4657. (substituteFormula LNN X1 (S (S n)) (var (S n)))) X2
  4658. (var (S (S n)))) X3 X4) X5 X6);
  4659. [ repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]);
  4660. apply (rebindForall LNN)
  4661. | idtac ]
  4662. | |-
  4663. (folProof.SysPrf LNN NN
  4664. (fol.iffH LNN
  4665. (substituteFormula LNN (forallH (S ?X6) ?X1) ?X2 (var (S ?X6))) _))
  4666. =>
  4667. apply
  4668. iffTrans
  4669. with
  4670. (substituteFormula LNN
  4671. (forallH X6 (substituteFormula LNN X1 (S X6) (var X6))) X2
  4672. (var (S X6)));
  4673. [ repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]);
  4674. apply (rebindForall LNN)
  4675. | idtac ]
  4676. | |- (folProof.SysPrf LNN NN (fol.iffH LNN (existH (S ?X1) ?X2) ?X3)) =>
  4677. apply
  4678. iffTrans with (existH X1 (substituteFormula LNN X2 (S X1) (var X1)));
  4679. [ apply (rebindExist LNN) | idtac ]
  4680. | |- (folProof.SysPrf LNN NN (fol.iffH LNN (forallH (S ?X1) ?X2) ?X3))
  4681. =>
  4682. apply
  4683. iffTrans
  4684. with (forallH X1 (substituteFormula LNN X2 (S X1) (var X1)));
  4685. [ apply (rebindForall LNN) | idtac ]
  4686. | |- (?X1 <> S ?X1) => apply n_Sn
  4687. | |- (?X1 <> S (S ?X1)) => apply n_SSn
  4688. | |- (?X1 <> S (S (S ?X1))) => apply n_SSSn
  4689. | |- (?X1 <> S (S (S (S ?X1)))) => apply n_SSSSn
  4690. | |- (S ?X1 <> ?X1) => apply H5; apply n_Sn
  4691. | |- (S (S ?X1) <> ?X1) => apply H5; apply n_SSn
  4692. | |- (S (S (S ?X1)) <> ?X1) => apply H5; apply n_SSSn
  4693. | |- (S (S (S (S ?X1))) <> ?X1) => apply H5; apply n_SSSSn
  4694. | |- (~ In _ _) => PRsolveFV A B n
  4695. end
  4696. | rewrite H9
  4697. | rewrite H10
  4698. | rewrite (subFormulaAnd LNN)
  4699. | rewrite (subFormulaImp LNN)
  4700. | rewrite (subFormulaNot LNN)
  4701. | rewrite H8
  4702. | rewrite (subTermVar1 LNN)
  4703. | rewrite (subTermVar2 LNN)
  4704. | rewrite subForallSpecial2;
  4705. let fail :=
  4706. (match goal with
  4707. | |- (?X1 <> ?X1) => constr:(false)
  4708. | _ => constr:(true)
  4709. end) in
  4710. match constr:(fail) with
  4711. | true => idtac
  4712. end
  4713. | rewrite subForallSpecial
  4714. | rewrite subExistSpecial2;
  4715. let fail :=
  4716. (match goal with
  4717. | |- (?X1 <> ?X1) => constr:(false)
  4718. | _ => constr:(true)
  4719. end) in
  4720. match constr:(fail) with
  4721. | true => idtac
  4722. end
  4723. | rewrite subExistSpecial ].
  4724. apply
  4725. iffTrans
  4726. with
  4727. (substituteFormula LNN (substituteFormula LNN A (S n) (natToTerm a0))
  4728. (S (S (S n))) (var (S (S n)))).
  4729. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4730. apply (subFormulaNil LNN).
  4731. PRsolveFV A B n.
  4732. apply (subFormulaNil LNN).
  4733. PRsolveFV A B n.
  4734. apply
  4735. iffTrans
  4736. with
  4737. (substituteFormula LNN
  4738. (substituteFormula LNN
  4739. (substituteFormula LNN (substituteFormula LNN betaFormula 1 Zero) 2
  4740. (var (S (S (S n))))) (S (S n)) (var (S n)))
  4741. (S (S (S n))) (var (S (S n)))).
  4742. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4743. apply (subFormulaNil LNN).
  4744. PRsolveFV A B n.
  4745. apply
  4746. iffTrans
  4747. with
  4748. (substituteFormula LNN
  4749. (substituteFormula LNN (substituteFormula LNN betaFormula 1 Zero) 2
  4750. (var (S (S (S n))))) (S (S (S n))) (var (S (S n)))).
  4751. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4752. apply (subFormulaNil LNN).
  4753. PRsolveFV A B n.
  4754. apply (subFormulaTrans LNN).
  4755. PRsolveFV A B n.
  4756. apply
  4757. iffTrans
  4758. with
  4759. (substituteFormula LNN
  4760. (substituteFormula LNN
  4761. (substituteFormula LNN
  4762. (substituteFormula LNN
  4763. (substituteFormula LNN
  4764. (substituteFormula LNN betaFormula 1
  4765. (var (S (S (S (S n)))))) 2 (var (S (S (S n))))) 0
  4766. (var (S (S n)))) (S (S n)) (var (S n)))
  4767. (S (S (S n))) (var (S (S n)))) (S (S (S (S n))))
  4768. (var (S (S (S n))))).
  4769. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4770. apply (subFormulaNil LNN).
  4771. PRsolveFV A B n.
  4772. apply
  4773. iffTrans
  4774. with
  4775. (substituteFormula LNN
  4776. (substituteFormula LNN
  4777. (substituteFormula LNN
  4778. (substituteFormula LNN
  4779. (substituteFormula LNN betaFormula 1 (var (S (S (S (S n))))))
  4780. 2 (var (S (S (S n))))) 0 (var (S n)))
  4781. (S (S (S n))) (var (S (S n)))) (S (S (S (S n))))
  4782. (var (S (S (S n))))).
  4783. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4784. apply (subFormulaTrans LNN).
  4785. PRsolveFV A B n.
  4786. apply
  4787. iffTrans
  4788. with
  4789. (substituteFormula LNN
  4790. (substituteFormula LNN
  4791. (substituteFormula LNN
  4792. (substituteFormula LNN
  4793. (substituteFormula LNN betaFormula 1 (var (S (S (S (S n))))))
  4794. 2 (var (S (S (S n))))) (S (S (S n)))
  4795. (var (S (S n)))) 0 (var (S n))) (S (S (S (S n))))
  4796. (var (S (S (S n))))).
  4797. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4798. apply (subFormulaExch LNN); PRsolveFV A B n.
  4799. apply
  4800. iffTrans
  4801. with
  4802. (substituteFormula LNN
  4803. (substituteFormula LNN
  4804. (substituteFormula LNN
  4805. (substituteFormula LNN betaFormula 1 (var (S (S (S (S n)))))) 2
  4806. (var (S (S n)))) 0 (var (S n))) (S (S (S (S n))))
  4807. (var (S (S (S n))))).
  4808. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4809. apply (subFormulaTrans LNN).
  4810. PRsolveFV A B n.
  4811. apply
  4812. iffTrans
  4813. with
  4814. (substituteFormula LNN
  4815. (substituteFormula LNN
  4816. (substituteFormula LNN
  4817. (substituteFormula LNN betaFormula 1 (var (S (S (S (S n)))))) 2
  4818. (var (S (S n)))) (S (S (S (S n)))) (var (S (S (S n))))) 0
  4819. (var (S n))).
  4820. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4821. apply (subFormulaExch LNN); PRsolveFV A B n.
  4822. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4823. apply
  4824. iffTrans
  4825. with
  4826. (substituteFormula LNN
  4827. (substituteFormula LNN
  4828. (substituteFormula LNN betaFormula 1 (var (S (S (S (S n))))))
  4829. (S (S (S (S n)))) (var (S (S (S n))))) 2
  4830. (var (S (S n)))).
  4831. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4832. apply (subFormulaExch LNN); PRsolveFV A B n.
  4833. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4834. apply (subFormulaTrans LNN).
  4835. PRsolveFV A B n.
  4836. apply
  4837. iffTrans
  4838. with
  4839. (substituteFormula LNN
  4840. (substituteFormula LNN
  4841. (substituteFormula LNN
  4842. (substituteFormula LNN
  4843. (substituteFormula LNN B (S n) (natToTerm a0))
  4844. (S (S (S n))) (var (S (S (S (S n))))))
  4845. (S (S n)) (var (S n))) (S (S (S n))) (var (S (S n))))
  4846. (S (S (S (S n)))) (var (S (S (S n))))).
  4847. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4848. apply (subFormulaExch LNN); PRsolveFV A B n.
  4849. apply
  4850. iffTrans
  4851. with
  4852. (substituteFormula LNN
  4853. (substituteFormula LNN
  4854. (substituteFormula LNN
  4855. (substituteFormula LNN
  4856. (substituteFormula LNN B (S n) (natToTerm a0))
  4857. (S (S n)) (var (S n))) (S (S (S n)))
  4858. (var (S (S (S (S n)))))) (S (S (S n)))
  4859. (var (S (S n)))) (S (S (S (S n)))) (var (S (S (S n))))).
  4860. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4861. apply (subFormulaExch LNN); PRsolveFV A B n.
  4862. apply
  4863. iffTrans
  4864. with
  4865. (substituteFormula LNN
  4866. (substituteFormula LNN
  4867. (substituteFormula LNN
  4868. (substituteFormula LNN B (S n) (natToTerm a0))
  4869. (S (S n)) (var (S n))) (S (S (S n))) (var (S (S (S (S n))))))
  4870. (S (S (S (S n)))) (var (S (S (S n))))).
  4871. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4872. apply (subFormulaNil LNN); PRsolveFV A B n.
  4873. apply
  4874. iffTrans
  4875. with
  4876. (substituteFormula LNN
  4877. (substituteFormula LNN (substituteFormula LNN B (S n) (natToTerm a0))
  4878. (S (S n)) (var (S n))) (S (S (S n))) (var (S (S (S n))))).
  4879. apply (subFormulaTrans LNN); PRsolveFV A B n.
  4880. apply iffSym.
  4881. apply (subFormulaTrans LNN); PRsolveFV A B n.
  4882. apply
  4883. iffTrans
  4884. with
  4885. (substituteFormula LNN
  4886. (substituteFormula LNN
  4887. (substituteFormula LNN
  4888. (substituteFormula LNN
  4889. (substituteFormula LNN betaFormula 1
  4890. (Succ (var (S (S (S (S n))))))) 2
  4891. (var (S (S (S n))))) (S (S n)) (var (S n)))
  4892. (S (S (S n))) (var (S (S n)))) (S (S (S (S n))))
  4893. (var (S (S (S n))))).
  4894. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4895. apply (subFormulaNil LNN); PRsolveFV A B n.
  4896. apply
  4897. iffTrans
  4898. with
  4899. (substituteFormula LNN
  4900. (substituteFormula LNN
  4901. (substituteFormula LNN
  4902. (substituteFormula LNN betaFormula 1
  4903. (Succ (var (S (S (S (S n))))))) 2 (var (S (S (S n)))))
  4904. (S (S (S n))) (var (S (S n)))) (S (S (S (S n))))
  4905. (var (S (S (S n))))).
  4906. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4907. apply (subFormulaNil LNN); PRsolveFV A B n.
  4908. apply
  4909. iffTrans
  4910. with
  4911. (substituteFormula LNN
  4912. (substituteFormula LNN
  4913. (substituteFormula LNN betaFormula 1 (Succ (var (S (S (S (S n)))))))
  4914. 2 (var (S (S n)))) (S (S (S (S n)))) (var (S (S (S n))))).
  4915. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4916. apply (subFormulaTrans LNN); PRsolveFV A B n.
  4917. apply
  4918. iffTrans
  4919. with
  4920. (substituteFormula LNN
  4921. (substituteFormula LNN
  4922. (substituteFormula LNN betaFormula 1 (Succ (var (S (S (S (S n)))))))
  4923. (S (S (S (S n)))) (var (S (S (S n))))) 2
  4924. (var (S (S n)))).
  4925. apply (subFormulaExch LNN); PRsolveFV A B n.
  4926. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4927. apply
  4928. iffTrans
  4929. with
  4930. (substituteFormula LNN
  4931. (substituteFormula LNN betaFormula (S (S (S (S n))))
  4932. (var (S (S (S n))))) 1
  4933. (substituteTerm LNN (Succ (var (S (S (S (S n))))))
  4934. (S (S (S (S n)))) (var (S (S (S n)))))).
  4935. apply (subSubFormula LNN); PRsolveFV A B n.
  4936. replace
  4937. (substituteTerm LNN (Succ (var (S (S (S (S n))))))
  4938. (S (S (S (S n)))) (var (S (S (S n))))) with
  4939. (Succ
  4940. (substituteTerm LNN (var (S (S (S (S n))))) (S (S (S (S n))))
  4941. (var (S (S (S n)))))).
  4942. rewrite (subTermVar1 LNN).
  4943. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4944. apply (subFormulaNil LNN); PRsolveFV A B n.
  4945. reflexivity.
  4946. apply
  4947. iffTrans
  4948. with
  4949. (substituteFormula LNN
  4950. (substituteFormula LNN
  4951. (substituteFormula LNN
  4952. (substituteFormula LNN A (S n) (natToTerm a0))
  4953. (S (S n)) (var (S n))) (S (S (S n))) (var (S (S n))))
  4954. (S (S (S (S (S n))))) (var (S (S (S (S n)))))).
  4955. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4956. apply (subFormulaNil LNN); PRsolveFV A B n.
  4957. apply
  4958. iffTrans
  4959. with
  4960. (substituteFormula LNN
  4961. (substituteFormula LNN (substituteFormula LNN A (S n) (natToTerm a0))
  4962. (S (S (S n))) (var (S (S n)))) (S (S (S (S (S n)))))
  4963. (var (S (S (S (S n)))))).
  4964. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4965. apply (subFormulaNil LNN); PRsolveFV A B n.
  4966. apply
  4967. iffTrans
  4968. with
  4969. (substituteFormula LNN (substituteFormula LNN A (S n) (natToTerm a0))
  4970. (S (S (S (S (S n))))) (var (S (S (S (S n)))))).
  4971. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4972. apply (subFormulaNil LNN); PRsolveFV A B n.
  4973. apply iffTrans with (substituteFormula LNN A (S n) (natToTerm a0)).
  4974. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4975. apply (subFormulaNil LNN); PRsolveFV A B n.
  4976. apply iffSym.
  4977. apply (subFormulaNil LNN); PRsolveFV A B n.
  4978. apply
  4979. iffTrans
  4980. with
  4981. (substituteFormula LNN
  4982. (substituteFormula LNN
  4983. (substituteFormula LNN
  4984. (substituteFormula LNN
  4985. (substituteFormula LNN
  4986. (substituteFormula LNN betaFormula 1 Zero) 2
  4987. (var (S (S (S (S (S n))))))) (S n)
  4988. (natToTerm a0)) (S (S n)) (var (S n)))
  4989. (S (S (S n))) (var (S (S n)))) (S (S (S (S (S n)))))
  4990. (var (S (S (S (S n)))))).
  4991. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  4992. apply (subFormulaTrans LNN); PRsolveFV A B n.
  4993. apply
  4994. iffTrans
  4995. with
  4996. (substituteFormula LNN
  4997. (substituteFormula LNN
  4998. (substituteFormula LNN
  4999. (substituteFormula LNN
  5000. (substituteFormula LNN betaFormula 1 Zero) 2
  5001. (var (S (S (S (S (S n))))))) (S (S n))
  5002. (var (S n))) (S (S (S n))) (var (S (S n))))
  5003. (S (S (S (S (S n))))) (var (S (S (S (S n)))))).
  5004. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5005. apply (subFormulaNil LNN); PRsolveFV A B n.
  5006. elim (le_not_lt (S (S (S (S (S n))))) (S n)).
  5007. rewrite H17.
  5008. apply le_n.
  5009. do 3 apply lt_S.
  5010. apply lt_n_Sn.
  5011. apply
  5012. iffTrans
  5013. with
  5014. (substituteFormula LNN
  5015. (substituteFormula LNN
  5016. (substituteFormula LNN (substituteFormula LNN betaFormula 1 Zero) 2
  5017. (var (S (S (S (S (S n))))))) (S (S (S n)))
  5018. (var (S (S n)))) (S (S (S (S (S n))))) (var (S (S (S (S n)))))).
  5019. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5020. apply (subFormulaNil LNN); PRsolveFV A B n.
  5021. apply
  5022. iffTrans
  5023. with
  5024. (substituteFormula LNN
  5025. (substituteFormula LNN (substituteFormula LNN betaFormula 1 Zero) 2
  5026. (var (S (S (S (S (S n))))))) (S (S (S (S (S n)))))
  5027. (var (S (S (S (S n)))))).
  5028. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5029. apply (subFormulaNil LNN); PRsolveFV A B n.
  5030. apply
  5031. iffTrans
  5032. with
  5033. (substituteFormula LNN (substituteFormula LNN betaFormula 1 Zero) 2
  5034. (var (S (S (S (S n)))))).
  5035. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5036. apply (subFormulaTrans LNN); PRsolveFV A B n.
  5037. apply iffSym.
  5038. apply (subFormulaTrans LNN); PRsolveFV A B n.
  5039. elim H19; symmetry in |- *; apply H17.
  5040. apply
  5041. iffTrans
  5042. with
  5043. (substituteFormula LNN
  5044. (substituteFormula LNN
  5045. (substituteFormula LNN
  5046. (substituteFormula LNN
  5047. (substituteFormula LNN
  5048. (substituteFormula LNN
  5049. (substituteFormula LNN
  5050. (substituteFormula LNN
  5051. (substituteFormula LNN betaFormula 1
  5052. (var (S (S (S (S n)))))) 2
  5053. (var (S (S (S n))))) (S (S (S n)))
  5054. (var (S (S (S (S (S n))))))) 0
  5055. (var (S (S n)))) (S n) (natToTerm a0))
  5056. (S (S n)) (var (S n))) (S (S (S n)))
  5057. (var (S (S n)))) (S (S (S (S n)))) (var (S (S (S n)))))
  5058. (S (S (S (S (S n))))) (var (S (S (S (S n)))))).
  5059. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5060. apply (subFormulaExch LNN); PRsolveFV A B n.
  5061. apply
  5062. iffTrans
  5063. with
  5064. (substituteFormula LNN
  5065. (substituteFormula LNN
  5066. (substituteFormula LNN
  5067. (substituteFormula LNN
  5068. (substituteFormula LNN
  5069. (substituteFormula LNN
  5070. (substituteFormula LNN
  5071. (substituteFormula LNN betaFormula 1
  5072. (var (S (S (S (S n)))))) 2
  5073. (var (S (S (S (S (S n))))))) 0
  5074. (var (S (S n)))) (S n) (natToTerm a0))
  5075. (S (S n)) (var (S n))) (S (S (S n)))
  5076. (var (S (S n)))) (S (S (S (S n)))) (var (S (S (S n)))))
  5077. (S (S (S (S (S n))))) (var (S (S (S (S n)))))).
  5078. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5079. apply (subFormulaTrans LNN); PRsolveFV A B n.
  5080. apply
  5081. iffTrans
  5082. with
  5083. (substituteFormula LNN
  5084. (substituteFormula LNN
  5085. (substituteFormula LNN
  5086. (substituteFormula LNN
  5087. (substituteFormula LNN
  5088. (substituteFormula LNN
  5089. (substituteFormula LNN betaFormula 1
  5090. (var (S (S (S (S n)))))) 2
  5091. (var (S (S (S (S (S n))))))) 0
  5092. (var (S (S n)))) (S (S n)) (var (S n)))
  5093. (S (S (S n))) (var (S (S n)))) (S (S (S (S n))))
  5094. (var (S (S (S n))))) (S (S (S (S (S n)))))
  5095. (var (S (S (S (S n)))))).
  5096. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5097. apply (subFormulaNil LNN); PRsolveFV A B n.
  5098. elim (le_not_lt (S (S (S (S (S n))))) (S n)).
  5099. rewrite H17.
  5100. apply le_n.
  5101. do 3 apply lt_S.
  5102. apply lt_n_Sn.
  5103. apply
  5104. iffTrans
  5105. with
  5106. (substituteFormula LNN
  5107. (substituteFormula LNN
  5108. (substituteFormula LNN
  5109. (substituteFormula LNN
  5110. (substituteFormula LNN
  5111. (substituteFormula LNN betaFormula 1
  5112. (var (S (S (S (S n)))))) 2 (var (S (S (S (S (S n)))))))
  5113. 0 (var (S n))) (S (S (S n))) (var (S (S n))))
  5114. (S (S (S (S n)))) (var (S (S (S n))))) (S (S (S (S (S n)))))
  5115. (var (S (S (S (S n)))))).
  5116. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5117. apply (subFormulaTrans LNN); PRsolveFV A B n.
  5118. apply
  5119. iffTrans
  5120. with
  5121. (substituteFormula LNN
  5122. (substituteFormula LNN
  5123. (substituteFormula LNN
  5124. (substituteFormula LNN
  5125. (substituteFormula LNN betaFormula 1 (var (S (S (S (S n))))))
  5126. 2 (var (S (S (S (S (S n))))))) 0 (var (S n)))
  5127. (S (S (S (S n)))) (var (S (S (S n))))) (S (S (S (S (S n)))))
  5128. (var (S (S (S (S n)))))).
  5129. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5130. apply (subFormulaNil LNN); PRsolveFV A B n.
  5131. apply
  5132. iffTrans
  5133. with
  5134. (substituteFormula LNN
  5135. (substituteFormula LNN
  5136. (substituteFormula LNN
  5137. (substituteFormula LNN
  5138. (substituteFormula LNN betaFormula 1 (var (S (S (S (S n))))))
  5139. 2 (var (S (S (S (S (S n))))))) (S (S (S (S n))))
  5140. (var (S (S (S n))))) 0 (var (S n))) (S (S (S (S (S n)))))
  5141. (var (S (S (S (S n)))))).
  5142. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5143. apply (subFormulaExch LNN); PRsolveFV A B n.
  5144. apply
  5145. iffTrans
  5146. with
  5147. (substituteFormula LNN
  5148. (substituteFormula LNN
  5149. (substituteFormula LNN
  5150. (substituteFormula LNN
  5151. (substituteFormula LNN betaFormula 1 (var (S (S (S (S n))))))
  5152. (S (S (S (S n)))) (var (S (S (S n))))) 2
  5153. (var (S (S (S (S (S n))))))) 0 (var (S n)))
  5154. (S (S (S (S (S n))))) (var (S (S (S (S n)))))).
  5155. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5156. apply (subFormulaExch LNN); PRsolveFV A B n.
  5157. apply
  5158. iffTrans
  5159. with
  5160. (substituteFormula LNN
  5161. (substituteFormula LNN
  5162. (substituteFormula LNN
  5163. (substituteFormula LNN betaFormula 1 (var (S (S (S n))))) 2
  5164. (var (S (S (S (S (S n))))))) 0 (var (S n)))
  5165. (S (S (S (S (S n))))) (var (S (S (S (S n)))))).
  5166. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5167. apply (subFormulaTrans LNN); PRsolveFV A B n.
  5168. apply
  5169. iffTrans
  5170. with
  5171. (substituteFormula LNN
  5172. (substituteFormula LNN
  5173. (substituteFormula LNN
  5174. (substituteFormula LNN betaFormula 1 (var (S (S (S n))))) 2
  5175. (var (S (S (S (S (S n))))))) (S (S (S (S (S n)))))
  5176. (var (S (S (S (S n)))))) 0 (var (S n))).
  5177. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5178. apply (subFormulaExch LNN); PRsolveFV A B n.
  5179. elim (le_not_lt (S (S (S (S (S n))))) (S n)).
  5180. rewrite <- H18.
  5181. apply le_n.
  5182. do 3 apply lt_S.
  5183. apply lt_n_Sn.
  5184. apply
  5185. iffTrans
  5186. with
  5187. (substituteFormula LNN
  5188. (substituteFormula LNN
  5189. (substituteFormula LNN betaFormula 1 (var (S (S (S n))))) 2
  5190. (var (S (S (S (S n)))))) 0 (var (S n))).
  5191. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5192. apply (subFormulaTrans LNN); PRsolveFV A B n.
  5193. apply iffSym.
  5194. apply
  5195. iffTrans
  5196. with
  5197. (substituteFormula LNN
  5198. (substituteFormula LNN
  5199. (substituteFormula LNN
  5200. (substituteFormula LNN betaFormula 1 (var (S (S (S n))))) 2
  5201. (var (S (S n)))) (S (S n)) (var (S (S (S (S n)))))) 0
  5202. (var (S n))).
  5203. apply (subFormulaExch LNN); PRsolveFV A B n.
  5204. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5205. apply (subFormulaTrans LNN); PRsolveFV A B n.
  5206. elim H19; symmetry in |- *; assumption.
  5207. apply
  5208. iffTrans
  5209. with
  5210. (substituteFormula LNN
  5211. (substituteFormula LNN
  5212. (substituteFormula LNN
  5213. (substituteFormula LNN
  5214. (substituteFormula LNN
  5215. (substituteFormula LNN B (S (S (S n)))
  5216. (var (S (S (S (S n)))))) (S n)
  5217. (natToTerm a0)) (S (S n)) (var (S n)))
  5218. (S (S (S n))) (var (S (S n)))) (S (S (S (S n))))
  5219. (var (S (S (S n))))) (S (S (S (S (S n)))))
  5220. (var (S (S (S (S n)))))).
  5221. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5222. apply (subFormulaNil LNN); PRsolveFV A B n.
  5223. apply
  5224. iffTrans
  5225. with
  5226. (substituteFormula LNN
  5227. (substituteFormula LNN
  5228. (substituteFormula LNN
  5229. (substituteFormula LNN
  5230. (substituteFormula LNN B (S (S (S n)))
  5231. (var (S (S (S (S n)))))) (S n) (natToTerm a0))
  5232. (S (S n)) (var (S n))) (S (S (S (S n))))
  5233. (var (S (S (S n))))) (S (S (S (S (S n)))))
  5234. (var (S (S (S (S n)))))).
  5235. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5236. apply (subFormulaNil LNN); PRsolveFV A B n.
  5237. apply
  5238. iffTrans
  5239. with
  5240. (substituteFormula LNN
  5241. (substituteFormula LNN
  5242. (substituteFormula LNN
  5243. (substituteFormula LNN
  5244. (substituteFormula LNN B (S n) (natToTerm a0))
  5245. (S (S (S n))) (var (S (S (S (S n))))))
  5246. (S (S n)) (var (S n))) (S (S (S (S n))))
  5247. (var (S (S (S n))))) (S (S (S (S (S n)))))
  5248. (var (S (S (S (S n)))))).
  5249. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5250. apply (subFormulaExch LNN); PRsolveFV A B n.
  5251. apply
  5252. iffTrans
  5253. with
  5254. (substituteFormula LNN
  5255. (substituteFormula LNN
  5256. (substituteFormula LNN
  5257. (substituteFormula LNN
  5258. (substituteFormula LNN B (S n) (natToTerm a0))
  5259. (S (S n)) (var (S n))) (S (S (S n)))
  5260. (var (S (S (S (S n)))))) (S (S (S (S n))))
  5261. (var (S (S (S n))))) (S (S (S (S (S n)))))
  5262. (var (S (S (S (S n)))))).
  5263. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5264. apply (subFormulaExch LNN); PRsolveFV A B n.
  5265. apply
  5266. iffTrans
  5267. with
  5268. (substituteFormula LNN
  5269. (substituteFormula LNN
  5270. (substituteFormula LNN
  5271. (substituteFormula LNN B (S n) (natToTerm a0))
  5272. (S (S n)) (var (S n))) (S (S (S n))) (var (S (S (S n)))))
  5273. (S (S (S (S (S n))))) (var (S (S (S (S n)))))).
  5274. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5275. apply (subFormulaTrans LNN); PRsolveFV A B n.
  5276. apply
  5277. iffTrans
  5278. with
  5279. (substituteFormula LNN
  5280. (substituteFormula LNN (substituteFormula LNN B (S n) (natToTerm a0))
  5281. (S (S n)) (var (S n))) (S (S (S n))) (var (S (S (S n))))).
  5282. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5283. apply (subFormulaNil LNN); PRsolveFV A B n.
  5284. elim (le_not_lt (S (S (S (S (S n))))) (S n)).
  5285. rewrite <- H17.
  5286. apply le_n.
  5287. do 3 apply lt_S.
  5288. apply lt_n_Sn.
  5289. apply iffSym.
  5290. apply
  5291. iffTrans
  5292. with
  5293. (substituteFormula LNN
  5294. (substituteFormula LNN
  5295. (substituteFormula LNN
  5296. (substituteFormula LNN B (S n) (natToTerm a0))
  5297. (S (S n)) (var (S n))) (S (S (S n))) (var (S (S n))))
  5298. (S (S n)) (var (S (S (S n))))).
  5299. apply (subFormulaNil LNN); PRsolveFV A B n.
  5300. apply (subFormulaTrans LNN); PRsolveFV A B n.
  5301. apply
  5302. iffTrans
  5303. with
  5304. (substituteFormula LNN
  5305. (substituteFormula LNN
  5306. (substituteFormula LNN
  5307. (substituteFormula LNN
  5308. (substituteFormula LNN
  5309. (substituteFormula LNN
  5310. (substituteFormula LNN betaFormula 1
  5311. (Succ (var (S (S (S (S n))))))) 2
  5312. (var (S (S (S (S (S n)))))))
  5313. (S n) (natToTerm a0)) (S (S n))
  5314. (var (S n))) (S (S (S n))) (var (S (S n))))
  5315. (S (S (S (S n)))) (var (S (S (S n))))) (S (S (S (S (S n)))))
  5316. (var (S (S (S (S n)))))).
  5317. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5318. apply (subFormulaTrans LNN); PRsolveFV A B n.
  5319. apply
  5320. iffTrans
  5321. with
  5322. (substituteFormula LNN
  5323. (substituteFormula LNN
  5324. (substituteFormula LNN
  5325. (substituteFormula LNN
  5326. (substituteFormula LNN
  5327. (substituteFormula LNN betaFormula 1
  5328. (Succ (var (S (S (S (S n))))))) 2
  5329. (var (S (S (S (S (S n))))))) (S (S n))
  5330. (var (S n))) (S (S (S n))) (var (S (S n))))
  5331. (S (S (S (S n)))) (var (S (S (S n))))) (S (S (S (S (S n)))))
  5332. (var (S (S (S (S n)))))).
  5333. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5334. apply (subFormulaNil LNN); PRsolveFV A B n.
  5335. elim (le_not_lt (S (S (S (S (S n))))) (S n)).
  5336. rewrite H17.
  5337. apply le_n.
  5338. do 3 apply lt_S.
  5339. apply lt_n_Sn.
  5340. apply
  5341. iffTrans
  5342. with
  5343. (substituteFormula LNN
  5344. (substituteFormula LNN
  5345. (substituteFormula LNN
  5346. (substituteFormula LNN
  5347. (substituteFormula LNN betaFormula 1
  5348. (Succ (var (S (S (S (S n))))))) 2
  5349. (var (S (S (S (S (S n))))))) (S (S (S n)))
  5350. (var (S (S n)))) (S (S (S (S n)))) (var (S (S (S n)))))
  5351. (S (S (S (S (S n))))) (var (S (S (S (S n)))))).
  5352. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5353. apply (subFormulaNil LNN); PRsolveFV A B n.
  5354. apply
  5355. iffTrans
  5356. with
  5357. (substituteFormula LNN
  5358. (substituteFormula LNN
  5359. (substituteFormula LNN
  5360. (substituteFormula LNN betaFormula 1
  5361. (Succ (var (S (S (S (S n))))))) 2 (var (S (S (S (S (S n)))))))
  5362. (S (S (S (S n)))) (var (S (S (S n))))) (S (S (S (S (S n)))))
  5363. (var (S (S (S (S n)))))).
  5364. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5365. apply (subFormulaNil LNN); PRsolveFV A B n.
  5366. apply
  5367. iffTrans
  5368. with
  5369. (substituteFormula LNN
  5370. (substituteFormula LNN
  5371. (substituteFormula LNN
  5372. (substituteFormula LNN betaFormula 1
  5373. (Succ (var (S (S (S (S n))))))) (S (S (S (S n))))
  5374. (var (S (S (S n))))) 2 (var (S (S (S (S (S n)))))))
  5375. (S (S (S (S (S n))))) (var (S (S (S (S n)))))).
  5376. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5377. apply (subFormulaExch LNN); PRsolveFV A B n.
  5378. apply
  5379. iffTrans
  5380. with
  5381. (substituteFormula LNN
  5382. (substituteFormula LNN
  5383. (substituteFormula LNN betaFormula 1 (Succ (var (S (S (S (S n)))))))
  5384. (S (S (S (S n)))) (var (S (S (S n))))) 2
  5385. (var (S (S (S (S n)))))).
  5386. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5387. apply (subFormulaTrans LNN); PRsolveFV A B n.
  5388. apply
  5389. iffTrans
  5390. with
  5391. (substituteFormula LNN
  5392. (substituteFormula LNN betaFormula 1 (Succ (var (S (S (S n)))))) 2
  5393. (var (S (S (S (S n)))))).
  5394. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5395. apply
  5396. iffTrans
  5397. with
  5398. (substituteFormula LNN
  5399. (substituteFormula LNN betaFormula (S (S (S (S n))))
  5400. (var (S (S (S n))))) 1
  5401. (substituteTerm LNN (Succ (var (S (S (S (S n))))))
  5402. (S (S (S (S n)))) (var (S (S (S n)))))).
  5403. apply (subSubFormula LNN); PRsolveFV A B n.
  5404. replace
  5405. (substituteTerm LNN (Succ (var (S (S (S (S n))))))
  5406. (S (S (S (S n)))) (var (S (S (S n))))) with
  5407. (Succ
  5408. (substituteTerm LNN (var (S (S (S (S n))))) (S (S (S (S n))))
  5409. (var (S (S (S n)))))).
  5410. rewrite (subTermVar1 LNN).
  5411. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5412. apply (subFormulaNil LNN); PRsolveFV A B n.
  5413. reflexivity.
  5414. apply iffSym.
  5415. apply (subFormulaTrans LNN); PRsolveFV A B n.
  5416. elim H19; symmetry in |- *; assumption.
  5417. apply
  5418. iffTrans
  5419. with
  5420. (substituteFormula LNN
  5421. (substituteFormula LNN
  5422. (substituteFormula LNN
  5423. (substituteFormula LNN betaFormula 2 (var (S (S (S n))))) 1
  5424. (var (S (S n)))) (S (S n)) (var (S n)))
  5425. (S (S (S n))) (var (S (S n)))).
  5426. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5427. apply (subFormulaNil LNN); PRsolveFV A B n.
  5428. apply
  5429. iffTrans
  5430. with
  5431. (substituteFormula LNN
  5432. (substituteFormula LNN
  5433. (substituteFormula LNN betaFormula 2 (var (S (S (S n))))) 1
  5434. (var (S n))) (S (S (S n))) (var (S (S n)))).
  5435. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5436. apply (subFormulaTrans LNN); PRsolveFV A B n.
  5437. apply
  5438. iffTrans
  5439. with
  5440. (substituteFormula LNN
  5441. (substituteFormula LNN
  5442. (substituteFormula LNN betaFormula 2 (var (S (S (S n)))))
  5443. (S (S (S n))) (var (S (S n)))) 1 (var (S n))).
  5444. apply (subFormulaExch LNN); PRsolveFV A B n.
  5445. repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]).
  5446. apply (subFormulaTrans LNN); PRsolveFV A B n.
  5447. apply H3. }
  5448. (* H end *)
  5449. intros n A g H0 B h H1. split.
  5450. + destruct H0 as (H0, H2). destruct H1 as (H1, H3). intros v H4.
  5451. assert (forall v : nat, In v (freeVarFormula LNN betaFormula) -> v <= 2).
  5452. { eapply proj1. apply betaRepresentable. }
  5453. assert (forall v : nat, v <> S (S n) -> v <= S (S n) -> v <= S n).
  5454. { intros v0 H6 H7. destruct (le_lt_or_eq _ _ H7) as [H8 | H8].
  5455. + apply lt_n_Sm_le. assumption.
  5456. + elim H6; assumption. }
  5457. unfold primRecSigmaFormula, minimize, existH, andH, forallH, impH, notH in H4;
  5458. repeat
  5459. match goal with
  5460. | H1:(?X1 = ?X2),H2:(?X1 <> ?X2) |- _ =>
  5461. elim H2; apply H1
  5462. | H1:(?X1 = ?X2),H2:(?X2 <> ?X1) |- _ =>
  5463. elim H2; symmetry in |- *; apply H1
  5464. | H:(v = ?X1) |- _ => rewrite H; clear H
  5465. | H:(?X1 = v) |- _ =>
  5466. rewrite <- H; clear H
  5467. | H:(In ?X3 (freeVarFormula LNN (fol.existH LNN ?X1 ?X2))) |- _ =>
  5468. assert (In X3 (list_remove nat eq_nat_dec X1 (freeVarFormula LNN X2)));
  5469. [ apply H | clear H ]
  5470. | H:(In ?X3 (freeVarFormula LNN (fol.forallH LNN ?X1 ?X2))) |- _ =>
  5471. assert (In X3 (list_remove nat eq_nat_dec X1 (freeVarFormula LNN X2)));
  5472. [ apply H | clear H ]
  5473. | H:(In ?X3 (list_remove nat eq_nat_dec ?X1 (freeVarFormula LNN ?X2))) |- _
  5474. =>
  5475. assert (In X3 (freeVarFormula LNN X2));
  5476. [ eapply In_list_remove1; apply H
  5477. | assert (X3 <> X1); [ eapply In_list_remove2; apply H | clear H ] ]
  5478. | H:(In ?X3 (freeVarFormula LNN (fol.andH LNN ?X1 ?X2))) |- _ =>
  5479. assert (In X3 (freeVarFormula LNN X1 ++ freeVarFormula LNN X2));
  5480. [ apply H | clear H ]
  5481. | H:(In ?X3 (freeVarFormula LNN (fol.impH LNN ?X1 ?X2))) |- _ =>
  5482. assert (In X3 (freeVarFormula LNN X1 ++ freeVarFormula LNN X2));
  5483. [ apply H | clear H ]
  5484. | H:(In ?X3 (freeVarFormula LNN (fol.notH LNN ?X1))) |- _ =>
  5485. assert (In X3 (freeVarFormula LNN X1)); [ apply H | clear H ]
  5486. | H:(In _ (freeVarFormula LNN (primRecSigmaFormulaHelp _ _ _))) |- _ =>
  5487. decompose sum (freeVarPrimRecSigmaFormulaHelp1 _ _ _ _ H); clear H
  5488. | H:(In _ (freeVarFormula LNN (primRecPiFormulaHelp _ _ _))) |- _ =>
  5489. decompose sum (freeVarPrimRecPiFormulaHelp1 _ _ _ _ H); clear H
  5490. | H:(In ?X3 (freeVarFormula LNN A)) |- _ =>
  5491. apply Nat.le_trans with n; [ apply H0; apply H | apply le_n_Sn ]
  5492. | H:(In ?X3 (freeVarFormula LNN B)) |- _ =>
  5493. apply H6; [ clear H | apply H1; apply H ]
  5494. | H:(In _ (_ ++ _)) |- _ =>
  5495. induction (in_app_or _ _ _ H); clear H
  5496. | H:(In _ (freeVarFormula LNN (substituteFormula LNN ?X1 ?X2 ?X3))) |- _ =>
  5497. induction (freeVarSubFormula3 _ _ _ _ _ H); clear H
  5498. | H:(In _ (freeVarFormula LNN (LT ?X1 ?X2))) |- _ =>
  5499. rewrite freeVarLT in H
  5500. | H:(In _ (freeVarTerm LNN (natToTerm _))) |- _ =>
  5501. elim (closedNatToTerm _ _ H)
  5502. | H:(In _ (freeVarTerm LNN Zero)) |- _ =>
  5503. elim H
  5504. | H:(In _ (freeVarTerm LNN (Succ _))) |- _ =>
  5505. rewrite freeVarSucc in H
  5506. | H:(In _ (freeVarTerm LNN (var _))) |- _ =>
  5507. simpl in H; decompose sum H; clear H
  5508. | H:(In _ (freeVarTerm LNN (fol.var LNN _))) |- _ =>
  5509. simpl in H; decompose sum H; clear H
  5510. end; try first [ assumption | apply le_n ].
  5511. assert (v <= 2) by auto. lia.
  5512. + apply H; auto.
  5513. Qed.
  5514. (* end *)
  5515.  
  5516. Fixpoint primRecFormula (n : nat) (f : PrimRec n) {struct f} : Formula :=
  5517. match f with
  5518. | succFunc => succFormula
  5519. | zeroFunc => zeroFormula
  5520. | projFunc n m _ => projFormula m
  5521. | composeFunc n m g h =>
  5522. composeSigmaFormula n n m (primRecsFormula n m g) (primRecFormula m h)
  5523. | primRecFunc n g h =>
  5524. primRecSigmaFormula n (primRecFormula n g) (primRecFormula (S (S n)) h)
  5525. end
  5526.  
  5527. with primRecsFormula (n m : nat) (fs : PrimRecs n m) {struct fs} :
  5528. Vector.t (Formula * naryFunc n) m :=
  5529. match fs in (PrimRecs n m) return (Vector.t (Formula * naryFunc n) m) with
  5530. | PRnil n => Vector.nil _
  5531. | PRcons n m f fs' =>
  5532. Vector.cons (Formula * naryFunc n) (primRecFormula n f, evalPrimRec n f) m
  5533. (primRecsFormula n m fs')
  5534. end.
  5535.  
  5536. Lemma primRecRepresentable1 :
  5537. forall (n : nat) (f : PrimRec n),
  5538. Representable n (evalPrimRec n f) (primRecFormula n f).
  5539. Proof.
  5540. intros n f.
  5541. elim f using
  5542. PrimRec_PrimRecs_ind
  5543. with
  5544. (P0 := fun (n m : nat) (fs : PrimRecs n m) =>
  5545. RepresentablesHelp n m (primRecsFormula n m fs) /\
  5546. extEqualVector _ _ (FormulasToFuncs n m (primRecsFormula n m fs))
  5547. (evalPrimRecs n m fs) /\
  5548. Vector.t_rect (Formula * naryFunc n) (fun _ _ => Prop) True
  5549. (fun (pair : Formula * naryFunc n) (m : nat)
  5550. (v : Vector.t _ m) (rec : Prop) =>
  5551. (forall v : nat, In v (freeVarFormula LNN (fst pair)) -> v <= n) /\
  5552. rec) m (primRecsFormula n m fs)).
  5553. + apply succRepresentable.
  5554. + apply zeroRepresentable.
  5555. + intros n0 m l. simpl in |- *. apply projRepresentable.
  5556. + simpl in |- *; intros n0 m g H h H0. decompose record H.
  5557. assert
  5558. (Representable n0
  5559. (evalComposeFunc n0 m (FormulasToFuncs n0 m (primRecsFormula n0 m g))
  5560. (evalPrimRec m h))
  5561. (composeSigmaFormula n0 n0 m (primRecsFormula n0 m g)
  5562. (primRecFormula m h))).
  5563. { apply composeSigmaRepresentable; auto. }
  5564. induction H2 as (H2, H5). split.
  5565. - assumption.
  5566. - apply
  5567. Representable_ext
  5568. with
  5569. (evalComposeFunc n0 m (FormulasToFuncs n0 m (primRecsFormula n0 m g))
  5570. (evalPrimRec m h)).
  5571. * apply extEqualCompose.
  5572. ++ assumption.
  5573. ++ apply extEqualRefl.
  5574. * assumption.
  5575. + simpl in |- *. intros n0 g H h H0.
  5576. apply primRecSigmaRepresentable; auto.
  5577. + simpl in |- *. tauto.
  5578. + simpl in |- *; intros n0 m p H p0 H0.
  5579. decompose record H0. clear H0.
  5580. repeat split; auto.
  5581. - induction H as (H, H0); auto.
  5582. - apply extEqualRefl.
  5583. - induction H as (H, H0); auto.
  5584. Qed.
  5585.  
  5586. Lemma primRecRepresentable :
  5587. forall (n : nat) (f : naryFunc n) (p : isPR n f),
  5588. Representable n f (primRecFormula n (proj1_sig p)).
  5589. Proof.
  5590. intros n f p.
  5591. assert
  5592. (Representable n (evalPrimRec n (proj1_sig p))
  5593. (primRecFormula n (proj1_sig p))).
  5594. { apply primRecRepresentable1. }
  5595. induction H as (H, H0). split.
  5596. + assumption.
  5597. + destruct p as (x, p).
  5598. eapply Representable_ext with (evalPrimRec n x); assumption.
  5599. Qed.
  5600.  
  5601. End Primitive_Recursive_Representable.
  5602.  
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!