compute3.lean

import data.set.basic
import data.nat.lattice
import data.ordmap.ordset
import data.erased
import tactic

universes u v

prefix `!`:100 := erased

/- "omniscient".  The `id` is to force the type to be `erased` -/
notation `omni `:0 s := ( ⟨_, s, rfl⟩ : erased _)

@[elab_as_eliminator]
lemma erased.elim {α : Type u} {P : !α → Prop} (h : ∀ x, P (erased.mk x)) (v : !α) : P v :=
begin
  convert h v.out,
  simp,
end

@[simp]
lemma erased.fst_mk {α : Type u} (x : α) : (erased.mk x).fst = (λ y, x = y) := rfl

lemma erased.singleton {α : Type u} (v : !α) : set_of v.1 = {v.out} :=
begin
  refine erased.elim (λ x, _) v,
  ext y,
  simp [eq_comm],
end

@[simp] lemma erased.mk_inj' {α} (a b : α) : erased.mk a = erased.mk b ↔ a = b :=
begin
  split,
  { intro h,
    have h' := congr_arg erased.out h,
    simpa using h', },
  { rintro rfl,
    refl, },
end

@[simp] lemma erased.out_inj' {α} (a b : !α) : a.out = b.out ↔ a = b :=
⟨erased.out_inj _ _, by { rintro rfl, refl }⟩

@[simp] lemma erased.omni_eq {α} (a : α) : (omni a) = erased.mk a := rfl

@[simp] lemma erased.mem_fst {α : Type u} (v : !α) (x : α) : v.fst x ↔ v.out = x :=
begin
  refine erased.elim (λ y, _) v,
  split; intro h; simpa using h,
end

lemma erased.exists {α : Type u} (v : !α) : ∃ x, v.1 x :=
begin
  use v.out,
  simp,
end

@[simp] lemma erased.eq_exists_some {α : Type u} (v : !α) : v.2.some = v.out :=
begin
  cases v,
  refl,
end

@[elab_as_eliminator]
def erased.rec {α : Type u} {β : Π (v : !α), Type*} (h : Π x, β (erased.mk x)) (v : !α) : !β v :=
begin
  convert erased.mk (h v.out),
  simp,
end

@[simp] lemma erased.rec_mk {α : Type u} {β : Π (v : !α), Type*} (h : Π x, β (erased.mk x)) (x : α) :
  erased.rec h (erased.mk x) = erased.mk (h x) :=
begin
  ext y,
  simp [erased.rec],
  have : ∀ x' (h' : x' = x) (h'' : !β (erased.mk x') = !β (erased.mk x)), (cast h'' (erased.mk (h x'))).out = h x,
  { rintros _ rfl, simp, },
  apply this,
  simp,
end

@[elab_as_eliminator]
def erased.rec' {α : Type u} {β : Π (v : !α), Type*} (h : Π x, !β (erased.mk x)) (v : !α) : !β v :=
begin
  refine ⟨λ y, (h v.out).1 _, _⟩,
  convert y, simp,
  refine erased.elim (λ x, _) v,
  use (h x).out,
  ext z,
  simp,
  have : ∀ x' (h' : x' = x) (h'' : β (erased.mk x) = β (erased.mk x')), (h x).out = z ↔ (h x').out = cast h'' z,
  { rintro _ rfl,
    simp, },
  apply this,
  simp,
end
/-
@[simp] lemma erased.rec'_mk {α : Type u} {β : Π (v : !α), Type*} (h : Π x, !β (erased.mk x)) (x : α) :
  erased.rec' h (erased.mk x) = h x :=
begin
  ext y,
  simp [erased.rec'],
  have : ∀ x, ∃ y, h x = erased.mk y := λ x, ⟨(h x).out, by simp⟩,
  choose f h' using this,
  simp [h'],
  generalize h'' : erased.mk (f x) = z,
  cases z,
  congr,
  ext y,
  generalize_proofs,
  have : ∀ x' (h' : x = x') (h'' : β (erased.mk x) = β (erased.mk x')), f (erased.mk x).out = cast h'' y ↔ z_fst y,
  { rintro _ rfl,
    simp [h'],
    have : (erased.mk (f x)).fst = z_fst, rw h'',
    subst z_fst,
    simp, },
  simp,
  apply this,

end
-/

def erased.set_unwrap {α : Type u} : set (!α) ≃ set α :=
{ to_fun := λ s, {x | erased.mk x ∈ s},
  inv_fun := λ s, {v | v.out ∈ s},
  left_inv := begin
    intro s,
    ext v,
    simp,
  end,
  right_inv := begin
    intro s,
    ext x,
    simp,
  end }

@[simp] lemma erased.set_unwrap_mem {α : Type u} (s : set (!α)) (x : α) : x ∈ erased.set_unwrap s ↔ erased.mk x ∈ s := iff.rfl

@[simp] lemma erased.set_wrap_mem {α : Type u} (s : set α) (v : !α) : v ∈ erased.set_unwrap.symm s ↔ v.out ∈ s := iff.rfl

def erased.set_remove {α : Type u} : !set α ≃ set α :=
{ to_fun := λ s, {x | x ∈ s.out},
  inv_fun := erased.mk,
  left_inv := begin
    intro s,
    simp,
  end,
  right_inv := begin
    intro s,
    simp,
  end }

attribute [simps] erased.monad

@[simps]
def erased.double {α : Type*} : !!α ≃ !α :=
{ to_fun := mjoin,
  inv_fun := pure,
  left_inv := begin
    intro s,
    simp [mjoin],
  end,
  right_inv := begin
    intro s,
    simp [mjoin]
  end }

def erased.dpush {α : Type*} {β : α → Type*}: !(Π (x : α), β x) ≃ (Π (x : α), !β x) :=
{ to_fun := λ f x, (do f' ← f,
                       pure (f' x)),
  inv_fun := λ f, (omni λ x, (f x).out),
  left_inv := λ f, by simp,
  right_inv := λ f, by simp }

def erased.push {α β : Type*} : !(α → β) ≃ (α → !β) := erased.dpush

class computable {α : Type*} (v : !α) :=
(compute : α)
(compute_spec : compute = v.out)

def erased.compute {α : Type*} (v : !α) [computable v] : α := computable.compute v

@[simp]
lemma erased.compute_spec {α : Type*} (v : !α) [computable v] : v.compute = v.out := computable.compute_spec

instance {α : Type*} (v : !α) : subsingleton (computable v) :=
⟨begin
  rintros ⟨a, ha⟩ ⟨b, hb⟩,
  subst a, subst b,
end⟩

instance computable_incl {α : Type*} (x : α) : computable (erased.mk x) :=
{ compute := x,
  compute_spec := by simp }

instance mem_incl_decidable {α : Type*} [decidable_eq α] (x : α) : decidable_pred (erased.mk x).fst :=
begin
  intro n,
  simp,
  apply_instance,
end

lemma compute_incl' {α : Type*} (x : α) : (erased.mk x).compute = x := rfl

@[simp]
lemma compute_incl {α : Type*} (x : α) (h : computable (erased.mk x)) :
  @erased.compute _ (erased.mk x) h = x :=
begin
  convert compute_incl' x,
end

@[simp]
lemma incl_compute {α : Type*} (v : !α) [h : computable v] : erased.mk v.compute = v :=
begin
  simp,
end

def computable_eqv' {α : Type*} [∀ (v : !α), computable v] : !α ≃ α :=
{ to_fun := λ v, v.compute,
  inv_fun := erased.mk,
  left_inv := λ v, by simp,
  right_inv := λ x, by simp }

noncomputable def ite' {α : Type*} (c : Prop) (x y : α) : α :=
by { classical, exact ite c x y }

abbreviation ite'.compute {α : Type*} (c : Prop) [decidable c] (x y : α) [computable (omni x)] [computable (omni y)] :
  computable (omni ite' c x y) :=
begin
  convert_to computable (erased.mk (ite c (erased.compute (omni x)) (erased.compute (omni y)))) using 2,
  simp [ite'],
  refine (λ x', _) x,
  refine (λ y', _) y,
  split_ifs; simp [h],
  use ite c (erased.compute (omni x)) (erased.compute (omni y)),
  simp,
end

attribute [instance] ite'.compute

--instance (α : Type*) : has_coe α (!α) := ⟨pure⟩

instance coe_computable (α : Type*) (x : α) : computable (omni x) :=
⟨x, by { change x = erased.out (pure x), simp, }⟩

def a := 5
def b := 22

def c := erased.compute (omni (ite' (true) 5 22))

#eval erased.compute (omni (ite' (true) 5 22))

instance nat.computable (v : !ℕ) [decidable_pred v.1] : computable v :=
{ compute := nat.find v.exists,
  compute_spec := by simpa [eq_comm] using nat.find_spec v.exists }

def Inf' (s : set ℕ) : !ℕ := omni Inf s

instance nat.Inf'_computable (s : set ℕ) [decidable_pred (∈ s)] [h : decidable s.nonempty] : computable (Inf' s) :=
begin
  tactic.unfreeze_local_instances,
  simp [Inf'],
  cases h,
  use 0, simp, symmetry, rw nat.Inf_eq_zero, right, rwa set.not_nonempty_iff_eq_empty at h,
  use nat.find h,
  simp [nat.Inf_def h],
  congr,
end

instance nat.Inf'_interval (a : ℕ) : computable (Inf' (set.Ici a)) :=
⟨a, by simp [Inf']⟩

#eval (Inf' (set.Ici 100)).compute

noncomputable
def foo : ℕ := classical.choice infer_instance

def foo2 : !ℕ := omni foo

noncomputable def nth' (p : ℕ → Prop) : ℕ → ℕ
| n := Inf { i : ℕ | p i ∧ ∀ k < n, nth' k < i }

def nth (p : ℕ → Prop) (n : ℕ) : !ℕ := omni nth' p n

abbreviation finset' (α : Type*) := !finset α

namespace finset'
variables {α : Type*}

instance is_set_like : set_like (finset' α) α :=
⟨λ f, {x | x ∈ f.out},
begin
  intro s,
  refine erased.elim (λ s, _) s,
  intro t,
  refine erased.elim (λ t, _) t,
  simp,
end⟩

@[simp] lemma mem_to_finset {s : finset' α} {x : α} : x ∈ s.out ↔ x ∈ s := iff.rfl

@[simp] lemma mem_incl {s : finset α} (x : α) : x ∈ erased.mk s ↔ x ∈ s :=
begin
  rw ←mem_to_finset,
  simp,
end

@[ext] theorem ext {s t : finset' α} (h : ∀ x, x ∈ s ↔ x ∈ t) : s = t := set_like.ext h

@[simp] lemma coe_to_finset (s : finset' α) : (s.out : set α) = s :=
by { ext, simp }

--def union (s t : finset' α) : finset' α :=
--⟨{u | by { classical, exact u = s.val ∪ t.val }}, _, rfl⟩

instance : has_union (finset' α) :=
⟨λ s t, omni by { classical, exact s.out ∪ t.out }⟩

@[simp]
lemma mem_union {s t : finset' α} (x : α) : x ∈ s ∪ t ↔ x ∈ s ∨ x ∈ t :=
begin
  change x ∈ erased.mk _ ↔ _,
  simp,
end

instance (s t : finset' α) [computable s] [computable t] [decidable_eq α] : computable (s ∪ t) :=
{ compute := s.compute ∪ t.compute,
  compute_spec := begin
    ext x,
    simp,
  end }

abbreviation a : finset' ℕ := omni ({1,2} : finset ℕ)
abbreviation b : finset' ℕ := omni ({2,3,4} : finset ℕ)

#eval (a ∪ b).compute

/- nonsense so far. is it possible to do the union using an ordset?

def of_ordset [preorder α] (s : ordset α) : finset' α := sval.incl ⟨s.val.to_list, sorry⟩

def to_ordset' [preorder α] (s : finset α) : ordset α := sorry

class conv_ordset {α : Type*} (x : α) (β : out_param $ Type*) [preorder β] :=
(to_ordset : ordset β)

@[priority 0]
instance conv_ordset1 [preorder α] (s : finset α) : conv_ordset s α := ⟨to_ordset' s⟩

instance conv_ordset2 [preorder α] (s : ordset α) : conv_ordset (of_ordset s) α := ⟨s⟩

instance [preorder α] : has_union (ordset α) := sorry

instance [preorder α] (s t : finset' α) [conv_ordset s α] [conv_ordset t α] : computable (s ∪ t) :=
{ compute := of_ordset (conv_ordset.to_ordset s ∪ conv_ordset.to_ordset t),
  compute_spec := begin
  end }

-/

end finset'