sorry out breaking changes

Author: markusdemedeiros

src/Iris/Algebra/DFrac.lean

@@ -20,10 +20,10 @@ abbrev DFrac F := LeibnizO (DFracK F)
 -- TODO: Delete this class. I have it now because the Fractional class is being
 -- changed concurrently. Also I'm certain that some of these fields will be derivable.
 class DFractional (F : Type _) extends Fractional F where
-  one_strict_max {y : F} : ¬(One.one + y ≤ One.one)
-  lt_irrefl : ¬(One.one < (One.one : F))
-  strict_pos {x y : F} : ¬(x + y = x)
-  lt_op_mono {x y z : F} : x + y ≤ z → y < z -- OK because positive
+  -- one_strict_max {y : F} : ¬(One.one + y ≤ One.one)
+  -- lt_irrefl : ¬(One.one < (One.one : F))
+  -- strict_pos {x y : F} : ¬(x + y = x)
+  -- lt_op_mono {x y z : F} : x + y ≤ z → y < z -- OK because positive
 
 section dfrac
 
@@ -34,9 +34,9 @@ variable {F : Type _} [DFractional F]
 instance : Inhabited (DFrac F) := ⟨⟨Discard⟩⟩
 
 abbrev valid : DFrac F → Prop
-| ⟨Own f⟩        => f ≤ One.one
+| ⟨Own f⟩        => Fractional.proper f -- f ≤ One.one
 | ⟨Discard⟩      => True
-| ⟨OwnDiscard f⟩ => f < One.one
+| ⟨OwnDiscard f⟩ => sorry -- Iris.fraction -- f < One.one
 
 abbrev pcore : DFrac F → Option (DFrac F)
 | ⟨Own _⟩        => none
@@ -70,6 +70,8 @@ instance DFrac_CMRA : CMRA (DFrac F) where
   valid_iff_validN := ⟨fun x _ => x, fun x => x 0⟩
   validN_succ := id
   validN_op_left {_ x y} := by
+    sorry
+    /-
     have Lleft {a' a : F} (H : a' + a < one) : a' < one := by
       rcases Fractional.lt_sum.mp H with ⟨r, Hr⟩
       exact (Fractional.lt_sum.mpr ⟨a + r, Hr.symm ▸ Fractional.assoc.symm⟩)
@@ -79,12 +81,16 @@ instance DFrac_CMRA : CMRA (DFrac F) where
     · exact (Fractional.add_le_mono <| Fractional.lt_le ·)
     · exact Lleft
     · exact Lleft
+    -/
   assoc {x y z} := by
+    sorry
+    /-
     rcases x with ⟨x|_|x⟩ <;>
     rcases y with ⟨y|_|y⟩ <;>
     rcases z with ⟨z|_|z⟩ <;>
     simp [op, Fractional.assoc]
-  comm {x y} := by rcases x with ⟨x|_|x⟩ <;> rcases y with ⟨y|_|y⟩ <;> simp [op, Fractional.comm]
+    -/
+  comm {x y} := sorry -- by rcases x with ⟨x|_|x⟩ <;> rcases y with ⟨y|_|y⟩ <;> simp [op, Fractional.comm]
   pcore_op_left {x y} := by rcases x with ⟨x|_|x⟩ <;> rcases y with ⟨y|_|y⟩ <;> simp
   pcore_idem {x y} := by rcases x with ⟨x|_|x⟩ <;> rcases y with ⟨y|_|y⟩ <;> simp
   pcore_op_mono {x y} := by
@@ -120,9 +126,9 @@ instance : CMRA.Exclusive (α := DFrac F) ⟨Own One.one⟩ where
   exclusive0_l y := by
     rcases y with ⟨y|_|y⟩ <;>
     simp only [CMRA.ValidN, valid]
-    · exact DFractional.one_strict_max
-    · exact DFractional.lt_irrefl
-    · exact DFractional.one_strict_max ∘ Fractional.lt_le
+    · sorry -- exact DFractional.one_strict_max
+    · sorry -- exact DFractional.lt_irrefl
+    · sorry -- exact DFractional.one_strict_max ∘ Fractional.lt_le
 
 instance {f : F} : CMRA.Cancelable (α := DFrac F) ⟨Own f⟩ where
   cancelableN {_ x y} := by
@@ -131,31 +137,31 @@ instance {f : F} : CMRA.Cancelable (α := DFrac F) ⟨Own f⟩ where
     simp [CMRA.ValidN, CMRA.op, op]
     all_goals intro H Hxyz
     all_goals (try have Hxyz' := LeibnizO.dist_inj Hxyz <;> simp at Hxyz')
-    · exact congrArg (LeibnizO.mk ∘ Own) (Fractional.cancel Hxyz')
-    · exact (DFractional.strict_pos (F := F) Hxyz'.symm).elim
-    · exact (DFractional.strict_pos (F := F) Hxyz').elim
-    · exact congrArg (LeibnizO.mk ∘ OwnDiscard) (Fractional.cancel Hxyz')
+    · sorry -- exact congrArg (LeibnizO.mk ∘ Own) (Fractional.cancel Hxyz')
+    · sorry -- exact (DFractional.strict_pos (F := F) Hxyz'.symm).elim
+    · sorry -- exact (DFractional.strict_pos (F := F) Hxyz').elim
+    · sorry -- exact congrArg (LeibnizO.mk ∘ OwnDiscard) (Fractional.cancel Hxyz')
 
 instance {f : F} : CMRA.IdFree (α := DFrac F) ⟨Own f⟩ where
   id_free0_r y := by
     rcases y with ⟨y|_|y⟩ <;> simp [CMRA.ValidN, CMRA.op, op] <;> intro H Hxyz
     all_goals (try have Hxyz' := LeibnizO.dist_inj Hxyz <;> simp at Hxyz')
-    exact (DFractional.strict_pos (F := F) Hxyz').elim
+    sorry -- exact (DFractional.strict_pos (F := F) Hxyz').elim
 
-theorem valid_own_iff {f : F} : ✓ (LeibnizO.mk (Own f)) ↔ f ≤ One.one := by simp [CMRA.Valid]
-theorem valid_own_one : ✓ (LeibnizO.mk (Own (One.one : F))) := valid_own_iff.mpr Fractional.le_refl
+-- theorem valid_own_iff {f : F} : ✓ (LeibnizO.mk (Own f)) ↔ f ≤ One.one := by simp [CMRA.Valid]
+-- theorem valid_own_one : ✓ (LeibnizO.mk (Own (One.one : F))) := valid_own_iff.mpr Fractional.le_refl
 
-theorem valid_op_own_r {dq : DFrac F} {q : F} : ✓ (dq • ⟨Own q⟩) → (q < One.one) := by
-  rcases dq with ⟨y|_|y⟩ <;> simp [CMRA.ValidN, CMRA.op, op, CMRA.Valid]
-  · exact DFractional.lt_op_mono
-  · exact DFractional.lt_op_mono ∘ Fractional.lt_le
+-- theorem valid_op_own_r {dq : DFrac F} {q : F} : ✓ (dq • ⟨Own q⟩) → (q < One.one) := by
+--   rcases dq with ⟨y|_|y⟩ <;> simp [CMRA.ValidN, CMRA.op, op, CMRA.Valid]
+--   · exact DFractional.lt_op_mono
+--   · exact DFractional.lt_op_mono ∘ Fractional.lt_le
 
-theorem valid_op_own_l {dq : DFrac F} {q : F} : ✓ (⟨Own q⟩ • dq) → (q < One.one) :=
-  valid_op_own_r ∘ CMRA.valid_of_eqv (CMRA.comm (y := dq))
+-- theorem valid_op_own_l {dq : DFrac F} {q : F} : ✓ (⟨Own q⟩ • dq) → (q < One.one) :=
+--   valid_op_own_r ∘ CMRA.valid_of_eqv (CMRA.comm (y := dq))
 
 theorem valid_discarded : ✓ (LeibnizO.mk Discard : DFrac F) := by simp [CMRA.Valid, valid]
 
-theorem valid_own_op_discarded {q : F} : ✓ (⟨Own q⟩ • ⟨Discard⟩ : DFrac F) ↔ q < One.one := by
-  simp [CMRA.op, op, CMRA.Valid, valid]
+-- theorem valid_own_op_discarded {q : F} : ✓ (⟨Own q⟩ • ⟨Discard⟩ : DFrac F) ↔ q < One.one := by
+--   simp [CMRA.op, op, CMRA.Valid, valid]
 
 end dfrac