proposition: Lemma majorAnyPR: forall n (x: PrimRec n), majorizedPR x Ack.
proof: Proof. intros n x; induction x using PrimRec_PrimRecs_ind with (P0 := fun n m y => majorizedSPR y Ack). - apply majorSucc. - apply majorZero. - apply majorProjection. - destruct IHx, IHx0; red; exists (2 + Nat.max x0 x1). intro v; simpl evalPrimRec; rewrite evalListComp. generalize (H0 (map (fun g0 : naryFunc n => evalList n v g0) (evalPrimRecs n m g))); intro H00; eapply Nat.le_trans. + auto. + generalize (H v); intro HH; transitivity (Ack x1 (Ack x0 (max_v v))). * apply Ack_mono_r; apply max_v_lub. rewrite MoreVectors.Forall_forall; intros. generalize ( max_v_ge m (map (fun g : naryFunc n => evalList n v g) (evalPrimRecs n m g)) a H1). intro H2;lia. * rewrite Nat.max_comm; apply nested_Ack_bound. - destruct IHx1 as [r Hg]; destruct IHx2 as [s Hh]. remember (evalPrimRec n x1) as g. remember (evalPrimRec _ x2) as h. pose(q := S (max r s)); red. remember (evalPrimRecFunc _ (evalPrimRec _ x1) (evalPrimRec _ x2)) as f. assert (L1 : forall i (v: t nat n) , v_apply f (i::v) <= Ack q (i + max_v v)). { induction i. - intros; subst f; rewrite evalListPrimrec_0. simpl plus; subst g; transitivity (Ack r (max_v v)). + auto. + apply Ack_mono_l; unfold q; lia. - intros; rewrite Heqf; rewrite evalListPrimrec_S; rewrite <- Heqf; rewrite <- Heqh. pose (z:= max_v (i :: evalList (S n) (i :: v) f :: v)). assert (H: v_apply h (i:: (v_apply f (i::v) :: v)) <= Ack s z) by ( unfold z; apply Hh). assert (H0: z <= Ack q (i+ max_v v)). { clear H; specialize (IHi v). remember (v_apply f (i::v)) as p. remember (Ack q (i + max_v v)) as t. simpl max_v in z; remember (max_v v) as u. assert (H: i <= t). { rewrite Heqt; transitivity (S i); auto. transitivity (Ack q i). apply le_S_Ack. apply Ack_mono_r. lia. } assert (H0: u <= t). { rewrite Hequ, Heqt; rewrite Hequ. transitivity (i + max_v v). - lia. - transitivity (S (i + max_v v)). lia. apply le_S_Ack. } lia. } assert (Ack s z <= Ack q (S i + max_v v)). { unfold q; simpl plus; rewrite Ack_S_S; fold q. transitivity (Ack (max r s) z). - apply Ack_mono_l; lia. - apply Ack_mono_r; auto. } lia. } exists (4+ q); intros. pose (z := max (hd v) (max_v (tl v))). simpl evalPrimRec; rewrite <- Heqf; rewrite (decomp _ _ v). remember (vfst v) as x; remember (tl v) as y. transitivity (Ack q (x + max_v y)). + apply L1. + transitivity (Ack q (2 * z)). * apply Ack_mono_r; unfold z; lia. * transitivity (Ack q (Ack 2 z)). -- rewrite Ack_2_n; apply Ack_mono_r; lia. -- simpl max_v; fold z; transitivity (Ack (2 + max 2 q) z). ++ rewrite Nat.max_comm; apply nested_Ack_bound. ++ apply Ack_mono_l; lia. - red;cbn; red; exists 0. intro; rewrite Ack_0; cbn; auto with arith. - red; cbn; red; destruct IHx, IHx0; exists (max x0 x1). intros v; cbn; specialize (H0 v). pose (X := (max_v (map (fun f : naryFunc n => v_apply f v) (evalPrimRecs n m p)))). fold X ; fold X in H0; specialize (H v). pose (Y := v_apply (evalPrimRec n x) v). fold Y; fold Y in H; apply Nat.max_lub. + transitivity (Ack x0 (max_v v)); auto. * apply Ack_mono_l; apply Nat.le_max_l. + transitivity (Ack x1 (max_v v)); auto. * apply Ack_mono_l; apply Nat.le_max_r. Qed.
imports: hydras(primRec Ack MoreVectors) Coq(Arith ArithRing List Lia Compare_dec)