From Undecidability.L.Datatypes Require Import LOptions LBool LNat Lists.
From Undecidability.L.Tactics Require Import LTactics ComputableTactics.
Require Import Nat.
Set Default Proof Using "Type".
Section demo.
Definition unit_enc := fun (x:unit) => I.
Instance register_unit : registered unit.
Proof.
register unit_enc.
Defined.
Definition on0 (f:nat->nat->nat) := f 0 0.
Instance term_on0 : computable on0.
Proof.
extract.
Qed.
Lemma test_Some_nat : computable (@Some nat).
Proof.
extract.
Qed.
Section PaperExample.
Import ComputableTactics.
Import ComputableTactics.Intern.
Goal computable orb.
Proof.
extractAs s.
computable_using_noProof s.
cstep.
cstep.
cstep.
all: cstep.
Qed.
Goal forall fT, computableTime' orb fT.
Proof.
intros.
extractAs s.
computable_using_noProof s.
cstep.
cstep. cstep. cstep.
1,2:cstep. solverec.
Abort.
Goal computableTime' orb (fun _ _ => (cnst "c1",fun _ _ => (cnst "c2",tt))).
Proof.
extract. solverec. Abort.
Goal computableTime' orb (fun _ _ => (1,fun _ _ => (3,tt))).
Proof.
extract. solverec.
Abort.
Import Datatypes.LNat.
Goal computable Nat.add.
Proof.
unfold Nat.add.
extractAs s.
computable_using_noProof s.
cstep.
all:cstep.
all:cstep.
Qed.
Goal computable (fix f (x y z : nat) := y + match y with | S (S y) => S (f x y z) | _ => 0 end).
extractAs s.
computable_using_noProof s.
cstep.
all:cstep.
all:cstep.
all:cstep.
Qed.
Lemma supported3 : computable (fun (b:bool) => if b then (fix f x := match x with S x => f x | 0 => 0 end) else S).
extractAs s.
computable_using_noProof s.
cstep.
cstep.
all:cstep.
all:cstep.
Qed.
Lemma unsupported : computable (fix f (y : nat) {struct y}:= match y with | S (S y) => f y | _ => S end).
extractAs s.
computable_using_noProof s.
repeat cstep.
Fail Guarded.
Abort.
Lemma workarround : let f := (fix f (z y : nat) {struct y}:= match y with | S (S y) => f z y | _ => S z end) in computable (fun y z => f z y).
Proof.
intros f. assert (computable f) by (unfold f;extract).
extract.
Qed.
Lemma unsupported2 : computable 10.
Proof.
extract. Fail reflexivity.
Abort.
Goal computable (fun n : nat => 10).
Proof.
extract.
Qed.
Import Datatypes.Lists.
Remove Hints term_map : typeclass_instances.
Lemma map_term A B (Rx : registered A) (Ry: registered B):
computable (@map A B).
Proof.
extractAs s.
computable_using_noProof s.
cstep.
cstep.
all:cstep.
Qed.
Lemma termT_map A B (Rx : registered A) (Ry: registered B):
computableTime' (@map A B) (fun f fT => (cnst "c",fun xs _ => (cnst ("f",xs),tt))).
Proof.
extractAs s.
computable_using_noProof s.
cstep.
cstep.
repeat cstep.
Abort.
Lemma termT_map A B (Rx : registered A) (Ry: registered B):
computableTime' (@map A B) (fun f fT => (cnst "c",fun xs _ => (cnst ("f",xs),tt))).
Proof.
extract. solverec.
Abort.
Lemma term_map (X Y:Type) (Hx : registered X) (Hy:registered Y):
computableTime' (@map X Y)
(fun f fT => (1,fun l _ => (fold_right (fun x res => fst (fT x tt) + res + 12) 8 l,tt))).
Proof.
extract.
solverec.
Qed.
End PaperExample.
End demo.
From Undecidability.L.Tactics Require Import LTactics ComputableTactics.
Require Import Nat.
Set Default Proof Using "Type".
Section demo.
Definition unit_enc := fun (x:unit) => I.
Instance register_unit : registered unit.
Proof.
register unit_enc.
Defined.
Definition on0 (f:nat->nat->nat) := f 0 0.
Instance term_on0 : computable on0.
Proof.
extract.
Qed.
Lemma test_Some_nat : computable (@Some nat).
Proof.
extract.
Qed.
Section PaperExample.
Import ComputableTactics.
Import ComputableTactics.Intern.
Goal computable orb.
Proof.
extractAs s.
computable_using_noProof s.
cstep.
cstep.
cstep.
all: cstep.
Qed.
Goal forall fT, computableTime' orb fT.
Proof.
intros.
extractAs s.
computable_using_noProof s.
cstep.
cstep. cstep. cstep.
1,2:cstep. solverec.
Abort.
Goal computableTime' orb (fun _ _ => (cnst "c1",fun _ _ => (cnst "c2",tt))).
Proof.
extract. solverec. Abort.
Goal computableTime' orb (fun _ _ => (1,fun _ _ => (3,tt))).
Proof.
extract. solverec.
Abort.
Import Datatypes.LNat.
Goal computable Nat.add.
Proof.
unfold Nat.add.
extractAs s.
computable_using_noProof s.
cstep.
all:cstep.
all:cstep.
Qed.
Goal computable (fix f (x y z : nat) := y + match y with | S (S y) => S (f x y z) | _ => 0 end).
extractAs s.
computable_using_noProof s.
cstep.
all:cstep.
all:cstep.
all:cstep.
Qed.
Lemma supported3 : computable (fun (b:bool) => if b then (fix f x := match x with S x => f x | 0 => 0 end) else S).
extractAs s.
computable_using_noProof s.
cstep.
cstep.
all:cstep.
all:cstep.
Qed.
Lemma unsupported : computable (fix f (y : nat) {struct y}:= match y with | S (S y) => f y | _ => S end).
extractAs s.
computable_using_noProof s.
repeat cstep.
Fail Guarded.
Abort.
Lemma workarround : let f := (fix f (z y : nat) {struct y}:= match y with | S (S y) => f z y | _ => S z end) in computable (fun y z => f z y).
Proof.
intros f. assert (computable f) by (unfold f;extract).
extract.
Qed.
Lemma unsupported2 : computable 10.
Proof.
extract. Fail reflexivity.
Abort.
Goal computable (fun n : nat => 10).
Proof.
extract.
Qed.
Import Datatypes.Lists.
Remove Hints term_map : typeclass_instances.
Lemma map_term A B (Rx : registered A) (Ry: registered B):
computable (@map A B).
Proof.
extractAs s.
computable_using_noProof s.
cstep.
cstep.
all:cstep.
Qed.
Lemma termT_map A B (Rx : registered A) (Ry: registered B):
computableTime' (@map A B) (fun f fT => (cnst "c",fun xs _ => (cnst ("f",xs),tt))).
Proof.
extractAs s.
computable_using_noProof s.
cstep.
cstep.
repeat cstep.
Abort.
Lemma termT_map A B (Rx : registered A) (Ry: registered B):
computableTime' (@map A B) (fun f fT => (cnst "c",fun xs _ => (cnst ("f",xs),tt))).
Proof.
extract. solverec.
Abort.
Lemma term_map (X Y:Type) (Hx : registered X) (Hy:registered Y):
computableTime' (@map X Y)
(fun f fT => (1,fun l _ => (fold_right (fun x res => fst (fT x tt) + res + 12) 8 l,tt))).
Proof.
extract.
solverec.
Qed.
End PaperExample.
End demo.