proposition: Lemma paPlusSym : forall a b : Term, SysPrf PA (a + b = b + a)%nt.
proof: Proof. assert (H: SysPrf PA (allH 1 0, v#0 + v#1 = v#1 + v#0)%nt). { apply induct. - rewrite (subFormulaForall LNT). induction (eq_nat_dec 0 1) as [a | b]. + discriminate a. + induction (In_dec eq_nat_dec 0 (freeVarT LNT.Zero)) as [a | b0]. * elim a. * apply induct. -- repeat rewrite (subFormulaEqual LNT). simpl in |- *; apply eqRefl. -- apply forallI. ++ apply closedPA. ++ repeat rewrite (subFormulaEqual LNT). simpl; apply impI. apply eqTrans with (LNT.Succ (v#0))%nt. ** apply sysWeaken. apply pa3 with (a := (LNT.Succ (var 0))%nt). ** apply eqTrans with (LNT.Succ (LNT.Zero + v#0))%nt. { apply eqSucc. apply eqTrans with (v#0 + LNT.Zero)%nt. - apply sysWeaken. apply eqSym. apply pa3. - apply Axm; right; constructor. } apply eqSym. apply sysWeaken. apply pa4 with (a := LNT.Zero) (b := (v#0)%nt). - apply forallI. + apply closedPA. + apply impI. rewrite (subFormulaForall LNT). induction (eq_nat_dec 0 1) as [a | b]. * discriminate a. * induction (In_dec eq_nat_dec 0 (freeVarT (LNT.Succ (v#1))%nt)). -- simpl in a. induction a as [H| H]. ++ discriminate. ++ contradiction. -- rewrite (subFormulaEqual LNT). simpl; apply forallI. ++ intros [x [H H0]]. destruct H0 as [x H0| x H0]. ** elim closedPA with 0. exists x; auto. ** induction H0; simpl in H. decompose sum H. discriminate H0. discriminate H1. ++ apply eqTrans with (LNT.Succ (v#0 + v#1))%nt. ** apply sysWeaken. apply pa4 with (a := var 0) (b := var 1). ** apply eqTrans with (LNT.Succ (v#1 + v#0))%nt. { apply eqSucc. apply forallSimp with 0. apply Axm; right; constructor. } apply sysWeaken. apply forallSimp with 0. apply induct. rewrite (subFormulaEqual LNT). simpl in |- *. apply eqTrans with (LNT.Succ (v#1))%nt. { fold (LNT.Succ (v#1 + LNT.Zero))%nt. apply eqSucc. apply pa3 with (a := (v#1)%nt). } apply eqSym. apply pa3 with (a := (LNT.Succ v#1)%nt). apply forallI. apply closedPA. apply impI. rewrite (subFormulaEqual LNT). simpl in |- *. apply eqTrans with (LNT.Succ (LNT.Succ v#1 + v#0))%nt. { fold (LNT.Succ (v#1 + LNT.Succ v#0))%nt. apply eqSucc. apply eqTrans with (LNT.Succ (v#1 + v#0))%nt. apply sysWeaken. apply pa4 with (a := (v# 1)%nt) (b := (v#0)%nt). apply Axm; right; constructor. } apply sysWeaken. apply eqSym. apply pa4 with (a := LNT.Succ (v#1)%nt) (b := (v#0)%nt). } intros a b; set (m := fun x : nat => match x with | O => a | S _ => b end) in *. replace (a + b = b + a)%nt with (subAllFormula LNT (v#0 + v#1 = v#1 + v#0)%nt (fun x : nat => match le_lt_dec 2 x with | left _ => var x | right _ => m x end)). + apply (subAllCloseFrom LNT). simpl; apply H. + simpl; destruct (le_lt_dec 2 0). * lia. * induction (le_lt_dec 2 1). -- lia. -- reflexivity. Qed.
imports: Coq(Ensembles List Arith Lia) hydras.Ackermann(subAll folReplace folProp folLogic3 NN LNN2LNT) hydras.Ackermann(NewNotations)