proposition: Lemma betaRepresentable : Representable 2 β βR.
proof: Proof. split. - intros v H. simpl in H. lia. - simpl; intros a a0; unfold βR. assert (H: forall (A : Formula) (v x a : nat), v <> x -> substF (existH v A) x (n2t a) = existH v (substF A x (n2t a))). { intros A v x a1 H; rewrite (substExHC _ A v x _ H ); trivial; apply closedNatToTerm. } assert (H0: forall (t1 t2 : Term) (v a : nat), substF (t1 < t2)%fol v (n2t a) = (substT t1 v (n2t a) < substT t2 v (n2t a))%fol). { intros ? ? ? ?; unfold LT at 1; now rewrite (subFormulaRelation LNN). } repeat first [ rewrite H; [| discriminate ] | rewrite H0 | rewrite (subFormulaAnd LNN) | rewrite (subFormulaEqual LNN) ]. simpl in |- *; repeat rewrite (subTermNil LNN). + assert (H1: SysPrf NN ((exH 3, v#3 < n2t a.+1 /\ (exH 4, v#4 < n2t a.+1 /\ (v#3 + v#4) * S_ (v#3 + v#4) + n2t 2 * v#3 = n2t 2 * n2t a /\ v#0 < S_ (v#3 * S_ (n2t a0)) /\ (exH 5, v#5 < S_ v#4 /\ v#0 + v#5 * S_ (v#3 * S_ (n2t a0)) = v#4))) <-> v#0 = n2t (β a a0))%fol); auto. apply iffI. * apply impI. apply existSys. -- apply closedNN. -- intros [H1 | H1]; try lia. simpl in H1; elim (closedNatToTerm _ _ H1). -- apply impE with (v#3 < n2t (S a))%fol. ++ apply impE with (exH 4, v#4 < n2t a.+1 /\ (v#3 + v#4) * Succ (v#3 + v#4) + n2t 2 * v#3 = n2t 2 * n2t a /\ v#0 < Succ (v#3 * Succ (n2t a0)) /\ (exH 5, v#5 < Succ v#4 /\ v#0 + v#5 * Succ (v#3 * Succ (n2t a0)) = v#4))%fol. ** apply sysWeaken. apply impI. apply existSys. --- apply closedNN. --- replace (freeVarF (v#3 < n2t (a.+1) -> v#0 = (n2t (β a a0)))%fol) with ((freeVarT (L:=LNN) (var 3) ++ freeVarT (n2t a.+1)) ++ freeVarF (v#0 = n2t (β a a0))%fol) by (rewrite <- freeVarLT; reflexivity). intros [H1 | H1]; try lia. destruct (in_app_or _ _ _ H1) as [H2 | H2]. +++ elim (closedNatToTerm _ _ H2). +++ destruct H2 as [H2| H2]; try lia. elim (closedNatToTerm _ _ H2). --- apply impTrans with (andH (equal (var 3) (n2t (car a))) (equal (var 4) (n2t (cdr a)))). +++ apply impI. apply impE with (equal (Plus (Times (Plus (var 3) (var 4)) (Succ (Plus (var 3) (var 4)))) (Times (n2t 2) (var 3))) (Times (n2t 2) (n2t a))). *** apply impE with (v#4 < n2t (S a))%fol. ---- apply impE with (v#3 < n2t (S a))%fol. ++++ do 2 apply sysWeaken. apply boundedLT; intros n H1. rewrite (subFormulaImp LNN). unfold LT at 1 in |- *. rewrite (subFormulaRelation LNN). simpl in |- *. rewrite subTermNil. **** replace (apply LNN Languages.Succ_ (Tcons (n2t a) (Tnil))) with (n2t (S a)); [| reflexivity ]. fold (LT (var 4) (n2t (S a))). apply boundedLT. intros n0 H2. repeat rewrite (subFormulaImp LNN). repeat rewrite (subFormulaAnd LNN). repeat rewrite (subFormulaEqual LNN). assert (H3: (substT (substT (Plus (Times (v#3 + v#4)%fol (Succ (Plus (var 3) (var 4)))) (Times (Succ (Succ Zero)) (var 3))) 3 (n2t n)) 4 (n2t n0)) = (Plus (Times (Plus (n2t n) (n2t n0)) (Succ (n2t n + n2t n0))%fol) (Times (Succ (Succ Zero)) (n2t n)))) . { simpl in |- *. repeat (rewrite (subTermNil LNN (n2t n))); [| apply closedNatToTerm]. reflexivity. } rewrite H3; clear H3. assert (H3: (substT (substT (Times (Succ (Succ Zero)) (n2t a)) 3 (n2t n)) 4 (n2t n0)) = (Times (n2t 2) (n2t a))). { simpl in |- *; repeat (rewrite (subTermNil _ (n2t a)); [| apply closedNatToTerm ]). reflexivity. } simpl in |- *. assert (forall (a b : nat) (s : Term), substT (n2t a) b s = n2t a). { intros; apply (subTermNil LNN). apply closedNatToTerm. } repeat rewrite H4. apply impTrans with (equal (n2t ((n + n0) * S (n + n0) + 2 * n)) (n2t (2 * a))). { apply impI. eapply eqTrans. - apply sysWeaken; apply eqSym; apply natPlus. - eapply eqTrans. + apply eqPlus. eapply eqTrans. * apply sysWeaken; apply eqSym; apply natTimes. * eapply eqTrans. -- apply eqTimes. ++ apply sysWeaken; apply eqSym. apply natPlus. ++ eapply eqTrans. ** apply sysWeaken; apply eqSym. simpl in |- *. apply eqSucc. apply natPlus. ** apply eqRefl. -- apply eqRefl. * apply sysWeaken; apply eqSym. apply natTimes. + eapply eqTrans. * apply Axm; right; constructor. * apply sysWeaken. replace (S_ (S_ (apply LNN Zero_ Tnil)))%fol with (n2t 2) by reflexivity. apply natTimes. } { rewrite cPairLemma1. destruct (eq_nat_dec a (cPair n n0)) as [e | e]. - rewrite e, cPairProjections1, cPairProjections2. apply impI. apply andI; apply eqRefl. - apply impI. apply contradiction with (equal (n2t (2 * cPair n n0)) (n2t (2 * a))). + apply Axm; right; constructor. + apply sysWeaken. apply natNE. lia. } **** apply closedNatToTerm. ++++ apply Axm; right; constructor. ---- eapply andE1. apply Axm; left; right; constructor. *** eapply andE1. eapply andE2. apply Axm; left; right; constructor. +++ repeat apply impI. apply impE with (existH 5 (andH (LT (var 5) (Succ (var 4))) (equal (Plus (var 0) (Times (var 5) (Succ (Times (var 3) (Succ (n2t a0)))))) (var 4)))). *** apply impE with (LT (var 0) (Succ (Times (var 3) (Succ (n2t a0))))). ---- rewrite <- (subFormulaId LNN (impH (LT (var 0) (Succ (Times (var 3) (Succ (n2t a0))))) (impH (existH 5 (andH (LT (var 5) (Succ (var 4))) (equal (Plus (var 0) (Times (var 5) (Succ (Times (var 3) (Succ (n2t a0)))))) (var 4)))) (equal (var 0) (n2t (β a a0))))) 3). apply impE with (substF (impH (LT (var 0) (Succ (Times (var 3) (Succ (n2t a0))))) (impH (existH 5 (andH (LT (var 5) (Succ (var 4))) (equal (Plus (var 0) (Times (var 5) (Succ (Times (var 3) (Succ (n2t a0)))))) (var 4)))) (equal (var 0) (n2t (β a a0))))) 3 (n2t (car a))). ++++ apply (subWithEquals LNN). apply eqSym. eapply andE1. apply Axm; right; constructor. ++++ rewrite <- (subFormulaId LNN (substF (impH (LT (var 0) (Succ (Times (var 3) (Succ (n2t a0))))) (impH (existH 5 (andH (LT (var 5) (Succ (var 4))) (equal (Plus (var 0) (Times (var 5) (Succ (Times (var 3) (Succ (n2t a0)))))) (var 4)))) (equal (var 0) (n2t (β a a0))))) 3 (n2t (car a))) 4). apply impE with (substF (substF (impH (LT (var 0) (Succ (Times (var 3) (Succ (n2t a0))))) (impH (existH 5 (andH (LT (var 5) (Succ (var 4))) (equal (Plus (var 0) (Times (var 5) (Succ (Times (var 3) (Succ (n2t a0)))))) (var 4)))) (equal (var 0) (n2t (β a a0))))) 3 (n2t (car a))) 4 (n2t (cdr a))). ***** apply (subWithEquals LNN). apply eqSym. eapply andE2. apply Axm; right; constructor. ***** do 2 apply sysWeaken. repeat first [ rewrite H; [| discriminate ] | rewrite H0 | rewrite (subFormulaImp LNN) | rewrite (subFormulaAnd LNN) | rewrite (subFormulaEqual LNN) ]. simpl in |- *. repeat (rewrite (subTermNil LNN); [| apply closedNatToTerm ]). repeat (rewrite (subTermNil LNN (n2t a0)); [| apply closedNatToTerm ]). repeat (rewrite (subTermNil LNN (n2t (β a a0))); [| apply closedNatToTerm ]). apply impTrans with (LT (var 0) (n2t (S (car a * S a0)))). { apply impI. apply impE with (substF (LT (var 0) (var 1)) 1 (n2t (S (car a * S a0)))). - unfold LT at 2 in |- *. rewrite (subFormulaRelation LNN). apply impRefl. - apply impE with (substF (v#0 < v#1)%fol 1 (Succ (Times (n2t (car a)) (Succ (n2t a0))))). + apply (subWithEquals LNN). apply sysWeaken. simpl. apply eqSucc. change (Succ (n2t a0)) with (n2t a0.+1). apply natTimes. + unfold LT at 2 in |- *. rewrite (subFormulaRelation LNN). apply Axm; right; constructor. } { apply boundedLT. intros n H1. repeat first [ rewrite H; [| discriminate ] | rewrite H0 | rewrite (subFormulaImp LNN) | rewrite (subFormulaAnd LNN) | rewrite (subFormulaEqual LNN) ]. simpl in |- *. repeat (rewrite (subTermNil LNN); [| apply closedNatToTerm ]). apply impI. apply existSys. - apply closedNN. - simpl in |- *. intro H2. destruct (in_app_or _ _ _ H2) as [H3 | H3]; elim (closedNatToTerm _ _ H3). - apply impE with (fol.equal (apply LNN Languages.Plus_ (Tcons (n2t n) (Tcons (apply LNN Languages.Times_ (Tcons (var 5) (Tcons (apply LNN Languages.Succ_ (Tcons (apply LNN Languages.Times_ (Tcons (n2t (car a)) (Tcons (apply LNN Languages.Succ_ (Tcons (n2t a0) (Tnil))) (Tnil)))) (Tnil ))) (Tnil)))) (Tnil )))) (n2t (cdr a))). + apply impE with (LT (var 5) (n2t (S (cdr a)))). apply sysWeaken. * apply boundedLT. intros n0 H2. repeat first [ rewrite H; [| discriminate ] | rewrite H0 | rewrite (subFormulaImp LNN) | rewrite (subFormulaAnd LNN) | rewrite (subFormulaEqual LNN) ]. simpl in |- *. repeat (rewrite (subTermNil LNN); [| apply closedNatToTerm ]). apply impI. destruct (eq_nat_dec n (β a a0)) as [e | e]. -- rewrite <- e. apply eqRefl. -- apply contradiction with (equal (n2t (n + n0 * S (car a * S a0))) (n2t (cdr a))). ++ eapply eqTrans; [| apply Axm; right; constructor ]. apply sysWeaken. eapply eqTrans. ** apply eqSym. apply natPlus. ** replace (apply LNN Languages.Plus_ (Tcons (n2t n) (Tcons (apply LNN Languages.Times_ (Tcons (n2t n0) (Tcons (apply LNN Languages.Succ_ (Tcons (apply LNN Languages.Times_ (Tcons (n2t (car a)) (Tcons (apply LNN Languages.Succ_ (Tcons (n2t a0) (Tnil))) (Tnil )))) (Tnil ))) (Tnil )))) (Tnil )))) with (Plus (n2t n) (Times (n2t n0) (Succ (Times (n2t (car a)) (Succ (n2t a0)))))) by reflexivity. apply eqPlus. --- apply eqRefl. --- eapply eqTrans. +++ apply eqSym. apply natTimes. +++ apply eqTimes. apply eqRefl. simpl in |- *. apply eqSucc. replace (Succ (n2t a0)) with (n2t (S a0)) by reflexivity. apply eqSym. apply natTimes. ++ apply sysWeaken. apply natNE. intro; elim e. unfold beta in |- *. destruct (div_eucl (coPrimeBeta a0 (car a)) (gtBeta a0 (car a)) (cdr a)) as [[a1 b0] H4]. simpl in H4. simpl in |- *. destruct H4 as (H4, H5). unfold coPrimeBeta in H4. rewrite Nat.add_comm in H3. eapply uniqueRem. ** apply Nat.lt_0_succ. ** exists n0; split; [symmetry |]; eauto. ** exists a1; split; eauto. * eapply andE1. apply Axm; right; constructor. + eapply andE2. apply Axm; right; constructor. } ---- eapply andE1. eapply andE2. eapply andE2. apply Axm; left; right; constructor. *** eapply andE2. eapply andE2. eapply andE2. apply Axm; left; right; constructor. ** eapply andE2. apply Axm; right; constructor. ++ eapply andE1. apply Axm; right; constructor. * apply impI. unfold beta in |- *. destruct (div_eucl (coPrimeBeta a0 (car a)) (gtBeta a0 (car a)) (cdr a)) as [x H1]. induction x as (a1, b). simpl in |- *. simpl in H1. destruct H1 as (H1, H2). apply existI with (n2t (car a)). rewrite (subFormulaAnd LNN). apply andI. -- apply sysWeaken. rewrite H0. simpl in |- *. rewrite subTermNil. ++ replace (apply LNN Languages.Succ_ (Tcons (n2t a) (Tnil ))) with (n2t (S a)) by reflexivity. apply natLT. apply Nat.lt_succ_r. apply Nat.le_trans with (cPair (car a) (cdr a)). apply cPairLe1. rewrite cPairProjections. apply le_n. ++ apply closedNatToTerm. -- rewrite H; try lia. ++ apply existI with (n2t (cdr a)). repeat rewrite (subFormulaAnd LNN). apply andI. ** apply sysWeaken. repeat rewrite H0. simpl in |- *. repeat rewrite (subTermNil LNN (n2t a)). --- replace (apply LNN Languages.Succ_ (Tcons (n2t a) (Tnil ))) with (n2t (S a)) by reflexivity. apply natLT. apply Nat.lt_succ_r. apply Nat.le_trans with (cPair (car a) (cdr a)). +++ apply cPairLe2. +++ rewrite cPairProjections. apply le_n. --- apply closedNatToTerm. --- apply closedNatToTerm. ** apply andI. --- repeat rewrite (subFormulaEqual LNN). simpl in |- *. repeat (rewrite (subTermNil LNN (n2t (car a))); [| apply closedNatToTerm ]). repeat (rewrite (subTermNil LNN (n2t a)); [| apply closedNatToTerm ]). replace (equal (apply LNN Languages.Plus_ (Tcons (apply LNN Languages.Times_ (Tcons (apply LNN Languages.Plus_ (Tcons (n2t (car a)) (Tcons (n2t (cdr a)) (Tnil )))) (Tcons (apply LNN Languages.Succ_ (Tcons (apply LNN Languages.Plus_ (Tcons (n2t (car a)) (Tcons (n2t (cdr a)) (Tnil )))) (Tnil ))) (Tnil)))) (Tcons (apply LNN Languages.Times_ (Tcons (apply LNN Languages.Succ_ (Tcons (apply LNN Languages.Succ_ (Tcons (apply LNN Languages.Zero_ (Tnil )) (Tnil ))) (Tnil ))) (Tcons (n2t (car a)) (Tnil )))) (Tnil )))) (apply LNN Languages.Times_ (Tcons (apply LNN Languages.Succ_ (Tcons (apply LNN Languages.Succ_ (Tcons (apply LNN Languages.Zero_ (Tnil )) (Tnil ))) (Tnil ))) (Tcons (n2t a) (Tnil ))))) with (equal (Plus (Times (Plus (n2t (car a)) (n2t (cdr a))) (Succ (Plus (n2t (car a)) (n2t (cdr a))))) (Times (n2t 2) (n2t (car a)))) (Times (n2t 2) (n2t a))) by reflexivity. apply eqTrans with (n2t ((car a + cdr a) * S (car a + cdr a) + 2 * car a)). +++ apply sysWeaken. apply eqSym. eapply eqTrans. *** apply eqSym. apply natPlus. *** apply eqPlus. ---- eapply eqTrans. ++++ apply eqSym. apply natTimes. ++++ apply eqTimes. **** apply eqSym. apply natPlus. **** simpl in |- *. apply eqSucc. apply eqSym. apply natPlus. ---- apply eqSym. apply natTimes. +++ rewrite cPairLemma1. apply eqSym. rewrite cPairProjections. apply sysWeaken. apply natTimes. --- apply andI. +++ rewrite <- (subFormulaId LNN (substF (substF (LT (var 0) (S_ (Times (var 3) (S_ (n2t a0))))) 3 (n2t (car a))) 4 (n2t (cdr a))) 0). apply impE with (substF (substF (substF (LT (var 0) (Succ (Times (var 3) (Succ (n2t a0))))) 3 (n2t (car a))) 4 (n2t (cdr a))) 0 (n2t b)). *** apply (subWithEquals LNN). apply eqSym. apply Axm; right; constructor. *** apply sysWeaken. repeat rewrite H0. simpl in |- *. repeat (rewrite (subTermNil LNN (n2t (car a))); [| apply closedNatToTerm ]). repeat (rewrite (subTermNil LNN (n2t a0)); [| apply closedNatToTerm ]). apply impE with (substF (LT (n2t b) (var 0)) 0 (Succ (Times (n2t (car a)) (Succ (n2t a0))))). ---- unfold LT at 1 in |- *. rewrite (subFormulaRelation LNN). simpl in |- *. repeat (rewrite (subTermNil LNN (n2t b)); [| apply closedNatToTerm ]). apply impRefl. ---- apply impE with (substF (LT (n2t b) (var 0)) 0 (n2t (S (car a * S a0)))). ++++ apply (subWithEquals LNN). simpl in |- *. apply eqSucc. replace (Succ (n2t a0)) with (n2t (S a0)) by reflexivity. apply eqSym. apply natTimes. ++++ rewrite H0. repeat (rewrite (subTermNil LNN (n2t b)); [| apply closedNatToTerm ]). rewrite (subTermVar1 LNN). apply natLT. apply H2. +++ repeat (rewrite H; [| discriminate ]). apply existI with (n2t a1). rewrite <- (subFormulaId LNN (substF3 (v#5 < S_ v#4 /\ v#0 + v#5 * S_ (v#3 * S_ (n2t a0)) = v#4)%fol 3 (n2t (car a)) 4 (n2t (cdr a)) 5 (n2t a1)) 0). apply impE with (substF4 (andH (LT (var 5) (S_ (var 4))) (equal (Plus (var 0) (Times (var 5) (S_ (Times (var 3) (S_ (n2t a0)))))) (var 4))) 3 (n2t (car a)) 4 (n2t (cdr a)) 5 (n2t a1) 0 (n2t b)). *** apply (subWithEquals LNN). apply eqSym. apply Axm; right; constructor. *** apply sysWeaken. repeat first [ rewrite H; [| discriminate ] | rewrite H0 | rewrite (subFormulaImp LNN) | rewrite (subFormulaAnd LNN) | rewrite (subFormulaEqual LNN) ]. simpl in |- *. repeat (rewrite (subTermNil LNN (n2t (car a))); [| apply closedNatToTerm ]). repeat (rewrite (subTermNil LNN (n2t a0)); [| apply closedNatToTerm ]). repeat (rewrite (subTermNil LNN (n2t (cdr a))); [| apply closedNatToTerm ]). repeat (rewrite (subTermNil LNN (n2t a1)); [| apply closedNatToTerm ]). apply andI. ---- replace (S_ (n2t (cdr a)))%fol with (n2t (S (cdr a))) by reflexivity. apply natLT. unfold coPrimeBeta in *. lia. ---- replace (apply LNN Languages.Plus_ (Tcons (n2t b) (Tcons (apply LNN Languages.Times_ (Tcons (n2t a1) (Tcons (apply LNN Languages.Succ_ (Tcons (apply LNN Languages.Times_ (Tcons (n2t (car a)) (Tcons (apply LNN Languages.Succ_ (Tcons (n2t a0) (Tnil ))) (Tnil )))) (Tnil ))) (Tnil )))) (Tnil )))) with (Plus (n2t b) (Times (n2t a1) (Succ (Times (n2t (car a)) (Succ (n2t a0)))))) by reflexivity. apply eqTrans with (n2t (a1 * coPrimeBeta a0 (car a) + b)). ++++ rewrite Nat.add_comm. apply eqSym. eapply eqTrans. **** apply eqSym. apply natPlus. **** apply eqPlus. +++++ apply eqRefl. +++++ eapply eqTrans. ***** apply eqSym. apply natTimes. ***** apply eqTimes. apply eqRefl. unfold coPrimeBeta in |- *. simpl in |- *. apply eqSucc. replace (Succ (n2t a0)) with (n2t (S a0)) by reflexivity. apply eqSym. apply natTimes. ++++ rewrite <- H1. apply eqRefl. + apply closedNatToTerm. Qed.
imports: Coq(Arith) hydras.Ackermann(extEqualNat subAll folProp subProp folReplace folLogic3 NN NNtheory primRec expressible) Coqprime(ChineseRem) Coq(Vector List Lia) hydras(ListExt cPair MoreDecidable) hydras(Compat815 ssrnat_extracts) Coq(Utf8)