inherit typeclass instances for a wrapper structure

Stream: general

[Kris Brown]

Hi, I have a simple wrapper

  @[derive decidable_eq]
  structure Address := (val : ℤ)

but want to assign some properties for it already defined for ints (e.g. linear_order) . Is there a straightforward way of defining instances like this beyond duplicating all the code for ints?

[Yury G. Kudryashov]

We have quite a few defs/lemmas that transfer instances along equivalences.

[Yury G. Kudryashov]

E.g., look at data/equiv/transfer_instance for algebraic types and docs#linear_order.lift etc for order.

[Kris Brown]

Thanks, that puts me on track to solve this! It feels basic but I'm going in circles trying to prove the equivalence. I can prove a bijection from int to Address but cannot prove an injection from Address to int, which is what I need

  -- linear_order.lift needs an injective function TO the type that already has
  -- a linear_order instance
  def cast_address (a:Address): ℤ := a.val

  -- needed to prove bij below
  lemma val_mk_inverse: ∀ z: Address, (Address.mk z.val) = z := begin
    intros, cases z, simp,
  end
  -- That the inverse of cast_address is surjective might be useful?
  lemma bij:  function.bijective Address.mk := begin
    unfold function.bijective,
    split, {finish}, -- injectivity handled automatically
    unfold function.surjective, intros,
    have H: Address.mk (b.val) = b := val_mk_inverse  b,
    exact ⟨b.val, H⟩
  end

  lemma inj: function.injective cast_address := begin
    unfold function.injective, intros a1 a2 castEq,
   unfold cast_address at castEq,
    have Hinj: function.injective Address.mk := bij.1,
      unfold function.injective at Hinj,

      -- have Hsur: function.surjective Address.mk := bij.2,

      -- unfold function.surjective at Hsur,

    cases Address.decidable_eq a1 a2,


    -- have Hsur: function.surjective Address.mk := bij.2,
    -- unfold function.surjective at Hsur,
    -- have h1 := Hsur a1, have h2 := Hsur a2,
    -- cases eq1: h1 with h1v h1', cases eq2: h2 with h2v h2',
    -- rw <-h1', rw <-h2', simp,
    -- have Hinj: function.injective Address.mk := bij.1,
    -- unfold function.injective at Hinj,
    -- have Hinj' := @Hinj h1v h2v,
    -- apply Hinj',
    -- simp,
  end

Is there an easy way to do this for a simple wrapper?

[Kris Brown]

Also not having luck trying to extract the the inverse from the bijection

  def inverse_of_bijection_is_injective: Σ' (f: Address → ℤ), function.injective f :=
    -- Error right at the start: "induction tactic failed,
    -- recursor 'Exists.dcases_on' can only eliminate into Prop"
    match function.bijective_iff_has_inverse.mp bij with
     | ⟨a ,b ⟩ := _
     end

Different error which I also don't fully grasp when I try this in tactic mode:

  def cast_to_int': Σ' (f: Address → ℤ), function.injective f := begin
    have H := function.bijective_iff_has_inverse.mp bij,
    existsi H, -- existsi tactic failed, type mismatch between given
               --term witness and expected type

    end

[Kevin Buzzard]

You shouldn't be proving things like bijective, you should be writing down functions in each direction and proving they're inverses of each other, ie making a term of type equiv Address int

[Kevin Buzzard]

To get an inverse operation from a bijection you need the axiom of choice -- why not just build the inverse explicitly and use that

[Chris Wong]

