Library hydras.MoreAck.Ack

From hydras Require Export Iterates Exp2.
From Coq Require Import Lia.
From Coq Require Import Program.Wf Arith.
From hydras Require Import ssrnat_extracts.

The famous Ackermann function

The following definition fails, because Coq cannot guess a decreasing argument.

Fail
  Fixpoint Ack (m n : nat) : nat :=
  match m, n with
  | 0, n ⇒ S n
  | m.+1, 0 ⇒ Ack m 1
  | m0.+1, p.+1 ⇒ Ack m0 (Ack m p)
  end.

Definition (with inner fixpoint)

Module Alt.

  Fixpoint Ack (m n : nat) : nat :=
    match m with
    | O ⇒ n .+1
    | p.+1 ⇒ let fix Ackm (n : nat) :=
                 match n with
                 | O ⇒ Ack p 1
                 | S q ⇒ Ack p (Ackm q)
                 end
             in Ackm n
    end.

End Alt.

Definition using the iterate functional:

   iterate : forall {A : Type}, (A -> A) -> nat -> A -> A

Allows to infer monotony properties of Ack (S m) from Ack m.

Fixpoint Ack (m:nat) : nat → nat :=
  match m with
  | 0 ⇒ S
  | n.+1 ⇒ fun k ⇒ iterate (Ack n) k .+1 1
  end.

Using the lexicographic ordering (post by Anton Trunov in stackoverflow (May 2018))

   Definition lex_nat (ab1 ab2 : nat × nat) : Prop :=
    match ab1, ab2 with
    | (a1, b1), (a2, b2) ⇒
      (a1 < a2) ∨ ((a1 = a2) ∧ (b1 < b2))
    end.

this is defined in stdlib, but unfortunately it is opaque

Lemma lt_wf_ind :
∀ n (P:nat → Prop), (∀ n, (∀ m, m < n → P m ) → P n ) → P n.

this is defined in stdlib, but unfortunately it is opaque too

  Lemma lt_wf_double_ind :
    ∀ P:nat → nat → Prop,
      (∀ n m,
          (∀ p (q:nat), p < n → P p q ) →
          (∀ p, p < m → P n p ) → P n m ) → ∀ n m, P n m.

  Lemma lex_nat_wf : well_founded lex_nat.

Module Alt2.

  Program Fixpoint Ack (ab : nat × nat) {wf lex_nat ab} : nat :=
    match ab with
    | (0, b) ⇒ b.+1
    | (a.+1 , 0) ⇒ Ack (a, 1)
    | (a.+1 , b.+1 ) ⇒ Ack (a, Ack (a.+1 , b))
    end.
  Example test1 : Ack (1, 2) = 4 := refl_equal.

  Example test2 : Ack (3, 4) = 125 := refl_equal.

End Alt2.

With the Equations plug-in

From Equations Require Import Equations.

#[ global ] Instance Lex_nat_wf : WellFounded lex_nat.
Defined.

Module Alt3.

  Equations ack (p : nat × nat) : nat by wf p lex_nat :=
    ack (0 , n ) := n.+1 ;
    ack (m .+1 , 0 ) := ack (m, 1);
    ack (m .+1 , n .+1 ) := ack (m, ack (m.+1 , n)).

End Alt3.

Exercise

Prove that the four definitions of the Ackermann function Ack , Alt.Ack, Alt2.Ack, and Alt3.ack are extensionnally equal

Usual equations

Lemma Ack_0 : Ack 0 = S.

Lemma Ack_S_0 m : Ack m .+1 0 = Ack m 1.

Lemma Ack_S_S : ∀ m p,
Ack m .+1 p .+1 = Ack m (Ack m .+1 p).

First values

Lemma Ack_1_n n : Ack 1 n = n .+2.

Lemma Ack_2_n n: Ack 2 n = 2 × n + 3.

Lemma Ack_3_n n: Ack 3 n = exp2 n .+3 - 3.

Lemma Ack_4_n n : Ack 4 n = hyper_exp2 n .+3 - 3.

monotony properties

We prove simultaneously 3 properties of Ack n by induction on m:

Ack m is strictly monotonous,
Ack m n > n
Ack m n ≤ Ack (S m) n

Section Ack_Properties.

  Let P (m:nat) := strict_mono (Ack m) ∧
                   S <<= (Ack m ) ∧
                   (∀ n, Ack m n ≤ Ack m .+1 n ).

  Remark P0 : P 0.

  Section Induc_step.
    Variable m:nat.
    Hypothesis Hm : P m.

    Remark Rem1 : strict_mono (Ack m .+1).

    Remark Rem2 : S <<= Ack m .+1.

    Remark Ack_m_mono_weak : ∀ n p, n ≤ p →
                                         Ack m n ≤ Ack m p.

    Remark Rem3 : ∀ n, Ack m .+1 n ≤ Ack m .+2 n.

    Lemma L5: P m .+1.

  End Induc_step.

  Lemma Ack_properties : ∀ m, P m.

End Ack_Properties.

Lemma le_S_Ack m : fun_le S (Ack m).

Lemma Ack_strict_mono m : strict_mono (Ack m).

Lemma Ack_mono_l m n : m ≤ n → ∀ p, Ack m p ≤ Ack n p.

Lemma Ack_mono_r m: ∀ n p, n ≤ p → Ack m n ≤ Ack m p.

Bounding nested calls of Ack

The following inequality is applied in the proof that Ack is not primitive recursive, allowing to eliminate patterns of the form Ack (Ack _ _ _).

 Lemma nested_Ack_bound : 
    forall k m n, Ack k (Ack m n) <= Ack (2 + max k m) n.

Section Proof_of_nested_Ack_bound.

  Remark R0 (m:nat): ∀ n, 2 + n ≤ Ack (2 + m) n.

  Remark R1 : ∀ m n, Ack m .+1 n .+1 ≤ Ack (2 + m) n.

  Remark R2 (m n:nat) : Ack m (Ack m n) ≤ Ack m .+1 n .+1.

  Remark R3 (m n:nat) : Ack m (Ack m n) ≤ Ack m .+2 n.

  Lemma nested_Ack_bound k m n :
    Ack k (Ack m n) ≤ Ack (2 + max k m) n.
End Proof_of_nested_Ack_bound.

Lemma Ack_Sn_plus : ∀ n p, n .+1 + p < Ack n .+1 p.

Ack is (partially) strictly monotonous in its first argument

Remark R5 m n : Ack m n .+1 < Ack m .+1 n .+1.

Lemma Ack_strict_mono_l : ∀ n m p, n < m →
Ack n p .+1 < Ack m p .+1.