From Undecidability.L Require Import Datatypes.LNat Tactics.LTactics.
Import Ring.
(* ** Computability of Ackermann *)
Fixpoint ackermann n : nat -> nat :=
match n with
0 => S
| S n => fix ackermann_Sn m : nat :=
match m with
0 => (fun _ => ackermann n 1)
| S m => (fun _ => ackermann n (ackermann_Sn m))
end true
end.
Lemma term_ackermann : computable ackermann.
Proof.
extract.
Qed.
Local Lemma Ack_pos n m : 0 < ackermann n m.
Proof.
revert m.
induction n as [n IHn] using lt_wf_ind. intros m.
induction m as [m IHm] using lt_wf_ind.
destruct n. all:destruct m.
all:eauto.
all:cbn in *. all:try lia.
all:eauto.
Qed.
Import Ring Arith. Import Lia.
Lemma termT_ackermann :
computableTime' ackermann
(fun x _ =>
(14,
fun y _ =>
(cnst("f",x,y),tt))).
Proof.
extract.
cbn. fold ackermann.
repeat (cbn ;intros;intuition idtac;try destruct _).
all:ring_simplify. all:try nia.
all:repeat change (fix ackermann_Sn (m : nat) : nat :=
match m with
| 0 => fun _ => ackermann x0 1
| S m0 => fun _ => ackermann x0 (ackermann_Sn m0)
end true) with (ackermann (S x0)). all: refine ( _:(_ >= _)).
(* Todo: find an f satisfying the 3 equations in the goal *)
Abort.
Import Ring.
(* ** Computability of Ackermann *)
Fixpoint ackermann n : nat -> nat :=
match n with
0 => S
| S n => fix ackermann_Sn m : nat :=
match m with
0 => (fun _ => ackermann n 1)
| S m => (fun _ => ackermann n (ackermann_Sn m))
end true
end.
Lemma term_ackermann : computable ackermann.
Proof.
extract.
Qed.
Local Lemma Ack_pos n m : 0 < ackermann n m.
Proof.
revert m.
induction n as [n IHn] using lt_wf_ind. intros m.
induction m as [m IHm] using lt_wf_ind.
destruct n. all:destruct m.
all:eauto.
all:cbn in *. all:try lia.
all:eauto.
Qed.
Import Ring Arith. Import Lia.
Lemma termT_ackermann :
computableTime' ackermann
(fun x _ =>
(14,
fun y _ =>
(cnst("f",x,y),tt))).
Proof.
extract.
cbn. fold ackermann.
repeat (cbn ;intros;intuition idtac;try destruct _).
all:ring_simplify. all:try nia.
all:repeat change (fix ackermann_Sn (m : nat) : nat :=
match m with
| 0 => fun _ => ackermann x0 1
| S m0 => fun _ => ackermann x0 (ackermann_Sn m0)
end true) with (ackermann (S x0)). all: refine ( _:(_ >= _)).
(* Todo: find an f satisfying the 3 equations in the goal *)
Abort.