To explain your error: bijective is defined as a Prop (does not contain data). But Σ is a Type (contains data) and so needs a concrete witness to construct. (Technically your code uses Σ' but the principle is the same.)

[Kris Brown]

I see now - thanks for explaining the error and connection to choice. And eventually was able to prove the injectivity (don't know why it took me so many attempts):

  structure Address:= (val: ℤ)
  def to_z (a:Address): ℤ := a.val

  lemma to_z_inj: function.injective to_z := begin
    unfold function.injective,
    intros  t1 t2 H,
    cases e1:t1, cases e2:t2,
    simp,unfold to_z at H,
    rw e1 at H, rw e2 at H, simp at H, exact H,
  end

[Kevin Buzzard]

The equiv is easier to make and all the lemmas which you're proving are already proved for general equivs.

import tactic

@[derive decidable_eq]
structure Address := (val : ℤ)

def cast_address (a:Address): ℤ := a.val

def inv_fun (n : ℤ) : Address := Address.mk n

def bij : equiv Address ℤ :=
{ to_fun := cast_address,
  inv_fun := inv_fun,
  left_inv := by {rintro ⟨n⟩, refl },
  right_inv := by {intro n, refl } }

lemma val_mk_inverse: ∀ z: Address, (Address.mk z.val) = z := bij.left_inv

lemma bij' :  function.bijective Address.mk := bij.symm.bijective

lemma inj: function.injective cast_address := bij.injective

[Kevin Buzzard]

If you are in a situation where you can write down the inverse, rather than just abstractly proving that a function is bijective (a weaker statement because it's a Prop rather than data) then you should write down the inverse; it makes your objects much easier to work with.

[Kenny Lau]

@Kris Brown what do you need this for? (#xy)

[Kris Brown]

I'll interpret that question pretty broadly. I'm working on a project for formally verified Go code. My initial work was modeling Hoare logic based on this resource (https://github.com/coq-community/hoare-tut) , and lately I've switched to modeling separation logic based on this resource (https://github.com/affeldt-aist/seplog/blob/master/seplog/seplog.v).

I've copied definitions of some of the core data structures to give a feel for the project.

  inductive GoTypeDecl: Type
   | gInt:  GoTypeDecl
   | gStr:  GoTypeDecl
   | gErr:  GoTypeDecl
   | gBool: GoTypeDecl
   | gPtr:  GoTypeDecl → GoTypeDecl
   | gRef:  string → GoTypeDecl

  inductive GoPrimType: Type
   | pInt:  ℤ  → GoPrimType
   | pStr:  string  → GoPrimType
   | pErr:  string  → GoPrimType
   | pBool: bool → GoPrimType
   | pPt: GoTypeDecl → ℤ → GoPrimType
   | pStruct' (name : string) (fields : finset string)
              (vals : ∀ s ∈ fields, GoPrimType) : GoPrimType

  structure GoStruct (name: string):=
     (fields: finset string) (vals : ∀ s ∈ fields, GoPrimType)

def type_dict: GoTypeDecl → Type
    | gStr    := string
    | gErr    := string
    | gInt    := ℤ
    | gBool   := bool
    | (gPtr _):= ℤ
    | (gRef s):= GoStruct s

  structure Address := (val: ℤ)
  structure Heap := (vals: finmap (λ _: Address, Σ dt: GoTypeDecl, type_dict dt))
  structure Store :=   (vals: finmap (λ _: string, Σ dt: GoTypeDecl, type_dict dt))
  structure Var (t: GoTypeDecl) := (name: string)

  inductive Expr: GoTypeDecl → Type
   | const  {α: GoTypeDecl}: type_dict α → Expr α
   | getvar {α: GoTypeDecl}: Var α → Expr α
   | relop {α: GoTypeDecl}:
      Relop → Expr α → Expr α → Expr gBool
   | binop {α: GoTypeDecl}:
      Binop → Expr α → Expr α → Expr α
   | unop {α: GoTypeDecl}:
      Unop → Expr α → Expr α
  | get_field {struct: string} {α: GoTypeDecl}:
      Expr (gRef struct) → string → Expr α
  | update_field {struct: string} {α: GoTypeDecl}: -- pure update/not mutation
      Expr (gRef struct) → string → Expr α → Expr (gRef struct)

  inductive cmd: Type
    | skip: cmd
    | assign   {α: GoTypeDecl}: Var α         → Expr α        → cmd
    | lookup   {α: GoTypeDecl}: Var α         → Expr (gPtr α) → cmd
    | mutation {α: GoTypeDecl}: Expr (gPtr α) → Expr α        → cmd
    | while:                    Expr gBool    → cmd           → cmd
    | seq:                      cmd           → cmd           → cmd
    | ifte:                     Expr gBool    → cmd           → cmd → cmd
    | declare  {α: GoTypeDecl}: Var (gPtr α)  → cmd
    | isnil    {α: GoTypeDecl}: Expr (gPtr α) → Var gBool     → cmd
    | call {β: GoTypeDecl} {struct: string}
           (callee: Expr (gRef struct)) -- object whose method is called
           (method: string)             -- Name of method
           (arg: list (Σ α, Expr α))    -- Values we want to pass to the func
           (result: Var β)              -- store result in this variable
           : cmd.

  structure Sig :=
    (args: list (string × GoTypeDecl))
    (return: list (string × GoTypeDecl))
    (receiver: string) (is_ptr: bool)

  structure GoStructDecl (s:string) :=
    (fields: pairmap string GoTypeDecl)
    (methods: pairmap string (Sig × cmd))

  structure Decls :=
    (structs: finmap ((λ s: string, Σ _:unit, GoStructDecl s)))

  def Ctx := Store × Heap ×  Decls

 -- semantics of expressions
  def eval: Π{α: GoTypeDecl}, Expr α → Store → option (type_dict α)
-- Semantics of program commands
inductive exec : option Ctx → cmd → option Ctx → Prop

-- [A bunch of lemmas related to separation logic, weakest preconditions]

To answer the question narrowly, I want to define a to_string method for Heap and I need to convert the map into a list of pairs that can be printed, which requires a decidable linear order on the keys. I could just use raw integers instead of defining Address, but I like the type-safety since integers are used in lots of places.