equivspv.lean

import data.equiv 

def is_valuation {R : Type} [comm_ring R] {α : Type} [linear_order α] (f : R → α) : Prop := true

structure valuations (R : Type) [comm_ring R] :=
(α : Type) [Hα : linear_order α] (f : R → α) (Hf : is_valuation f)

instance to_make_next_line_work (R : Type) [comm_ring R] (v : valuations R) : linear_order v.α := v.Hα

instance valuations.setoid (R : Type) [comm_ring R] : setoid (valuations R) := {
  r := λ v w, ∀ r s : R, valuations.f v r ≤ v.f s ↔ w.f r ≤ w.f s,
  iseqv := ⟨λ v r s,iff.rfl,λ v w H r s,(H r s).symm,λ v w x H1 H2 r s,iff.trans (H1 r s) (H2 r s)⟩
}

def Spv1 (R : Type) [comm_ring R] := quotient (valuations.setoid R)

def Spv2 (R : Type) [comm_ring R] := 
  {ineq : R → R → Prop // ∃ v : valuations R, ∀ r s : R, ineq r s ↔ v.f r ≤ v.f s}

#check Spv1 _ -- Type 1
#check Spv2 _ -- Type

def to_fun (R : Type) [comm_ring R] : Spv1 R → Spv2 R :=
quotient.lift (λ v,(⟨λ r s, valuations.f v r ≤ v.f s,⟨v,λ r s,iff.rfl⟩⟩ : Spv2 R))
  (λ v w H,begin dsimp,congr,funext,exact propext (H r s) end) 

noncomputable def inv_fun (R : Type) [comm_ring R] : Spv2 R → Spv1 R :=
λ ⟨ineq,H⟩,⟦classical.some H⟧

set_option pp.implicit true 

noncomputable definition they_are_the_same (R : Type) [comm_ring R] : equiv (Spv1 R) (Spv2 R) :=
{ to_fun := to_fun R,
  inv_fun := inv_fun R,
  left_inv := λ vs,begin
    cases (quotient.exists_rep vs) with v Hv,
    rw ←Hv,
    apply quotient.sound,
    intros r s,
    have H := classical.some_spec (to_fun R vs).property,
    rw (H r s).symm, -- fails
    /-
    rewrite tactic failed, did not find instance of the pattern in the target expression
  (classical.some _).f r ≤ (classical.some _).f s
state:
R : Type,
_inst_1 : comm_ring R,
vs : Spv1 R,
v : valuations R,
Hv : ⟦v⟧ = vs,
r s : R,
H : ∀ (r s : R), (to_fun R vs).val r s ↔ (classical.some _).f r ≤ (classical.some _).f s
⊢ (classical.some _).f r ≤ (classical.some _).f s ↔ v.f r ≤ v.f s
    -/
  end,
  right_inv := λ s2,begin
    cases s2 with rel Hrel,
    apply subtype.eq,
    dsimp,
    unfold inv_fun,
    funext r s,
    sorry
  end 
}