From Undecidability.L Require Import Tactics.LTactics.
Require Import Numbers.BinNums.
From Undecidability.L.Datatypes Require Import LNat LBool.
From Complexity.L Require Import LBinNums LComparison.

Import Nat. 
#[export]
Instance termT_Pos_compare_cont : computableTime' Pos.compare_cont (fun _ _ => (5,fun x _ => (1,fun y _ => (min (Pos.size_nat x) (Pos.size_nat y)*17,tt)))).
Proof.
  unfold Pos.compare_cont.
  extract. solverec.
Qed.

#[export]
Instance term_Pos_compare : computableTime' Pos.compare (fun x _ => (7,fun y _ => (min (Pos.size_nat x) (Pos.size_nat y)*17,tt))).
Proof.
  change Pos.compare with (fun x => Pos.compare x). unfold Pos.compare. set (WorkAround:=Pos.compare_cont).
  extract. solverec.
Qed.

#[export]
Instance termT_N_compare : computableTime' N.compare (fun x _ => (1,fun y _ => (min (N.size_nat x) (N.size_nat y)*17+ 16,tt))).
Proof.
  unfold N.compare. set (WorkAround:=Pos.compare).
  extract. solverec.
Qed.

Import N.
#[export]
Instance termT_N_leb : computableTime' N.leb (fun x _ => (1,fun y _ => (Nat.min (N.size_nat x) (N.size_nat y)*17+ 22,tt))).
Proof.
  extract. solverec.
Qed.

#[export]
Instance termT_N_ltb : computableTime' N.ltb  (fun x _ => (1,fun y _ => (Nat.min (N.size_nat x) (N.size_nat y)*17+ 22,tt))).
Proof.
  extract. solverec.
Qed.

#[export]
Instance termT_N_eqb : computableTime' N.eqb  (fun x _ => (1,fun y _ => (Nat.min (N.size_nat x) (N.size_nat y)*17+ 22,tt))).
Proof.
  eapply computableTimeExt with (x:=fun x y : N => match (x ?= y)%N with
                       | Eq => true
                       | _ => false
                                                end).
  -repeat intro. hnf. now rewrite N.eqb_compare.
  -extract. solverec.
Qed.
