-
-
Save lykmast/4b32d6e319e8f6efdcdd593c78425616 to your computer and use it in GitHub Desktop.
Ackermann proofs with sniper (without subset types)
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment