Create option instances

option_instances.lean

import tactic

class linear_ordered_comm_group (α : Type)
    extends comm_group α, linear_order α :=
(mul_le_mul_left : ∀ {a b : α}, a ≤ b → ∀ c : α, c * a ≤ c * b)

class linear_ordered_comm_monoid (α : Type)
    extends comm_monoid α, linear_order α :=
(mul_le_mul_left : ∀ {a b : α}, a ≤ b → ∀ c : α, c * a ≤ c * b)

variables {α : Type}

section

inductive option.le [has_le α] : option α → option α → Prop
| bottom (x : option α) : option.le none x
| lifted {x y : α} : x ≤ y → option.le (some x) (some y)
variables [linear_order α]
instance option.linear_order : linear_order (option α) :=
{ le := option.le
, le_refl := by intros x ; cases x ; constructor ; refl
, le_trans := by { introv h₀ h₁ ; cases h₀ ; [ skip, cases h₁ ] ;
                   constructor, transitivity ; assumption  }
, le_antisymm := by { introv h₀ h₁ ; cases h₀ ; cases h₁, refl,
                      congr, apply le_antisymm h₀_a h₁_a, }
, le_total := by { introv, cases a, left, constructor,
                   cases b, right, constructor,
                   cases le_total a b ; [ left, right ] ;
                   constructor ; assumption } }

end

namespace tactic
open tactic.interactive

open list nat

meta def zip_gaols_core : list expr → list α → list (list expr) → (α → tactic unit) → tactic unit
 | gs [] ys f := set_goals (ys.reverse.join ++ gs)
 | [] _ ys f  := set_goals (ys.reverse.join)
 | (g :: gs) (x :: xs) ys f :=
   do set_goals [g],
      f x,
      gs' ← get_goals,
      zip_gaols_core gs xs (gs' :: ys) f

meta def zip_gaols (xs : list α) (f : α → tactic unit) : tactic unit :=
do gs ← get_goals,
   zip_gaols_core gs xs [] f

meta def break_option' (f : list expr → tactic unit) : list expr → list expr → tactic unit
 | xs [] := f xs.reverse
 | xs (y :: ys) :=
   do y ← get_local y.local_pp_name,
      zs ← cases_core y,
      zip_gaols zs $ λ ⟨_,z,_⟩, do
        let xs' := if h : z = [] then xs
                                 else z.last h :: xs,
        try (break_option' xs' ys)

meta def break_option (xs : list expr) (f : list expr → tactic unit) : tactic unit :=
break_option' f [] xs

open lean.parser interactive interactive.types

meta def interactive.mk_option_instance : tactic unit :=
do field ← get_current_field,
   xs ← intros,
   break_option xs $ λ xs,
   (do
     defn ← mk_mapp field ([none,none]),
     let defn := defn.mk_app xs,
     refine ``(some %%defn)
     <|> refine ``(congr_arg some %%defn)
     <|> refine ``(option.le.lifted %%defn) )
   <|> refine ``(none)
   <|> () <$ constructor

end tactic

variable [linear_ordered_comm_monoid α]
instance : linear_ordered_comm_monoid (option α) :=
by { refine_struct { .. option.linear_order }
     ; mk_option_instance,
  }