Ackermann proofs with sniper (without subset types)

Ack_sniper.v

From Sniper Require Import Sniper.
From SMTCoq Require SMTCoq.
Require Import ZArith.
Require Import Program.Utils.
Open Scope Z_scope.
Set Bullet Behavior "Strict Subproofs".
Section ack_proof.

(* We define ack as an uninterpreted function in order not to mess with equations etc. *)
Variable ack : Z -> Z -> Z.


(* ack_1-3 come from the definition of ack. *)
Hypothesis ack_1 : forall n, n>=0 -> ack 0 n = n + 1.
Hypothesis ack_2 : forall m, m > 0 -> ack m 0 = ack (m-1) 1.
Hypothesis ack_3 : forall m n, m > 0 -> n > 0 -> ack m n = ack (m-1) (ack m (n-1)).



Theorem ack_gt_snd (m n: Z): m>=0 -> n>=0 -> ack m n > n.
  destruct (dec (m=?0)).
  - snipe. Undo.
    smt.
    (* Both smt (from SMTCOq) and snipe can solve the goal *)
  - (* axiomatizing the (lexicographic) inductive hypothesis: *)
    assert (forall m' n',
      (m'>=0 -> n'>=0
        -> m' < m \/ m' = m /\ n' < n
        -> ack m' n' > n')
      -> ack m n > n)
     as ack_gt_snd
     by admit.
    destruct (dec (n=?0)).
    + pose proof (ack_gt_snd (m-1) 1). snipe.
    + pose proof (ack_gt_snd (m-1) (ack m (n-1))).
      pose proof (ack_gt_snd m (n-1)).
      snipe. Undo.
      smt. 
      (* Both smt (from SMTCOq) and snipe can solve the goal *)
Admitted.

(* If the admitted lemma is used the proof breaks, so we add it as a hypothesis. *)
Hypothesis ack_gt_snd' : forall m n:Z, m>=0 -> n>=0 -> ack m n > n.


(*  now we can prove ack_snd_plus_one (which doesn't require induction) *)
Theorem ack_snd_plus_one (m n: Z):m >=0 -> n >= 0 -> ack m (n+1) > (ack m n).
intros.
  destruct (dec (m =? 0)).
  + snipe.
  + pose proof (ack_gt_snd' (m-1) n). snipe.
Qed.

(* We can also prove ack_mon_snd by axiomatizing the inductive hypothesis. *)
Theorem ack_mon_snd (m n p: Z): m>=0 -> n>=0 -> p>=0 -> n > p -> ack m n > ack m p.
  destruct (dec (n =? p + 1)).
  + pose proof (ack_snd_plus_one m p). snipe.

  + (* axiomatizing the inductive hypothesis: *)
  assert (forall m' k p', m' >= 0 -> k >= 0 -> p' >= 0 -> k < n -> k > p -> ack m' k > ack m' p') as ind
  by admit.
  pose proof (ack_snd_plus_one m (n-1)).
  pose proof (ind m (n-1) p). snipe.
Admitted.


End ack_proof.